Filter
Top Products
32 CHAPTER 3. FURTHER CAML
and here is a recursive function to evaluate such expressions:
#let rec eval =
fun (Integer i) -> i
| (Sum(e1,e2)) -> eval e1 + eval e2
| (Product(e1,e2)) -> eval e1 * eval e2;;
eval : expression -> int = <fun>
#eval (Product(Sum(Integer 1,Integer 2),Integer 5));;
it : int = 15
Such abstract syntax trees are a useful representation which allows all sorts of
manipulations. Often the first step programming language compilers and related
tools take is to translate the input text into an ‘abstract syntax tree’ according to
the parsing rules. Note that conventions such as precedences and bracketings are
not needed once we have reached the level of abstract syntax; the tree structure
makes these explicit. Recursive types similar to these are used in HOL Light to
define logical entities like terms.
3.4.4 The subtlety of recursive types
A recursive type may contain nested instances of other type constructors, including
the function space constructor. For example, consider the following:
#type (’a)embedding = K of (’a)embedding->’a;;
Type embedding defined.
If we stop to think about the underlying semantics, this looks disquieting. Con-
sider for example the special case when ’a is bool. We then have an injective
function K:((bool)embedding->bool)->(bool)embedding. This directly contra-
dicts Cantor’s theorem that the set of all subsets of X cannot be injected into X.
4
Hence we need to be more careful with the semantics of types. In fact α → β
cannot be interpreted as the full function space, or recursive type constructions
like the above are inconsistent. However, since all functions we can actually create
are computable, it is reasonable to restrict ourselves to computable functions only.
With that restriction, a consistent semantics is possible, although the details are
complicated.
The above definition also has interesting consequences for the type system. For
example, we can now define a recursion operator without any explicit use of recur-
sion, by using K as a kind of type cast.
5
The use of let is only used for the sake of
efficiency, but we do need the extra argument z in order to prevent looping under
CAML’s evaluation strategy.
#let Y h =
let g (K x) z = h (x (K x)) z in
g (K g);;
Y : ((’a -> ’b) -> ’a -> ’b) -> ’a -> ’b = <fun>
#let fact = Y (fun f n -> if n = 0 then 1 else n * f(n - 1));;
fact : int -> int = <fun>
#fact 6;;
it : int = 720
4
Proof: consider C = {i(s) | s ∈ ℘(X) and i(s) ∈ s}. If i : ℘(X) → X is injective, we have
i(C) ∈ C ≡ i(C) ∈ C, a contradiction. This is similar to the Russell paradox, and in fact probably
inspired it. The analogy is even closer if we consider the equivalent form that there is no surjection
j : X → ℘(X), and prove it by considering {s | s ∈ j(s)}.
5
Readers familiar with untyped λ-calculus may note that if the Ks are deleted, this is essentially
the usual definition of the Y combinator.