Filter
Top Products
58 CHAPTER 6. IMPLEMENTATION IN CAML
mk_type :string * hol_type list -> hol_type creates a composite type given
the name of a type constructor and a list of component types of the right length.
It fails if the name is not that of a constructor, or if the constructor’s arity doesn’t
match the length of the list.
#mk_type("bool",[mk_vartype "A"]);;
Uncaught exception: Failure "mk_type: wrong number of arguments to bool"
#mk_type("bool",[]);;
it : hol_type = ‘:bool‘
#mk_type("fun",[it; it]);;
it : hol_type = ‘:bool->bool‘
dest_vartype :hol_type -> string reverses the effect of mk_vartype, i.e.
takes a type variable and returns its name. It fails if the type isn’t a type vari-
able.
#dest_vartype ‘:A‘;;
it : string = "A"
#dest_vartype ‘:bool‘;;
Uncaught exception: Failure "dest_vartype: type constructor not a variable"
#dest_vartype (mk_vartype "bool");;
it : string = "bool"
Analogously, dest_type :hol_type -> string * hol_type list reverses the
effect of mk_type, and fails if given a type variable.
#dest_type ‘:bool‘;;
it : string * hol_type list = "bool", []
#dest_type ‘:A‘;;
Uncaught exception: Failure "dest_type: type variable not a constructor"
#dest_type ‘:bool->bool‘;;
it : string * hol_type list = "fun", [‘:bool‘; ‘:bool‘]
The functions is_type :hol_type -> bool and is_vartype :hol_type -> bool
test whether a HOL type is a composite type or a type variable respectively.
6.2 Terms
The CAML function get_const_type :string -> hol_type finds the type of the
appropriately-named constant, or fails if there is no constant of that name. Some
constants have polymorphic type, meaning a type including type variables. Such a
constant can have any type that arises from replacing the component type variables
consistently by other types. For example the equality constant is a curried operator
of two arguments, but the types of the arguments are arbitrary, provided they are
the same:
#get_const_type "=";;
it : hol_type = ‘:A->(A->bool)‘
In such cases, the type returned by get_const_type is a most general type, and
can be specialized by setting type variables appropriately. In general, terms feature
instances of polymorphic constants. The type of an arbitrary term can by found
using type_of :term -> hol_type, e.g.