% FILE. . . . . /home/hak/ngo/doc/hak/design/kernel.tex
% EDIT BY . . . Hassan Ait Kaci
% ON MACHINE. . Latitude314.Ilog.Fr
% STARTED ON. . Tue May 28 18:55:18 2002

% Last modified on Mon Oct 17 09:56:31 2005 by hak

\chapter{The kernel language}%
\label{KernelLanguage}

\Section{Kernel expression}%
{Expression}

\Section{Processing a kernel expression}%
{processing}
Typically, upon being read, an \texttt{Expression} will be:
\begin{Enumerate} 

\item {\em ``name-sanitized''}---in the context of a \texttt{Sanitizer}
to discriminate between local names and global names, and establish
pointers from the local variable occurrences to the abstraction that
introduces them, and from global names to entries in the global symbol
table;

 
\item {\em type-checked}---in the context of a \texttt{TypeChecker}
to discover whether it has a type at all, or several possible ones (only
expressions that have a unique unambiguous type are further processed);

\item  {\em ``sort-sanitized''}---in the context of a
\texttt{Sanitizer} to discriminate between those local variables that
are of primitive Java types (\texttt{int} or \texttt{double}) or of
\texttt{Object} type (this is necessary because the set-up means to use
unboxed values of primitive types for efficiency reasons); this second
``sanitization'' phase is also used to compute offsets for local names
({\em i.e.}, so-called {\em de Bruijn indices}) for each type sort;

\item {\em compiled}---in the context of a \texttt{Compiler} to
generate the sequence of instructions whose execution in an appropriate
runtime environment will evaluate the expression;
 
\item {\em executed}---in the context of a \texttt{Runtime} to
execute its sequence of instructions.
\end{Enumerate} 

\SUBSECTION{Sanitizer}

A {\em sanitizer} is an object that ``cleans up''---so to speak---an
expression of its remaining ambiguities as it is being processed. There
are two kinds of ambiguities that must be ``sanitized:''
\begin{Itemize}
\item after parsing, it must be determined which identifiers are the
names of {\em local} variables \vs\ those of {\em global} variables; 
\item after type-checking, it must be determined the runtime sort of
every abstraction parameter and use this to compute the local variable
environment offsets of each local variable.\footnote{These offsets are
the so-called {\em de Bruijn} indices of $\lambda$-calculus~\cite{secd}.
Or rather, their sorted version.}
\end{Itemize}
Thus a sanitizer is a discriminator of names and sorts.\footnote{It has
occurred to this author that his choice of the word ``sanitizer'' is
perhaps a tad of a misnomer---``discriminator'' may be a better choice.
This also goes for the \iPACK{\lPACK{\dPACK{\kPACK{\CLASS{Sanitizer}}}}}
class' method names (\ie, \texttt{discriminateNames} and
 \texttt{discriminateSorts}  rather than \texttt{sanitizeNames} and
\texttt{sanitizeSorts}).}

\SUBSECTION{Typechecker}

The type checker is in fact a type inference machine that synthesizes
missing type information by type unification. It may be (and often is)
used as a type-checking automaton when types are (partially) present.

Each expression must specify its own \texttt{typeCheck(TypeChecker)}
method that encodes its formal typing rule.

\SUBSECTION{Compiler}

This is the class defining a compiler object. Such an object serves as
the common compilation context shared by an \texttt{Expression} and the
subexpressions comprising it. Each type of expression representing a
syntactic construct of the kernel language defines a
\texttt{compile(Compiler)} method that specifies the way the construct
is to be compiled in the context of a given compiler.  Such a compiler
object consists of attributes and methods for generating straightline
code which consists of the sequence of instructions corresponding to a
top-level expression and its subexpressions.

Upon completion of the compilation of a top-level expression, a
resulting code array is extracted from the sequence of instructions,
which may then be executed in the context of a \texttt{Runtime} object,
or, in the case of a \texttt{Definition}, be saved in the code array in
the \texttt{Definition}'s \texttt{codeEntry()} field---a
\texttt{DefinedEntry} object, which encapsulates its code entry point,
which in turn may then be used to access the defined symbol's code for
execution).

Each expression construct of the kernel must therefore specify a
compiling rule. Such a rule expresses how the abstract syntax construct
maps into a straightline code sequence.

\Section{Description of kernel expressions}{description}

The class \texttt{Expression} is the mother of all expressions in the
kernel language.  It specifies the prototypes of the methods that must
be implemented by all expression subclasses. The subclasses of
\texttt{Expression} are:

\begin{Itemize}
\item \texttt{Constant}:
     constant (void, boolean, integer, real number,
     object);\footnote{Section~\ref{Constant}.}
 
