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.