RankNTypes and Church Numbers

Question

I am trying to study church numbers in Haskell by specifying numbers like this, with the idea that a positive integer n is basically an expression that applies a function of the following type to a value of type t for n times.

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

With this idea, I can define zero , successor , plus , mult following ways:

 zero :: Nat zero = \ft -> t succ :: Nat -> Nat succ n = \f -> f . (nf) plus :: Nat -> Nat -> Nat plus mn = \f -> (mf) . (nf) mult :: Nat -> Nat -> Nat mult mn = \f -> m (nf) -- Equal to \f -> (m . n) f -- Pointfree version mult' :: Nat -> Nat -> Nat mult' = (.) 

When I try to define exponentiation, I would like to try to apply the same reasoning that allowed me to determine multiplication, namely apply mult m n times to 1 .

This leads to the following code

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

But it checks the type with the following error from the 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 typechecker is not creating the type for n correctly, ideally type t should be created using another ( t -> t ) for the expression to pass.

What bothers me is that the following typechecks code:

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

Could someone explain what the problem is here? Why is the first definition of exp' not typecheck, but the second exp typecheks?

Thanks!

Answer 1

The reason it does not work is due to several incompatible instances that are not even allowed in Haskell. If you include -XImpredicativeTypes , you can get it to compile:

 {-# LANGUAGE ImpredicativeTypes #-} ... exp' :: Nat -> Nat -> Nat exp' mn = n (mult m) (succ zero) 

The second version of typechecks, because mult' has a higher type of rank, although by definition it is equal to (.) , So type checking continues in different ways. Since type (.) Is simpler (rank 1), type checking will be performed more often.

The docs gHC ImpredicativeTypes ImpredicativeTypes does not work, so I would caution against using it. A typical way around this is to simply use newtype :

 newtype Nat' = N { instN :: Nat } exp'' :: Nat -> Nat -> Nat exp'' mn = instN $ n (\(N q) -> N $ mult mq) (N $ succC zero) 

---

To see an invalid instance in action, you can use printed holes:

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

This will report type forall a . (Nat -> Nat) -> Nat -> (a -> a) -> a -> a forall a . (Nat -> Nat) -> Nat -> (a -> a) -> a -> a , which matches (Nat -> Nat) -> Nat -> Nat . Since you are placing n , you need to concatenate this type with forall a . (a -> a) -> a -> a forall a . (a -> a) -> a -> a , which involves creating an instance of a variable of type a using the Nat polytype.