2

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 ?

Improve this question

2 Answers 2

Reset to default
3

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,

  • the function three with type ((int -> int) -> int -> int),
  • the function succ with type (int -> int)
  • the initial argument 0 with type int

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.

Improve this answer
Sign up to request clarification or add additional context in comments.

Comments

2

For the first part

Let's just consider:

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)

What can we infer about types here?

Obviously, you've identified that n must be int, since it's both being subtracted and compared to another int.

int -> ... -> ... -> ...

As one example if we call church_of_int 3 what does that look like? It returns a function that takes a function that takes a function f and a value x, which we denote as type 'a. So f takes a value of type 'a and turns it into...

Well, the result of f x is passed where church_of_int expects a value of type a, so the type of f must be 'a -> 'a.

Now that we know the inferred types of f and x, we can finish the type signature of church_of_int.

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

Second block

With regards to:

let three f x = church_of_int 3 f x

This could just be the following using partial application.

let three = church_of_int 3

In this case the type signature ('a -> 'a) -> 'a -> 'a shouldn't be surprising.

Third block

three (fun x -> x + 1) 0

Let's consider how this evaluates, with (fun x -> x + 1) subbed out for the partial application of the addition operator ((+) 1).

church_of_int 3 ((+) 1) 0

3 doesn't equal 0 so we get back fun f x -> church_of_int (n-1) f (f x), which we apply to (3 - 1), ((+) 1) and ((+) 1) 0.

So now we've called:

church_of_int 2 ((+) 1) 1

Evaluate this and we get:

church_of_int 1 ((+) 1) 2

Since 1 isn't 0:

church_of_int 0 ((+) 1) 3

Now, though, n is 0, so we get a function where f is never applied to anything, so it doesn't matter. We just return x, which is 3.

Fourth part

Consider the definition of three again.

let three = church_of_int 3

The type is:

('a -> 'a) -> 'a -> 'a

The first argument to three is a function that maps a value of type 'a to another value of the same type. Let's rewrite that type signature a bit.

('a -> 'a) -> ('a -> 'a)

If we partially apply three three we get a function with the following type, which looks a lot like the type of three.

('_a -> '_a) -> '_a -> '_a

The effect of applying three to three is to get another function that takes a new function that takes a function and an initial value. We can apply this endlessly. Perhaps the syntax makes more sense if we look at it this way:

let f = ((+) 1 in ((three three) f) 0

And we can see this "exponentiation" by defining a few more functions.

# let two f x = church_of_int 2 f x let three f x = church_of_int 3 f x let four f x = church_of_int 4 f x;; val two : ('a -> 'a) -> 'a -> 'a = <fun> val three : ('a -> 'a) -> 'a -> 'a = <fun> val four : ('a -> 'a) -> 'a -> 'a = <fun> # let inc x = x + 1;; val inc : int -> int = <fun> # two two inc 0;; - : int = 4 # two four inc 0;; - : int = 16 # two two two inc 0;; - : int = 16 # two two four inc 0;; - : int = 256
Improve this answer

Comments

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.