Example: A Higher-Order Fun Puzzle

Let us first introduce a type definition as follows:

typedef I (a:t@ype) = a -<cloref1> a

Given a type T, I(T) is for a closure-function that maps a given input value of type T to an output value of the same type T. Given a function f of type I(T), we can compose f with itself to form another function, which just applies f twice to a given argument. The following function template twice does precisely the described function composition:

fn{a:t0p} twice (f: I(a)):<cloref> I(a) = lam (x) => f (f (x))

Let us now take a look at some interesting code involving twice that is also likely to be puzzling:

// typedef I0 = int typedef I1 = I(I0) typedef I2 = I(I1) typedef I3 = I(I2) // val Z = 0 val S = lam (x: int): int =<cloref> x + 1 val ans0 = twice<I0>(S)(Z) val ans1 = twice<I1>(twice<I0>)(S)(Z) val ans2 = twice<I2>(twice<I1>)(twice<I0>)(S)(Z) val ans3 = twice<I3>(twice<I2>)(twice<I1>)(twice<I0>)(S)(Z) //

Note that the type definitions I0, I1, I2, and I3 are introduced to make the above code more easily accessible.

Obviously, Z stands for the integer 0 and S for the successor function on integers. Also, ans0 equals 2 as it is the result of applying S to Z twice. Let S2 be the function that applies S twice. It is clear that ans1 is the result of applying S2 to Z twice and thus equals 4. With a bit more effort, one should be able to figure out that the value of ans2 is 16. What is the value of ans3? In general, what is the nth value in the sequence of ans0, ans1, ans2, etc.? I leave these questions as exercises for the interested reader.

Please find on-line the entire code in this section plus some additional code for testing.