types.tex

%!TEX root = reference.tex
\chapter{Types}
\label{types}
\index{type system}
\Sr is a strongly, statically, typed language. That means that all values and all variables must have a unique well-defined type that is determinable by inspecting the text of the program -- effectively at `compile time'.

The type system of \Sr consists of a method for declaring new types, for annotating variables (and by extension programs) with their types and a system of verifying the type consistency of programs.

\section{What is a Type?}
A \ntRef{Type} is an expression that denotes a set of values. 
\begin{aside}
Although a type is an expression, type expressions should not be confused with normal expressions. Types generally play no part in evaluation.
\end{aside}
Viewed as sets, types have some particular properties: no value may be a member of more than one type set; all values are members of exactly one type set.

A \ntRef{TypeDefinition} introduces a new type and defines what values belong to the type. A \ntRef{TypeAnnotation} is an assertion that a particular expression has a certain type.

For many simple cases, a type is denoted by an identifier. For example, the type identifier \q{string} denotes the set of all strings. More explicitly, a value has type \q{string} iff\footnote{The term `iff' means `if and only if'.} it belongs to the set denoted by the symbol \q{string}.

Many value-sets are effectively infinite in size: the size of the set of \q{string}s is essentially unbounded; as is the set of \q{integer} values.

In addition to sets of values denoted by identifiers; there are other kinds of value sets that have more complex type expressions. For example, the set of \emph{function values} is denoted not by a single type expression but a \emph{schema} of type expressions -- each taking a form such as:
\begin{alltt}
(t\sub1\sequence{,}t\subn)=>t
\end{alltt}
For example, the type expression
\begin{alltt}
(integer)=>string
\end{alltt}
denotes the set of functions that take an \q{integer} as an argument and produce a \q{string} value. Like the set of all integers, this set is also infinite in size.

The language for denoting types is quite expressive. It is possible to have types that are parameterized; that is they are composed from other type expressions. It is also possible to have types that are not explicitly named but are defined by constraints.

A simple example of a parameterized type is the \q{cons} type: a \q{cons} type expression always involves the mention of another type -- the type of elements of the list. The type expression
\begin{alltt}
cons of string
\end{alltt}
denotes the type expression associated with lists whose elements are all string values. Other examples of \q{cons} type include lists of integers:
\begin{alltt}
cons of integer
\end{alltt}
and even lists of lists of string valued functions:
\begin{alltt}
cons of cons of ((integer)=>string)
\end{alltt}
\noindent\begin{aside}
Technically, the \q{cons} symbol in:
\begin{alltt}
cons of integer
\end{alltt}
\index{type function}
is a \ntRef{TypeConstructor}: it takes a type as an argument and returns another type as result.
\end{aside}
Often it is convenient to be able to `talk' about types without being specific about the type itself; for this purpose we use \ntRef{TypeVariable}s.

There are two ways in which a type variable is distinguished: either by an explicit quantifier (\ntRef{UniversalType} or \ntRef{ExistentialType}) or by prefixing a \q{\pcent{}} in front of the identifier. The type expression:
\begin{alltt}
cons of \pcent{}t
\end{alltt}
denotes a list type of some unspecified element type.

\begin{aside}
The value set associated with this type expression is a little more difficult to visualize than the set of lists of integers (say). \q{cons of \pcent{}t} denotes a set of list values; but without more information \emph{we cannot say} what the complete values look like -- it is dependent on the meaning of the type variable \q{\pcent{}t}.
\end{aside}

\begin{aside}
In order to properly understand the interpretation of a type variable one must understand how the type variable is 'bound'. In general, there are three possibilities: the type variable may be identified with (equal to) another type; the type variable may be bound by a universal quantifier or by an existential quantifier.

A universally quantified type (see Section~\vref{universalType}) denotes a type that allows all possible instantiations for the type variable. For example, function types often involve universal types. A universally typed function is expected to work `for all values' of the type variable -- which, in turn, means that the function definition can make no assumptions about the actual type.

Existentially quantified types (see Section~\vref{existentialType}) are  used to denote \emph{abstract types}; i.e., the existential quantifier signals that there is a type that should be treated as an opaque `black box'.
\end{aside}

\begin{aside}
It is not required to annotate a type variable with a leading \q{\pcent{}}. If an identifier is identified as a type variable by virtue of the fact that it is bound by an explicit quantifier then the leading \q{\pcent{}} is not required.

However, for exposition purposes, especially where it is not clear what the binding of a type variable may be, we will use an explicit \q{\pcent{}} to identify type variables.
\end{aside}

\subsubsection{Type Safety}
The connection between the argument type of a \q{cons} type expression and the actual elements of lists is denoted by a \emph{type inference rule}. Type inference rules are rules for relating expressions and statements in the language to the types associated with that statement. For example, the rule:
\begin{prooftree}
\AxiomC{\typeprd{E}{El\sub1}{T}\sequence{\ }\typeprd{E}{El\subn}{T}}
\UnaryInfC{\typeprd{E}{\q{cons of [}El\sub1\sequence{,}El\subn\q{]}}{\q{cons of }T}}
\end{prooftree}
says that if the expressions \emph{El\sub1} through \emph{El\subn} all have type \emph{T}, then the list expression
\begin{alltt}
cons of [\emph{El\sub1}\sequence{,}\emph{El\subn}]
\end{alltt}
has type \q{cons of} T. This is the formal way of stating that all elements of a list must have the same type.

The general form of a type inference rule that is determining a type (sometimes called a type judgment) is:
\begin{prooftree}
\AxiomC{\mbox{\emph{Condition}}}
\UnaryInfC{\typeprd{E}{X}{T}}
\end{prooftree}
This should be read as
\begin{quote}
If \emph{Condition} is satisfied, then we can infer from the context \emph{E} that \emph{X} has type \emph{T}
\end{quote}
where the symbol \tinfers{} can be read as `type implication'. In general, the type of an expression depends on the context that it is found. 

\paragraph{Type Annotations}
In most cases it is not necessary to explicitly declare the type of a variable. However, it is good practice to declare explicitly the types of programs; especially within \ntRef{ThetaEnvironment}s.

For example, a generic function \q{consLength} that takes a \q{cons} list and returns an integer would have the declaration:
\begin{lstlisting}
consLength has type 
  for all t such that (cons of t)=>integer
\end{lstlisting}
This is an example of a universally quantified type -- see Section~\vref{universalType} for more details.

\paragraph{Kind Annotations}
\label{kindAnnotation}
Just as values have types, and the language system arranges to ensure that types are preserved, so types have \emph{kinds}. A \ntRef{Kind} is a `kind of type'.

\begin{aside}
Type \ntRef{Kind}s allow the language to keep track of the expected arity of a type: i.e., how many type arguments the type expected.
\end{aside}

\section{Type Expressions}
\label{typeExpressions}
\index{forms of types}
\index{type expressions}

Figure~\vref{typeFig} illustrates the top-levels of the different kinds of type expressions that the \Sr programmer will encounter.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{Type}&\arrow&\ntRef{TypeExpression}\\
&\choice&\ntRef{TypeVariable}\ \choice\ \ntRef{ReferenceType}\\
&\choice&\ntRef{TupleType}\\
&\choice&\ntRef{RecordType}\\
&\choice&\ntRef{FunctionType}\ \choice\ \ntRef{PatternType}\ \choice\ \ntRef{ConstructorType}\\
&\choice&\ntRef{UniversalType}\ \choice\ \ntRef{ExistentialType}\\
&\choice&\ntRef{Type}\ \q{where}\ \ntRef{TypeConstraint}\\
&\choice&\q{(}\ \ntRef{Type}\ \q{)}\\
&\choice&\ntRef{EncapsulatedType}
\end{eqnarray*}
\caption{Types of Types}
\label{typeFig}
\end{figure}

There are two main kinds of type expressions -- so-called \emph{structural} type expressions and \emph{named} type expression. A structural type expression encodes by convention the permitted \emph{forms} of values of that type. By contrast, a named type expression is defined via some form of \ntRef{TypeDefinition}.

A classic example of a structural type expression is the function type. A function type expression defines both the types of the arguments and result type of the function. But, more importantly, it signals that the value is a function.

A good example of a named type is the standard \q{integer} type. The word \q{integer} does not signal by itself that the allowable operations on integer values include arithmetic, comparison and so on. That information must come from additional statements and declarations. 

One of the other differences between structural and named type expressions is that the latter may be used to denote \emph{recursive} types, whereas the former cannot.

\begin{aside}
A recursive type is one whose values may contain elements that are themselves of the same type. For example, in a \q{tree} type: the nodes of the tree are typically themselves trees.
\end{aside}

\subsection{Type Expressions}
\label{typeNames}
\index{type}

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{TypeExpression}&\arrow&\ntRef{TypeConstructor}\ \q{of}\,\ntRef{TypeArgument}\\
&\choice&\ntRef{Identifier}\\
\ntDef{TypeArgument}&\arrow&\ntRef{Type}\\
&\choice&\q{(}\,\ntRef{Type}\sequence{,}\ntRef{Type}\q{)}\\
\ntDef{TypeConstructor}&\arrow&\ntRef{Identifier}\\
&\choice&\ntRef{TypeVar}
\end{eqnarray*}
\caption{Type Expressions}
\label{typeExpressionFig}
\end{figure}

A \ntRef{TypeExpression} is a term that identifies a class of values by name. The name may or may not have \ntRef{TypeArgument}s -- in which case, the type is said to be \emph{parameterized}.
\index{type!parameterized}
\index{parameterized types}

\subsubsection{Simple Types}
\label{simpleType}
\index{type!simple}
A simple type is \ntRef{TypeExpression} with no type arguments. Some simple types are pre-defined, Table~\vref{predefinedTypes} gives a table of such types.
\index{standard!simple types}

\begin{table}[h]
\begin{center}
\caption{Standard Pre-defined Types\label{predefinedTypes}}
\begin{tabular}{|ll|}
\hline
Type&Description\\
\hline
\tt boolean&used for logical values and conditions\\
\tt float&type of floating point numbers\\
\tt integer&type of 32-bit integer values\\
\tt long&type of 64-bit integer values\\
\tt decimal&type of decimal values\\
\tt string&type of string values\\
\tt quoted&type of abstract syntax\\
\tt astLocation&type of location marker\\
\tt exception&type of exception token\\
\hline
\end{tabular}
\end{center}
\end{table}

\subsubsection{Parameterized Types}
\label{parameterizedType}
\index{type!parameterized}
\index{parameterized type}

A parameterized \ntRef{TypeExpression} consists of a \ntRef{TypeConstructor} applied to one of more \ntRef{Type} arguments. For example, the standard \q{cons} type constructor has one type argument -- the type of elements of the \q{cons}.

Where a parameterized type has one type argument, the argument may be written without parentheses.
\begin{aside}
Excepting if the argument type is itself a tuple; in which case two parentheses will be needed.
\end{aside}
If the type name has two or more arguments, then the type arguments are enclosed in parentheses and separated by commas.

A parameterized type has a \emph{type arity} -- the number of type arguments it expects. This is defined when the type itself is defined. It is an error to write a type expression involving an incorrect number of type arguments.

Parameterized types may be defined using a \ntRef{TypeDefinition} statement.

\subsubsection{Variable Type Constructors}
\label{variableConstructor}
\index{type!variable constructor}
\index{type constructor expression}

A type expression of the form:
\begin{lstlisting}[mathescape=true]
%c of (%t$\sub1\sequence{,}$%t$\subn$)
\end{lstlisting}
denotes a rather special form of type: a type constructor expression. Like other parameterized type expressions, this expression does not denote a single type; but a set of types. For example, the type expression:
\begin{lstlisting}
%c of integer
\end{lstlisting}
denotes a type `something of \q{integer}'.

A subsequent constraint on \q{\pcent{}c} may cause it to be bound to the \ntRef{TypeConstructor} \q{cons} (say), in which case the type expression becomes ground to the parameterized type expression `\q{cons of integer}'.

Such type expressions are of most use in certain forms of \ntRef{Contract} where the contract is about a certain form of parameterized type.

\begin{aside}
Unlike parameterized type expressions, it is not possible to `define' a variable type constructor type. I.e., while we can define the \q{cons} type (see above) with a \ntRef{TypeDefinition} statement, we cannot define the type \q{\pcent{}c of integer} with an analogous statement.
\end{aside}

