Does OCaml's type system prevent it from modeling Church numerals?

Question

As a pass-time, I'm trying to implement all kinds of problems that were presented in a course (concerned with Lambda Calculus and various programming concepts) I took at the university. So, I'm trying to implement Church numerals and associated operators in OCaml (also as an exercise in OCaml).

This is the code so far:

let church_to_int n =
    n (fun x -> x + 1) 0;;

let succ n s z =
    s (n s z)

let zero = fun s z -> z

let int_to_church i =
    let rec compounder i cont =
        match i with
        | 0 -> cont zero
        | _ -> compounder (i - 1) (fun res -> cont (succ res))
    in
    compounder i (fun x -> x)

let add a b = (b succ) a

let mul a b = (b (add a)) zero

So, it seems to work, but then it breaks down. Let's consider these definitions:

let three = int_to_church 3
let four = int_to_church 4
church_to_int (add three four) // evaluates to 7
church_to_int (add four three) // throws type error - see later

I get that the error thrown has to do with the type polymorphism of the Church numerals when they're defined (see SO question), and then it's resolved after the closures are invoked once. However, I don't seem to understand why the type inconsistency error is thrown in this case:

let three = int_to_church 3
let four = int_to_church 4
church_to_int (mul three four) // throws type error - see later

Any thoughts?

The specific errors:

1.

Error: This expression has type (int -> int) -> int -> int                                                 but an expression was expected of type                                                                ((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) ->                                    
         ((((int -> int) -> int -> int) -> (int -> int) -> int -> int) ->
          ((int -> int) -> int -> int) -> (int -> int) -> int -> int) ->
         'd
       Type int is not compatible with type ('a -> 'b) -> 'c -> 'a 

2.

Error: This expression has type                                                                              ((((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) ->                                             (('d -> 'd) -> 'd -> 'd) -> 'e) ->                                                       
          ((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) ->
          (('d -> 'd) -> 'd -> 'd) -> 'e) ->
         (((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) ->
          (('d -> 'd) -> 'd -> 'd) -> 'e) ->
         ((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) ->
         (('d -> 'd) -> 'd -> 'd) -> 'e
       but an expression was expected of type
         ((((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) ->
           (('d -> 'd) -> 'd -> 'd) -> 'e) ->
          'e) ->
         ('f -> 'g -> 'g) -> 'h
       The type variable 'e occurs inside
       ((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) ->
       (('d -> 'd) -> 'd -> 'd) -> 'e

Answer 1

Well i was a bit rusty with lambda-calculus, but after few discussions with some wise old men, i came to this answer : YES, writing that way, OCaml's type system do not allow the writing of Church numerals.

The real problem here is with your addition term :

let add a b = b succ a

wich has the following type

(((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) -> 'd -> 'e) -> 'd -> 'e

Where the arguments of add have not the same type. This is a bit sad since we naively expect the addition to be commutative. You can easily verify this when writing :

let double a = add a a (* produces type error - the type variable occurs ... *)

This error means that you're trying to unify one type with a "bigger" type i.e that contains it (ex: unifying 'a with 'a -> 'a). OCaml does not allow that (unless if you set the -rectypes option wich allows cyclic types). To understand better what's going on, let's add type annotations to help the typer (i'll change a bit your notations for sake of clarity):

type 'a church = ('a -> 'a) -> 'a -> 'a
let zero : 'a church = fun f x -> x
let succ n : 'a church = fun f x -> f (n f x)

Now let's go back to the add term and annotate it a bit to see what the typer has to say:

let add (a:'a church) b = a succ b (* we only annotate "a" to let the typer infer the rest *)

This produces a very odd type :

'a church church -> 'a church -> 'a church

That gets interesting: why is the first arg typed as an 'a church church?

The answer is the following : Here, a church integer is a value that takes a moving function of type 'a -> 'a (a self-map in mlahematics) that can browse a space, and an starting point ('a) that belongs to that space.

Here, if we specify that the parameter a has type 'a church, than 'a represent the space in which we can move. Since succ, the moving function of a, operates over the church, than 'a here is it self an 'a church, thus making the parameter a an 'a church church.

This is not at all the type we wanted at the begining ... but that justifies why the type system do not allow your values three and four as both 1st and snd argument of add.

One solution can be to write add in a different way :

let add a b f x = a f (b f x)

Here, both a and b have the same moving function, and thus the same type, but you do not enjoy anymore the beautiful writing with the partial application ...

An other solution which makes you keep this beautiful writing would be to use universal types, that allow a larger kind of polymorphism:

type nat = {f:'a.('a -> 'a) -> 'a -> 'a}
(* this means “for all types ‘a” *)

let zero : nat = {
  f=fun f x -> x
}

let succ n : nat = {
  f= fun f x -> f (n.f f x)
}

let add (a:nat) (b:nat) = a.f succ b

let double a = add a a (* Now this has a correct type *)

let nat_to_int n =
  n.f (fun x -> x + 1) 0;;

let nat_four = succ (succ (succ (succ zero)))

let eight_i = double nat_four |> nat_to_int //returns 8

But this solution is a bit more verbose than your initial one.

Hope it was clear.