Substraction not Definable in Simply Typed Lambda Calculus

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.