\begin{aside}
A variable constructor is equivalent to a regular type variable with a \ntRef{HasKind} constraint. I.e., 
\begin{lstlisting}[mathescape=true]
%c of (%t$\sub1\sequence{,}$%t$\subn$)
\end{lstlisting}
is equivalent to:
\begin{lstlisting}[mathescape=true]
%c of (%t$\sub1\sequence{,}$%t$\subn$) where %c has kind type of (type$\sequence{,}$type)
\end{lstlisting}
A \q{\pcent{}c} appearing on its own is assumed to have unknown arity, compatible with
\begin{lstlisting}
c where c has kind type
\end{lstlisting}
in cases where the type variable \q{c} is explicitly bound by a quantifier.
This is described more fully in Section~\vref{hasKindConstraint}.
\end{aside}

\subsection{Tuple Types}
\label{tupleType}
A tuple type is a tuple of types; written as a sequence of type expressions enclosed in parentheses.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{TupleType}&\arrow&\q{()}\\
&\choice&\q{((}\ntRef{Type}\q{))}\\
&\choice&\q{(}\ntRef{Type}\sequence{,}\ntRef{Type}\,\q{)}\plustwo
\end{eqnarray*}
\caption{Tuple Type}
\label{tupleTypeFig}
\end{figure}

A tuple type denotes a fixed grouping of elements. Each element of the tuple may have a different type.

There are two special cases in \ntRef{TupleType}s: the empty tuple and the singleton tuple type.

\subsubsection{Empty Tuple}
\index{tuple!empty tuple type}
The empty tuple type:
\begin{lstlisting}
()
\end{lstlisting}
refers to the empty tuple. It is useful primarily for writing function types where the function has no arguments:
\begin{lstlisting}
()=>string
\end{lstlisting}
When used as the return type of a function, the \q{()} type denotes a void result:
\begin{lstlisting}
(integer)=>()
\end{lstlisting}
\begin{aside}
The \q{()} type -- sometimes referred to as the \emph{unit type} -- is also used to denote the return type of some actions.
\end{aside}

\subsubsection{Singleton Tuple}
\index{tuple!singleton tuple type}

A singleton tuple must be written with two parentheses. This is to disambiguate such terms from simple expression parentheses. A type expression of the form:
\begin{lstlisting}
(integer)
\end{lstlisting}
is equivalent to just the \q{integer} type; whereas 
\begin{lstlisting}
((integer))
\end{lstlisting}
denotes the single element tuple type whose element type is \q{integer}.

\subsection{Record Type}
\label{recordType}
A \ntRef{RecordType} is a type expression that denotes a named association of fields and types. A record type is written as a sequence of type annotations enclosed in braces.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{RecordType}&\arrow&\q{\{}\,\ntRef{Annotation}\sequence{;}\ntRef{Annotation}\ \q{\}}\\
\ntDef{TypeEquality}&\arrow&\q{type}\ \ntRef{Identifier}\ \q{=}\ \ntRef{Type}
\end{eqnarray*}
\caption{Record Type}
\label{recordTypeFig}
\end{figure}

Record types are used as the type of anonymous records (see Section~\vref{anonRecord}). They are also the basis of other features of the type language -- including the \ntRef{ConstructorType} and \ntRef{Contract}s.

Two record types are equivalent if their elements are pair-wise equivalent. Note that the \emph{order} of elements is not important. For example, given the types:
\begin{lstlisting}
{a has type string ; b has type integer }
\end{lstlisting}
and
\begin{lstlisting}
{b has type integer ; a has type %t }
\end{lstlisting}
these types unify, provided that \q{\pcent{}t} is unifiable with \q{string}.

\begin{aside}
\begin{aside}
All user-defined types -- i.e., types defined by an \ntRef{AlgebraicType} definition -- have a \ntRef{RecordType} interface associated with them. This, as is detailed in Section~\vref{algebraicInterface}, defines a type for all of the fields in any of the constructors for the type. In turn, this permits a \ntRef{RecordAccess} expression to apply to a user-defined type as well as a \ntRef{RecordType}.
\end{aside}
\end{aside}

\subsection{Function Type}
\label{functionType}
\index{function type}
\index{type!function}
A function type denotes a function value. It takes the form of a possibly empty sequence of argument types -- denoting the types of the arguments to the function -- enclosed in parentheses; followed by the result type of the function. Figure~\vref{functionTypeFig} highlights the form of the function type.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{FunctionType}&\arrow&\q{(}\,\ntRef{Type}\sequence{,}\ntRef{Type}\ \q{) =>}\ \ntRef{Type}
\end{eqnarray*}
\caption{Function Type}
\label{functionTypeFig}
\end{figure}

For example, a function of two arguments -- an \q{integer} and a \q{string} that returns a list of \q{string}s has a type that takes the form:
\begin{lstlisting}
(integer,string) => cons of string
\end{lstlisting}

\subsubsection{Procedure Type}
\label{procedureType}
\index{procedure type}
\index{type!procedure}

A procedure is an abstraction of an action. I.e., a procedure is a function that does not return a value but is executed purely for its side effect(s). This is expressed in the form of procedure types, which take the form of a function type that returns an empty tuple:
\begin{lstlisting}[mathescape=true]
($\ntRef{Type}\sub1\sequence{,}\ntRef{Type}\subn$)=>()
\end{lstlisting}

For example, a procedure that takes \q{string} and \q{integer} arguments would have the type signature:
\begin{lstlisting}
(string,integer)=>()
\end{lstlisting}
And the type:
\begin{lstlisting}
()=>()
\end{lstlisting}
denotes the type of a procedure that takes no arguments.


\subsection{Pattern Abstraction Type}
A \ntRef{PatternAbstraction} is an abstraction of a pattern. Pattern abstractions allow patterns to be treated as first class values -- i.e., passed in as arguments to programs and bound to variables -- and they may be applied in contexts where patterns are valid.

The form of a pattern abstraction type is defined in Figure~\vref{patternAbTypeFig}.
\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{PatternType}&\arrow&\q{(}\,\ntRef{Type}\sequence{,}\ntRef{Type}\ \q{) <= }\ntRef{Type}
\end{eqnarray*}
\caption{Pattern Type}
\label{patternAbTypeFig}
\end{figure}

Pattern abstractions match a pattern, and `extract' values from that pattern; values that, in turn, may be matched against where the pattern abstraction is applied.
For example, a \ntRef{PatternAbstraction} that matches \q{string}s that are intended to denote \q{integer} literals, and extracts such an \q{integer} would have the type
\begin{lstlisting}
(integer) <= string
\end{lstlisting}

\subsection{Constructor Type}
\label{constructorType}
\index{constructor type}
\index{type!constructor}

A constructor is a special function that is introduced in an \ntRef{AlgebraicType} definition.
\begin{aside}
Constructors are special because they can be viewed simultaneously as a function and as a pattern. Hence the form of the constructor reflects that bidirectionality.
\end{aside}
The form of a constructor type is given in Figure~\vref{constructorTypeFig}.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{ConstructorType}&\arrow&\ntRef{Type}\ \q{<=>}\ \ntRef{Type}
\end{eqnarray*}
\caption{Constructor Type}
\label{constructorTypeFig}
\end{figure}
The left hand side of a constructor type should either be a \ntRef{TupleType} or an \ntRef{RecordType} -- depending on whether the denoted constructor is a labeled tuple constructor or a record constructor.
\begin{aside}
\ntRef{ConstructorType}s are most used in the context of the signatures of \emph{abstract data types}: where a type and its constructors are `exported' from a record.
\end{aside}

\subsection{Reference Type}
\label{referenceType}
\index{reference type}
\index{type!ref@\q{ref}}
A re-assignable variable is given a \q{ref}erence type.

\begin{figure}[H]
\begin{eqnarray*}
\ntDef{ReferenceType}&\arrow&\q{ref}\ \ntRef{Type}
\end{eqnarray*}
\caption{Reference Type}
\label{referenceTypeFig}
\end{figure}

Reference types allow the programmer to distinguish re-assignable variables from other values; in particular they allow one to distinguish between binding to the \emph{value} of a re-assignable variable or to its \emph{name}.

\begin{aside}
The latter is not as common, but is important to support abstractions involving re-assignable variables.
\end{aside}

\subsection{Type Variables}
\label{typeVariable}
\index{type!variable}

A type variable is a variable which may be bound to a type. Depending on whether the scope of a type variable is explicitly determined or implicitly determined, type variables may be written as regular identifiers or as identifiers prefixed by a \q{\pcent{}} or \q{\pcent{}\pcent{}} mark.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{TypeVariable}&\arrow&\q{\pcent{}}\,\ntRef{Identifier}\\
&\choice&\ntRef{Identifier}
\end{eqnarray*}
\caption{Type Variables}
\label{typeVariableFig}
\end{figure}

\subsubsection{Type Variable Kind}
Type variables are associated with a \ntRef{Kind} -- which constrains the kinds (sic) of types that the type variables may be bound to. For example, a \ntRef{Kind} of \q{type} implies that the type variable may be bound to any valid type -- but may not be bound to a \ntRef{TypeConstructor}.

A type variable introduced using the \q{\pcent{}} notation has an implicit \ntRef{Kind} of \q{type}.

\begin{aside}
The different kinds of type variable may not be mixed: it is not permissible to bind a type variable to a \ntRef{TypeConstructor}, and vice versa.

For example, given:
\begin{lstlisting}
type cons of t is nil or cons(t, cons of t);
\end{lstlisting}
A type variable \q{\pcent{}s} may be bound to a type expression such as \q{cons of string}.
\end{aside}

\subsubsection{Scope of Type Variables}
\label{typeVarScope}
\index{type!variable!scope}

All type variables have a scope which generally follows the scoping rules for normal variables.

There are two particular cases that are important: type variables introduced via \ntRef{TypeDefinition}s and those introduced via explicitly quantified type expressions.

A variable introduced in the head of an \ntRef{AlgebraicType} definition, or in the head of a \ntRef{Contract} definition are in scope throughout the definition or contract respectively.

\subsection{Universal Types}
\label{universalType}
\index{types!universally quantified}
\index{universally quantified type}
\index{for all@\q{for all}}
A universal type denotes a type that is valid for all substitutions of a type variable.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{UniversalType}&\arrow&\q{for all}\ \ntRef{TypeVariable}\sequence{,}\ntRef{TypeVariable}\ \q{such that}\ \ntRef{Type}
\end{eqnarray*}
\caption{Universal Type Expression}
\label{universalTypeFig}
\end{figure}
In most situations, it is not necessary to explicitly annotate a type as universal. For example, universal types are automatically inferred for function definitions when they are determined to be parameterized.

One case where explicit universal quantification is necessary is when a function or other program element requires a function argument which is itself parameterized,\footnote{This can happen if function-valued argument to a function is going to be used in different situations within the function then that argument needs to explicitly marked as universal.} then the argument type must be explicitly marked as universal -- the type system cannot infer such usages. 

For example, the  \q{dblFilter} function in Program~\vref{dblFilter} applies a \q{map} function in two different situations -- one for each element of each pair in the input list.
\begin{program}
\begin{lstlisting}
dblFilter has type for all u,v such that 
     (for all t such that (t)=>t, cons of ((u,v)))=>cons of ((u,v))
fun dblFilter(M,cons of []) is cons of []
 |  dblFilter(M,cons of [(A,B),..L]) is
      cons of [(M(A),M(B)),..dblFilter(M,L)]
\end{lstlisting}
\caption{A \q{double} filter}\label{dblFilter}
\end{program}
Without the explicit type annotation for \q{M}, type inference will infer that the type of \q{A} is the same as the type of \q{B} because \q{M} is applied to both.

It is important to note that any actual function argument supplied to \q{dblFilter} will itself have to be generic -- i.e., its type will also be universally quantified.

\begin{aside}
It not not necessary to use the \q{\pcent{}} prefix for type variables that are explicitly bound by a quantifier.
\end{aside}


\subsection{Existential Types}
\label{existentialType}
\index{types!existentially quantified}
\index{existentially quantified type}
\index{exists\q{exists}}
An existential type denotes an \emph{abstract} type.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{ExistentialType}&\arrow&\q{exists}\ \ntRef{TypeVariable}\sequence{,}\ntRef{TypeVariable}\ \q{such that}\ \ntRef{Type}
\end{eqnarray*}
\caption{Existential Type Expression}
\label{existentialTypeFig}
\end{figure}

An existentially quantified type denotes a type within which there is an \emph{abstract type}: i.e., the type exists but the expression is not explicit about which type. 

