RankNTypes and Church numerals

Question

I'm trying to study church numerals in Haskell by giving the numbers a type like this, with the idea that a natural number n is basically the expression that applies the function in the following type to the value of type t for n times.

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

With that idea, I can define zero, successor, plus, mult in the following ways:

zero :: Nat
zero = \f t -> t

succ :: Nat -> Nat
succ n = \f -> f . (n f)

plus :: Nat -> Nat -> Nat
plus m n = \f -> (m f) . (n f)

mult :: Nat -> Nat -> Nat
mult m n = \f -> m (n f) -- Equal to \f -> (m . n) f

-- Pointfree version
mult' :: Nat -> Nat -> Nat
mult' = (.)

When I try to define exponentiation, I'd like to try applying the same reasoning that allowed me to define multiplication, namely applying mult m n times to 1.

This leads to the following code

exp' :: Nat -> Nat -> Nat
exp' m n = n (mult m) (succ zero)

But this does type check with the following error from GHC:

  Couldn't match type ‘t’ with ‘t1’
  ‘t’ is a rigid type variable bound by
    the type signature for:
      exp' :: forall t. Nat -> Nat -> (t -> t) -> t -> t
    at church.lhs:44:3
  ‘t1’ is a rigid type variable bound by
    a type expected by the context:
      forall t1. (t1 -> t1) -> t1 -> t1
    at church.lhs:44:17
  Expected type: ((t -> t) -> t -> t) -> (t -> t) -> t -> t
    Actual type: Nat -> Nat

The error seems to say that the typechecker is not instantiating the type for n properly, ideally type t should be instantiated with another (t -> t) for the expression to go through.

What's also confusing me is that the following code typechecks:

exp :: Nat -> Nat -> Nat
exp m n = n ((.) m) (succ zero) -- replace mult by (.)

Would someone mind explaining what's the problem here? Why does the first definition of exp' not typecheck but the second exp typecheks?

Thanks!

Flaminius

Answer 1

The reason that it doesn't work is it involves several impredicative instantiations, which isn't even normally allowed in Haskell. If you turn on -XImpredicativeTypes, you can get it to compile:

{-# LANGUAGE ImpredicativeTypes #-} 

...

exp' :: Nat -> Nat -> Nat
exp' m n = n (mult m) (succ zero) 

The second version typechecks because mult' has a higher rank type, even though it is definitionally equal to (.), so typechecking proceeds differently. Since the type of (.) is simpler (rank 1) typechecking will succeed more often.

The GHC docs warn ImpredicativeTypes does not work so I would caution against using it. The typical way to get around this it to simple use a newtype:

newtype Nat' = N { instN :: Nat } 

exp'' :: Nat -> Nat -> Nat
exp'' m n = instN $ n (\(N q) -> N $ mult m q) (N $ succC zero) 

---

To see the impredicative instantiation in action, you can use typed holes:

exp' :: Nat -> Nat -> Nat
exp' m n = _ (mult m) (succC zero) 

This will report the type forall a . (Nat -> Nat) -> Nat -> (a -> a) -> a -> a, which is the same as (Nat -> Nat) -> Nat -> Nat. Since you place n there, you have to unify this type with forall a . (a -> a) -> a -> a, which involves instantiating the type variable a with the polytype Nat.

Mosby