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 `a`

:

```
> 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
```

### Ref.

Oleg Kiselyov, Predecessor and lists are not representable in simply typed lambda-calculus.