Existential types are most often used in the type signatures of abstract data types. For example, the term in the statement:
\begin{lstlisting}
def R is {
  type integer counts as el;
  fun op(X,Y) is X+Y
}
\end{lstlisting}
has type:
\begin{lstlisting}
exists el such that { el has kind type; op has type (el,el)=>el }
\end{lstlisting}

\begin{aside}
Note that the fact that within the record the type \q{el} is identified as \q{integer} does not escape the record itself. Externally, the existence of the type is known but not what it is.

It is permissible to refer to the type within the record by a dot reference.
\end{aside}

\begin{aside}
Existentially quantified types are generally not inferred for variables: i.e., if a variable has an existential type then that must be explicitly annotated.

Existential types are inferred, however, for \ntRef{Record}s that contain a \ntRef{TypeDefinition} statement.
\end{aside}

\subsubsection{Encapsulated Types}
\label{encapsulatedType}
\index{encapsulated type}
\index{type!encapsulated in record}
\index{existential type}
\index{heterogenous types}
An \ntRef{EncapsulatedType} is a reference to a type that is embedded within a record.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{EncapsulatedType}&\arrow&\ntRef{Identifier}\sequence{\q{.}}\ntRef{Identifier}
\end{eqnarray*}
\caption{Encapsulated Type}
\label{encapsulatedTypeFig}
\end{figure}

As noted in Section~\vref{existentialType}, record literals may have types embedded within them. Such a record type is existentially quantified.

It is possible to access the type embedded within such a record -- albeit with some restrictions:
\begin{itemize}
\item The form of an \ntRef{EncapsulatedType} reference is limited to terms of the form:
\begin{lstlisting}
R.t
\end{lstlisting}
where \q{R} is a \ntRef{Variable} whose type interface contains the type \q{t}.

More generally, an \ntRef{EncapsulatedType} reference may involve a sequence of field names where each intermediate field name refers to a sub-record:
\begin{lstlisting}
R.f1.f2.t
\end{lstlisting}
\item The `value' of an encapsulated type is strictly opaque: it is assumed to be different to all other types. Which means that effectively \emph{only} the other fields of the record variable \q{R} contain functions and values that can be used in conjunction.
\end{itemize}

For example, consider the \q{group} type defined in Program~\vref{groupExample}.

\begin{program}
\begin{lstlisting}
type group is group{
  el has kind type where equality over el
  
  zero has type el
  op has type (el,el)=>el
  inv has type (el)=>el
}
\end{lstlisting}
\caption{The \q{group} Type}
\label{groupExample}
\end{program}

\begin{aside}
A \q{group} literal is analogous to a mathematical group: a set which is closed under a binary operation and whose elements have an inverse.

The contents of a \q{group} literal contain the definitions of the elements, the binary operation, the zero element and the inverse function.
\end{aside}
\begin{aside}
The qualification of the \q{el} type that it supports \q{equality} allows convenient access to equality of group elements. Without such a qualification, equality would not be possible for programs using \q{group} values.
\end{aside}

\begin{aside}
An additional requirement for a group is that its operation is associative. Such a property cannot be expressed in terms of type constraints.
\end{aside}

A \q{group} literal that implements the group for \q{integer}s is shown in Program~\vref{integerGroup}.
\begin{program}
\begin{lstlisting}
def IG is group{
  type integer counts as el
  def zero is 0
  def op is (+)
  fun inv(X) is -X
}
\end{lstlisting}
\caption{The \q{integer} \q{group} Record}
\label{integerGroup}
\end{program}
The \q{IG} value contains the elements of a group value. We can, for example, access the \q{zero} of \q{IG} using the statement:
\begin{lstlisting}
def IZ is IG.zero
\end{lstlisting}
If we wanted to explicitly declare the type of \q{IZ}, then we could use:
\begin{lstlisting}
IZ has type IG.el
\end{lstlisting}
This asserts that \q{IZ}'s type is whatever the encapsulated type within \q{IG} is.

It is possible to construct functions over \q{group}s that refer to encapsulated types. For example, the \q{invertGroup} function in Program~\vref{invertGroupProgram} constructs a new group by `inverting' the operation.

\begin{program}
\begin{lstlisting}
invertGroup has type (group)=>group
fun invertGroup(G) is group{
  type G.el counts as el
  def zero is G.zero
  fun op(X,Y) is G.op(G.inv(X),G.inv(Y))
  fun inv(X) is G.inv(X)
}
\end{lstlisting}
\caption{A \q{group} Inverting Function}
\label{invertGroupProgram}
\end{program}

\section{Type Constraints}
\label{typeConstraints}
\index{type!constraints}

A \ntRef{TypeConstraint} is a constraint on a \ntRef{Type}; usually implying a constraint on the possible binding of a \ntRef{TypeVariable}. 
\begin{aside}
Even though they primarily affect \ntRef{TypeVariable}s, \ntRef{TypeConstraint}s are attached `on the end' of the type expression that references the constraint.
\end{aside}
Generally, a \ntRef{TypeConstraint} on a \ntRef{TypeVariable} restricts in some sense the possible bindings for that type variable. For example, a \ntRef{Contract} refers to a named collection of functions and a \ntRef{TypeVariable} constrained by a \ntRef{ContractConstraint} means that any concrete instantiation of the \ntRef{TypeVariable} must be to a \ntRef{Type} that \q{implement}s the \ntRef{Contract}.

Similarly, a \ntRef{FieldConstraint} constrains the \ntRef{TypeVariable} so that any binding must be to a \ntRef{Type} that has the named field in its definition.

For example, using \q{arithmetic} as a constraint allows us to say `the type can be anything that implements a form of arithmetic'. The type expression:
\begin{lstlisting}
%t where arithmetic over %t
\end{lstlisting}
denotes this kind of constrained type.

\begin{aside}
\begin{aside}
It is possible to view a type variable binding itself as a form of constraint: if we bind the type variable \q{\pcent{}t} to the type \q{integer} then we are constraining the type \q{\pcent{}t} to be equal to \q{integer}.
\end{aside}\end{aside}

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{TypeConstraint}&\arrow&\ntRef{ContractConstraint}\\
&\choice&\ntRef{FieldConstraint}\\
&\choice&\ntRef{InstanceConstraint}\\
&\choice&\ntRef{HasKindConstraint}\\
&\choice&\ntRef{TupleConstraint}\\
&\choice&\ntRef{TypeConstraint}\ \q{and}\ \ntRef{TypeConstraint}
\end{eqnarray*}
\caption{Type Constraints}
\label{typeConstraintFig}
\end{figure}

A type expression of the form:
\begin{lstlisting}
(%t)=>%t where comparable over %t and arithmetic over %t
\end{lstlisting}
denotes a unary function type for any type that implements both the \q{comparable} and the \q{arithmetic} contracts (see Sections~\vref{comparisonPredicates} and \vref{arithmeticContract}).

\begin{aside}
In many cases type inference will automatically result in constraints being added to type expressions. 
\end{aside}

It is possible mix different forms of \ntRef{TypeConstraint}; for example, if a \ntRef{TypeVariable} must be bound to a type that implements the \q{comparable} contract as well as having the \q{integer}-typed \q{ident} attribute, the type expression:
\begin{lstlisting}
comparable over %t and %t implements { ident has type integer }
\end{lstlisting}
captures this.

\begin{aside}
If a constrained type variable is unified with another type variable, then the constraints of the two variables are merged. It may be that such a merging of constraints is not possible; in such a case, the unification will fail.
\end{aside}

\subsection{Contract Constraints}
\label{contractContraint}
\index{type!constraints!contract}
\index{contract constraint}
A \ntRef{ContractConstraint} is a requirement on a \ntRef{Type} -- or tuple of \ntRef{Type}s -- that whatever type it is, that there must exist an \q{implementation} of the \ntRef{Contract} for the \ntRef{Type} (see Section~\vref{contracts}).

For example, the type constraint expression:
\begin{lstlisting}
comparable over %t
\end{lstlisting}
means that the type variable \q{\pcent{}t} may only unify with concrete types that implement the \q{comparable} contract.
\begin{aside}
If \q{\pcent{}t} is unified with another type variable, then the constraints on both type variables are \emph{merged}.
\end{aside}

\begin{aside}
Since only named types may implement \ntRef{Contract}s, it is also not permissible to unify the constrained variable with an structural type -- such as a function type.
\end{aside}

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{ContractConstraint}&\arrow&\ntRef{Identifier}\ \q{over}\ \ntRef{TypeArgument}\ [\,\q{determines}\ \ntRef{TypeArgument}\,]
\end{eqnarray*}
\caption{Contract Constraint}
\label{contractConstraintFig}
\end{figure}

It is possible for \ntRef{ContractConstraint}s to reference more than one type. For example, the standard \q{coercion} contract (see Program~\vref{typeCoercionContractFig}) references two types. A \q{coercion} \ntRef{ContractConstraint} will therefore look like:
\begin{lstlisting}[mathescape=true]
coercion over ($\emph{srcType}$, $\emph{dstType}$)
\end{lstlisting}
where \q{\emph{srcType}} represents the `source' type of the coercion and \q{\emph{dstType}} represents the `destination' type.

If the \q{determines} clause is used, then the \ntRef{Contract} being referenced must have a \emph{functional dependency}
\index{functional dependency}
associated with it.
\begin{aside}
Conversely, if a \ntRef{Contract} has a functional dependency, then any constraint referring to it must also have a \q{determines} clause.
\end{aside}
The \q{determines} clause identifies which type(s) are `dependent' on the type argument(s) of the \ntRef{Contract}. (See Section~\vref{ContractFunctionalDependency}).

\subsection{Field Constraints}
\label{attributeConstraint}
\index{type!field}
\index{type!constraints!field}

A \emph{FieldConstraint} is a requirement on a variable that whatever type it is, it should have particular attributes of particular types defined for it.

\begin{figure}[H]
\begin{eqnarray*}
\ntDef{FieldConstraint}&\arrow&\ntRef{Type}\ \q{implements}\ \{\ntRef{TypeAnnotation}\sequence{;}\ntRef{Annotation}\}
\end{eqnarray*}
\caption{Field Constraint}
\label{attributeConstraintFig}
\end{figure}

For example, in
\begin{lstlisting}
%r implements { alpha has type string; beta has type long }
\end{lstlisting}
if \q{\pcent{}r} is unified against a concrete type then that type's \ntRef{RecordType} interface (see Section~\vref{algebraicInterface}) must contain both of \q{alpha} and \q{beta}. In addition, the fields must be of the right types.

\begin{aside}
It is also possible to require that an \ntRef{EncapsulatedType} exists. For example, the constraint:
\begin{lstlisting}
s implements { elem has kind type }
\end{lstlisting}
requires that any actual binding for type \q{s} must include the embedded type \q{elem}.
\end{aside}

\subsection{Instance Constraint}
\label{instanceConstraint}
\index{type!constraints!instance}
An \ntRef{InstanceConstraint} is a requirement on a variable that any instantiation of the variable is an `instance of' a type -- typically that is a universally quantified type.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{InstanceConstraint}&\arrow&\ntRef{TypeVar}\ \q{instance of}\ \ntRef{Type}
\end{eqnarray*}
\caption{Instance Type Constraint}
\label{instanceConstraintFig}
\end{figure}

For example, in 
\begin{lstlisting}
%r instance of (for all t such that (t)=>t)
\end{lstlisting}
we establish a constraint on \q{\pcent{}r} that any binding of \q{\pcent{}r} must be some specialization of the function type:
\begin{lstlisting}
for all t such that (t)=>t
\end{lstlisting}
Note that this would permit, for example, \q{\pcent{}r} to be bound to the \q{integer} function type:
\begin{lstlisting}
(integer)=>integer
\end{lstlisting}
because this type is an instance of the \ntRef{UniversalType}.

\begin{aside}
\ntRef{InstanceConstraint}s typically arise from type inference itself; rather than being deliberately written by the programmer. 
\end{aside}


