Filter
Top Products
4 CHAPTER 1. INTRODUCTION
This however hides quite a lot of processing. Quotations are expanded (by a
front-end filter separate from CAML proper) into a call of a term parser and type
inferencer. This not only analyzes the syntactic structure of the term but works
out types for the term as a whole and all its subterms. For example, it knows that
the constant 1 has type num, and that the left and right arguments of + must have
the same type, which is also the type of the result. Hence it decides that x and
the term as a whole must also have type num. If the user tries to enter a term that
cannot be typed, e.g. ‘(1 <= 2) + 3‘, the typechecker will fail. If, on the other
hand, there is not enough type information to fix the types of all subterms, type
variables are invented and a warning given:
#‘x‘;;
Warning: inventing type variables
it : term = ‘x‘
The use can annotate the term or any subterms with types by writing a colon
followed by a type, e.g.
#‘x:num‘;;
it : term = ‘x‘
The parser does not allow the same variable to have different types in the same
term.
4
It is possible to create such terms by hand using the functions described
later, but is apt to look confusing. Note that identically-named variables with
different types are treated as different. Types, rather than terms, can be entered
by simply omitting the term, i.e. starting the quotation with a colon, e.g.
#‘:bool‘;;
it : hol_type = ‘:bool‘
HOL types and terms are not actually ML abstract types (they could easily be
made so by separately compiling the modules), but the user is expected to use the
standard interface functions. These restrict formation to those that are well-formed
and well-typed. So even using the basic constructors, it is impossible to create, for
example, a term that adds a number and a boolean value. Theorems can also only
be created by, at bottom, a small set of basic functions. One of these is the function
REFL which takes a term t as an argument and returns a rather trivial theorem
saying that t is equal to itself:
#REFL ‘x + 1‘;;
it : thm = |- x + 1 = x + 1
HOL prints theorems using an ASCII approximation to the conventional ‘turn-
stile’ symbol . If a theorem has assumptions, these are printed to the left of the
turnstile. For example, another primitive function ASSUME takes a term p of Boolean
type and returns the theorem (once again rather trivial) that under the assumption
that p holds, p holds:
#ASSUME ‘p:bool‘;;
it : thm = p |- p
#ASSUME ‘1‘;;
Uncaught exception: Failure "ASSUME: not a proposition"
4
Or more precisely, in the same scope. Separately bound instances can have different types —
see later.