How to work with higher rank types

Question

Playing with the church numerals. I run into the situation I can't guide the GHC type-checker around higher order types.

First I wrote an version, without any type signatures:

module ChurchStripped where

zero z _ = z
inc n z s = s (n z s)
natInteger n = n 0 (1+)

add a b = a b inc

{-
*ChurchStripped> natInteger $ add (inc $ inc zero) (inc $ inc $ inc zero)
5
-}

mult a b = a zero (add b)

{-
*ChurchStripped> natInteger $ mult (inc $ inc zero) (inc $ inc $ inc zero)
6
-}

The inferred type of mult is horrible, so I tried to clean-up the types with a type definitions:

module Church where

type Nat a = a -> (a -> a) -> a

zero :: Nat a
zero z _ = z

inc :: Nat a -> Nat a
inc n z s = s (n z s)

natInteger :: Nat Integer -> Integer
natInteger n = n 0 (1+)

{- `add :: Nat a -> Nat a -> Nat a` doesn't work, and working signature looks already suspicious -}

add :: Nat (Nat a) -> Nat a -> Nat a
add a b = a b inc

{-
*Church> natInteger $ add (inc $ inc zero) (inc $ inc $ inc zero)
5
-}

mult :: Nat (Nat a) -> Nat (Nat a) -> Nat a
mult a b = a zero (add b)

{-
*Church> natInteger $ mult (inc $ inc zero) (inc $ inc $ inc zero)
6
-}

It works, but the types aren't as clean as they could be. Following the System F definitions I tried:

{-# LANGUAGE RankNTypes #-}

module SystemF where

type Nat = forall a. a -> (a -> a) -> a

zero :: Nat
zero z _ = z

inc :: Nat -> Nat
inc n z s = s (n z s)

natInteger :: Nat -> Integer
natInteger n = n 0 (1+)

{- This doesn't work anymore

add :: Nat -> Nat -> Nat
add a b = a b inc

   Couldn't match type `forall a1. a1 -> (a1 -> a1) -> a1'
                 with `a -> (a -> a) -> a'
   Expected type: (a -> (a -> a) -> a) -> a -> (a -> a) -> a
     Actual type: Nat -> a -> (a -> a) -> a
   In the second argument of `a', namely `inc'
   In the expression: a b inc
   In an equation for `add': add a b = a b inc

-}

I guess it should be possible to write add with Nat -> Nat -> Nat type signature, but I have no idea how.

P.S. actually I started from the bottom, but it maybe easier to present this problem this way.

Answer 1

bennofs is right, you really want to help the typechecker along here, in particular in add where you need to instantiate the a in forall a . a -> (a -> a) -> a with Nat (ie, the same forall a . ... type).

One way to do that is to introduce a newtype that wraps the polymorphic type:

newtype Nat' = N Nat

Now you can go between Nat and Nat' via N, and back using unN

unN :: Nat' -> Nat
unN (N n) = n

(It's worth noting at this point that newtype Nat' = N Nat is a different beast from data Nat2 = forall a . N2 (a -> (a -> a) -> a). The latter requires -XExistentialQuantification because it says that for some particular choice of a, you can make a Nat2. On the other hand, the former still says that if you have a -> (a -> a) -> a for any arbitrary a, then you can make a Nat'. For Nat' you need -XRankNTypes, but you don't need existentials.)

Now we can also make inc' to increment a Nat':

inc' :: Nat' -> Nat'
inc' (N n) = N (inc n)

And we're ready to add:

add :: Nat -> Nat -> Nat
add n m = unN (n (N m) inc')

The reason this works is because now instead of trying to convince GHC to instantiate the type of n with a polymorphic type ∀ a . a -> (a -> a) -> a on its own, the N acts as a hint.

Example:

> natInteger (add (inc zero) (inc zero))
2

Answer 2

I don't understand RankNTypes well enough to tell why your original example doesn't work, but if you pack Nat into a data type, then it works:

{-# LANGUAGE RankNTypes #-}

module SystemF where

data Nat = Nat (forall a. (a -> (a -> a) -> a))

zero :: Nat
zero = Nat const

inc :: Nat -> Nat
inc (Nat n) = Nat $ \z s -> s $ n z s

natInteger :: Nat -> Integer
natInteger (Nat n) = n 0 (1+)

add :: Nat -> Nat -> Nat
add (Nat a) b = a b inc

Now the Nat type is a real data type, which helps the type checker, because it doesn't have to deal with the polymorphic type all the time, only when you actually "unpack" it.

Answer 3

Here's my implementation of Church numerals:

type Nat = forall a . (a→a) → (a→a)

zero :: Nat
zero _ = id

one  :: Nat
one    = id

inc :: Nat → Nat
inc a f = f . a f

add :: Nat → Nat → Nat
add a b f = (a f) . (b f)

mul :: Nat → Nat → Nat
mul a b = a . b

nat :: Integer → Nat
nat 0 = zero
nat n = inc $ nat (n-1)

unnat :: Nat → Integer
unnat f = f (+ 1) 0

It is much easier to work with them flipped (function to apply N times first, its argument second). Everything just comes out, well, naturally.

EDIT: this solution is also limited, the types are not right just like in the original question and it will break down at some point.