\subsection{Has Kind Constraint}
\label{hasKindConstraint}
\index{type!constraints!has kind}
An \ntRef{HasKindConstraint} is a requirement on a variable that any instantiation of the variable `has the right kind'.

The kind of a type refers to whether the type is a regular type or a type constructor. It also encodes the expected number of type arguments -- in the case that the variable should be bound to a type constructor.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{HasKindConstraint}&\arrow&\ntRef{TypeVar}\ \q{has kind}\ \ntRef{Kind}
\end{eqnarray*}
\caption{Has Kind Type Constraint}
\label{hasKindConstraintFig}
\end{figure}

For example, in 
\begin{lstlisting}
%c has kind type
\end{lstlisting}
we establish a constraint on \q{\pcent{}c} that any binding of \q{\pcent{}c} must be a \ntRef{Type} (in particular, it may not be bound to a type constructor.

The constraint:
\begin{lstlisting}
%d has kind type of (type,type)
\end{lstlisting}
establishes the constraint that \q{\pcent{}d} must be bound to a type constructor (\emph{not} a \ntRef{Type}) or arity two. Given this constraint, it would not be legal to bind \q{\pcent{}d} to the standard type constructor \q{cons} (say) -- because \q{cons} is a type constructor of one argument.

\subsection{Tuple Constraint}
\label{tupleConstraint}
\index{type!constraints!tuple}

A \emph{TupleConstraint} is a requirement on a variable that it is a tuple type.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{TupleConstraint}&\arrow&\ntRef{Type}\ \q{is tuple}
\end{eqnarray*}
\caption{Tuple Type Constraint}
\label{tupleConstraintFig}
\end{figure}

For example, in
\begin{lstlisting}
%r is tuple
\end{lstlisting}
if \q{\pcent{}r} is unified against a concrete type then that type must be a \ntRef{TupleType}.

\section{Type Annotations}
\label{typeAnnotation}
An \ntRef{Annotation} is a statement that declares a variable to have a certain \ntRef{Type} or a \ntRef{Type} to have a certain \ntRef{Kind}.

For example, 
\begin{lstlisting}
alpha has type for all t such that (t)=>string
\end{lstlisting}
is a \ntRef{TypeAnnotation}, whereas
\begin{lstlisting}
el has kind type
\end{lstlisting}
is a \ntRef{KindAnnotation}.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{Annotation}&\arrow&\ntRef{TypeAnnotation}\ \choice\ \ntRef{KindAnnotation}\\
\ntDef{TypeAnnotation}&\arrow&\ntRef{Identifier}\ \q{has}\ \q{type}\ \ntRef{Type}\\
\ntDef{KindAnnotation}&\arrow&\ntRef{Identifier}\ \q{has}\ \q{kind}\ \ntRef{Kind}\ [\,\q{where}\ \ntRef{TypeConstraint}\,]\\
\ntDef{Kind}&\arrow&\q{type}\\
&\choice&\q{type of type}\\
&\choice&\q{type of (type}\sequence{,}\q{type)}
\end{eqnarray*}
\caption{Type Annotations}
\label{typeAnnotationFig}
\end{figure}


\section{Type Definitions}
\label{typeDefinitions}
\index{type!definition}
A type definition is a statement that introduces a new type into the current scope. There are two forms of type definition statement: the \ntRef{TypeAlias} definition and the \ntRef{AlgebraicType} definition. In addition, the \ntRef{TypeWitness} is used to `declare' a type.
\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{TypeDefinition}&\arrow&\ntRef{TypeAlias}\ \choice\ \ntRef{AlgebraicType}\ \choice\ \ntRef{TypeWitness}
\end{eqnarray*}
\caption{Type Definition Statements}
\label{typeDefinitionFig}
\end{figure}

\subsection{Type Alias}
\label{typeAlias}
\index{type!alias} 
A type alias is a statement that introduces a new type name by mapping it to an existing type expression.
\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{TypeAlias}&\arrow&\q{type}\ \ntRef{TypeSpec}\ \q{is}\ \q{alias}\ \q{of}\ \ntRef{Type}
\end{eqnarray*}
\caption{Type Alias Definition Statement}
\label{typeAliasDefinitionFig}
\end{figure}

\begin{aside}
Type aliases may be parameterized -- in the sense that the type being defined may be parameterized and that the definiens may also be parameterized.

Note that the any type variables on the right hand side of a \ntRef{TypeAlias} statement must also have been mentioned on the left hand side.
\end{aside}

For example, the statement:
\begin{lstlisting}
type time is alias of integer
\end{lstlisting}
declares a new type that is an alias for \q{time} -- i.e., that it is actually equivalent to the \q{integer} type.
\begin{aside}
Type aliases allow the programmer to signal that a particular type is being used in a special way. In addition, during program development, type aliases are useful to provide markers for types that will be elaborated further with a regular algebraic definition.
\end{aside}
\begin{aside}
Type aliases have no run-time presence. In fact, they may be viewed as a simple form of type macro -- type expressions that match the left hand side are replaced by the type expression on the right hand side. However, type aliases have some definite constraints: a type alias may not be, directly or indirectly, recursive.
\end{aside}

\subsection{Algebraic Type Definitions}
\label{algebraicTypeDefinitions}
An algebraic type definition is a statement that introduces a new type; it also defines the possible values associated with the type.

As illustrated in Figure~\vref{algebraicDefinitionFig}, an algebraic type definition introduces the new type and defines one or more \ntRef{Constructor}s -- separated by the \q{or} keyword.

A \ntRef{Constructor} is a specification of a value of a type; i.e., constructors `paint a picture' of the shape of potential values of the type.

There are three kinds of \ntRef{Constructor}: enumerated symbols, labeled tuple constructors and labeled record constructors.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{AlgebraicType}&\arrow&\q{type}\ \ntRef{TypeSpec}\ \q{is}\,\ntRef{Constructor}\,\sequence{or}\,\ntRef{Constructor}\\
\ntDef{TypeSpec}&\arrow&\ntRef{Identifier}\ [\,\q{of}\ \ntRef{TypeArgSpec}\,]\\
\ntDef{TypeArgSpec}&\arrow&\ntRef{TypeVariable}\\
&\choice&\q{(}\,\ntRef{TypeVariable}\sequence{,}\ntRef{TypeVariable}\q{)}\\
&\choice&\ntRef{TypeArgSpec}\ \q{where}\ \ntRef{TypeConstraint}\\
\ntDef{Constructor}&\arrow&\ntRef{EnumeratedSymbol}\\
&\choice&\ntRef{LabeledTuple}\\
&\choice&\ntRef{RecordConstructor}
\end{eqnarray*}
\caption{Algebraic Type Definition Statement}
\label{algebraicDefinitionFig}
\end{figure}

\begin{aside}
Most standard built-in types have type-specific constructors. For example, lists have a list notation, \q{dictionary}s have a dictionary notation and so on. Such constructors may not be defined using the algebraic type definition notation -- for example, the constructors for the \q{integer} type are denoted by the normal decimal notation for integers.
\end{aside}

\begin{aside}
As elaborated below, each `arm' of an algebraic type definition defines a value or set of values that belong to the type. There is a slightly more formal way of expressing this: an algebraic type definition induces a set of free functions. 

\begin{aside}
\index{constructor!bijection}
Free functions are technically bijections -- they are one-to-one -- i.e., they have inverses. In programming languages, free functions are used as data structuring tools; but mathematically they are functions.
\end{aside}

For example, the type definition:
\begin{lstlisting}
type person is someone(string,integer) 
            or noone
\end{lstlisting}
induces the constructor function for \q{someone}:
\begin{lstlisting}
someone has type (string,integer) <=> person;
\end{lstlisting}
The enumerated symbol has a simpler type:
\begin{lstlisting}
noone has type person;
\end{lstlisting}
The complete set of constructor functions introduced within an algebraic type definition is complete: i.e., they define all the possible values of the type.
\end{aside}

\begin{aside}
A given label, whether it is used as an \ntRef{EnumeratedSymbol}, the label of a \ntRef{LabeledType} or a \ntRef{LabeledRecord} can be defined only once. I.e., it is not permitted to `share' constructor labels across different types.
\end{aside}

\subsubsection{Enumerated Symbol}
\label{enumSymbol}
\index{constructor!enumerated symbol}
\index{enumerated symbol}
\index{type!enumerated}
An enumerated symbol is written as an identifier. The fact that an identifier has been mentioned in a type definition is sufficient to `mark' it as a value -- and not as a variable for example.
\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{EnumeratedSymbol}&\arrow&\ntRef{Identifier}
\end{eqnarray*}
\caption{Enumerated Symbols}
\label{enumSymbolFig}
\end{figure}

The standard type \q{boolean} is defined in terms of two enumerated symbols: \q{true} and \q{false}:
\begin{lstlisting}
type boolean is true or false
\end{lstlisting}

\begin{aside}
An enumerated symbol must be unique across all types within the scope of the type definition.
\end{aside}

\paragraph{Type Safety}
An enumerated symbol occurring within a type definition has the defined type:
\begin{prooftree}
\AxiomC{$E\tinfers{}\q{type}\ T\ \q{is}\ \ldots\,\q{or}\,\emph{Ident}\ \q{or}\,\ldots$}
\UnaryInfC{\typeprd{E}{\emph{Ident}}{T}}
\end{prooftree}

\subsubsection{Labeled Tuple Constructor}
\label{conFun}
\index{constructor!positional constructor}
\index{positional constructor}
\index{type!positional constructor}
A labeled tuple expression or pattern is written in the style of a function call. The specification of the labeled tuple uses \emph{types} in argument positions to denote the type of the corresponding argument.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{LabeledTuple}&\arrow&\ntRef{Identifier}\q{(}\ntRef{Type}\sequence{,}\ntRef{Type}\,\q{)}
\end{eqnarray*}
\caption{Labeled Tuple Specifier}
\label{positionalConFig}
\end{figure}

For example, a type definition for wrapping return values with an error code could have a definition:
\begin{lstlisting}
type returnType of t is error(string) or ok(t)
\end{lstlisting}
A function returning a value of type \q{returnType} would either return \q{ok(\emph{value})} or \q{error("\emph{message}")}, where the message explained the error.

Labeled tuples are well suited to situations where the number of arguments is limited and fairly obvious.

\begin{aside}
Any type variables that are referred to within a \ntRef{LabeledTuple} constructor must either be bound by explicit quantifiers or must appear in the head of the \ntRef{AlgebraicType} definition itself.
\end{aside}

\paragraph{Type Safety}
A labeled tuple occurring within a type definition is equivalent to a constructor function definition, whose type is given by:
\begin{prooftree}
\AxiomC{$E\tinfers{}\q{type}\ T\ \q{is}\ \ldots\,\q{or}\,\emph{F}\q{(}\emph{T\sub1}\sequence{,}\emph{T\subn}\q{)}\ \q{or}\,\ldots$}
\UnaryInfC{\typeprd{E}{\emph{F}}{\q{(}\emph{T\sub1}\sequence{,}\emph{T\subn}\q{)<=>}T}}
\end{prooftree}

\subsubsection{Record Constructor}
\label{aggCon}
\index{constructor!record constructor}
\index{record constructor}
\index{type!record constructor}
Labeled records denote constructors whose elements are addressed by name rather than by argument position. A labeled record specification consists of a collection type annotations (see Figure~\vref{typeAnnotationFig}), separated by semicolons. In addition, the record specification may include \emph{default} values for some (or all) of the attributes of the record.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{RecordConstructor}&\arrow&\ntRef{Identifier}\q{\{}\,\ntRef{ElementType}\ \sequence{;}\ntRef{ElementType}\ \q{\}}\\
\ntDef{ElementType}&\arrow&\ntRef{Annotation}\\
&\choice&\ntRef{Identifier}\ \q{default}\ \q{is}\ \ntRef{Expression}\\
&\choice&\ntRef{Identifier}\ \q{default}\ \q{:=}\ \ntRef{Expression}\\
&\choice&\q{fun}\ \ntRef{Identifier}\q{(}\ntRef{Variable}\sequence{,}\ntRef{Variable}\q{)}\,\q{default}\,\q{is}\,\ntRef{Expression}
%&\choice&\q{assert}\ \ntRef{Condition}
\end{eqnarray*}
\caption{Labeled Record Constructor}
\label{aggregateConFig}
\end{figure}
If there is more than one record constructor for a type then any attributes that they have in common must have the same type associated with them. For example, the type definition for a two-three tree structure is illustrated in Program~\vref{twoThree}.
\begin{program}
\begin{lstlisting}
type twoThree of s is 
  three{ left has type twoThree of s; 
         label has type s;
         right has type twoThree of s
       }
  or two{ left has type twoThree of s; 
         right has type twoThree of s
       }
  or empty;
\end{lstlisting}
\caption{A \q{twoThree} tree type}\label{twoThree}
\end{program}
The \q{left} and \q{right} attributes in the two constructors are required to have the same type because they are shared by the two records.
\begin{aside}
Notice how the type annotations for the \q{left} and \q{right} sub-tree uses the same type identifier as in the definition itself. This marks \q{twoThree} as a \emph{recursive} type.
\end{aside}

