# Polymorphic Types in Haskell without Constructors?

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.