Here's another puzzle:

Is it possible in OCaml to define a variable-argument function? For example, can one define a function `f`

and values `a`

and `z`

such that the following assertions hold:

assert (f z = 0); assert (f a z = 1); assert (f a a z = 2); assert (f a a a z = 3); ...

Once you've got that, how about generalizing it to a variable-argument sum, i.e. define

`f`

, `a`

, and `z`

such that:

assert (f (a i1) (a i2) ... (a ik) z = i1 + i2 + ... + ik);

Or, if you want to eliminate the parens, define an `f`

, `a`

, and `z`

such that:

assert (f a i1 a i2 ... a ik z = i1 + i2 + ... + ik);

This is very Similar to a typesafe printf solution I’ve seen.

let a x =

fun f -> f (x + 1);;

let z x = x;;

let f g = g 0;;

For the generalized version, a is instead implemented as:

let a x =

fun y f -> f (x + y);;

Continuations are crazy powerful!

For the first one:

let z sum = sum

let a sum g =

g (sum + 1)

let f g =

g 0

For the second and third one only a changes:

let a i sum g =

g (i + sum)

This works with or without parenthesis.

I’m enjoying the puzzles! I’m no stranger to Church numerals so this wasn’t a major challenge, but no matter how many times I code CN’s it always feels like magic when they work. Also, version 3 is a neat trick that I wasn’t expecting.

My solution is the same as the one at the bottom of this page, but here is some intuition. The way I looked at this was to think about “f”, “f a” and “(f a) a” as being values Zero, One and Two such that Zero z = 0, One z = 1, Two z = 2, etc. Say that Zero, One and Two all have some type Num; the idea is that each represents the corresponding integer, applying “a” to a Num produces the representation of the next integer, and applying “z” to a Num produces the actual integer to which it corresponds.

One way of representing integers using functions is to use values of type ‘a -> (‘a -> ‘a) -> ‘a (the intuition being that given such a value, you supply a base case and an iterator, and the iterator is iterated correspondingly many times starting from the base). That doesn’t quite work here; instead an alternative representation seems to be needed, where the representation actually holds the integer itself.

Letting the type Num be (int -> ‘a) -> ‘a, we can define f (aka Zero) to be

let f = fun g -> g 0

Such a representation can be “quizzed” by providing a function that accepts the value stored within, does something with it (possibly changing its type), and returns it. In the first case above, “f z”, we just want the value unchanged at type int, so define

let z = fun x -> x

Now all we need is a value “a” such that applying “a” to a value of type Num produces another value of type Num corresponding to the next integer. To do this, we can extract the encapsulated integer from the value of type Num, increment it, and form another value of type Num. This is done by defining:

let a x = fun g -> g (x + 1)

of type int -> Num, and then applying it to values of type Num as required. Having then done the incrementing (“(f a) a” perhaps) starting from Zero (aka “f”), you then apply “z” to get back the value of type int. Cunning.

It seems we all have the same

solution :-). One thing I hadn’t noticed until Milan pointed it out

was the the solutions to puzzles two and three are the same. It only

works becaus the operation is commutative. For a case where it won’t

work, consider defining `f`, `a`, `z` such that:

assert (f z = []);

assert (f a x1 z = [x1]);

assert (f a x1 a x2 z = [x1; x2]);

assert (f a x1 a x2 a x3 z = [x1; x2; x3]);

The solutions with and without parentheses require different `a`’s.

As for the original problem, the most surprising part to me is that

the types work out. Here’s some code that helps me understand why.

module type S = sig

type ‘a t

val f : ‘a t -> ‘a

val a : (‘a t -> ‘a) t

val z : int t

end

module F (M : S) = struct

open M

type ‘a f = ‘a t -> ‘a

type ‘a a = (‘a t -> ‘a) t

type u0 = int

type a0 = u0 t

type u1 = a0 -> u0

type a1 = u0 a

type u2 = a1 -> u1

type a2 = u1 a

type u3 = a2 -> u2

type a3 = u2 a

let () =

let z : a0 = z in

let a1 : a1 = a in

let a2 : a2 = a in

let a3 : a3 = a in

let ((f0 : u0 f) : a0 -> int) = f in

let ((f1 : u1 f) : a1 -> a0 -> int) = f in

let ((f2 : u2 f) : a2 -> a1 -> a0 -> int) = f in

let ((f3 : u3 f) : a3 -> a2 -> a1 -> a0 -> int) = f in

assert (f0 z = 0);

assert (f1 a1 z = 1);

assert (f2 a2 a1 z = 2);

assert (f3 a3 a2 a1 z = 3);

;;

end

module M : S = struct

type ‘a t = int -> ‘a

let f g = g 0

let a i g = g (i + 1)

let z i = i

end

module Z = F (M)