\paragraph{Type Safety}
As with labeled tuples, a labeled record occurring in a type definition is effectively a definition of a constructor function:
\begin{prooftree}
\AxiomC{$E\tinfers{}\q{type}\ T\ \q{is}\ \ldots\,\q{or}\,\emph{F}\q{\{}A\sub1\ \q{has type}\ \emph{T\sub1}\sequence{;} A\subn\ \q{has type}\ \emph{T\subn}\q{\}}\ \q{or}\,\ldots$}
\UnaryInfC{\typeprd{E}{\emph{F}}{\q{\{}A\sub1\ \q{has type}\ \emph{T\sub1}\sequence{;} A\subn\ \q{has type}\ \emph{T\subn}\q{\}<=>}T}}
\end{prooftree}

\paragraph{Default Values}
\label{defaultValues}
\index{type!record constructor!default values}
\index{default values!record constructor}

It is permitted to associate a default value with a field of an record constructor. A default value is simply an expression for an attribute that is used should a particular record literal expression (see Section~\vref{recordLiteral}) not contain a value for that field.

For example, for convenience, we might add \q{default} annotations in the \q{twoThree} type defined above, resulting in the type definition in Program~\vref{twoThreeDef}.
\begin{program}
\begin{lstlisting}
type twoThree of s is
  three{ left has type twoThree of s;
         left default is empty;
         label has type s;
         right has type twoThree of s;
         right default is empty;
       }
  or two{ left has type twoThree of s; 
         left default is empty;
         right has type twoThree of s;
         right default is empty;
       }
  or empty;
\end{lstlisting}
\caption{A \q{twoThree} tree type with defaults}\label{twoThreeDef}
\end{program}

\begin{aside}
\index{expressions!default}
\index{variable!scope}
A default value expression for an attribute is evaluated in the scope that is valid for the type definition itself. The default value expression may reference variables that are in scope at the point of type definition. The default value expression may also reference \emph{other} fields of the record constructor -- as though they were variables -- provided that they themselves do not have \q{default}s associated with them.

For example, in this definition of \q{Person}:
\begin{lstlisting}
type Person is someone{
  name has type string;
  dob has type date;
  age has type ()=>float;
  fun age() default is now()-dob;
}
\end{lstlisting}
there is a \q{default} definition of the \q{age} field that is used if a given \q{someone} record literal does not mention a value for \q{age}. This \q{default} definition makes use of the \q{dob} field as though it were a free variable of the \q{age} function.
\end{aside}

\subparagraph{Defaults of \q{ref} Fields}
\index{expressions!default!assignable field}
\index{ref field@\q{ref} field!default value}
To declare a \q{default} value for a \q{ref} field, the form:
\begin{lstlisting}[mathescape=true]
$\ntRef{Identifier}$ default := $\ntRef{Expression}$
\end{lstlisting}
should be used. For example, in the type:
\begin{lstlisting}
type account is account{
  balance has type ref long;
  balance default := 0L
}
\end{lstlisting}
the \q{balance} field is a \q{ref} field, and its default value is \q{0L}.

\subsubsection{Type Variables and Safe Algebraic Type Definitions}
\index{type variables in an algebraic type definition}
\index{constructor type variables}
For an \ntRef{AlgebraicType} definition to be safe requires a constraint on type variables within the definition. In particular, it is not permitted to `introduce' a type variable in any of the constructors in the definition. 

\begin{aside}
Specifically, any unbound type variables mentioned in a type definition must also occur within the \ntRef{TypeSpec}.
\end{aside}

For example, the type definition:
\begin{lstlisting}
type opaque is op(%t)
\end{lstlisting}
is not valid because the type variable \q{\pcent{}t} mentioned in the \q{op} constructor is not mentioned in the \ntRef{TypeSpec}.

\begin{aside}
The reason for this is that type safety cannot be guaranteed for such constructors. For example, consider the invalid function:
\begin{lstlisting}
fun badOp(op(23)) is false;
\end{lstlisting}
The type signature for \q{badOp} is 
\begin{lstlisting}
badOp has type (opaque)=>boolean
\end{lstlisting}
and, according to type inference rules, an expression such as:
\begin{lstlisting}
badOp(op("alpha"))
\end{lstlisting}
would be type safe. However, this expression will lead to a run-time failure when the integer 23 is compared against the string \q{"alpha"}.
\end{aside}

\begin{aside}
Note that the converse case, where a type variable is mentioned in the \ntRef{TypeSpec} is not mentioned in a constructor defined within the type definition is perfectly valid.
\end{aside}

It \emph{is} possible to have type variables mentioned in a constructor that are not defined in the \ntRef{TypeSpec}. The constraint is that such type variables must be closed by quantification.

For example, the type definition:
\begin{lstlisting}
type univ is univ(for all t such that t)
\end{lstlisting}
is a legally valid \ntRef{AlgebraicType} definition; albeit one that is quite restricted. Locally quantified types are commonly associated with function types:
\begin{lstlisting}
type uniFun is uniFun(for all t such that (t,t)=>t)
\end{lstlisting}

\subsection{Automatic Synthesis of Contract Implementations}
\index{automatically synthesizing implementations}
\index{implementing contracts@\q{implementing} contracts}

In some cases, the `regular' implementation of a contract by be predicted by examining the algebraic type definition itself. The \Sr compiler automatically generates implementations of the \q{equality} and the \q{pPrint} contracts, for example, by inspecting the type definition itself.

A programmer may extend this system of atomically implementing contracts by implementing a special macro whose name is of the form \q{implement\_\q{name}}. A type definition that is marked:
\begin{lstlisting}[mathescape=true]
type person is some{
  name has type string;
} or noOne 
  implementing $\ntRef{Identifier}$
\end{lstlisting}
will result in the macro \q{implement\_\q{name}} being invoked on the type definition. 

This is used, for example, to allow coercion between types and the standard \q{quoted} type to be synthesized, instead of being constructed manually.

\subsection{Algebraic Interface Record}
\label{algebraicInterface}
An \ntRef{AlgebraicType} definition induces an interface that is composed of all the fields in any of the \ntRef{RecordConstructor}s that are defined within the definition.

This interface -- which takes the form of a \ntRef{RecordType} -- contains a \ntRef{Annotation} for every \ntRef{Annotation} that is present in a \ntRef{RecordConstructor}.

For example, the interface for the \q{account} type above consists of:
\begin{lstlisting}
{
  balance has type ref long;
}
\end{lstlisting}

This interface is used when determining the type soundness of a \ntRef{RecordAccess} expression.
\begin{aside}
The condition noted above that two fields of the same name in two \ntRef{RecordConstructor}s of the same \ntRef{AlgebraicType} must have the same type can be formalized by declaring that the interface of an \ntRef{Algebraic} type must be well formed (which is only possible if there is only a single \ntRef{Annotation} for a given field).
\end{aside}

\subsection{Type Witness Definition}
\label{countsAs}

A \ntRef{TypeWitness} definition declares that a given type exists. It is used to assert that a given existential type exists.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{TypeWitness}&\arrow&\q{type}\ \ntRef{Type}\ \q{counts as}\ \ntRef{Identifier}
\end{eqnarray*}
\caption{Type Witness Statement}
\label{typeCountsAsFig}
\end{figure}

For example, in the expression:
\begin{lstlisting}
group{
  type integer counts as elem;
  fun inv(X) is -X;
  fun op(X,Y) is X+Y;
  def zero is 0;
}
\end{lstlisting}
the statement:
\begin{lstlisting}
type integer counts as elem
\end{lstlisting}
asserts that the type \q{integer} is a witness for the existentially quantified type \q{elem}.
\begin{aside}
\ntRef{TypeWitness} statements are inherently internal statements: the witness type itself is not exposed by the record that contains the \ntRef{TypeWitness} statement.
\end{aside}

\section{Contracts}
\label{contracts}
\index{type!contracts}
A contract is a specification of a set of functions and action procedures that form a coherent collection of functionality. Associated with a \ntRef{Contract} are one or more \ntRef{Type}s -- the contract is said to be `over' those types.

\subsection{Contract Definition}
\label{ContractDefinition}
\index{type!contracts!definition}

A contract definition is a statement that defines the functions and action procedures associated with a contract. As can be seen in Figure~\vref{ContractFig}, a contract statement associates a contract name -- together with a set of type variables -- with a set of \ntRef{TypeAnnotation}s that define the elements of the contract. Within the \ntRef{Contract} statement, a \ntRef{TypeAnnotation} may refer to the type(s) in the contract head.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{Contract}&\arrow&\q{contract}\ \ntRef{ContractSpec}\ \q{is}\\
&&\q{\{}\,\ntRef{ElementType}\sequence{;}\ntRef{ElementType}\,\q{\}}\\
\ntDef{ContractSpec}&\arrow&\ntRef{Identifier}\ \q{over}\ \ntRef{TypeArgSpec}\ [\,\q{determines}\ \ntRef{TypeArgSpec}\ ]
\end{eqnarray*}
\caption{Contract Statement}
\label{ContractFig}
\end{figure}

For example, the contract that underlies type coercion (see Section~\vref{typeCoercionExpression}) is:
\begin{lstlisting}
contract coercion over (s,t) is {
  coerce has type (s)=>t
}
\end{lstlisting}

\index{default values!contract}
A contract statement may also include \emph{defaults} for the names defined in the contract. If a given contract implementation does not give an implementation for a name that has a default associated for it, then the default is used.

\begin{aside}
Default specifications may use variables that are in scope at the point of the contract specification.\footnote{This is generally not the same scope as where a contract implementation is given.}
\end{aside}

\begin{aside}
An important usage pattern for contracts is to represent \emph{abstract types}. An abstract type is one defined by its contract rather than one defined by an explicit type definition.

For example, the \q{arithmetic} contract in Program~\vref{arithmeticContractProg} defines a set of arithmetic functions. However, it can also be interpreted as a definition of an abstract type of arithmetic values -- the values that implement the \q{arithmetic} contract.
\end{aside}

\subsubsection{Functional Dependencies}
\label{ContractFunctionalDependency}
\index{type!contracts!functional dependencies}
\index{functional dependencies in contracts}
\index{determines@\q{determines}}

For certain forms of contract, it may be that the type parameters may not all be independent of each other. For example, consider the standard \q{iterable} contract (defined in Program~\vref{iterateContractProg}) which reads:
\begin{lstlisting}
contract iterable over coll determines el is {
  iterate has type 
    for all r such that 
      (coll,(el,IterState of r)=>IterState of r,IterState of r) => 
        IterState of r;
}
\end{lstlisting}
The intention of the \q{iterable} contract is to support processing collections of elements in a sequential manner. The type parameter \q{coll} identifies the collection to be iterated over; and the type parameter \q{el} identifies the type of each element.

However, the collection's type uniquely determines the type of each element: the element type is not independent of the collection. For example, to iterate over a \q{cons of \pcent{}t}, each element will be of type \q{\pcent{}t}; and to iterate over a \q{string} each element will be a \q{integer} even though the \q{string} type does not mention \q{integer}.

\begin{aside}
Each \q{integer} represents a unicode code point in the \q{string}.
\end{aside}

Using a \q{determines} clause in a \q{contract} -- and in corresponding contract \q{implementation} statements -- allows the contract designer to signal this relationship.

\subsection{Contract Implementation}
\label{ContractImplementation}
\index{type!contracts!implementation}

A contract implementation is a specification of how a contract may be implemented for a specific type combination.

\begin{figure}[htbp]
\begin{eqnarray*}
\ntDef{Implementation}&\arrow&\q{implementation}\ \ntRef{ContractSpec}\ [\,\q{default}\,]\ \q{is}\ \ntRef{Expression}
\end{eqnarray*}
\caption{Contract Implementation Statement}
\label{ContractImplementationFig}
\end{figure}
The \ntRef{Type}s mentioned in \ntRef{ContractSpec} must be either \ntRef{TypeExpression}s or, in the case of a \q{default} implementation, \ntRef{TypeVariable}s.
\begin{aside}
In particular, it is not permitted to define an \q{implementation} of a contract for \ntRef{FunctionType}s, \ntRef{PatternType}s, nor for \ntRef{UniversalType}s or \ntRef{ExistentialType}s.
\begin{aside}
It is permissible, however, to implement \ntRef{Contract}s for \ntRef{TupleType}s and \ntRef{RecordType}s.
\end{aside}
\end{aside}

The body of a contract \q{implementation} must be an expression that gives a definition for each of the elements of the \q{contract} specification.

\begin{aside}
A \q{contract} implementation may either take the form of a regular \ntRef{AnonymousRecord} or an anonymous \ntRef{ThetaRecord}.
\end{aside}

Usually, the implementation of a \q{contract} is fairly straightforward. Program~\vref{consSize}, for example, gives the implementation of the standard \q{sizeable} contract for the \q{cons} type.

\begin{program}
\begin{lstlisting}
implementation sizeable over cons of \pcent{}e is {
  fun size(nil) is 0
   |  size(cons(_,T)) is size(T)+1
  fun isEmpty(nil) is true
   |  isEmpty(_) default is false
}
\end{lstlisting}
\caption{Implementation of \q{sizeable} for \q{cons} values\label{consSize}}
\end{program}

\subsubsection{Implementing Contracts with Functional Dependencies}
\label{implContractFunctionalDependency}
\index{type!contracts!functional dependencies}

Implementing a contract which has a functional dependency is exactly analogous to implementing a regular contract. The dependent type(s) must be identified in the \q{implementation} statement. For example, the initial part of the implementation of the \q{arithmetic} contract between \q{integer}s and \q{float}s is:
\begin{lstlisting}[mathescape=true]
implementation arithmetic over (integer,float) determines float is {
  fun integer(L) + float(R) is float(__integer_float(L),R)
  $\ldots$
\end{lstlisting}
Note that this implementation implies that whenever an integer value is involved with a floating point value, the result will always be floating point.

\subsubsection{Default Contract Implementation}
\label{defaultImplementation}
\index{default implementation of contracts}
\index{type!contracts!implementation!default}
\index{default@\q{default}}

A \q{default} implementation for a contract denotes an implementation to use for a contract when there is no known implementation. This can occur in two common situations: where a contract function is used that references a type that does not have an implementation for the contract, and where there is no type information.

\begin{aside}
It is strongly recommended that the \q{default} implementation is generic; i.e., that the definition of the individual functions are generic. The contract type should be denoted by a variable and all the contract functions should be generic.

For example, the implementation statement:
\begin{lstlisting}
implementation equality over %t default is {
  fun L=R is __equal(L,R)
}
\end{lstlisting}
uses a generic internal definition of \q{\_\_equal}.
\end{aside}

As noted above, a \q{default} implementation is only used in restricted circumstances:
\begin{description}
\item[No available implementation] If a contract is referenced for a type that does not implement the contract then the \q{default} implementation will be used. 

For example, given a contract:
\begin{lstlisting}
contract foo over t is {
  bar has type (t)=>boolean;
}
\end{lstlisting}
and the functional expression:
\begin{lstlisting}
bar("fred")
\end{lstlisting}
then, if \q{foo} is not implemented for \q{string}s then the \q{default} implementation will be used for this expression. Of course, if there is no \q{default} implementation then a compile error will be flagged.
\item[Variable type]
In a few circumstances a reference may be made to a contract involving no known types. For example, in the condition:
\begin{lstlisting}
def XX is nil=nil
\end{lstlisting}
there is a hidden type variable associated with the enumerated symbol \q{nil}. 
\begin{aside}
The symbol \q{nil} is from the standard definition of \q{cons}:
\begin{lstlisting}
type cons of t is nil or cons(t,cons of t)
\end{lstlisting}
\end{aside}
Since the type of \q{nil} is `under-constrained' -- i.e., the type of \q{nil} as an expression involves a type variable that is not constrained at all by the \q{nil} symbol -- even if \q{equality} is implemented for many types there is no way of knowing which implementation to use in this situation. In this case, a \q{default} implementation will be used if provided.
\end{description}


