% FILE. . . . . /home/hak/ngo/doc/hak/design/types.tex
% EDIT BY . . . Hassan Ait Kaci
% ON MACHINE. . Latitude314.Ilog.Fr
% STARTED ON. . Fri May 31 09:29:52 2002

% Last modified on Mon Oct 17 10:21:14 2005 by hak

\chapter{The type language}%
\label{TypeLanguage}

\section{Overview}

We first define some basic terminology regarding the type system and
operations on types.

\subsection{Polymorphism}

Here, by ``{\em polymorphism},'' we mean ML-polymorphism (\ie,
$2${\em nd}-order universal)---with a few differences that will be
explained along the way---in other words, types presented with a grammar
such as:
\begin{bnflist}
\bnfrule{Type}{SimpleType $\;|\;$ TypeScheme}
\bnfrule{SimpleType}{BasicType   $\;|\;$ FunctionType $\;|\;$ TypeParameter }
\bnfrule{BasicType}{\INT\ $\;|\;$ \REAL\ $\;|\;$ \BOOL\ $\;|\;$ \ldots }
\bnfrule{FunctionType}{\funtype{SimpleType}{SimpleType}}
\bnfrule{TypeParameter}{\TYPE{\alpha} $\;|\;$ \TYPE{\alpha'} $\;|\;$ \ldots $\;|\;$
                        \TYPE{\beta} $\;|\;$ \TYPE{\beta'} $\;|\;$ \ldots}
\bnfrule{TypeScheme}{\TYPE{\forall} TypeParameter \TYPE{.} Type}
\end{bnflist}
that ensures that universal type quantifiers occur only at the outset of
a polymorphic type.\footnote{Or more precisely that $\forall$ never
occurs nested inside a function type arrow $\rightarrow$. This
apparently innocuous detail ensures decidability of type inference. BTW,
the $2${\em nd} order comes from the fact that the quantifier applies
to {\em type} parameters (as opposed to $1${\em st} order, if it
had applied to {\em value} parameters). The {\em universal} comes
from $\forall$, of course.}

\subsection{Multiple Type Overloading}

This is also often called {\em ad hoc} polymorphism. When enabled (the
default), this allows a same identifier to have several unrelated types.
Generally, it is restricted to names with functional types. However,
since functions are first-class citizens, this restriction makes no
sense, and therefore the default is to enable multiple type overloading
for all types.

Note that there is no established technology that prevails for
supporting {\em both} ML-polymorphic type inference and multiple type
overloading. Here (and in several other parts of this overall design) I
have had to innovate and put to use techniques from (Constraint) Logic
Programming to be able to prove the combination of types supportable by
this architecture.

\subsection{Currying}

Currying is an operation that exploits the following mathematical
isomorphism of types:\footnote{For the intrigued reader curious to know
what deep connection there might be between functional types and Indian
cooking, the answer is, {\em ``None whatsoever!''} The word was
coined after Prof.~Haskell B.~Curry's last name. Curry was one of the
two mathematicians/logicians (along with Robert Feys) who conceived
{\em Combinator Logic} and
{\em Combinator Calculus}, and made extensive use of the isomorphism
of Equation~(\ref{curry})---hence the folklore's use of the verb
{\em to curry---(currying, curryed),---} in French:
{\em curryfier---(curryfication, curryfi\'e)}, to mean transforming a
function type of several arguments into that of a function of one
argument. The homonymy is often amusingly mistaken for an exotic way of
[un]spicing functions.}
\begin{equation}\label{curry}
\FUNTYPE{T,T'}{T''} \;\simeq\; \FUNTYPE{T}{(\FUNTYPE{T'}{T''})}
\end{equation}
which can be generalized to its multiple form:
\begin{equation}\label{mcurry}
\FUNTYPE{T_1,\ldots,T_n}{T} \;\simeq\;
\FUNTYPE{T_1,\ldots,T_k}{(\funtype{T_{k+1},\ldots,T_n}{T})}
\;\;\;k=1,\ldots,n-1
\end{equation}

When function currying is enabled, this means that
type-checking/inference must build this equational theory into the type
unification rules in order to consider types equal modulo this
isomorphism.

\subsection{Standardizing}

As a result of, \eg, currying, the shape of a function type may change
in the course of a type-checking/inference process. Type comparison may
thus be tested on various structurally different, although syntactically
congruent, forms of a same type. A type must therefore assume a
canonical form in order to be compared. This is what
{\em standardizing} a type does.

Standardizing is a two-phase operation that first {\em flattens} the
domains of function types, then
{\em renames} the type parameters. 
The flattening phase simply amounts to uncurrying as much as possible by
applying Equation~(\ref{curry}) as a rewrite rule, although
{\em backwards} (\ie, from right to left) as long as it applies. The
second phase (renaming) consists in making a consistent 
copy of all types reachable from a type's root.

\subsection{Copying}

Copying a type is simply taking a duplicate twin of the graph reachable
from the type's root. Sharing of pointers coming from the fact that type
parameters co-occur are recorded in a parameter substitution table (in
our implementation, simply a \texttt{java.util.HashMap}) along the way,
and thus consistent pointer sharing can be easily made effective.

\subsection{Equality}

Testing for equality must be done modulo a parameter substitution table
(in our implementation, simply a \texttt{java.util.HashMap}) that
records pointer equalities along the way, and thus equality up to
parameter renaming can be easily made effective.

A tableless version of equality also exists for which each type
parameter is considered equal only to itself.

\subsection{Unifying}

Unifying two types is the operation of filling in missing information
(\ie, type parameters) in each with existing information from the other
by side-effecting (\ie, binding) the missing information (\ie, the type
parameters) to point to the part of the existing information from the
other type they should be equal to (\ie, their values). Note that, like
logical variables in Logic Programming, type parameters can be bound
to one another and thus must be dereferenced to their values.

\subsection{Boxing/Unboxing}

The kernel language is polymorphically typed. Therefore, a function
expression that has a polymorphic type must work for all instantiations
of this type's type parameters into either primitive unboxed types (\eg,
\INT, \REAL, \etc) or boxed types. The problem this poses is: how can we
compile a polymorphic function into code that would correctly know what
the actual runtime sorts of the function's runtime arguments and
returned value are, {\em before the function type is actually
instantiated into a (possibly monomorphic) type}?\footnote{Besides
compiling distinct copies for all possible runtime sort instantiations
(like, \eg, C++ template functions), nor recompiling each time a
specific instantiation is needed. The former is not acceptable because
its tends to inflate the code space explosively. The latter can neither
be envisaged because it goes against a few (rightfully) sacrosanct
principles like separate compilation and abstract library
interfacing---imagine having to recompile code from a library everytime
you want to use it!}  The problem was addressed by Xavier Leroy 10 years
ago~\cite{leroy-boxing} and he proposed a solution.\footnote{This
solution is the one implemented in the CAML compiler~\cite{caml}.}
Leroy's method is based on the use of type annotation that enables a
source-to-source transformation. This source transformation is the
automatic generation of {\em wrappers} and
{\em unwrappers} for boxing and unboxing expressions whenever
necessary.  After that, compiling the transformed source as usual will be
guaranteed to be correct on all types.

I adapted and improved the main idea from Leroy's solution so that:
\begin{Itemize}
\item the type annotation and rules are greatly simplified;
\item no source-to-source transformation is needed;
\item un/wrappers generation is done at code-generation time.
\end{Itemize}
This saves a great amount of space and time.

\Section{The type system}
{typesystem}

The type system consists of two complementary parts: a {\em static} and a
{\em dynamic} part.\footnote{See Appendix Section~\ref{CompleteTypes} on
Page~\pageref{CompleteTypes} for the complete class hierarchy of types in the package
\texttt{ilog.language.design.types}.} The former takes care of verifying all type
constraints that are statically decidable (\ie, before
actually running the program). The latter pertains to type constraints
that must wait until execution time to decide whether those (involving
runtime values) may be decided. This is called dynamic type-checking and
is best seen (and conceived) as an {\em incremental} extension of the
static part.

A type is either a static type, or a dynamic type.  A static type is a
type that is checked before runtime by the type-checker. A dynamic type
is a wrapper around a type that may need additional runtime information
in order to be fully verified. Its static part must be (and is!) checked
statically by the static type checker, but the compiler may complete
this by issuing runtime tests at adequate places in the code it
generates; namely, when:
\begin{Itemize}
\item binding abstraction parameters of this type in an application, or
\item assigning to local and global variable of this type, or
\item updating an array slot, a tuple component, or an object's field,
of this type.
\end{Itemize}

There are two kinds of dynamic types:
\begin{Itemize}  
  \item Extensional types---defined with explicit extensions (either
         statically provided or dynamically computed runtime values):
         \begin{Itemize}
             \item Set extension type;
             \item Int range extension type (close interval of ints);
             \item Real range extension type (close interval of reals).
         \end{Itemize}
         A special kind of set of int type is used to define enumeration
         types (from actual symbol sets) through opaque type definitions.
  \item Intensional types---defined using any runtime
         boolean condition to be checked at runtime, calls to which are
         tests generated statically; \eg non-negative numbers (\ie,
         \texttt{int+}, \texttt{float+}).
\end{Itemize}    

\section{Static types}

The static type system...

\subsection{Primitive types}

\subsubsection{Boxable types}

\begin{Itemize}
      \item  \VOID\
      \item  \INT\
      \item  \REAL\
      \item  \CHAR\
      \item  \BOOL\
\end{Itemize}

\subsubsection{Boxed types}

Built-in type constants (\eg, \STRING).

\subsection{Type constructors}

\subsubsection{Function types}
\subsubsection{Tuple types}

Position tuple types

Named tuple types

\subsubsection{Array types}

$0$-based int-indexed arrays

Int range-indexed arrays

Set-indexed arrays

Multidimensional arrays

\subsubsection{Collection types}

Set, bag, and list types

\subsubsection{Class types}

This is the type of object structures. It declares an {\em interface}
(or member type signature) for a class of objects and the members comprising
its structure. It holds information for compiling field access and update,
and enables specifying an {\em implementation} for methods manipulating
objects of this type.

A class implementation uses the information declared in its interface.
It is interpreted as follows: only non-method members---hereafter called
{\em fields}---correspond to actual slots in an object structure that is
an instance of the class and thus may be updated. On the other hand, all
members (\ie, both fields and method members) are defined as global {\em
functions} whose first argument stands for the object itself (that may
be referred to as `\KRNL{\This}').

The syntax we shall use for a class definition is of the form:
\begin{equation}
\KRNL{\Class\;\id{classname}
\;\{\;\meta{interface}\;\}\;}\meta{[}\KRNL{\;\{\;\meta{implementation}\}\;}\meta{]}
\end{equation}
The {\em interface} block specifies the type signatures of the {\em
members} ({\em fields} and {\em methods}) of the class \, and possibly
initial values for fields. The {\em implementation} block is optional
and gives the definition of (some or all of) the methods.

For example, one can declare a class to represent a simple counter as
follows: 
\begin{equation}\label{CounterClass}
\KRNL{\begin{array}{lrl}
\Class \; \id{Counter} & \{ & \id{value} : \INT = 1; \\
                &           & \Method\; \id{set} : \FUNTYPE{\INT}{\id{Counter}}; \\
                & \}          & \\
                & \{          & \id{set} (\id{value} : \INT) : \id{Counter}  =
                                       (\This.\id{value} = \id{value}); \\
                & \} & 
\end{array}}
\end{equation}
The first block specifies the interface for the class type \id{Counter}
defining two members: a field \id{value} of type \INT\ and a method
\id{set} taking an argument of type \INT\ and returning a \id{Counter}
object. It also specifies an initialization expression (\KRNL{1}) for
the \id{value} field. Specifying a field's initialization is
optional---when missing, the field will be initialized to a null value
of appropriate type: \KRNL{0} for an \INT, \KRNL{0.0} for a \REAL,
\KRNL{\false} for a \BOOL, \KRNL{'\backslash000'} for a \CHAR,
\KRNL{\texttt{""}} for a \STRING, \KRNL{\void} for
\VOID,\footnote{Strictly speaking, a field of type \VOID\ is useless
since it can only have the unique value of this type (\ie, \void). Thus,
a \void\ field should arguably be disallowed. On the other hand,
allowing it is not semantically unsound and may be tolerated for the
sake of uniformity.} and \KRNL{\NULL{T}} for any other type
\TYPE{T}. The implementation block for the \id{Counter} class defines
the body of the \id{set} method.  Note that a method's implementation
can also be given outside the class declaration as a function whose
first argument's type is the class. For example, we could have defined
the \id{set} method of the class \id{Counter} as:
\begin{equation}
\KRNL{
\Def\; \qid{Counter}{set} (\id{x} : \id{Counter}, \id{n} : \INT) : \id{Counter}
= (\id{x}.\id{value} = \id{n});
}
\end{equation}

On the other hand, although a field is also semantically a function
whose first argument's type is a class, it may {\em not} be defined
outside its class. Defining a declared field outside a class
declaration causes an error. This is because the code of a field is
always fixed and defined to return the value of an object's slot
corresponding to the field.  Note however that one may define a unary
function whose argument is a class type outside this class when it is
not a declared field for this class. It will be understood as a
{\em method} for the class (even though it takes no extra argument
and may be invoked in "dot notation" without parentheses as a field
is) and thus act as a "static field" for the class. Of course field
updates using dot notation will not be allowed on these pseudo
fields. However, they (like any global variable) may be (re)set using
a global (re)definition at the top level, or a nested global
assignment.

Note also that a field may be functional without being a method---the
essential difference being that a field is part of the structure of
every object instance of a class and thus may be updated within an
object instance, while a method is common to all instances of a class
and may not be updated within a particular instance, but only globally
for all the class' instances.

Thus, everytime a \id{Counter} object is created with \New, as in, for example:
\begin{equation}
\KRNL{\id{c} = \New\ \id{Counter};}
\end{equation}
the value \KRNL{1} will be used to initialize the slot that corresponds
to the location of the \id{value} field.  Then, field and method
invocation can be done using the familiar "dot notation"; \eg:
\begin{equation}
\KRNL{\begin{array}{l}
\id{c}.\id{set}(\id{c}.\id{value}+2);	\\
     \id{write}(\id{c}.\id{value});
\end{array}}
\end{equation}

This will set \id{c}'s \id{value} field to \KRNL{3} and print out this
value.  This code is exactly equivalent to:
\begin{equation}
\KRNL{\begin{array}{l}
     \qid{Counter}{set}(\id{c},\qid{Counter}{value}(\qid{Counter}{c})+2);	\\
     \id{write}(\qid{Counter}{value}(\qid{Counter}{c}));
\end{array}}
\end{equation}

Indeed, field and method invocation simply amounts to functional
application. This scheme offers the advantage that an object's fields
and methods may be manipulated as functions (\ie, as first-class
citizens) and no additional setup is needed for type-checking and/or
type inference when it comes to objects.

Incidentally, some or all type information may be omitted while
specifying a class's {\em implementation} (though not its
{\em interface}) as long as non-ambiguous types may be
inferred. Thus, the implementation block for class \id{Counter} in class
definition~(\ref{CounterClass}) could be written more simply as:
\begin{equation}
\KRNL{ \{ \; \id{set} (\id{n}) = (\id{value} = \id{n}); \; \} }
\end{equation}

Declaring a class type and defining its implementation causes the
following:

\begin{Itemize}
 
\item the name of the class is entered with a new type for it in the
      type table (an object comprising symbol tables, of type
      \iPACK{\lPACK{\dPACK{\tPACK{\CLASS{Tables}}}}}, where its type
      definition associates it with a \texttt{ClassType} whose class
      structure is encapsulated by an object of type
      \iPACK{\lPACK{\dPACK{\tPACK{\CLASS{ClassInfo}}}}} where code
      entries for all its members' types are recorded;

\item each field of a distinct type is assigned an offset in an
      array of slots (per sort);

\item each method and field expression is name-sanitized, type-checked,
      and sort-sanitized after closing it into an abstraction taking
      \This\ as first argument;

\item each method definition is then compiled into a global definition,
      and each field is compiled into a global function corresponding
      to accessing its value from the appropriate offset;

\item finally, each field's initialization expression is compiled and
      recorded in the \texttt{ClassType} to be used at object
      creation time. An object may be created at run-time (using the
      \New\ operator followed by a class name).
     
\end{Itemize}

\subsection{Polymorphic types}

\section{Type definitions}

Before we review dynamic types, we shall describe how one can define new
types using existing types.  Type definitions are provided both for
convenience of making programs more legible by giving ``logical'' names
(or terms) to otherwise verbose types, and that of hiding information
details of a type making it act as a new type altogether. The former
facility is that of providing
{\em aliases} to types (exactly like a preprocessor's macros get
expanded right away into their textual equivalents), while the latter
offers the convenience of defining {\em new} types in terms of
existing ones, but hiding this information. It follows from this
distinction that a type alias is {\em always} structurally equivalent
to its value (in fact an alias disappears as soon as it is read in,
being parsed away into the structure defining it). By contrast, a
defined type is
{\em never} structurally equivalent to its value nor any other
type---it is only equivalent to itself. To enable meaningful computation
with a defined type, two meta-(de/con)structors are thus provided: one
for explicitly
{\em casting} a defined type into the type that defines it, and one
explicitly seeing a type as a specified defined type (if such a defined
type does exist and with this type as definition).

The class \iPACK{\lPACK{\dPACK{\tPACK{\CLASS{Tables}}}}} contains the
symbol tables for global names and types. The name spaces of the
identifiers denoting type and non-type (global or local) names (which
are kept in the global symbol table) are disjoint---so there are no name
conflicts between types and non-type identifiers.

The \txt{typeTable} variable contains the naming table for types and
the \txt{symbolTable} variable contains the naming table for other
(non-type) global names.

This section will unfold all the type-related data-structures starting
from the class that manages symbols:
\iPACK{\lPACK{\dPACK{\tPACK{\CLASS{Tables}}}}}. The names can be those of
types and values. They are {\em global} names.\footnote{At the moment,
there is no name qualification or namespace management. When this service
is provided, it will also be through the
\iPACK{\lPACK{\dPACK{\tPACK{\CLASS{Tables}}}}} class.} The type namespace
is independent of the value namespace---\ie, the same name can denote a
value and a type.

\subsection{Type aliasing}

\subsection{Type hiding}

\section{Dynamic types}

Dynamic types are to be checked, if possible statically (at least
their static part is), at least in two particular places of an expression. Namely,
\begin{Itemize}
\item at assignment/update time; and,
\item at (function) parameter-binding time.
\end{Itemize}
This will ensure that the actual value placed in the slot expecting a
certain type does respect additionnal constraints that may only be
verified with some runtime values.  Generally, dynamic types are
so-called {\em dependent} types (such as, \eg,
\texttt{array\_of\_size}$(n)$, a ``safe'' array type depending on the
array size that may be only computed at runtime---\ie, {\em \`a la}
Java arrays.).

From this, we require that a class implementing the \texttt{DynamicType}
interface provides a method \texttt{public boolean verifyCondition()}
that is invoked systematically by code generated for dynamically typed
function parameters and for locations that are the target of updates
({\em i.e}, array slot update, object field update, tuple field
update) at compilation of abstractions and various assignment
constructs. Of this class, three subclasses derive their properties:
\begin{Itemize}
\item extensional types;
\item Boolean-assertion types;
\item non-negative number types.
\end{Itemize}

We shall consider here a few such dynamic types
(motivated esssentially by the need expressed
for \opl, and hence \ngo, types). Namely,
\begin{Itemize}
\item extensional types;
\item intensional types (\eg, non-negative numbers)
\end{Itemize}

An {\em extensional} type is a type whose elements are determined to be members of
a predetermined and fixed extension (\ie, any runtime value that denotes a
collection---such as a set, an int range, a float range, or an enumeration). Such
types pose the additional problem of being usable at compile-time to restrict the
domains of other variables. However, some of those variables' values may only fully
be determined at runtime. These particular dynamic types have therefore a simple
\texttt{verifyCondition()} method that is automatically run as soon as the
extension is known. It just verifies that the element is a {\em bona fide} member
of the extension), otherwise it relies on a more complicated scheme based on the
notion of {\em contract}. Basically, a contract-based type is an extensional type
that does not have an extension (as yet) but already carries the obligation that
some particular individual constants be part of their extensions. Those elements
consitute ``contracts'' that must be honored as soon as the type's extension becomes
known (either positively---eliminating the contract, or negatively---causing a type
error).

\subsection{Extensional types}

Set types

Int range types

Float range types

Enum types

\subsection{Intensional types}

\subsubsection{Example: non-negative numbers}

Define new (opaque) types \id{Nat} as a dynamically constrained \INT\
type...

