I probably wrote this a couple of years ago when I was studying polymorphic types.
What happens if we have only monomorphic type when we define church numerals? Let us represent church numerals by the type
(a -> a) -> a -> a for some monomorphic
> import Prelude hiding (succ, pred) > type N a = (a -> a) -> a -> a
Zero and successor can still be defined. Their values do not matter.
> zero :: N a > zero = error "" > succ :: N a -> N a > succ = error ""
Also assume we have pairs predefined:
> pair a b = (a,b)
We can even define primitive recursion, only that it does not have the desired type:
primrec :: (N -> b -> b) -> b -> N -> b
Instead we get the type below:
> primrec :: (N a -> b -> b) -> b -> N (N a, b) -> b > primrec f c n = > snd (n (\z -> pair (succ (fst z)) > (f (fst z) (snd z))) > (pair zero c))
Therefore, predecessor does not get the type
pred :: N a -> N a we want. Instead we have:
> pred :: N (N a, N a) -> N a > pred = primrec (\n m -> n) zero