Filter
Top Products
3.3. FURTHER EXAMPLES 23
a name, while the second uses the special syntactic sugar for function declarations,
where the arguments are written after the function name to the left of the equals
sign. For example, the following is a valid declaration of a function add4, which can
be used to add 4 to its argument:
#let add4 x =
let y = successor x in
let z = let w = successor y in
successor w in
successor z;;
add4 : int -> int = <fun>
#add4 1;;
it : int = 5
It is instructive to unravel this declaration according to the above grammar. A
toplevel phrase, terminated by two successive semicolons, may be either an expres-
sion or a declaration.
3.3 Further examples
It is easy to define by recursion a function that takes a positive integer n and a
function f and returns f
n
, i.e. f ◦ · ·· ◦ f (n times):
#let rec funpow n f x =
if n = 0 then x
else funpow (n - 1) f (f x);;
funpow : int -> (’a -> ’a) -> ’a -> ’a = <fun>
We can apply funpow just to the first argument, and this encodes a natural
number as a function that takes a function as an argument then iterates it the
appropriate number of times, a so-called Church numeral.
3
Since functions aren’t
printed, we can’t actually look at the expression representing a Church numeral:
#funpow 6;;
it : (’_a -> ’_a) -> ’_a -> ’_a = <fun>
However it is straightforward to define an inverse function to funpow that takes
a Church numeral back to a machine integer:
#let defrock n = n (fun x -> x + 1) 0;;
defrock : ((int -> int) -> int -> ’a) -> ’a = <fun>
#defrock(funpow 32);;
it : int = 32
We can define some of the arithmetic operations on Church numerals. Under-
standing these definitions thoroughly is a good exercise.
3
The basic idea was used earlier by Wittgenstein (1922), 6.021.