Filter
Top Products
18 CHAPTER 2. A TASTE OF CAML
illustration of why this might be so. It is still an open problem whether the following
function terminates for all arguments, the assertion that it does being known as the
Collatz conjecture:
8
#let rec collatz n =
if n <= 1 then 0
else if even(n) then collatz(n / 2)
else collatz(3 * n + 1);;
collatz : int -> int = <fun>
What is clear, though, is that if it does halt it returns 0. Now consider the
following trivial function:
#let f (x:int) = 0;;
f : int -> int = <fun>
By deciding the equation collatz = f, the computer would settle the Collatz
conjecture. It is easy to concoct other examples for open mathematical problems.
It is possible to trap out applications of the equality operator to functions and
datatypes built up from them as part of typechecking, rather than at runtime. This
is the approach taken by Standard ML. Types that do not involve functions in
these ways are known as equality types, since it is always valid to test objects of
such types for equality. On the negative side, this makes the type system much
more complicated. However one might argue that static typechecking should be
extended as far as feasibility allows.
Further reading
Numerous textbooks on ‘functional programming’ include a general introduction
to the field and a contrast with imperative programming — browse through a few
and find one that you like. A detailed and polemical advocacy of the functional
style is given by Backus (1978), the main inventor of FORTRAN. A good elementary
introduction to CAML Light and functional programming is Mauny (1995). Paulson
(1991) is another good textbook, though based on Standard ML.
8
A good survey of this problem, and attempts to solve it, is given by Lagarias (1985). Strictly,
we should use unlimited precision integers rather than machine arithmetic. We will see later how
to do this.