\subsubsection{Recursive Contract Implementations}

More complex contract implementations may require the use of auxiliary function definitions; and hence may involve the use of \q{let} or \q{using} expressions.

For example, Program~\vref{consCompare} implements the \q{comparable} contract for \q{cons} values.
\begin{program}
\begin{lstlisting}
implementation comparable over cons of t where
      comparable over t and equality over t
  is{
    fun X < Y is consLess(X,Y)
    fun X =< Y is consLessEq(X,Y)
    fun X > Y is consLess(Y,X)
    fun X >= Y is consLessEq(Y,X)
  } using {
    consLess has type for all t such that
      (cons of t,cons of t)=>boolean
    fun consLess([],[_ ,.. _]) is true
     |  consLess([X,..L1],[X,..L2]) is consLess(L1,L2)
     |  consLess([X,.._], [Y,.._]) where X<Y is true
     |  consLess(_,_) default is false
    
    consLessEq has type for all t such that
      (cons of t,cons of t)=>boolean
    fun consLessEq([],_) is true
     |  consLessEq([X,..L1],[Y,..L2]) where X=<Y is
          consLessEq(L1,L2)
     |  consLessEq(_,_) default is false
  }
\end{lstlisting}
\caption{Implementation of \q{comparable} for \q{cons} values\label{consCompare}}
\end{program}


\begin{aside}
The implementation of \q{comparable} for \q{cons} types is based on a requirement that the individual elements of lists must also be compared. Hence the clause
\begin{lstlisting}
cons of t where comparable over t and equality over t
\end{lstlisting}
in the head of the \q{contract} \q{implementation} statement in Program~\vref{consCompare}. The primary job of the definition of \q{<} within Program~\vref{consCompare} is to show how \q{cons} values may be compared. Our definition of inequality for \q{cons} values assumes that:
\begin{enumerate}[a.]
\item empty lists are less than any non-empty list;
\item one non-empty list is less than another if the first element is less than the first element of the second; and finally
\item if the first elements of the two lists are identical then we consider the tails of each list.
\end{enumerate}
\begin{aside}
The curious reader may wonder why we introduce a new name \q{consLessEq} in order to define \q{=<} (and, by extension \q{consLess} for \q{<} etc.). The reason for this has to do with limitations on type inference in the context of recursive programs: within the equations that define a function, any \emph{use} of the function symbol must represent a recursive use. For example, in the equation:
\begin{lstlisting}
fun consLessEq([X,..L1],[Y,..L2]) where X=<Y is
      consLessEq(L1,L2);
\end{lstlisting}
the occurrence of \q{consLessEq} in the right hand side of the equation represents a recursive call to the function (\q{consLessEq}) being defined.

However, if we tried to define \q{=<} without the use of the auxiliary name we would get two occurrences of \q{=<} which really represent different functions:
\begin{lstlisting}
fun cons of [X,..L1] =< cons of [Y,..L2] where X=<Y is L1 =< L2
\end{lstlisting}
However, the two occurrences of \q{=<} refer to \emph{different} kinds of use: one is as a `normal' overloaded occurrence of \q{=<} and once as a recursive call to the function being defined.

Normally, outside of the definition of the function, it is permitted to allow a given function to be used in different uses -- always assuming that the types are consistent. However, within the definition of a function, all occurrences of the function symbol must refer to the same function.

In the case of the \q{=<} equation above, the type inference system would not be able to distinguish a recursive call from a call to a different overloaded function of the same name; and would assume that both uses of \q{=<} are intended to be part of the definition. This, in turn, would result in a type error being generated.

In summary, when defining an overloaded function like \q{=<}, we have to introduce an auxiliary function to `carry' the recursion.
\end{aside}
\end{aside}

In defining the implementation of a contract, each of the variables that are part of the contract must either be defined or have a default definition within the \q{contract} specification itself.

\subsection{Resolving Overloaded Definitions}
\label{overloading}
\index{type!contracts!resolving}
\index{overloading}
\index{resolving overloaded definitions}

When a program refers to a contract-defined function -- i.e., a variable that is declared within a \q{contract} -- then that reference must be \emph{resolved} to an actual program before the program can be said to be executable.

For example, consider the expression:
\begin{lstlisting}
A+3
\end{lstlisting}
The \q{(+)} function is part of the \q{arithmetic} contract (see Section~\vref{arithmeticContract}) which means that we need to resolve the call to \q{(+)} to an actual implemented function.

The type signature for \q{(+)} is:
\begin{lstlisting}
for all t such that (t,t)=>t where arithmetic over t
\end{lstlisting}
where the constraint
\begin{lstlisting}
arithmetic over t
\end{lstlisting}
is satisfied for any \q{t} for which there is an \q{implementation} of \q{arithmetic}. 

In this case we know, because \q{3} is an \q{integer} that the type of \q{A} must also be \q{integer} -- as is the type of the whole expression. So, the actual constraint after taking type inference into account is:
\begin{lstlisting}
arithmetic over integer
\end{lstlisting}
which \emph{is} satisfied because there is a standard implementation of \q{arithmetic} for \q{integer}.

Implementations can be viewed as functions whose value is a record of all the elements of the defined contract. For example, the implementation function of \q{arithmetic} over \q{integer} has a definition that is similar to:
\begin{lstlisting}[mathescape=true]
fun arithmetic#integer() is arithmetic{
    fun X+Y is _integer_plus(X,Y);
    $\ldots$
  }
\end{lstlisting}

Resolving the expression \q{A+3} is achieved by replacing the abstract function \q{(+)} with an actual function:
\begin{lstlisting}
arithmetic#integer().+(A,3)
\end{lstlisting}

In some cases, there is not sufficient information about the types of variables to fully resolve the appropriate definition to use. In this case, it must be true that the type(s) involved must be variable and that they `surface' to a point where the type variable(s) are generalized.

Consider the function:
\begin{lstlisting}
fun addSq(X,Y) is X+Y*Y
\end{lstlisting}

The type of \q{X} and \q{Y} are not completely known, and are denoted by the same type variable (\q{t}) say; \q{t} is, however, a constrained type that is bound by the scope of the \q{addSq} function itself. In fact, the type signature of \q{addSq} reflects this:
\begin{lstlisting}
for all t such that (t,t)=>t where arithmetic over t
\end{lstlisting}
The \q{arithmetic} contract requirement has surfaced to the same level where the type variable \q{t} is bound.

In general, where an overloaded name is used, there are two permitted possibilities: the type constraints implied by the overloaded name are subsumed by an explicit type equality or the type variable is bound in some \ntRef{ThetaEnvironment}.

\begin{aside}
The third possibility: where the constrained type is a type variable but is not bound by a \ntRef{ThetaEnvironment} is an error -- an unresolved overloaded identifier error.
\end{aside}

There is not enough information here to `fix' an actual implementation to use within the definition of \q{addSq}; and so we resolve by rewriting the \q{addSq} function to take an additional argument -- the \q{arithmetic} dictionary represented by the variable \q{D}:
\begin{lstlisting}
fun addSq#(D) is let{
  fun addSq'(X,Y) is D.+(X,D.*(Y,Y));
} in addSq'
\end{lstlisting}
In addition (sic), we will have to also resolve all \emph{calls} to \q{addSq} as well. A call to \q{addSq} such as:
\begin{lstlisting}
addSq(A,3)
\end{lstlisting}
will be rewritten to:
\begin{lstlisting}
addSq#(arithmetic#integer())(A,3)
\end{lstlisting}
because we know from the presence of the literal integer that \q{addSq} is being used with \q{integer} arguments.

