Filter
Top Products
Chapter 6
Implementation in CAML
The above description of HOL’s logical basics abstracted away somewhat from its
actual realization in CAML. However it has a fairly direct realization as three CAML
types to represent HOL types, terms and theorems. (Note the object-meta distinc-
tion here: one has a CAML type of data structures representing HOL types.) These
CAML types are all treated as abstract, with members only being created via spe-
cial interface functions.
1
This guards against construction of meaningless types
(e.g. using undefined type constructors), ill-typed terms, and theorems that have
not been proved using the primitive rules.
6.1 Types
Each HOL type is either a type variables, or a type constructor applied to other
types. Primitive types like bool are treated as nullary constructors, i.e. constructors
with no arguments. We will now show some of the most useful CAML functions for
manipulating types.
get_type_arity :string -> int finds the arity of the appropriately-named
type constructor. If there is no type constructor with that name, it fails. For
example:
#get_type_arity "bool";;
it : int = 0
#get_type_arity "fun";;
it : int = 2
#get_type_arity "con";;
Uncaught exception: Failure "find"
The rest of the functions divide nicely into three groups: those for creating HOL
types, those for breaking them apart, and those for testing their structure.
mk_vartype :string -> hol_type creates a type variable with the requested
name. This is permissible even if there is also a type constant of that name, but
can look confusing. For example:
#mk_vartype "A";;
it : hol_type = ‘:A‘
#mk_vartype "bool";;
it : hol_type = ‘:bool‘
1
This could actually be enforced by the CAML system by separately compiling the modules.
57