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