Resolving for contract implementations `pushes out' from expressions such as \q{A+3} outward until all references to contracts have been resolved by explicit implementations.
\begin{aside}
It is an error for the top-level of a program to contain unresolved references to contracts.
\end{aside}

The formal rules for satisfying (and hence resolving) contract constraints are shown in Section~\vref{overloading}.


\subsection{Standard Contracts}
\label{standardContracts}
\index{type!contracts!standard}
\index{standard!contracts}

The language defines a few contracts as standard. These cover, for example, the concepts of \q{equality}, \q{comparable}, and \q{sizeable} entities and the \q{arithmetic} operations. These contracts are integral to the semantics of the language.

\begin{longtable}[hbtp]{|lll|}
\caption{Standard Contracts}\label{standardContractTable}\\ 
\hline
Contract&Description&\\
\hline
\endhead
\hline
\multicolumn{3}{r}{{\emph{\small Continued on next page}}}
\endfoot
\hline
\endlastfoot
\tt equality over \pcent{}t&Definition of equality&See page~\pageref{equalityPredicates}\\
\tt comparable over \pcent{}t&Definition of comparability&See page~\pageref{comparisonPredicates}\\
\tt arithmetic over \pcent{}t&Basic arithmetic&See page~\pageref{arithmeticContract}\\
\tt math over \pcent{}t&Misc math functions&See page~\pageref{mathContract}\\
\tt trig over \pcent{}t&Trigonometry functions&See page~\pageref{trigContract}\\
\tt bitstring over \pcent{}t&Bitwise functions&See page~\pageref{bitString}\\
\tt sizeable over \pcent{}t&Definition of \q{size} and \q{empty}&See page~\pageref{sizeableContract}\\
\tt sequence over \pcent{}t&Sequences of values&See page~\pageref{sequenceContract}\\
\tt indexable over \pcent{}t&Random access&See page~\pageref{indexableContract}\\
\tt iterable over \pcent{}t&Iteration over collections&See page~\pageref{iterableContract}\\
\tt coercion over (\pcent{}s,\pcent{}t)&Coerce between types&See page~\pageref{typeCoercionContract}\\
\tt speech over \pcent{}a&Actor speech actions&See page~\pageref{speechContract}\\
\tt pPrint over \pcent{}t&Pretty Print Display&See page~\pageref{pPrintContract}\\
\tt computation over \pcent{}\pcent{}c&Computation Expressions&See page~\pageref{computationContractProg}\\
\tt execution over \pcent{}\pcent{}c&Computation Expressions&See page~\pageref{executionContractProg}\\
\end{longtable}

\section{Type System}
\label{typeSystem}
\index{type!system}

The type system consists of a language of type expressions and a set of rules for showing consistency between types and programs. 

The foundation of these rules are the rules that relate one type to another; and the primary relationship involved here is subsumption.

In addition there are rules for determining when various constraints are satisfied and there are rules that relate specific expressions to types.

\subsection{Type Subsumption}
\label{typeSubsumption}

The type system is based on the concept of type \emph{subsumption}. One type subsumes another if either it is already equivalent under some substitution or it is `more general' than the other.
\begin{aside}
The intuition is that if a function expects a certain kind of argument then either a value of exactly that type or one that is more general may be supplied.
\end{aside}

We express this formally in terms of a subsumption relation \subsume:
\[
T\sub1\subsume{}T\sub2
\]
is read as
\begin{quote}
$T\sub1$ subsumes, or is more general than, $T\sub2$.
\end{quote}
In general, type checking takes place in a certain context. For subsumption, this context defines available implementations of contracts as well as recording the types of variables. Furthermore, subsumption is likely to lead to the instantiation of type variables. Hence, in general, the predicate that we establish takes the form:
\[\entail{E,\theta\sub{in}}{T\sub1\subsume{}T\sub2}\leadsto\theta\sub{out}\]
where \ensuremath{\theta} 
takes the form \ensuremath{\{x\sub1/t\sub1\sequence{,}x\subn/t\subn}\} 
and defines a substitution of types t\subi{} for type variables x\subi{} where a given variable occurs at most once in the left hand side of a $x\subi/t\subi$ pair.

\begin{aside}
We do not take account of constraints at this time.
\end{aside}

\subsubsection{Subsumption of Basic Types}

\begin{itemize}
\item One \ntRef{TypeExpression} subsumes another if they have the same arity, and if their type constructors and type arguments pairwise subsume:
\begin{prooftree}
\AxiomC{\entail{E,\theta\sub0}{t\sub1\subsume u\sub1\leadsto\theta\sub1}\sequence{\ }\entail{E,\theta\sub{n-1}}{t\subn\subsume u\subn\leadsto\theta\subn}}
\AxiomC{\entail{E,\theta\subn}{C\sub1\subsume C\sub2\leadsto\theta}}
\BinaryInfC{\entail{E,\theta\sub0}{C\sub1\ \q{of}\ (t\sub1\sequence{,}t\subn)\ \subsume\ C\sub2\ \q{of}\ (u\sub1\sequence{,}u\subn)\leadsto\theta}}
\end{prooftree}
where $t\subi$ and $u\subi$ are \ntRef{Type} expressions  and $C\sub1$ and $C\sub2$ are \ntRef{TypeConstructor}s.

\item If a type variable $v$ is already in the unifier then we look it up:
\begin{prooftree}
\AxiomC{\ensuremath{v/t\sub1\in\theta\subi}}
\AxiomC{\entail{E,\theta\subi}{t\sub1\subsume{}t\sub2\leadsto\theta\sub{o}}}
\BinaryInfC{\entail{E,\theta\subi}{v\subsume{}t\sub2\leadsto\theta\sub{o}}}
\end{prooftree}

\begin{prooftree}
\AxiomC{\ensuremath{v/t\sub2\in\theta\subi}}
\AxiomC{\entail{E,\theta\subi}{t\sub1\subsume{}t\sub2\leadsto\theta\sub{o}}}
\BinaryInfC{\entail{E,\theta\subi}{t\sub1\subsume{}v\leadsto\theta\sub{o}}}
\end{prooftree}

\item A type variable $v$ may be inserted into the unifier:
\begin{prooftree}
\AxiomC{\ensuremath{v/t\notin\theta\subi}}
\AxiomC{\ensuremath{v\notin{}t\sub2}}
\BinaryInfC{\entail{E,\theta}{v\subsume{}t\sub2\leadsto\theta\cup\{v/t\sub2\}}}
\end{prooftree}
where the condition \ensuremath{v\notin{}t} means that $v$ does not occur free in type $t$.
\begin{prooftree}
\AxiomC{\ensuremath{v/t\notin\theta\subi}}
\AxiomC{\ensuremath{v\notin{}t\sub1}}
\BinaryInfC{\entail{E,\theta}{t\sub1\subsume{}v\leadsto\theta\cup\{v/t\sub1\}}}
\end{prooftree}

\end{itemize}

\subsubsection{Subsumption of Tuples and Records}
\begin{itemize}

\item One \ntRef{TupleType} subsumes another if they are of the same length and each of their successive elements pairwise subsume.
\begin{prooftree}
\AxiomC{\entail{E,\theta\sub0}{t\sub1\subsume u\sub1\leadsto\theta\sub1}\sequence{\quad}\entail{E,\theta\sub{n-1}}{t\subn\subsume u\subn\leadsto\theta\subn}}
\UnaryInfC{\entail{E,\theta\sub0}{(t\sub1\sequence{,}t\subn)\ \subsume\ (u\sub1\sequence{,}u\subn)\leadsto\theta\subn}}
\end{prooftree}
where $t\subi$ and $u\subi$ are types.


\item One \ntRef{RecordType} subsumes another if every element of the first pairwise subsumes a corresponding element of the second. For the purposes of this exposition we assume that neither type contains any encapsulated types: this case is dealt with below under existential quantification.


\begin{prooftree}
\AxiomC{\entail{E,\theta\sub0}{t\sub0\subsume u\sub1\leadsto\theta\sub1}\sequence{\quad}\entail{E,\theta\sub{n-1}}{t\subn\subsume{} u\subn\leadsto\theta\subn}}
\UnaryInfC{\entail{E,\theta\sub0}{\q{\{}f\sub1=t\sub1\sequence{;}f\subn=t\subn\q{\}}\ \subsume\ \q{\{}f\sub1=u\sub1\sequence{;}f\subn=u\subn\q{;..\}}\leadsto\theta\subn}}
\end{prooftree}
where the $f\subi$ are distinct labels of fields and the trailing \q{;..} is intended to signify that there may be additional elements that are not considered.

\end{itemize}

\subsubsection{Subsumption of Function Types}

The rules for subsumption for function types introduces the concept of \emph{contravariance}.

\begin{itemize}

\item A function type $F\sub1$ subsumes $F\sub2$ if the result types subsume and the argument types contra-subsume:

\begin{prooftree}
\AxiomC{\entail{E,\theta\subi}{r\sub1\subsume{}r\sub2\leadsto\theta\sub0}}
\AxiomC{\entail{E,\theta\sub0}{a\sub2\subsume{}a\sub1\leadsto\theta\sub{o}}}
\BinaryInfC{\entail{E,\theta\subi}{a\sub1\q{=>}r\sub1\subsume{}a\sub2\q{=>}r\sub2\leadsto\theta\sub{o}}}
\end{prooftree}

The subsumption relation is inverted for the argument types of the two function types. This reflects the intuition that for one function type to subsume another its result type must subsume the latter but the argument type of the latter should subsume (be more general than) the former.
\begin{aside}
Without contravariance it becomes difficult and awkward to combine functions together. 
\end{aside}

\item The subsumption relation for pattern types is similar to that for function types:
\begin{prooftree}
\AxiomC{\entail{E,\theta\subi}{r\sub1\subsume{}r\sub2\leadsto\theta\sub0}}
\AxiomC{\entail{E,\theta\sub0}{a\sub2\subsume{}a\sub1\leadsto\theta\sub{o}}}
\BinaryInfC{\entail{E,\theta\subi}{r\sub1\q{<=}a\sub1\subsume{}r\sub2\q{<=}a\sub2\leadsto\theta\sub{o}}}
\end{prooftree}

\item Subsumption for constructor types requires equivalence rather than subsumption. This is because a constructor may be used both as a pattern and as a function. We use the \equivt{} to denote this. We do not need to introduce a completely new definition for \equivt{}, instead we can define it in terms of \subsume:

\begin{prooftree}
\AxiomC{\entail{E,\theta\subi}{t\sub1\subsume{}t\sub2\leadsto\theta\sub0}}
\AxiomC{\entail{E,\theta\sub0}{t\sub2\subsume{}t\sub1\leadsto\theta\sub{o}}}
\BinaryInfC{\entail{E,\theta\subi}{t\sub1\equivt{}t\sub2\leadsto\theta\sub{o}}}
\end{prooftree}

Given this definition of \equivt{}, we can define subsumption for constructor types:
\begin{prooftree}
\AxiomC{\entail{E,\theta\subi}{r\sub1\equivt{}r\sub2\leadsto\theta\sub0}}
\AxiomC{\entail{E,\theta\sub0}{a\sub2\equivt{}a\sub1\leadsto\theta\sub{o}}}
\BinaryInfC{\entail{E,\theta\subi}{r\sub1\q{<=>}a\sub1\subsume{}r\sub2\q{<=>}a\sub2\leadsto\theta\sub{o}}}
\end{prooftree}

Clearly, this definition is symmetric wrt the two constructor types, and we can also establish:
\begin{prooftree}
\AxiomC{\entail{E,\theta\subi}{r\sub1\equivt{}r\sub2\leadsto\theta\sub0}}
\AxiomC{\entail{E,\theta\sub0}{a\sub2\equivt{}a\sub1\leadsto\theta\sub{o}}}
\BinaryInfC{\entail{E,\theta\subi}{r\sub2\q{<=>}a\sub2\subsume{}r\sub1\q{<=>}a\sub1\leadsto\theta\sub{o}}}
\end{prooftree}

\end{itemize}

\subsubsection{Subsumption of Quantified Types}
Subsumption of quantified types must take into account the implied semantics of the quantifiers: a \ntRef{UniversalType} is less general than its bound type and so on.

For simplicity of presentation we assume that all quantified types have been alpha-renamed so that no two quantified terms have the same bound variable.

\begin{itemize}
\item Any type subsumes its universally quantified variant if its subsumes a `refreshed' variant of the latter:

\begin{prooftree}
\AxiomC{\entail{E,\theta\subi}{t\sub1\subsume{}t'\sub2\leadsto\theta\sub{o}}}
\AxiomC{\ensuremath{t'\sub2=t\sub2[x/x']}}
\BinaryInfC{\entail{E,\theta\subi}{t\sub1\subsume\q{for all x such that }t\sub2\leadsto\theta\sub{o}}}
\end{prooftree}
where $x'$ is a variable not occurring elsewhere and $t[x/u]$ refers to the result of replacing occurrences of $x$ in $t$ with $u$.


\item A universally quantified type subsumes a type if the bound type of the former subsumes the latter without binding the bound variable.

\begin{prooftree}
\AxiomC{\entail{E,\theta\subi}{t\sub1\subsume{}t\sub2\leadsto\theta\sub{o}}}
\AxiomC{\ensuremath{x/t\notin\theta\sub{o}}}
\BinaryInfC{\entail{E,\theta\subi}{\q{for all x such that }t\sub1\subsume{}t\sub2\leadsto\theta\sub{o}}}
\end{prooftree}

\item An existentially quantified type subsumes a type if a `refreshed' variant of the 
former subsumes the latter:

