ocamlcurrying

Partial applications and currying in functional programming

It's been hours and I can't understand this example in OCaml.

I don't know how to think about this so I'll try giving my process of thought.

The question is : For each definition or expression, give the type and value (<fun> included)

Here is the entire code (toplevel) :

let rec church_of_int n = 
    if n = 0 then fun f x -> x
    else fun f x -> church_of_int (n-1) f (f x);;

let three f x = church_of_int 3 f x;;

three (fun x -> x + 1) 0;;

three three (fun x -> x + 1) 0;;

1) First block

let rec church_of_int n = 
  if n = 0 then fun f x -> x
  else fun f x -> church_of_int (n-1) f (f x);;

This is a function which takes an int because of int operator "-" n-1 and returns a function which takes two arguments 'a and 'b. The function returned returns the same type of 'b because of the fun f x -> x.

Therefore the type is :

int -> ('a -> 'b) -> 'b = <fun>

But the toplevel says :

val church_of_int : int -> ('a -> 'a) -> 'a -> 'a = <fun>

I don't get it...

2) Second block

let three f x = church_of_int 3 f x;;

For the second block, three takes a function and an int and applies it to the returned function of church_of_int.

Therefore, the type is :

('a -> 'b) -> int -> 'b = <fun>

Toplevel says :

val three : ('a -> 'a) -> 'a -> 'a = <fun>

3) Third block

three (fun x -> x + 1) 0;;

Here, we apply a function and an int to three.

We need to compute

church_of_int 3 (fun x -> x + 1) 0

church_of_int 3 = fun f x -> church_of_int 2 f (f x)

church_of_int 2 = fun f x -> church_of_int 1 f (f x)

church_of_int 1 = fun f x -> church_of_int 0 f (f x)

church_of_int 0 = fun f x -> x

THEN

church_of_int 1 = fun f x -> ((fun f x -> x) f (f x)) = fun f x -> f x

church_of_int 2 = fun f x -> ((fun f x -> f x) f f(x)) = fun f x -> f (f x)

church_of_int 3 = fun f x -> ((fun f x -> f (f x)) f f(x)) = fun f x -> f (f (f x))

therefore,

church_of_int 3 (fun x -> x + 1) 0 = 3

Toplevel confirms this is correct.

4) Fourth block

three three (fun x -> x + 1) 0;;

Here it gets incredibly messy. On one side, we know that three (fun x -> x + 1) 0 = 3

then

three 3 is a partial application

on the other the toplevel returns 27.

Can you please help me fix my mistakes and my process of thought to get the correct types and results ?

Solution

  • This is a function which takes an int because of int operator "-" n-1 and returns a function which takes two arguments 'a and 'b. The function returned returns the same type of 'b because of the fun f x -> x. Therefore the type is :

    int -> ('a -> 'b) -> 'b = <fun>

    Let's look closer into the definition,

    let rec church_of_int n = 
 if n = 0 then fun f x -> x
 else fun f x -> church_of_int (n-1) f (f x)

    From the first branch of the if expression we indeed can infer that the return type is a function that takes two arguments and returns the last, i.e.,

    int -> ('a -> 'b -> 'b)

    which we can rewrite (using the right associativity of the -> type operator as),

    int -> 'a -> 'b -> 'b

    Notice, how your train of thoughts diverged from the right path - as you represent a function that takes two arguments and returns the second as ('a -> 'b) -> 'b. You placed parentheses incorrectly, in fact, your type represents a function that takes a single argument, which is itself a function that takes any argument and returns the value of type 'b.

    But let's go back to our definition. We used only the information from one branch of the if expression, so we missed some of the available information. From the else branch, church_of_int (n-1) f (f x) we can see that the first argument (which type we ascribed with 'a) is a function itself, because of application (f x), so we can refine 'a to function type. We see that it is applied to x, which we know has type 'b, moreover, the result of application is passed to the second parameter, which we inferred as 'b from the first branch, so we know that the type of f is 'b -> 'b. Now we substitute 'a with ('b -> 'b) and get,

    int -> ('b -> 'b) -> 'b -> 'b

    which is equivalent modulo variable names to the type inferred by the OCaml toplevel.

    So what does this type mean, or more specifically what does the church_of_int n expression define? This function applies n times the passed function f to the passed argument x. The type of the argument doesn't matter as we never use it, we just apply f to it n times.

    With that knowledge we can easily digest let three f x = church_of_int 3 f x. It applies f to x three times. So the type is ('a -> 'a) -> 'a -> 'a (we still wait for f and x to be passed).

    And if we pass fun x -> x + 1 as the function and 0 as the initial value, then three (fun x -> x + 1) 0 is a three-fold application of that function to 0. Let's name fun x -> x + 1 as succ, so three succ 0 is succ (succ (succ 0))), i.e., a third successor of zero, which is three.

    Now the hard part, let's try to understand the three three (fun x -> x + 1) 0 expression. First of all, let's rewrite it as three three succ 0.

    The first question that you might have is why three is able to accept more than two parameters? Since three has type ('a -> 'a) -> 'a -> 'a the second parameter 'a could be a function itself. We know that succ has type int -> int, so we substitute 'a with (int -> int),

    ((int -> int) -> (int -> int)) -> (int -> int) -> (int -> int)

    let's remove some parenthesis,

    ((int -> int) -> int -> int) -> (int -> int) -> int -> int

    which gives us a function that takes three arguments,

    And three three succ applies three three times to succ. So let's unfold it,

    three three succ
===========================
three (three (three succ))

    We already know that three succ adds 3 to the passed argument, so it is x + 3, let's name it plus3 and rewrite,

    three three succ
===========================
three (three (three succ))
=================== (three succ => plus3)
three (three plus3)

    If we will repeat plus3 three times, i.e., x + 3 + 3 + 3 this is the same as x + 9, so we can rewrite it as,

    three three succ
=========================== 
three (three (three succ))
=================== (three succ => plus3)
three (three plus3)
=================== (three plus3 => plus9)
three plus9

    Now, the last step, repetition x + 9 + 9 + 9 is x+27, so we can do the final rewrite,

    three three succ
=========================== 
three (three (three succ))
=================== (three succ => plus3)
three (three plus3)
=================== (three plus3 => plus9)
three plus9
=========== (three plus9 => plus27)
plus27

    so in the end three three succ x creates a function that is semantically equivalent to fun x -> x + 27, and three three succ 0 gives us 27.