I wrote this during Feb. 2005. Since it occurs to me every once in a while and I kept forgetting the details, I’d better keep a note.

I was trying to simulate church numerals and primitive recursion in second rank polymorphism of Haskell, and I thought I could do it without introducing a constructor by `newtype`

. Church’s encoding of natural numbers can be expressed by the type:

`> type N = forall a . (a -> a) -> a -> a`

### Basics

We first define `zero`

, `succ`

, and some constants:

```
> zero :: N
> zero = \f -> \a -> a
> succ :: N -> N
> succ n = \f -> \a -> f (n f a)
> toInt :: N -> Int
> toInt n = n (1+) 0
> one, two, three :: N
> one = succ zero
> two = succ one
> three = succ two
```

Addition and multiplication can be defined as usual:

```
> add, mul :: N -> N -> N
> add m n = \f -> \a -> m f (n f a)
> mul m n = \f -> \a -> m (n f) a
```

### Predecessor

Even `pred`

typechecks — at least this particular version of `pred`

:

```
> pred :: N -> N
> pred n f x = n (\g h -> h (g f)) (const x) id
```

I am more familiar with another way to implement `pred`

, which uses pairs. This `pred`

, on the other hand, can be understood by observing that the “fold” part returns a function that abstracts away the outermost `f`

:

```
pred n f x = dec n id
where dec 0 = \h -> x
dec (1+n) = \h -> h (f^n x)
```

### Exponential

I know of two ways to define `exp`

. However, only this one typechecks:

```
> exp :: N -> N -> N
> exp m n = n m
```

Another definition, making use of `mul`

, does *not* typecheck!

```
exp :: N -> N -> N
exp m n = n (mul m) one
```

GHC returns a rather cryptic error message “Inferred type is less polymorphic than expected. Quantified type variable `a’ escapes.” The real reason is that polymorphic types in Haskell can only be instantiated with monomorphic types. If we spell out the explicit type applications, we get:

` exp (m::N) (n::N) = n [N] ((mul m)::N->N) (one::N)`

which is not allowed. On the other hand, the previous definition of `exp`

does not instantiate type variables to polymorphic types:

```
exp (m::N) (n::N) = /\b -> \(f::(b->b)) -> \(x::b) -> n[b->b] (m[b]) f x
```

For the same reason, primitive recursion does not type check:

```
primrec :: (N -> a -> a) -> a -> N -> a
primrec f c n =
snd (n (\z -> pair (succ (fst z))
(f (fst z) (snd z)))
(pair zero c))
```

nor does the pair-based definition of `pred`

.

To overcome the problem we have to wrap `N`

in `newtype`

. The solution was presented by Oleg Kiselyov.