\begin{prooftree}
\AxiomC{\entail{E,\theta\subi}{t'\sub1\subsume{}t\sub2\leadsto\theta\sub{o}}}
\AxiomC{\ensuremath{t'\sub1=t\sub1[x/x']}}
\BinaryInfC{\entail{E,\theta\subi}{\q{exists x such that }t\sub1\subsume{}t\sub2\leadsto\theta\sub{o}}}
\end{prooftree}

\item A type subsumes its existentially quantified variant if 
the former subsumes the bound type of the latter without affecting the bound variable.

\begin{prooftree}
\AxiomC{\entail{E,\theta\subi}{t\sub1\subsume{}t\sub2\leadsto\theta\sub{o}}}
\AxiomC{\ensuremath{x/t\notin\theta\sub{o}}}
\BinaryInfC{\entail{E,\theta\subi}{t\sub1\subsume{}\q{exists x such that }t\sub2\leadsto\theta\sub{o}}}
\end{prooftree}

\end{itemize}


%\subsection{Satisfying Constraints}
%
%\subsubsection{Satisfying Contract Constraints}
%\label{satisfyingContracts}
%\index{contract constraint!satisfiability}
%\index{satisfiability!contract constraint}
%\index{resolving contract constraints}
%
%A \ntRef{ContractConstraint} of the form:
%\begin{lstlisting}[mathescape=true]
%\emph{Contract} over (\emph{Type\sub1}\sequence{,}\emph{Type\subn}) \ldots
%\end{lstlisting}
%or
%\begin{alltt}
%\emph{Contract} over (\emph{Type\sub1}\sequence{,}\emph{Type\subn}) determines (\emph{Type\sub{n+1}}\sequence{,}\emph{Type\sub{n+m}}) \ldots
%\end{alltt}
%\index{determines@\q{determines}}
%is satisfiable if all of \emph{Type\sub1} through \emph{Type\subn} are \ntRef{TypeExpression}s and there is an \q{implementation} for the types denoted. I.e., the constraint is satisfiable if there is a statement of the form:
%\begin{alltt}
%implementation \emph{Contract} over (\emph{T\sub1}\sequence{,}\emph{T\subn}) \ldots
%\end{alltt}
%or
%\begin{alltt}
%implementation \emph{Contract} over (\emph{T\sub1}\sequence{,}\emph{T\subn}) determines (\emph{T\sub{n+1}}\sequence{,}\emph{T\sub{n+m}}) \ldots
%\end{alltt}
%respectively; where \emph{Type\subi} unifies with \emph{T\subi} for each $i$.
%
%\begin{aside}
%The determined types (\emph{T\sub{n+1}}\sequence{,}\emph{T\sub{n+m}}) take part in the satisfiability of a contract; but they do not determine the applicability of a contract implementation. I.e. only the types mentioned before the \q{determines} clause actually affect the selection of the implementation.
%
%The intuition is that there is a dependency between the determined types and the main types: they are not independent.
%\end{aside}
%
%A \q{default} implementation of the form:
%\begin{alltt}
%implementation \emph{Contract} over (\emph{V\sub1}\sequence{,}\emph{V\subn}) default is \ldots
%\end{alltt}
%or, for contracts with functional dependencies, if it takes the form:
%\begin{alltt}
%implementation \emph{Contract} over (\emph{V\sub1}\sequence{,}\emph{V\subn})
%         determines (\emph{V\sub{n+1}}\sequence{,}\emph{V\sub{n+m}}) default is \ldots
%\end{alltt}
%where all of \q{\emph{V\subi}} are \ntRef{TypeVariable}s satisfies the \ntRef{ContractConstraint} for \q{\emph{Contract}} if \emph{Type\subi} unify with \emph{V\subi}.
%
%\begin{aside}
%A \ntRef{ContractConstraint} that has a \q{determines} clause can only be satisfied by an \q{implementation} that also has a matching \q{determines} clause. Conversely, a \ntRef{ContractConstraint} that does not have a \q{determines} clause can only be satisfied by implementations that also do not have a \q{determines} clause.
%\end{aside}
%
%\begin{aside}
%This unification may induce other constraints, including constraints that require resolution of contracts.
%\end{aside}
%
%It is an error if there are more than one non-\q{default} candidates for satisfying a contract constraint. It is also an error if there are no candidates to satisfy the constraint.
%
%\begin{aside}
%One of the less obvious requirements in satisfying contract constraints is that the contract constraint must already be partially determined. In particular, the 'top-level' of the types in the constraint must be known -- unless the \q{default} implementation is used.
%\end{aside}
%
%\subsubsection{Consistency of Contract Constraints}
%A \ntRef{TypeVariable} may not be constrained by inconsistent type constraints.
%
%Two \ntRef{ContractConstraint}s are consistent if either they are about different contracts, or if they are about the same contract the corresponding contract types are unifiable. In the latter case, the determined types (if present) must also unify.
%
%\subsubsection{Satisfying Attribute Constraints}
%An \ntRef{FieldConstraint} takes the form:
%\begin{alltt}
%\ntRef{Type} implements \{ \ntRef{Identifier}\sub1 has type \ntRef{Type}\sub1\sequence{;}\ntRef{Identifier}\subn has type \ntRef{Type}\subn \}
%\end{alltt}
%An \ntRef{FieldConstraint} is satisfiable if the left-hand \ntRef{Type} is an \ntRef{AlgebraicType} whose definition is such that for each \ntRef{Identifier}\subi{} has a \ntRef{LabeledRecord} that includes a \ntRef{TypeAnnotation} for the \ntRef{Identifier} and whose corresponding type also unifies with \ntRef{Type}\subi.
%
%\subsubsection{Consistency of Attribute Constraints}
%Two \ntRef{FieldConstraint}s are consistent if either they are about different fields, or if they are about the same fields then corresponding field types must be unifiable.
%
%A \ntRef{TypeVariable} can be constrained by any number of \ntRef{FieldConstraint}s -- provided that they are consistent with each other. Similarly, a \ntRef{TypeVariable} can be constrained by combinations of \ntRef{ContractConstraint}s and \ntRef{FieldConstraint}s.

%\subsection{Type Inference}
%\label{typeConstraints}
%\index{type!constraints}
%A type inference constraint is a predicate relating elements of the program and any type expressions; the general form of which is:
%\begin{prooftree}
%\AxiomC{\mbox{\emph{Condition}}}
%\UnaryInfC{\typeprd{E}{X}{T}}
%\end{prooftree}
%This should be read as
%\begin{quote}
%If \emph{Condition} is satisfied, then we can infer from the context \emph{E} that \emph{X} has type \emph{T}
%\end{quote}
%where the symbol \tinfers{} can be read as `type implication'. In general, the type of an expression depends on the context that it is found. The context of a type expression can be defined as a set of \emph{bindings} of names to values. Mostly these values are types -- the types of the names involved. But the environment also contains type definitions -- where the binding is from a name to a type.
%
%For example, the rule that determines if a function application is type-safe, and what resulting type of the expression is, is:
%\begin{prooftree}
%\AxiomC{\typeprd{E}{F}{\q{(}t\sub1,\ldots,t\subn\q{)}\q{=>}}\emph{R}}
%\AxiomC{\typeprd{E}{\q{(}a\sub1,\ldots,a\subn\q{)}}{\q{(}t\sub1,\ldots,t\subn\q{)}}}
%\BinaryInfC{\typeprd{E}{F\q{(}a\sub1,\ldots,a\subn\q{)}}{R}}
%\end{prooftree}
%This type rule implicitly calls for the unification of the type associated with the function and the types associated with the arguments to the function.
%
%The type rule for a variable bears some explanation:
%\begin{prooftree}
%\AxiomC{$X:T\in{}E$}
%\UnaryInfC{\typeprd{E}{X}{\rm{refresh}(T)}}
%\end{prooftree}
%This can be read as
%\begin{quote}
%if the variable \emph{X} has type \emph{T} in the environment \emph{E}, then the type of an \emph{occurrence} of the variable is refresh(T).
%\end{quote}
%\index{refreshing type variables}
%\index{type!variable!refreshing}
%\index{renaming type variables}
%\index{variable!type of}
%refresh(T) is the result of rewriting a universally quantified types with a new type with new type variables. For example, the type
%\begin{alltt}
%cons of \pcent{}t
%\end{alltt}
%is better understood as being
%\begin{alltt}
%for all \pcent{}t such that cons of \pcent{}t\footnote{See Section \vref{universalType}.}
%\end{alltt}
%and refreshing this type means stripping the quantifier and replacing all occurrences of \q{\pcent{}t} with a new variable:
%\begin{alltt}
%\emph{refresh}(for all \pcent{}t such that cons of \pcent{}t) = cons of \pcent{}t2341
%\end{alltt}
%where \q{\pcent{}t2341} is a `new' type variable that does not occur anywhere else.
%\begin{aside}
%This procedure of refreshing a universally quantified type is equivalent to the logical operation of \emph{variable renaming}. In this process, type variables are replaced with new type variables that do not occur elsewhere. In addition, the universal quantifiers within a logical formula are moved to the outermost left-hand side of the formula.
%\end{aside}

%\subsection{Type Generalization}
%\label{typeGeneralization}
%\index{type!generalization}
%\index{generalized types}
%The complement of refreshing types is type \emph{generalization}. Like refreshing, generalizing a type involves moving type quantifiers; in this case, quantifiers are moved inward rather than outward.
%
%\index{theta environment}
%In a \ntRef{ThetaEnvironment}, definitions of programs -- functions, procedures and patterns -- involve a combination of inferring types based on the forms of the expressions and patterns and type generalization.
%
%For example, the rules of type inference will give a function expression such as:
%\begin{alltt}
%(function(X) is X)
%\end{alltt}
%a type assignment of:
%\begin{alltt}
%(\pcent{}t)=>\pcent{}t
%\end{alltt}
%
%However, if a variable (\q{f}) within a \ntRef{ThetaEnvironment} is bound to such a value then the variable is given the type:
%\begin{alltt}
%for all \pcent{}t such that (\pcent{}t)=>\pcent{}t
%\end{alltt}
%\begin{aside}
%This assumes that the type variable \q{\pcent{}t} is not referenced by any expression in the containing scope.
%
%It also assumes that the variable is not a re-assignable variable -- which in any case has a non-program type: a \q{ref} function type rather than a function type.
%\end{aside}
%This is justified by the possibility of safely re-using the \q{f} function. For example, suppose that the \ntRef{ThetaEnvironment} also contains other definitions that reference \q{f}:
%\begin{alltt}
%foo(X) is f(X)+1;
%\ldots
%bar(A) is f(A)++"a"
%\end{alltt}
%The function \q{f} is used twice, but with different types for its argument; in one case \q{f} is used with an \q{integer} argument, in the other it is used with a \q{string} argument. It is safe to do so because the defining equation for \q{f} does not rely on the actual type of its argument. 
%
%The formal description of this involves several steps:
%\begin{enumerate}
%\item A program definition -- such as a function definition -- of the form:
%\begin{alltt}
%f(\emph{Ptn\sub1}\sequence{,}\emph{Ptn\subn}) is \emph{Exp}
%\end{alltt}
%is equivalent to the variable definition:
%\begin{alltt}
%f is (function(\emph{Ptn\sub1}\sequence{,}\emph{Ptn\subn}) is \emph{Exp})
%\end{alltt}
%I.e., in what follows, we are only concerned with variable definitions whose type is a program type.\footnote{A function may be defined by multiple equations. This does not materially alter this analysis.}
%
%\item For such a variable definition, type safety requires that the value has a program type. For brevity we deal with the function case only, but this analysis applies to all program definitions.
%
%\item
%The defined variable is given a quantified type according to the type inference rule:
%\begin{prooftree}
%\AxiomC{\typeprd{E}{Ex}{T\sub{Ex}}}
%\AxiomC{(\,\q{f}\,,\ \q{for all \pcent{}t\subi{} such that }\emph{T\sub{Ex}}\,)$\in\ $E}
%\BinaryInfC{\typesafe{E}{\q{f is }Ex}}
%\end{prooftree}
%where \q{\pcent{}t\subi} is the subset of the type variables occurring in $T\sub{Ex}$ that do not occur otherwise in \emph{E}.
%\end{enumerate}
%
%\begin{aside}
%Logically, generalization is valid for \emph{any} type. However, the generalization rule is only applied to programmatic types -- such as function types, procedure types and pattern types.
%
%The reason is that these elements are inherently re-usable and their values do not `carry stateful information'.
%\end{aside}
%
%\begin{aside}
%Generalization of types is not applied to certain kinds of definition within a \ntRef{ThetaEnvironment}. In particular, it is not applied to re-assignable variables and it is not applied to \ntRef{MemoFunction} defined variables.
%
%In the case of \ntRef{MemoFunction}s, their execute-once semantics is not consistent with the re-usability assumption behind type generalization.
%\end{aside}