Let us first introduce a type definition as follows:
// 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) //
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.