\item \texttt{Abstraction}:
     functional abstraction ({\em \`a la} $\lambda$-calculus);\footnote{Section~\ref{Abstraction}.}
 
\item \texttt{Application}:
     functional application;
 
\item \texttt{Local}:
     local name;
 
\item \texttt{Parameter}:
     a function's formal parameter (really a pseudo-expression
     as it is not fully processed as a real expression and is used
     as a shared type information repository for all occurrences
     in a function's body of the variable it stands for);
 
\item \texttt{Global}:
     global name;

\item \texttt{Dummy}:
     temporary place holder in lieu of a name prior to being discriminated
     into a local or global one.

\item \texttt{Definition}:
     definition of a global name with an expression defining it
     in a global store;
 
\item \texttt{IfThenElse}:
     conditional;
 
\item \texttt{AndOr}:
     non-strict boolean conjunction and disjunction;
 
\item \texttt{Sequence}:
     sequence of expressions (presumably with side-effects);
 
\item \texttt{Let}:
     lexical scoping construct;
 
\item \texttt{Loop}:
     conditional iteration construct;
 
\item \texttt{ExitWithValue}:
     non-local function exit;
 
\item \texttt{Assignment}:
     construct to set the value of a \texttt{local}
     or a \texttt{global} variable;
 
\item \texttt{NewArray}:
     construct to create a new (multidimensional) array;
 
\item \texttt{ArraySlot}:
     construct to access the element of an array;
 
\item \texttt{ArraySlotUpdate}:
     construct to update the element of an array;
 
\item \texttt{Tuple}:
     construct to create a new position-indexed tuple;
 
\item \texttt{NamedTuple}:
     construct to create a new name-indexed tuple;
 
\item \texttt{TupleProjection}:
     construct to access the component of a tuple;
 
\item \texttt{TupleUpdate}:
     construct to update the component of a tuple;
 
\item \texttt{NewObject}:
     construct to create a new object;
 
\item \texttt{DottedNotation}:
     construct to emulate the traditional object-oriented ``dot''
     dereference notation;
 
\item \texttt{FieldUpdate}:
     construct to update the value of an object's field;
 
\item \texttt{ArrayExtension}:
     construct denoting a literal array;

\item \texttt{ArrayInitializer}:
     construct denoting a syntactic convenience for specifying
     initialization of an array from an extension;

\item \texttt{Homomorphism}:
     construct denoting a monoid homomorphism;

\item \texttt{Comprehension}:
     construct denoting a monoid comprehension;

%\item \texttt{CompiledExpression}:
%     pre-compiled code encapsulated as an expression;

\end{Itemize}

In this section, we are going to give a detailed description of each
kernel construct. The description of an expression will have the
following items:
\begin{Itemize}\itemsep0pt
\item \SYNTAX
\item \SEMANTICS
\item \TYPING
\item \COMPILING
\end{Itemize}

\SYNTAX

This describes the abstract syntax form of the kernel expression.
A kernel expression will be written in \KRNL{blue}.

\SEMANTICS

This describes informally the meaning of the expression.  The notation
\DNT{e}, where \KRNL{e} is an abstract syntax expression, denotes the
(mathematical) semantic {\em denotation} of \KRNL{e}.  The notation \TDNT{T}, where
\TYPE{T} is a type, denotes the (mathematical) semantic
{\em denotation} of \TYPE{T}---namely, \TDNT{T} is the set of all
abstract denotations \DNT{e}'s such that kernel expression \KRNL{e} has
type \TYPE{T}.

\TYPING

This describes formally the logical rules for typing the kernel expression.
A type will be written in \TYPE{red}.

A {\em typing judgment} is a formula of the form
\gammajudgment{e}{T}, and is read as: ``{\em under typing
context $\Gamma$, expression \KRNL{e} has type \TYPE{T}.}''

In its simplest form, a {\em typing context} $\Gamma$ is a function
mapping the parameters of $\lambda$-abstractions to their types. In the
formal presentation of an expression's typing rule, the context keeps
the type binding under which the typing derivation has progressed up to
applying the rule in which it occurs.

The notation $\Gamma\tsubst{x}{T}$ denotes the context defined from
$\Gamma$ as follows:
\begin{equation}\label{contextextention}
\Gamma\tsubst{x}{T}(\KRNL{y}) \;\eqd\; \left\{ \begin{array}{ll}
                                \TYPE{T} & \mbox{if $\KRNL{y}=\KRNL{x}$}; \\
                                \Gamma(\KRNL{x}) & \mbox{otherwise}.
                                \end{array}\right.
\end{equation}

A {\em typing rule} is a formula of the form:
\begin{equation}
\typerule{J_1,\ldots,J_n}%
{J}
\end{equation}
where $J$ and the $J_i$'s, $i=0,\ldots,n,\; n\geq0$, are
typing judgments. This ``fraction'' notation expresses
essentially an implication: when all the formulae of the rule's
{\em premises} (the $J_i$'s in the fraction's ``numerator'') hold,
then the formula in the rule's {\em conclusion} (the fraction's
``denominator'') holds too.  When $n=0$, the rule has no premise---\ie,
the premise is tautologically {\em true} (\eg, $0=0$)---the rule is
called an {\em axiom} and is written with an empty ``numerator.''

A {\em conditional} typing rule is a typing rule of the form:
\begin{equation}\label{condrule}
\ctyperule{J_1,\ldots,J_n}%
{J}%
{c(J_1,\ldots,J_n)}
\end{equation}
where $c$ is a boolean metacondition involving the rule's judgments.

A typing rule (or axiom), whether or not in conditional form, is usually
read backwards (\ie, upwards) from the rule's {\em conclusion} (the
bottom part, or ``denominator'') to the rule's {\em premises} (the
top part, or ``numerator'').  Namely, the rule of the form:
\begin{equation}\label{typingrule}
\typerule{\judgment{\Gamma_1}{e_1}{T_1},\;\ldots,\;\judgment{\Gamma_n}{e_n}{T_n}}{\gammajudgment{e}{T}}
\end{equation}
is read thus:
\begin{quote}
{\em ``The expression \KRNL{e} has type \TYPE{T} under typing context
$\Gamma$ \meta{if} the expression \KRNL{e_1} has type \TYPE{T_1} under
typing context $\Gamma_1$, \meta{and} \ldots, the expression \KRNL{e_n}
has type \TYPE{T_n} under typing context $\Gamma_n$.''}
\end{quote}

For example,
\[
\typerule{\gammajudgment{c}{\BOOL},\;
          \gammajudgment{e_1}{T},\;\;
          \gammajudgment{e_2}{T}}%
         {\gammajudgment{\IfThenElse{c}{e_1}{e_2}}{T}}
\]

is read thus:
\begin{quote}
{\em ``The expression $\IfThenElse{c}{e_1}{e_2}$ has type \TYPE{T}
under typing context $\Gamma$ \meta{if} the expression \KRNL{c} has type \BOOL\
under typing context $\Gamma$ \meta{and} if both expressions \KRNL{e_1} and
\KRNL{e_2} have the same type \TYPE{T} under the same typing context $\Gamma$.''}
\end{quote}

With judgments spelled-out, a conditional typing rule~(\ref{condrule})
looks like:
\begin{equation}\label{ctypingrule}
\ctyperule{\judgment{\Gamma_1}{e_1}{T_1},\;\ldots,\;\judgment{\Gamma_n}{e_n}{T_n}}{\gammajudgment{e}{T}}
{c(\Gamma,\Gamma_1,\ldots,\Gamma_n,
   \KRNL{e},\KRNL{e_1},\ldots,\KRNL{e_n},
   \TYPE{T},\TYPE{T_1},\ldots,\TYPE{T_n})}
\end{equation}
where
$c(\Gamma,\Gamma_1,\ldots,\Gamma_n,
   \KRNL{e},\KRNL{e_1},\ldots,\KRNL{e_n},
   \TYPE{T},\TYPE{T_1},\ldots,\TYPE{T_n})$
is a boolean meta-condition involving the contexts, expressions, and types. Such
a rule is read thus: 
\begin{quote}
{\em ``\meta{if} the meta-condition holds, \meta{then}
the expression \KRNL{e} has type \TYPE{T} under typing context
$\Gamma$ \meta{if} the expression \KRNL{e_1} has type \TYPE{T_1} under
typing context $\Gamma_1$, \meta{and} \ldots, the expression \KRNL{e_n}
has type \TYPE{T_n} under typing context $\Gamma_n$.''}
\end{quote}

An example of a conditional rule is that of abstractions that must take
into account whether or not the abstraction is {\em exitable}---\ie, it
may be exited non-locally:\footnote{See Sections~\ref{Abstraction}
and~\ref{ExitWithValue}.}
\[
\ctyperule{\judgment{\Gamma\tsubst{x_1}{T_1}\cdots\tsubst{x_n}{T_n}}{e}{T}}
          {\gammajudgment{\Abstraction{x_1,\ldots,x_n}{e}}{\funtype{T_1,\ldots,T_n}{T}}}
          {\mbox{\Abstraction{x_1,\ldots,x_n}{e} is not exitable}}.
\]

Similarlly, a {\em typing axiom}:
\begin{equation}\label{typingaxiom}
\typeaxiom{\gammajudgment{e}{T}}
\end{equation}
is read as, {\em ``The expression \KRNL{e} has type \TYPE{T} under
typing context $\Gamma$.''} and a {\em conditional typing axiom} is a
typing axiom of the form:
\begin{equation}\label{condtypingaxiom}
\ctypeaxiom{\gammajudgment{e}{T}}{c(\Gamma,\KRNL{e},\TYPE{T})}
\end{equation}
where $c(\Gamma,\KRNL{e},\TYPE{T})$ is a boolean meta-condition on typing context $\Gamma$,
expression \KRNL{e}, and type \TYPE{T} and is read as,
{\em ``\meta{if} the meta-condition $c(\Gamma,\KRNL{e},\TYPE{T})$
holds \meta{then} the expression \KRNL{e} has type \TYPE{T}
under typing context $\Gamma$.''}
We shall see examples of typing axioms in Sections~\ref{Constant} and~\ref{Parameter}.

\COMPILING

This describes the way the expression's components are mapped into a
straightline sequence of instructions.  An instruction (or generally any
instruction sequence) will be written in \inst{magenta}. Any
meta-information annotation used in code instructions or instruction
sequences will be written in \meta{green}.

The compiling rule for expression \KRNL{e} is given as a function
\compile{\_} of the form:
\begin{equation}
\compilerule{e}
{ & \inst{instruction}\meta{$_1$} \\
  & \vdots \\
  & \inst{instruction}\meta{$_n$} \\
}
\end{equation}

\SUBSECTION{Constant}

Constants represents the built-in primitive (unconstructed) data
elements of the kernel language.

\SYNTAX


A {\em Constant} expression is an atomic literal. Objects of class
\texttt{Constant} denote literal constants: the integers (\eg,
\KRNL{-1}, \KRNL{0}, \KRNL{1}, \etc), the real numbers (\eg,
\KRNL{-1.23}, \dots, \KRNL{0.0}, \ldots, \KRNL{1.23}, \etc), the
characters (\eg, \KRNL{'a'}, \KRNL{'b'}, \KRNL{'@'}, \KRNL{'\#'}, \etc),
and the constants \KRNL{\void}, \KRNL{\true}, and \KRNL{\false}. The
constant \KRNL{\void} is of type \VOID, such that:
\[
\TDNT{\VOID} \;\eqd\; \{ \DNT{\void} \}
\]
and the constants
\KRNL{\true}  and
\KRNL{\false} of type \BOOL, such that:
\[
\TDNT{\BOOL} \;\eqd\; \{ \DNT{\false}, \DNT{\true} \}.
\]

Other built-in types are:
\[
\begin{array}{l@{\;\eqd\;}l}
\TDNT{\INT}  &  \ZZ  \;=\;  \{ \ldots, \KRNL{\dnt{-1}}, \KRNL{\dnt{0}}, \KRNL{\dnt{1}}, \ldots \}
\\ [1.8ex]
\TDNT{\REAL}  &  \RR  \;=\;  \{ \ldots, \KRNL{\dnt{-1.23}}, \ldots,
                                \KRNL{\dnt{0.0}}, \ldots, \KRNL{\dnt{1.23}}, \ldots \}
\\ [1.8ex]
\TDNT{\CHAR}  &  \mbox{set of all Unicode characters}
\\ [1.8ex]
\TDNT{\STRING}  &  \mbox{set of all finite strings of Unicode characters.}
\end{array}
\]

Thus, the \texttt{Constant} expression class is further subclassed into:
\texttt{Int},
\texttt{Real},
\texttt{Char},
\texttt{NewObject},
and \texttt{BuiltinObjectConstant},
whose instances denote, respectively:
integers,
floating-point numbers,
characters,
new objects,
and built-in object constants (\eg, strings).

\TYPING


The typing rules for each kind of constant are:

\begin{equation}\label{constantrules}
\begin{array}{rl@{\;\;\;}l}
\mbox{\small\texttt{[void]}}
&
\typeaxiom{\gammajudgment{\KRNL{\void}}{\VOID}}
\\ \\ \\
\mbox{\small\texttt{[true]}}
&
\typeaxiom{\gammajudgment{\KRNL{\true}}{\BOOL}}
\\ \\ \\
\mbox{\small\texttt{[false]}}
&
\typeaxiom{\gammajudgment{\KRNL{\false}}{\BOOL}}
\\ \\ \\
\mbox{\small\texttt{[int]}}
&
\typeaxiom{\gammajudgment{\KRNL{n}}{\INT}} & \COND{\mbox{\KRNL{n} is an integer}}
\\ \\ \\
\mbox{\small\texttt{[real]}}
&
\typeaxiom{\gammajudgment{\KRNL{n}}{\REAL}} & \COND{\mbox{\KRNL{n} is a floating-point number}}
\\ \\ \\
\mbox{\small\texttt{[char]}}
&
\typeaxiom{\gammajudgment{\KRNL{c}}{\CHAR}} & \COND{\mbox{\KRNL{c} is a character}}
\\ \\ \\
\mbox{\small\texttt{[string]}}
&
\typeaxiom{\gammajudgment{\KRNL{s}}{\STRING}} & \COND{\mbox{\KRNL{s} is a string}}
\end{array}
\end{equation}

We postpone for now the typing of object constants until we understand object types.

\SUBSECTION{Abstraction}

\SYNTAX


This is the standard $\lambda$-calculus functional abstraction, possibly
with multiple parameters. Rather than using the conventional $\lambda$
notation, we write an abstraction as:
\begin{equation}\label{abstractionsyntax}
\Abstraction{x_1,\ldots,x_n}{e}
\end{equation}
where the \KRNL{x_i}'s are 
{\em abstraction parameters}---identifiers denoting  variables
local to the expression \KRNL{e}, the abstraction's {\em body}.

\TYPING


There are two cases to consider depending on whether the abstraction is
or not {\em exitable}. An exitable abstraction is one that
corresponds to a real source language's function from which a user may
exit non-locally.\footnote{See \ExitWithValue{v} in
Section~\ref{ExitWithValue}, on Page~\pageref{ExitWithValue}.} Other
(non-exitable) abstractions are those that are implicitly generated by
syntactic desugaring of surface syntax---\eg, see Sections~\ref{Let}
and~\ref{Comprehension}. It is the responsibility of the parser to
identify the two kinds of abstractions and mark as exitable all and only
those abstractions that should be.

\begin{equation}\label{abstractionrule}
\ctyperule{\judgment{\Gamma\tsubst{x_1}{T_1}\cdots\tsubst{x_n}{T_n}}{e}{T}}
          {\gammajudgment{\Abstraction{x_1,\ldots,x_n}{e}}{\funtype{T_1,\ldots,T_n}{T}}}
          {\mbox{\Abstraction{x_1,\ldots,x_n}{e} is not exitable}}
\end{equation}

If the abstraction is exitable however, we must record it in the typing
context. Namely,let $\KRNL{a} = \Abstraction{x_1,\ldots,x_n}{e}$; then,
\begin{equation}\label{exitableabstractionrule}
\ctyperule{\judgment{\Gamma\exitable{a}\tsubst{x_1}{T_1}\cdots\tsubst{x_n}{T_n}}{e}{T}}
          {\gammajudgment{a}{\funtype{T_1,\ldots,T_n}{T}}}
          {\mbox{\KRNL{a} is exitable}}
\end{equation}
where $\Gamma\exitable{a}$ is the same context as $\Gamma$ except that
$\KRNL{\aleph_{\Gamma\exitable{a}}} \;\eqd\; \KRNL{a}$.

\SUBSECTION{Application}

\SYNTAX

\begin{equation}\label{applicationsyntax}
\Application{f}{e_1,\ldots,e_n}
\end{equation}

\TYPING

\begin{equation}\label{applicationrule}
\typerule{\gammajudgment{e_1}{T_1},\;\cdots,\;
          \gammajudgment{e_n}{T_n},\;\;\;
          \gammajudgment{f}{\funtype{T_1,\ldots,T_n}{T}}}
         {\gammajudgment{\Application{f}{e_1,\ldots,e_n}}{{T}}}
\end{equation}

\SUBSECTION{Local}

\SUBSECTION{Parameter}

\SUBSECTION{Global}

\SUBSECTION{Dummy}

\SUBSECTION{Definition}

\SUBSECTION{IfThenElse}

\SYNTAX

\[\IfThenElse{c}{e_1}{e_2}\]

\SEMANTICS

\TYPING

\begin{equation}\label{iterule}
\typerule{\gammajudgment{c}{\BOOL},\;
          \gammajudgment{e_1}{T},\;\;
          \gammajudgment{e_2}{T}}%
         {\gammajudgment{\IfThenElse{c}{e_1}{e_2}}{T}}
\end{equation}

\COMPILING

\begin{equation}\label{itecompile}
\compilerule{\IfThenElse{c}{e_1}{e_2}}
{  & \compile{c} \\
   & \JumpOnFalse\ \LAB{jof} \\
   & \compile{e_1} \\
   & \Jump\ \LAB{jmp} \\
\LAB{jof}: & \compile{e_2} \\
\LAB{jmp}: & \ldots}
\end{equation}

\SUBSECTION{AndOr}

\SYNTAX

\[
\AndOr{e_1}{e_2}
\]

\TYPING

\begin{equation}\label{andorrule}
\typerule{\gammajudgment{e_1}{\BOOL},\;\;
          \gammajudgment{e_2}{\BOOL}}%
         {\gammajudgment{\AndOr{e_1}{e_2}}{\BOOL}}
\end{equation}

\SUBSUBSECTION{And}

\COMPILING

\begin{equation}\label{andcompile}
\compilerule{\AND{e_1}{e_2}}
{  & \compile{e_1} \\
   & \JumpOnFalse\ \LAB{jof} \\
   & \compile{e_2} \\
   & \JumpOnTrue\ \LAB{jot} \\
\LAB{jof}: & \PushFalse \\
   & \Jump\ \LAB{jmp} \\
\LAB{jot}: & \PushTrue \\
\LAB{jmp}: & \ldots}
\end{equation}

\SUBSUBSECTION{Or}

\COMPILING

\begin{equation}\label{orcompile}
\compilerule{\OR{e_1}{e_2}}
{  & \compile{e_1} \\
   & \JumpOnTrue\ \LAB{jot} \\
   & \compile{e_2} \\
   & \JumpOnFalse\ \LAB{jof} \\
\LAB{jot}: & \PushTrue \\
   & \Jump\ \LAB{jmp} \\
\LAB{jof}: & \PushFalse \\
\LAB{jmp}: & \ldots}
\end{equation}

\SUBSECTION{Sequence}

\SYNTAX

\[
\Sequence{e_1}{e_n}
\]

\TYPING

\begin{equation}\label{sequencerule}
\typerule{\gammajudgment{e_1}{\TYPE{T_1}},\;\;
          \ldots,\;\;
          \gammajudgment{e_n}{\TYPE{T_n}}}
         {\gammajudgment{\Sequence{e_1}{e_n}}{\TYPE{T_n}}}
\end{equation}

\COMPILING

\begin{equation}\label{sequencecompile}
\compilerule{\Sequence{e_1}{e_n}}
{  & \compile{e_1} \\
   & \Pop{e_1} \\
   & \vdots \\
   & \compile{e_n}
}
\end{equation}

\SUBSECTION{Let}

\SUBSECTION{Loop}

\SYNTAX

\begin{equation}\label{loopsyntax}
\Loop{c}{e}
\end{equation}
where \KRNL{c} and \KRNL{e} are expressions.

\SEMANTICS


\TYPING

\begin{equation}\label{looprule}
\typerule{\gammajudgment{c}{\BOOL},\;\;
          \gammajudgment{e}{T}}%
         {\gammajudgment{\Loop{c}{e}}{\VOID}}
\end{equation}

\COMPILING

\begin{equation}\label{loopcompile}
\compilerule{\Loop{c}{e}}
{\LAB{loop}: & \compile{c} \\
             & \JumpOnFalse\ \LAB{jof} \\
             & \compile{e} \\
             & \Jump\ \LAB{loop} \\
\LAB{jof}:   & \PushVoid}
\end{equation}

\SUBSECTION{ExitWithValue}

\SYNTAX

\begin{equation}\label{exitwithvaluesyntax}
\ExitWithValue{v}
\end{equation}
where \KRNL{v} is an expression.

\SEMANTICS

Normally, exiting from an abstraction is done simply by ``falling off''
(one of) the tip(s) of the expression tree of the abstraction's
body. This operation is captured by the simple operational semantics of
each of the three \inst{Return} instructions. Namely, when executing a
\inst{Return} instruction, the runtime performs the following three-step
procedure:
\begin{Enumerate}
\item
it pops the result from its result stack;\footnote{Where {\em stack}
here means ``stack of {\em appropriate} runtime sort;'' approppriate,
that is, as per the instruction's sort---\viz, \inst{int}, \inst{real},
or runtime \inst{object}.}
\item
it restores the latest saved runtime state (popped off the saved-state
stack);
\item
it pushes the result popped in Step~1 onto the restored state's own
result stack.
\end{Enumerate}

However, it is also often desirable, under certain circumstances, that
computation {\em not} be let to proceed further at its current level of
nesting of \text{exitable} abstractions. Then, computation may be
allowed to return right away from this current nesting (\ie, as if
having fallen off this level of exitable abstraction) when the
conditions for this to happen are met. Exiting an abstraction thus must
also return a specific value that may be a function of the context.
This is what the kernel construction \ExitWithValue{v} expresses. This
kernel construction is provided in order to specify that the current
local computation should terminate without further ado, and exit with
the value denoted by the specified expression.

\TYPING

Now, there are several notions in the above paragraphs that need some
clarification. For example, what an {\em ``exitable''} abstraction
is, and why worry about a dedicated construct in the kernel language for
such a notion if it does nothing more than what is done by a
\inst{Return} instruction.

First of all, from its very name $\ExitWithValue{v}$ assumes that
computation has {\em entered} that from which it must
{\em exit}. This is an {\em exitable} abstraction; that is, the
latest $\lambda$-abstraction having the property of being
{\em exitable}. Not all abstractions are exitable. For example, any
abstraction that is generated as part of the target of some other kernel
expression's syntacting sugar (\eg, $\Let{x_1=e_1;\ldots;x_n=e_n;}{e}$
or $\Comprehension{\oplus}{e}{\IN{x_1}{e_1},\ldots,\IN{x_n}{e_n}}$, and
more generally any construct that hide implicit abstractions within),
will {\em not} be deemed exitable.

Secondly, exiting with a value $\KRNL{v}$ means that the type $\TYPE{T}$
of $\KRNL{v}$ must be congruent with what the return type of the
abstraction being exited is. In other words:
\begin{equation}\label{ewvrule}
\typerule{\gammajudgment{\aleph_\Gamma}{\funtype{T'}{T}},\;\;
          \gammajudgment{v}{T}}%
         {\gammajudgment{\ExitWithValue{v}}{T}}
\end{equation}
where \KRNL{\aleph_\Gamma} denotes the latest {\em exitable}
abstraction in the context $\Gamma$.

The above scheme indicates the following necessities:
\begin{Enumerate}
\item The typing rules for an abstraction deemed exitable must record in
its typing context $\Gamma$ the latest exitable abstraction, if any such
exists; (if none does, a static semantics error is triggered to indicate
that it is impossible to exit from anywhere before first entering
somewhere).\footnote{See Typing Rule~\ref{exitableabstractionrule} on
Page~\pageref{exitableabstractionrule}.}
\item Congruently, the \Apply\ instruction of an exitable closure must
take care of chaining this exitable closure before it pushes a new state
for it in the saved state stack of the runtime system with the last
saved exitable closure, and mark the saved state as being exitable;
(dually, this exitable state stack must also be popped upon ``falling
off''---\ie, normally exiting---an exitable closure. That is, whenever
an exitable state is restored).
\item New \inst{NL\_Return} instructions (for each runtime
sort) must be defined like their corresponding \inst{Return} instructions
except that the runtime state to restore is the one popped out of the
exitable state stack.
\end{Enumerate}

\COMPILING

\begin{equation}\label{ewvcompile}
\compilerule{\ExitWithValue{v}}
{  & \compile{v} \\
   & \NonlocalReturn{v}
}
\end{equation}

\SUBSECTION{Assignment}

\SUBSECTION{NewArray}

\SUBSECTION{ArraySlot}

\SUBSECTION{ArraySlotUpdate}

\SUBSECTION{ArrayExtension}

\SUBSECTION{ArrayInitializer}

\SUBSECTION{Tuple}

\SUBSECTION{NamedTuple}

\SUBSECTION{TupleProjection}

\SUBSECTION{TupleUpdate}

\SUBSECTION{NewObject}

\SUBSECTION{DottedNotation}

This class represents a syntactic construct that is often used,
albeit with different, though related, interpretations. A dotted
notation is an expression (most often an application, but it could be
any composition---of {\em what/with what} to be determined
according to partial type analysis).

Thus, this class can be used to represent a particular kind of
functional applications {\em \`a la} object-oriented
programming; or (equivalently), arrow composition in Category
Theory. More precisely, it represents the application (resp.,
composition) of an \texttt{Expression} to (resp., with) another
\texttt{Expression}, those \texttt{Expression}s being determined
according to the type of the expression on the {\em left} of the
"dot".

Thus, a dotted notation is interpreted as follows.

A \texttt{DottedNotation} object is a wrapper of an expression---most
often, of an application, but more generally, of any composition. It is
a binary expression of the form \KRNL{e_1.e_2}, where \KRNL{e_1} and
\KRNL{e_2} are expressions. This is interpreted depending on the type of
\KRNL{e_1} as follows:

\begin{Itemize}
\item if \KRNL{e_1}'s type is a class {\em \texttt{C}},
then this is interpreted as:
\[
\KRNL{\Mangle{e_1}\Args{e_1}}
\]
where \Mangle(o:C,e) is some "mangling" of the name of the member of the
object expression \META{o} of class type \META{$C$} being so-referred,
and \Args{e} is either the empty string or the args of the member
expression \META{$e$}.

For example, consider:
\begin{verbatim}
counter.set(1);
\end{verbatim}
when \texttt{counter : Counter} is an object of class \texttt{Counter},
with method (say) \texttt{Counter\_set : (Counter, int) -> int}. Then,
for example, a default "mangling" \Mangle{C,member} may simply
concatenate the names of the class and the member separated with an
underscore character ('\texttt{\_}'), followed by '\texttt{(}', the
object, and '\texttt{)}'; in other words:
\Mangle{counter:Counter,set(1)} = "\texttt{Counter\_set(counter)}" and
\Args{\mathtt{set(1)} = "\mathtt{(1)}"}. Therefore,
\begin{verbatim}
counter.set(1) ====> Counter_set(counter)(1);
\end{verbatim}
that is:
\begin{verbatim}
counter.set(1) ====> Counter_set(counter,1);
\end{verbatim}

\item if \KRNL{e_1}'s type is a tuple type \TYPE{\Tuple{T_1,\ldots,T_n}}
or \TYPE{\Tuple{l_1:T_1,\ldots,l_n:T_n}}, then this is interpreted as:

\[
\Project{e_2}(e_1)
\]

where $\Project{e}$ is a tuple {\em projection} of type
\TYPE{\Tuple{T_1,\ldots,T_n} \map T_k} and $\mathtt{e} = \mathtt{k},
k=1,\ldots,n$, or of type
\TYPE{\Tuple{l_1:T_1,\ldots,l_n:T_n} \map T_k} and $\mathtt{e} = \mathtt{l_k},
k=1,\ldots,n$.  This is interpreted as:

\[
TupleProjection(e_1,e_2) : T_k.
\]

For example:
\[
\mathtt{\Tuple{name:="a",number:=1}.name \leadsto
\TupleProjection{\Tuple{name:="a",number:=1}}{name}}
\]
In other words,
\[
\mathtt{\g{proj}_name : \Tuple{name:string,number:int} \map string
(\Tuple{name:="a",number:=1\rangle}) : string}
\]

\item  Otherwise, the default is simply to interpret this as the application:
\[
\mathtt{member\_name(e_2)(e_1)(\Args{e_2})}
\]
This default behavior can be overridden and customized through the methods:
\texttt{setNoDefault()} and
\texttt{setDefault(Expression)}.
\end{Itemize}



\SUBSECTION{FieldUpdate}

\SUBSECTION{Homomorphism}

By {\em homomorphism} me mean specifically {\em monoid} homomorphism.
For our purposes, a monoid is a set of data values or structures (\ie, a
data type) endowed with an associative binary operation and an identity
element. Examples are:
\begin{quote}
\begin{tabular}{lll}
\textbf{Type}  & \textbf{Operation}  & \textbf{Identity}
\\ \hline
\INT           & \KRNL{+_\INT}       & \KRNL{0}
\\[1.2ex]
\INT           & \KRNL{*_\INT}       & \KRNL{1}
\\[1.2ex]
\INT           & \KRNL{\MaxOp_\INT}    & \KRNL{-\infty_\INT}
\\[1.2ex]
\INT           & \KRNL{\MinOp_\INT}    & \KRNL{+\infty_\INT}
\\[1.2ex]
\REAL          & \KRNL{+_\REAL}      & \KRNL{0.0}
\\[1.2ex]
\REAL          &  \KRNL{*_\REAL}     & \KRNL{1.0}
\\[1.2ex]
\REAL          & \KRNL{\MaxOp_\REAL}   & \KRNL{-\infty_\REAL}
\\[1.2ex]
\REAL          & \KRNL{\MinOp_\REAL}   & \KRNL{+\infty_\REAL}
\\[1.2ex]
\BOOL          & \KRNL{\OrOp_\BOOL}  & \KRNL{\false}
\\[1.2ex]
\BOOL          & \KRNL{\AndOp_\BOOL} & \KRNL{\true}
\\[1.2ex]
{\em set} data structures
                  & set union             & the empty set \KRNL{\{\}}
\\[1.2ex]
{\em list} data structures
                  & list concatenation    & the empty list \KRNL{[]}
\\[1.2ex]
\multicolumn{3}{l}{\ldots}
\\[1.2ex]\hline
\end{tabular}
\medskip
\end{quote}

Monoid homomorphisms are quite useful for expressing a certain kind of
iteration declaratively. 

\SYNTAX

This is the class of objects denoting (monoid) homomorphisms. Such an
expression means to iterate through a collection, applying a function to
each element, accumulating the results along the way with an operation, and
returning the end result. More precisely, it is the built-in version of the
general computation scheme whose instance is the following {\em ``hom''}
functional, which may be formulated recursively, for the case of a list
collection, as:

\begin{equation}\label{homrec}
\begin{array}{l@{\;=\;}l}
\textbf{hom}_\oplus^{\ID(\oplus)}(f) [] & \ID(\oplus) \\[1.2ex]
\textbf{hom}_\oplus^{\ID(\oplus)}(f) [H|T] & f(H)
                                             \oplus
                                             \textbf{hom}_\oplus^{\ID(\oplus)}(f) T
\end{array}
\end{equation}

Clearly, this scheme extends a function {\em f} to a homomorphism of monoids,
from the monoid of lists to the monoid defined by \Mon{\oplus}{\ID(\oplus)}.

Thus, an object of this class denotes the result of applying such a homomorphic
extension of a function ({\em f}) to an element of collection monoid
({\em i.e.}, a data structure such as a set, a list, or a bag), the image
monoid being implicitly defined by the binary operation ($\oplus$)---also
called the {\em accumulation} operation. It is made to work iteratively.


For technical reasons, we need to treat specially so-called {\em collection}
homomorphisms; {\em i.e.}, those whose accumulation operation constructs a
collection, such as a set. Although a collection homomorphism can conceptualy be
expressed with the general scheme, the function applied to an element of the
collection will return a collection ({\em i.e.}, a {\em free} monoid) element,
and the result of the homomorphism is then the result of tallying the partial
collections coming from applying the function to each element into a final
``concatenation.'' 

Other (non-collection) homomorphisms are called {\em primitive} homomorphisms.
For those, the function applied to all elements of the collection will return a
{\em computed} element that may be directly composed with the other results.
Thus, the difference between the two kinds of (collection or primitive)
homomorphisms will appear in the typing and the code generated (collection
homomorphism requiring an extra loop for tallying partial results into the final
collection). It is easy to make the distinction between the two kinds of
homomorphisms thanks to the type of the accumulation operation (see below).

Therefore, a {\em collection homomorphism} expression constructing a collection
of type \TYPE{coll(T)} consists of:
\begin{Itemize}
\item  the collection iterated over---of type  \TYPE{coll'(T')};
\item  the iterated function applied to each element---of type
       \FUNTYPE{T'}{coll(T)}; and,
\item  the operation ``adding'' an element to a collection---of
       type \FUNTYPE{T,coll(T)}{coll(T)}.
\end{Itemize}

T'  {\em primitive homomorphism} computing a value of type \TYPE{T} consists of:
\begin{Itemize}
\item  the collection iterated over---of type \TYPE{coll'(T')};
\item  the iterated function applied to each element---of type \FUNTYPE{T'}{T}; and,
\item  the monoid operation---of type \FUNTYPE{T,T}{T}.
\end{Itemize}

Even though the scheme of computation for homomorphisms described above
is correct, it is not often used, especially when the function already
encapsulates the accumulation operation, as is always the case when the
homomorphism comes from the desugaring of a {\em comprehension}---see
below). Then, such a homomorphism will directly side-effect the
collection structure specified as the identity element with a function
of the form \Abstraction{x}{x \oplus \ID(\oplus)} (\ie, adding element
\KRNL{x} to the collection) and dispense altogether with the need to
accumulate intermediate results. We shall call those homomorphisms
{\em in-place} homomorphisms. To distinguish them and enable the
suprression of intermediate computations, a flag indicating that the
homomorphism is to be computed in-place is provided.  Both primitive and
collection homomorphisms can be specified to be in-place. If nothing
regarding in-place computation is specified for a homomorphism, the
default behavior will depend on whether the homomorphism is collection
(default is in-place), or primitive (default is {\em not}
in-place). Methods to override the defaults are provided.


For an in-place homomorphism, the iterated function encapsulates the operation,
which affects the identity element, which thus accumulates intermediate results
and no further composition using the operation is needed.  This is especially
handy for collections that are often represented, for (space and time)
efficiency reasons, by iteratable bulk structures constructed by allocating an
empty structure that is filled in-place with elements using a built-in
{\em ``add''} method guaranteeing that the resulting data structure
is canonical---{\em i.e.}, that it abides by the algebraic properties
of its type of collection ({\em e.g.}, adding an element to a set
will not create duplicates,
{\em etc.}).


Although monoid homomorphisms are defined as expressions in the kernel, they are
not meant to be represented directly in a surface syntax (although they could,
but would lead to rather cumbersome and not very legible expressions). Rather,
they are meant to be used for expressing higher-level expressions known as
{\em monoid comprehensions}, which offer the advantage of the familar (set)
comprehension notation used in mathematics, and can be translated into monoid
homomorphisms to be type-checked and evaluated.

A monoid comprehension is an expression of the form:
\begin{equation}\label{comprehensionsyntax}
\KRNL{\Monoid{\oplus} \COMP{e}{q_1, \ldots, q_n}} 
\end{equation}
where \KRNL{\Monoid{\oplus}} define a monoid, \KRNL{e} is an expression, and the
\KRNL{q\_i}'s are {\em qualifiers}. A qualifier is either an
expression \KRNL{e} or a pair \KRNL{\IN{x}{e}}, where \KRNL{x} is a variable and
\KRNL{e} is an expression. The sequence of qualifiers may also be
empty. Such a monoid comprehension is just syntactic sugar that can be
expressed in terms of homomorphisms as follows:

\begin{equation}\label{comprehension-desugaring}
\begin{array}{l@{\;\eqd\;}l}
\KRNL{\Monoid{\oplus} \COMP{e}{}} & \KRNL{e \oplus \ID(\oplus)} \\ [1.5ex]
\KRNL{\Monoid{\oplus} \COMP{e} {\IN{x}{e}', Q }} &
\KRNL{\Hom{e'}{\lambda x.\Comprehension{\oplus}{e}{Q}}{\oplus}} \\ [1.5ex]
\KRNL{\Monoid{\oplus} \COMP{e} {c, Q }} &
\KRNL{\ite{c}{\Monoid{\oplus} \COMP{e} { Q }}{\ID(\oplus)}}
\end{array}
\end{equation}

% {\small\begin{verbatim}
% [op,id]{e | } = op(e,id);
% 
% [op,id]{e | x <- e', Q} = hom(e',lambda> x.[op,id]{e | Q}, op, id);
% 
% [op,id]{e | c, Q} = if c then [op,id]{e | Q} else id;
% \end{verbatim}}
This is explained more formally in Section~\ref{Comprehension}.

Comprehensions are also interesting as they may be subject to transformations
leading to more efficient evaluation than their simple ``nested loops''
operational semantics (by using ``unnesting'' techniques and using relational
operations as implementation instructions).

\SUBSECTION{Comprehension}

The concept of monoid homomorphism is useful for expressing a formal
semantics of iteration over collections. However, it is not very
convenient as a programming construct. A natural notation for such a
construct that is both conspicuous and can be expressed in terms of
monoid homomorphisms is a \emph{monoid comprehension}. This notion
generalizes the familiar notation used for writing a set in comprehension
(as opposed to writing it in extension) using a pattern and a formula
describing its elements (as oppposed to listing all its elements). For
example, the set comprehension $\{\pr(x,x^2)\;|\;x\in\NN, \exists
n.x=2n\}$ describes the set of pairs $\pr(x,x^2)$ (the \emph{pattern}),
verifying the formula $x\in\NN, \exists n.x=2n$ (the \emph{qualifier}).\

This notation can be extended to any (primitive or collection) monoid
$\oplus$. The syntax of a monoid comprehension is an expression of the
form \comp{\oplus}{e}{Q} where \KRNL{e} is an expression called the
\emph{head} of the comprehension, and $Q$ is called its qualifier and is
a sequence $q_1,\ldots,q_n$, $n\geq0$, where each $q_i$ is either
\begin{Itemize}

\item a \emph{generator} of the form $x\from e$, where $x$ is a variable
and \KRNL{e} is an expression; or,

\item a \emph{filter} $\phi$ which is a boolean condition.
\end{Itemize}
In a monoid comprehension expression \comp{\oplus}{e}{Q}, the monoid
operation $\oplus$ is called the \emph{accumulator}.

As for semantics, the meaning of a monoid comprehension is defined
in terms of monoid homomorphisms.
\begin{definition}[Monoid Comprehension]\label{moncompdef}
The meaning of a monoid comprehension over a monoid $\oplus$ is defined
inductively as follows:
\[\renewcommand{\arraystretch}{1.6}
\begin{array}{l@{\;\eqd\;}l}
\comp{\oplus}{e}{} & \left\{\begin{array}{ll}
                            \U{\oplus}(e) & \mbox{if $\oplus$ is a
                            collection monoid} \\
                            e & \mbox{if $\oplus$ is a primitive monoid}
                            \end{array}\right. \\
\comp{\oplus}{e}{x\from e', Q} &
                            \HOM{\odot}{\oplus}[\abs{x}{\comp{\oplus}{e}{Q}}](e')
                            \\
\comp{\oplus}{e}{c, Q} & \ite{c}{\comp{\oplus}{e}{Q}}{\Z{\oplus}}
\end{array}
\]
such that $e:\Ty{\oplus}$, $e':\Ty{\odot}$, and $\odot$ is a collection
monoid.
\end{definition}
Note that although the input monoid $\oplus$ is explicit, each generator
$x\from e'$ in the qualifier has an implicit collection monoid $\odot$
whose characteristics can be inferred with polymorphic typing rules.

Although Definition~\ref{moncompdef} can be effectively computed using
nested loops (\ie, using the iteration semantics~(\ref{homrec})), such would
be in general rather inefficient. Rather, an optimized implementation can
be achieved by various syntactic transformation expressed as rewrite
rules. Thus, the principal benefit of using monoid comprehensions is to
formulate efficient optimizations on a simple and uniform general syntax
of expressions irrespective of specific monoids.

Thus, monoid comprehensions allow the formulation of ``declarative iteration.''
Note the fact mentioned earlier that a homomorphism coming from the translation
of a comprehension encapsulates the operation in its function. Thus, this is
generally taken to advantage with operations that cause a side-effect on their
second argument to enable an in-place homomorphism to dispense with unneeded
intermediate computation.

Section~\ref{Comprehension-class} gives a detailed explanation of the
syntactic desugaring of a pattern-directed high-level syntax of
comprehensions into more basic kernel expressions.

\input{kernel/Comprehension}
