doc-src/Ref/theories.tex

Minor edits to discussion of use_thy

%% $Id$

\chapter{Theories, Terms and Types} \label{theories}
\index{theories|(}\index{signatures|bold}
\index{reading!axioms|see{{\tt extend_theory} and {\tt assume_ax}}}
Theories organize the syntax, declarations and axioms of a mathematical
development.  They are built, starting from the Pure theory, by extending
and merging existing theories.  They have the \ML{} type \ttindex{theory}.
Theory operations signal errors by raising exception \ttindex{THEORY},
returning a message and a list of theories.

Signatures, which contain information about sorts, types, constants and
syntax, have the \ML{} type~\ttindexbold{Sign.sg}.  For identification,
each signature carries a unique list of {\bf stamps}, which are~\ML{}
references (to strings).  The strings serve as human-readable names; the
references serve as unique identifiers.  Each primitive signature has a
single stamp.  When two signatures are merged, their lists of stamps are
also merged.  Every theory carries a unique signature.

Terms and types are the underlying representation of logical syntax.  Their
\ML{} definitions are irrelevant to naive Isabelle users.  Programmers who wish
to extend Isabelle may need to know such details, say to code a tactic that
looks for subgoals of a particular form.  Terms and types may be
`certified' to be well-formed with respect to a given signature.

\section{Defining Theories}
\label{DefiningTheories}

Theories can be defined either using concrete syntax or by calling certain
\ML-functions (see \S\ref{BuildingATheory}).  Figure~\ref{TheorySyntax}
presents the concrete syntax for theories.  This grammar employs the
following conventions: 
\begin{itemize}
\item Identifiers such as $theoryDef$ denote nonterminal symbols.
\item Text in {\tt typewriter font} denotes terminal symbols.
\item \ldots{} indicates repetition of a phrase.
\item A vertical bar~($|$) separates alternative phrases.
\item Square [brackets] enclose optional phrases.
\item $id$ stands for an Isabelle identifier.
\item $string$ stands for an ML string, with its quotation marks.
\item $k$ stands for a natural number.
\item $text$ stands for arbitrary ML text.
\end{itemize}

\begin{figure}[hp]
\begin{center}
\begin{tabular}{rclc}
$theoryDef$ &=& $id$ {\tt=} $name@1$ {\tt+} \dots {\tt+} $name@n$
                            [{\tt+} $extension$]\\\\
$extension$ &=& [$classes$] [$default$] [$types$] [$arities$] [$consts$]
                [$trans$] [$rules$] {\tt end} [$ml$]\\\\
$classes$ &=& \ttindex{classes} $class$ \dots $class$ \\\\
$class$ &=& $id$ [{\tt<} $id@1${\tt,} \dots{\tt,} $id@n$] \\\\
$default$ &=& \ttindex{default} $sort$ \\\\
$sort$ &=& $id$ ~~$|$~~ {\tt\{} $id@1${\tt,} \dots{\tt,} $id@n$ {\tt\}} \\\\
$name$ &=& $id$ ~~$|$~~ $string$ \\\\
$types$ &=& \ttindex{types} $typeDecl$ \dots $typeDecl$ \\\\
$typeDecl$ &=& $name${\tt,} \dots{\tt,} $name$ $k$
               [{\tt(} $infix$ {\tt)}] \\\\
$infix$ &=& \ttindex{infixl} $k$ ~~$|$~~ \ttindex{infixr} $k$ \\\\
$arities$ &=& \ttindex{arities} $arityDecl$ \dots $arityDecl$ \\\\
$arityDecl$ &=& $name${\tt,} \dots{\tt,} $name$ {\tt::} $arity$ \\\\
$arity$ &=& [{\tt(} $sort${\tt,} \dots{\tt,} $sort$ {\tt)}] $id$ \\\\
$consts$ &=& \ttindex{consts} $constDecl$ \dots $constDecl$ \\\\
$constDecl$ &=& $name@1${\tt,} \dots{\tt,} $name@n$ {\tt::} $string$
                [{\tt(} $mixfix$ {\tt)}] \\\\
$mixfix$ &=& $string$
             [ [\quad{\tt[} $k@1${\tt,} \dots{\tt,} $k@n$ {\tt]}\quad] $k$]\\
       &$|$& $infix$ \\
       &$|$& \ttindex{binder} $string$ $k$\\\\
$trans$ &=& \ttindex{translations} $transDecl$ \dots $transDecl$ \\\\
$transDecl$ &=& [ {\tt(}$string${\tt)} ] $string$ 
  [ {\tt=>} $|$ {\tt<=} $|$ {\tt==} ] [ ($string$) ] $string$ \\\\
$rules$ &=& \ttindex{rules} $rule$ \dots $rule$ \\\\
$rule$ &=& $id$ $string$ \\\\
$ml$ &=& \ttindex{ML} $text$
\end{tabular}
\end{center}
\caption{Theory Syntax}
\label{TheorySyntax}
\end{figure}

The different parts of a theory definition are interpreted as follows:
\begin{description} 
\item[$theoryDef$] A theory has a name $id$ and is an
  extension of the union of theories $name@1$ \dots $name@n$ with new
  classes, types, constants, syntax and axioms. The basic theory, which 
  contains only the meta-logic, is called {\tt Pure}.

  If $name@i$ is a string, then theory $name@i$ is {\em not} used in building
  the base of theory $id$. Strings stand for ML-files rather than
  theory-files and document the dependence if $id$ on additional files. This
  is required because $name@1$ \dots $name@n$ are loaded automatically when
  theory $id$ is (re)built. See Chapter~\ref{LoadingTheories} for details.
\item[$class$] The new class $id$ is declared as a subclass of existing
  classes $id@1$ \dots $id@n$.  This rules out cyclic class structures.
  Isabelle automatically computes the transitive closure of subclass
  hierarchies.  Hence it is not necessary to declare $c@1 < c@3$ in addition
  to $c@1 < c@2$ and $c@2 < c@3$.
\item[$default$] introduces $sort$ as the new default sort for type
  variables.  Unconstrained type variables in an input string are
  automatically constrained by $sort$; this does not apply to type variables
  created internally during type inference.  If omitted,
  the default sort is the same as in the parent theory.
\item[$sort$] is a finite set $id@1$ \dots $id@n$ of classes; a single class
  $id$ abbreviates the singleton set {\tt\{}$id${\tt\}}.
\item[$name$] is either an alphanumeric identifier or an arbitrary string.
\item[$typeDecl$] Each $name$ is declared as a new type constructor with
  $k$ arguments.  Only binary type constructors can have infix status and
  symbolic names ($string$).
\item[$infix$] declares a type or constant to be an infix operator of
  precedence $k$ associating to the left ({\tt infixl}) or right ({\tt
    infixr}).
\item[$arityDecl$] Each existing type constructor $name@1$ \dots $name@n$
  is given the additional arity $arity$.
\item[$constDecl$] The new constants $name@1$ \dots $name@n$ are declared to
  be of type $string$.  For display purposes they can be annotated with
  $mixfix$ declarations.
\item[$mixfix$] $string$ is a mixfix template of the form {\tt"}\dots{\tt\_}
  \dots{\tt\_} \dots{\tt"} where the $i$-th underscore indicates the position
  where the $i$-th argument should go, $k@i$ is the minimum precedence of
  the $i$-th argument, and $k$ the precedence of the construct.  The list
  \hbox{\tt[$k@1$, \dots, $k@n$]} is optional.

  Binary constants can be given infix status.

  A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em
    binder} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated
  like $f(F)$; $p$ is the precedence of the construct.
\item[$transDecl$] Specifies a syntactic translation rule, that is a parse 
  rule ({\tt =>}), a print rule ({\tt <=}), or both ({\tt ==}).
\item[$rule$] A rule consists of a name $id$ and a formula $string$.  Rule
  names must be distinct.
\item[$ml$] This final part of a theory consists of ML code, 
  typically for parse and print translations.
\end{description}
The $mixfix$, $transDecl$ and $ml$ sections are explained in more detail in 
the {\it Defining Logics} chapter of the {\it Logics} manual.


\subsection{Classes and types}
\index{*arities!context conditions}

Type declarations are subject to the following two well-formedness
conditions:
\begin{itemize}
\item There are no two declarations $ty :: (\vec{r})c$ and $ty :: (\vec{s})c$
  with $\vec{r} \neq \vec{s}$.  For example
\begin{ttbox}
types ty 1
arities ty :: ({\ttlbrace}logic{\ttrbrace}) logic
        ty :: ({\ttlbrace}{\ttrbrace})logic
\end{ttbox}
leads to an error message and fails.
\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
  (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
  for $i=1,\dots,n$.  The relationship $\preceq$, defined as
\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
expresses that the set of types represented by $s'$ is a subset of the set of
types represented by $s$.  For example
\begin{ttbox}
classes term < logic
types ty 1
arities ty :: ({\ttlbrace}logic{\ttrbrace})logic
        ty :: ({\ttlbrace}{\ttrbrace})term
\end{ttbox}
leads to an error message and fails.
\end{itemize}
These conditions guarantee principal types~\cite{nipkow-prehofer}.


\section{Loading Theories}
\label{LoadingTheories}
\subsection{Reading a new theory}

Each theory definition must reside in a separate file.  Let the file {\it
  tf}{\tt.thy} contain the definition of a theory called $TF$ with parent
theories $TB@1$ \dots $TB@n$.  Calling \ttindexbold{use_thy}~{\tt"}{\it
  TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file
{\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. \indexbold{automatic
loading}  Any of the parent theories that have not been loaded yet are read now
by recursive {\tt use_thy} calls until either an already loaded theory or {\tt
  Pure} is reached.  Therefore one can read a complete logic by just one {\tt
use_thy} call if all theories are linked appropriately.  Afterwards an {\ML}
structure~$TF$ containing a component {\tt thy} for the new theory and
components $r@1$ \dots $r@n$ for the rules is declared; it also contains the
definitions of the {\tt ML} section if any. Unless
\ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it tf}{\tt.thy.ML}
is deleted if no errors occurred. Finally the file {\it tf}{\tt.ML} is read, if
it exists; this file normally contains proofs involving the new theory.


\subsection{Filenames and paths}
\indexbold{filenames}

The files defining the theory must have the lower case name of the theory
with {\tt".thy"} or {\tt".ML"} appended.  On the other hand
\ttindex{use_thy}'s parameter has to be the exact theory name.  Optionally
the name can be preceded by a path to specify the directory where the
files can be found.  If no path is provided the reference variable
\ttindexbold{loadpath} is used which contains a list of paths that are
searched in the given order.  After the {\tt".thy"}-file for a theory has
been found, the same path is used to locate the (optional) {\tt".ML"}-file.

It is also possible to provide only a {\tt".ML"}-file, with no
{\tt".thy"}-file.  In this case the {\tt".ML"}-file must declare an \ML{}
structure having the theory's name.  If both the {\tt".thy"}-file and a
structure declaration in the {\tt".ML"}-file exist, then the latter
declaration is used.  See {\tt ZF/ex/llist.ML} for an example.


\subsection{Reloading a theory}
\index{reloading a theory}

\ttindex{use_thy} keeps track of all loaded theories and stores information
about their files.  If it finds that the theory to be loaded was already read
before, the following happens: First the theory's files are searched at the
place they were located the last time they were read. If they are found, their
time of last modification is compared to the internal data and {\tt use_thy}
stops if they are equal. In case the files have been moved, {\tt use_thy}
searches them the same way a new theory would be searched for.  After all these
tests have been passed, the theory is reloaded and all theories that depend on
it (those that have its name in their $theoryDef$) are marked as out-of-date.

As changing a theory often makes it necessary to reload all theories that
(indirectly) depend on it, \ttindexbold{update} should be used instead of {\tt
use_thy} to read a modified theory.  This function reloads all changed
theories and their descendants in the correct order.


\subsection{Pseudo theories}
\indexbold{pseudo theories}

There is a problem with \ttindex{update}: objects created in \ML-files that do
not belong to a theory (see explanation of $theoryDef$ in
\ref{DefiningTheories}).  These files are read manually between {\tt use_thy}
calls and define objects used in different theories.  As {\tt update} only
knows about the theories there still exist objects with references to the old
theory version after the new one has been read.  This (most probably) will
produce the fatal error
\begin{center} \tt
Attempt to merge different versions of theory: $T$
\end{center}

Therefore there is a way to link theories and the $orphaned$ \ML-files. The
link from a theory to an \ML-file has been mentioned in
Chapter~\ref{DefiningTheories} (strings in $theoryDef$).  But to make this
work and to establish a link in the opposite direction we need to create a
{\it pseudo theory}.  Let's assume we have an \ML-file named {\tt orphan.ML}
that depends on theory $A$ and is itself used in theory $B$.  To link the
three we have to create the file {\tt orphan.thy} containing the line
\begin{ttbox}
orphan = A
\end{ttbox}
and add {\tt "orphan"} to the list of $B$'s parents.  Creating {\tt
  orphan.thy} is necessary because of two reasons: First it enables automatic
loading of $orphan$'s parents and second it creates the \ML{}-object {\tt
  orphan} that is needed by {\tt use_thy} (though it is not added to the base
of theory $B$).  If {\tt orphan.ML} depended on no theory then {\tt Pure}
would have been used instead of {\tt A}.

For an extensive example of how this technique can be used to link over 30
files and read them by just two {\tt use_thy} calls have a look at the ZF
logic.


\subsection{Removing a theory}
\index{removing theories}

If a previously read file is removed the \ttindex{update} function will keep
on complaining about a missing file.  The theory is not automatically removed
from the internal list to preserve the links to other theories in case one
forgot to adjust the {\tt loadpath} after moving a file.  To manually remove a
theory use \ttindexbold{unlink_thy}.


\subsection{Using Poly/\ML}
\index{Poly/\ML}
\index{reference variables}

As the functions for reading theories depend on reference variables one has to
take into consideration the way Poly/\ML{} handles them.  They are only saved
together with the state if they were declared in the current database.  E.g.
changes made to a reference variable declared in the $Pure$ database are $not$
saved if made while using a child database.  Therefore a new {\tt Readthy}
structure has to be declared by
\begin{ttbox}
structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
Readthy.loaded_thys := !loaded_thys;
open Readthy;
\end{ttbox}
in every newly created database.  By copying the contents of the old reference
variable loaded_thys the list of already loaded theories is preserved. Of
course this is not necessary if no theories have been read yet.


\section{Basic operations on theories}
\subsection{Extracting an axiom from a theory}
\index{theories!extracting axioms|bold}\index{axioms}
\begin{ttbox} 
get_axiom: theory -> string -> thm
assume_ax: theory -> string -> thm
\end{ttbox}
\begin{description}
\item[\ttindexbold{get_axiom} $thy$ $name$] 
returns an axiom with the given $name$ from $thy$, raising exception
\ttindex{THEORY} if none exists.  Merging theories can cause several axioms
to have the same name; {\tt get_axiom} returns an arbitrary one.

\item[\ttindexbold{assume_ax} $thy$ $formula$] 
reads the {\it formula} using the syntax of $thy$, following the same
conventions as axioms in a theory definition.  You can thus pretend that
{\it formula} is an axiom; in fact, {\tt assume_ax} returns an assumption.
You can use the resulting theorem like an axiom.  Note that 
\ttindex{result} complains about additional assumptions, but 
\ttindex{uresult} does not.

For example, if {\it formula} is
\hbox{\tt a=b ==> b=a} then the resulting theorem might have the form
\hbox{\tt\frenchspacing ?a=?b ==> ?b=?a  [!!a b. a=b ==> b=a]}
\end{description}

\subsection{Building a theory}
\label{BuildingATheory}
\index{theories!constructing|bold}
\begin{ttbox} 
pure_thy: theory
merge_theories: theory * theory -> theory
extend_theory: theory -> string
        -> (class * class list) list 
           * sort
           * (string list * int)list
           * (string list * (sort list * class))list
           * (string list * string)list * sext option
        -> (string*string)list -> theory
\end{ttbox}
Type \ttindex{class} is a synonym for {\tt string}; type \ttindex{sort} is
a synonym for \hbox{\tt class list}.
\begin{description}
\item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax
  of the meta-logic.  There are no axioms: meta-level inferences are carried
  out by \ML\ functions.
\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
  theories $thy@1$ and $thy@2$.  The resulting theory contains all types,
  constants and axioms of the constituent theories; its default sort is the
  union of the default sorts of the constituent theories.
\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
      ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
\hfill\break   %%% include if line is just too short
is the \ML-equivalent of the following theory definition:
\begin{ttbox}
\(T\) = \(thy\) +
classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
        \dots
default {\(d@1,\dots,d@r\)}
types   \(tycon@1\),\dots,\(tycon@i\) \(n\)
        \dots
arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
        \dots
consts  \(b@1\),\dots,\(b@k\) :: \(\tau\)
        \dots
rules   \(name\) \(rule\)
        \dots
end
\end{ttbox}
where
\begin{tabular}[t]{l@{~=~}l}
$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
$types$   & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
\\
$consts$  & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
$rules$   & \tt[("$name$",$rule$),\dots]
\end{tabular}

If theories are defined as in \S\ref{DefiningTheories}, new syntax is added
as mixfix annotations to constants.  Using {\tt extend_theory}, new syntax can
be added via $sextopt$ which is either {\tt None}, or {\tt Some($sext$)}.  The
latter case is not documented.

$T$ identifies the theory internally.  When a theory is redeclared, say to
change an incorrect axiom, bindings to the old axiom may persist.  Isabelle
ensures that the old and new theories are not involved in the same proof.
Attempting to combine different theories having the same name $T$ yields the
fatal error
\begin{center} \tt
Attempt to merge different versions of theory: $T$
\end{center}
\end{description}


\subsection{Inspecting a theory}
\index{theories!inspecting|bold}
\begin{ttbox} 
print_theory  : theory -> unit
axioms_of     : theory -> (string*thm)list
parents_of    : theory -> theory list
sign_of       : theory -> Sign.sg
stamps_of_thy : theory -> string ref list
\end{ttbox}
These provide a simple means of viewing a theory's components.
Unfortunately, there is no direct connection between a theorem and its
theory.
\begin{description}
\item[\ttindexbold{print_theory} {\it thy}]  
prints the theory {\it thy\/} at the terminal as a set of identifiers.

\item[\ttindexbold{axioms_of} $thy$] 
returns the axioms of~$thy$ and its ancestors.

\item[\ttindexbold{parents_of} $thy$] 
returns the parents of~$thy$.  This list contains zero, one or two
elements, depending upon whether $thy$ is {\tt pure_thy}, 
\hbox{\tt extend_theory $thy$} or \hbox{\tt merge_theories ($thy@1$, $thy@2$)}.

\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
returns the stamps of the signature associated with~$thy$.

\item[\ttindexbold{sign_of} $thy$] 
returns the signature associated with~$thy$.  It is useful with functions
like {\tt read_instantiate_sg}, which take a signature as an argument.
\end{description}


\section{Terms}
\index{terms|bold}
Terms belong to the \ML{} type \ttindexbold{term}, which is a concrete datatype
with six constructors: there are six kinds of term.
\begin{ttbox}
type indexname = string * int;
infix 9 $;
datatype term = Const of string * typ
              | Free  of string * typ
              | Var   of indexname * typ
              | Bound of int
              | Abs   of string * typ * term
              | op $  of term * term;
\end{ttbox}
\begin{description}
\item[\ttindexbold{Const}($a$, $T$)] 
is the {\bf constant} with name~$a$ and type~$T$.  Constants include
connectives like $\land$ and $\forall$ (logical constants), as well as
constants like~0 and~$Suc$.  Other constants may be required to define the
concrete syntax of a logic.

\item[\ttindexbold{Free}($a$, $T$)] 
is the {\bf free variable} with name~$a$ and type~$T$.

\item[\ttindexbold{Var}($v$, $T$)] 
is the {\bf scheme variable} with indexname~$v$ and type~$T$.  An
\ttindexbold{indexname} is a string paired with a non-negative index, or
subscript; a term's scheme variables can be systematically renamed by
incrementing their subscripts.  Scheme variables are essentially free
variables, but may be instantiated during unification.

\item[\ttindexbold{Bound} $i$] 
is the {\bf bound variable} with de Bruijn index~$i$, which counts the
number of lambdas, starting from zero, between a variable's occurrence and
its binding.  The representation prevents capture of variables.  For more
information see de Bruijn \cite{debruijn72} or
Paulson~\cite[page~336]{paulson91}.

\item[\ttindexbold{Abs}($a$, $T$, $u$)] 
is the {\bf abstraction} with body~$u$, and whose bound variable has
name~$a$ and type~$T$.  The name is used only for parsing and printing; it
has no logical significance.

\item[\tt $t$ \$ $u$] \index{$@{\tt\$}|bold}
is the {\bf application} of~$t$ to~$u$.  
\end{description}
Application is written as an infix operator in order to aid readability.
For example, here is an \ML{} pattern to recognize first-order formula of
the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
\begin{ttbox} 
Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
\end{ttbox}


\section{Certified terms}
\index{terms!certified|bold}\index{signatures}
A term $t$ can be {\bf certified} under a signature to ensure that every
type in~$t$ is declared in the signature and every constant in~$t$ is
declared as a constant of the same type in the signature.  It must be
well-typed and must not have any `loose' bound variable
references.\footnote{This concerns the internal representation of variable
binding using de Bruijn indexes.} Meta-rules such as {\tt forall_elim} take
certified terms as arguments.

Certified terms belong to the abstract type \ttindexbold{Sign.cterm}.
Elements of the type can only be created through the certification process.
In case of error, Isabelle raises exception~\ttindex{TERM}\@.

\subsection{Printing terms}
\index{printing!terms|bold}
\begin{ttbox} 
Sign.string_of_cterm :      Sign.cterm -> string
Sign.string_of_term  : Sign.sg -> term -> string
\end{ttbox}
\begin{description}
\item[\ttindexbold{Sign.string_of_cterm} $ct$] 
displays $ct$ as a string.

\item[\ttindexbold{Sign.string_of_term} $sign$ $t$] 
displays $t$ as a string, using the syntax of~$sign$.
\end{description}

\subsection{Making and inspecting certified terms}
\begin{ttbox} 
Sign.cterm_of   : Sign.sg -> term -> Sign.cterm
Sign.read_cterm : Sign.sg -> string * typ -> Sign.cterm
Sign.rep_cterm  : Sign.cterm -> \{T:typ, t:term, 
                                 sign: Sign.sg, maxidx:int\}
\end{ttbox}
\begin{description}
\item[\ttindexbold{Sign.cterm_of} $sign$ $t$] \index{signatures}
certifies $t$ with respect to signature~$sign$.

\item[\ttindexbold{Sign.read_cterm} $sign$ ($s$, $T$)] 
reads the string~$s$ using the syntax of~$sign$, creating a certified term.
The term is checked to have type~$T$; this type also tells the parser what
kind of phrase to parse.

\item[\ttindexbold{Sign.rep_cterm} $ct$] 
decomposes $ct$ as a record containing its type, the term itself, its
signature, and the maximum subscript of its unknowns.  The type and maximum
subscript are computed during certification.
\end{description}


\section{Types}
\index{types|bold}
Types belong to the \ML{} type \ttindexbold{typ}, which is a concrete
datatype with three constructors.  Types are classified by sorts, which are
lists of classes.  A class is represented by a string.
\begin{ttbox}
type class = string;
type sort  = class list;

datatype typ = Type  of string * typ list
             | TFree of string * sort
             | TVar  of indexname * sort;

infixr 5 -->;
fun S --> T = Type("fun",[S,T]);
\end{ttbox}
\begin{description}
\item[\ttindexbold{Type}($a$, $Ts$)] 
applies the {\bf type constructor} named~$a$ to the type operands~$Ts$.
Type constructors include~\ttindexbold{fun}, the binary function space
constructor, as well as nullary type constructors such
as~\ttindexbold{prop}.  Other type constructors may be introduced.  In
expressions, but not in patterns, \hbox{\tt$S$-->$T$} is a convenient
shorthand for function types.

\item[\ttindexbold{TFree}($a$, $s$)] 
is the {\bf free type variable} with name~$a$ and sort~$s$.

\item[\ttindexbold{TVar}($v$, $s$)] 
is the {\bf scheme type variable} with indexname~$v$ and sort~$s$.  Scheme
type variables are essentially free type variables, but may be instantiated
during unification.
\end{description}


\section{Certified types}
\index{types!certified|bold}
Certified types, which are analogous to certified terms, have type 
\ttindexbold{Sign.ctyp}.

\subsection{Printing types}
\index{printing!types|bold}
\begin{ttbox} 
Sign.string_of_ctyp :      Sign.ctyp -> string
Sign.string_of_typ  : Sign.sg -> typ -> string
\end{ttbox}
\begin{description}
\item[\ttindexbold{Sign.string_of_ctyp} $cT$] 
displays $cT$ as a string.

\item[\ttindexbold{Sign.string_of_typ} $sign$ $T$] 
displays $T$ as a string, using the syntax of~$sign$.
\end{description}


\subsection{Making and inspecting certified types}
\begin{ttbox} 
Sign.ctyp_of  : Sign.sg -> typ -> Sign.ctyp
Sign.rep_ctyp : Sign.ctyp -> \{T: typ, sign: Sign.sg\}
\end{ttbox}
\begin{description}
\item[\ttindexbold{Sign.ctyp_of} $sign$ $T$] \index{signatures}
certifies $T$ with respect to signature~$sign$.

\item[\ttindexbold{Sign.rep_ctyp} $cT$] 
decomposes $cT$ as a record containing the type itself and its signature.
\end{description}

\index{theories|)}