% FILE. . . . . /home/hak/d/ilt/doc/hak/prelim/main.tex
% EDIT BY . . . Hassan Ait-Kaci
% ON MACHINE. . Latitude407
% STARTED ON. . Thu Oct 23 05:09:11 2003

% Last modified on Thu Oct 23 05:09:20 2003 by hak

\documentclass[11pt]{article}

\usepackage{times}
\usepackage{a4}
\usepackage{pstricks}
\usepackage{pst-node}
\usepackage{html}

\input{main.mac}

\begin{document}

%\bodytext{BGCOLOR="white"}

\title{\matisse:\\ \opl\ Redesigned as an Object Query Language\footnote{This is an incomplete draft reporting work in progress.}
}
\author{\large{\hak} \\[2ex]
ILOG, S.A. \\
B.P.~85 - 9, rue de Verdun \\
94253 Gentilly, France \\ [2ex]
\texttt{hak@ilog.fr}
}
\maketitle

\begin{abstract}
In this document, I undertake the design of the declarative part of
an \opl-like language (here, provisionally called ``\matisse'')
using formal concepts from the state of the art in object-oriented
database query languages. I start with an analysis of the constructs
(data structures and operations) used by \opl\ for defining a model,
arguing that the declarative part of \opl\ may be viewed essentially
as a query language over complex data structures, including
collections (such as lists, arrays, sets, and bags). In order to
explicate the precise meaning and optimized implementation of
expressions involving these constructs (such as arbitrarily nested
aggregates, joins, and user-defined functions), I proceed to review
prominent proposals from recent research in object query language
design purporting to embody formally and efficiently queries over
objects and collections thereof, and discuss their merits and
shortcomings for the specific needs of a language such as
\matisse. I then adapt some of these ideas to propose a core algebra
and calculus with the goal of capturing all the declarative
expressivity of \opl\ without any of its current limitations nor
quirks of uniformity, trying to provide the most general, yet
efficient, language conveniences.
\end{abstract}


\section{Introduction}

Programs expressed in the \opl\ language~\cite{opl-book} typically
consist of two separate parts: a model definition and an optional search
specification. The model definition is purely declarative and amounts to
declaring data structures and setting up a model consisting of set of
algebraic constraints with, possibly, an objective ``function'' to
optimize. The search part is not declarative and consists of explicit
indications on how to proceed with searching for solutions of a defined
model. We are only interested here in the purely declarative part of
\opl---the model definition. Upon scrutiny, one realizes that defining a
model amounts to declaring data structures and specifying a model as a
syntactic object expression constructed out of these structures using
data manipulation operations. Thus, the main idea of this work is based
on the realization that an \opl\ model definition can in fact all be
formulated as an expression of an object query
language~\cite{ooql-principles}.

The motivation for redesigning the declarative part of \opl\ at all
stems from the fact that it suffers from several undue
shortcomings~\cite{opl-critique}. While several of these are cosmetic in
nature, some are the result of not having recognized that the operations
and data types for the representation and manipulation of data it needs
have been well studied in the area of object query languages. As a
result, \opl\ provides useful conveniences that feel very appealing to
the user but unfortunately work only for very limited cases, falling
short of supporting these constructs in their full generality. This
state of affairs ends up frustrating the user who is led to expect much
more flexibility than is actually supported, not understanding what
caused a {\em bona fide} expression to be flagged as disallowed when
other similar ones are allowed.  My proposal is to attempt redesigning
\opl\ to support in their full generality all the data definition and
manipulation conveniences it offers, taking inspiration in recent work
in object query language design.


This document is organized as follows. Section~\ref{history} briefly
recounts what one needs to know about query languages.
Section~\ref{oplasoql} examines \opl's constructs for defining
models and argues that it all falls within the object query language
paradigm. In Section~\ref{review}, I present recent work proposing
formal algebras and calculi for expressing the precise semantics and
efficient implementations of object query languages. In
Section~\ref{discussion}, I discuss the specific \emph{desiderata}
for \matisse\ in the light of the reviewed formalisms.  In
Section~\ref{redesign}, I proceed to adapt these ideas to our needs
to arrive at an algebra and a calculus sufficient to express
precisely \opl\ constructs in their full generality, to be used as
the formal basis for a kernel language into which to ``desugar''
a more convenient surface syntax.

\section{A brief history of query languages}
\label{history}

The relational model for databases proposed by
Codd~\cite{codd-70,codd-79,codd-book} owed its resounding success to
using a simple, yet powerful, mathematical formalism to capture the
representation and manipulation of data. It made a clear distinction
between the formal semantics of its constructs and operations (the
{\em Relational Algebra}) and the effective computation of query
expressions taking their meaning in the Relational Algebra (the {\em
Relational Calculus}). In its essence, the only mathematical
formalism used by Relational Algebra is elementary Set Theory. This
enabled expressing simply and elegantly database queries whose
semantic correctness is straightforward to establish due to the pure
declarativity of the Relational Algebra. It also enabled using the
formal algebraic properties of its operations (such as
commutativity, associativity, \etc) to optimize implementation of
the Relation Calculus while provably preserving a query's formal
meaning.  Thus, the Relational Calculus provides the kernel language
in which to express the various constructs of a practical query
language based on relations, which are ascribed a precise formal
semantics in the Relational Algebra.  Such a practical query
language has been proposed, and well accepted, as a standard known
as the Structured Query Language (SQL).\footnote{See,
\eg,~\cite{SQL} for an excellent, easily accessible tutorial.}

Object-oriented databases have evolved out of the relational model
by allowing more flexibility in the form taken by the data and
incorporating the object-oriented notions of type encapsulation and
inheritance. The added flexibility consists essentially in allowing
arbitrary nesting of record object structures (\ie, tuples) and
collections (\ie, sets, bags, lists, \etc). In other words, whereas
the relational model deals exclusively with relations over tuples of
primitive types (\ie, sets of flat tuples---so-called ``relational
normal forms''), the object model imposes no such restriction.  The
other added conveniences---(polymorphic) typing, inheritance, and
class/method encapsulation---have been introduced for the same
obvious reasons as for general-purpose programming languages (\ie,
data abstraction, reusability, modularity, \etc). As it turns out,
the mere task of dealing with non-normal form objects alone in the
same simple formal fashion as was done in the relational model (\ie,
providing an algebra and a calculus that can be optimized thanks to
the algebra's equational theory) has been a hard task to
tackle. Only recently have some elegant, yet powerful, formalisms
emerged that begin to meet the
challenge~\cite{buneman-etal-94,vandenberg-phd,wong-phd}.  In other
words, these formalisms are good candidates to stand with respect to
OQL, the ODMG Object Query Language standard~\cite{oql}, as the
relational algebra and calculus stand with respect to SQL.

While the work done in the past twenty or so years in programming
language design theory has made object-orientation and typing an
orthogonal issue to the underlying computational model, one does need an
underlying calculus to start with (\eg, in order to have C++, one needs
to have C first). In other words, given a calculus, be it functional,
logical, or imperative, it is not a major task to recast it as an
object-oriented calculus by adapting its syntax and typing rules to deal
with encapsulation and inheritance, while keeping its underlying
computational model. My intention, thus, is to start with a ``flat''
typed object algebra and calculus rich enough to express and optimize
the construction of a constraint model from a high-level definition of
the kind supported by \opl, and delay incorporating true
object-orientation until such a basic formalism is at hand.  Indeed,
providing full object-orientation for \matisse\ is only a second phase
which should unfold relatively straightforwardly once its basic
formalism has been designed.

\section{\opl\ as an object query language}
\label{oplasoql}

Let us consider an OPL program defining a transportation model.  A
certain set of \emph{products} are manufactured and consumed in a set of
\emph{cities}. Data describing the \emph{supply} is given specifying how
much of each product is manufactured at each city, how much of each
product is consumed at each city, and how much it costs per unit of
product to be shipped from each city to each city. We want to establish
how much of each good to transport between cities in such a way as to
meet the demand within the supply and minimize the total cost.

The complete listing of an OPL program defining a model for a
transportation problem is given in Appendix Section~\ref{transpmod}.
%on Page~\pageref{transpmod}
I will refer to the line numbers of that listing in the following
discussion.


\ignore{The two declarations,
{\small\begin{verbatim}
enum Cities   { Paris, Lyon, Marseille };
enum Products { bands, coils, plate };
\end{verbatim}}
\noindent define two enumeration types (\ie, ordered sets of symbols),
\texttt{Cities} and \texttt{Products}, whose elements are specified
between braces. Such types can then be used for indexing array
elements using more readable symbolic names rather than plain
integer values. The declaration,
{\small\begin{verbatim}
float+ limit  = 150;
\end{verbatim}}
\noindent defines a variable identifier \texttt{limit} whose type is a
non-negative floating-point number, and initialized to a particular
constant $(150.0)$.
The declarations,
{\small\begin{verbatim}
float+ supply [ Products, Cities ] = [ [ 40,  70,  80 ]
                                     , [ 80, 160, 180 ]
                                     , [ 20,  30,  30 ]
                                     ];

float+ demand [ Products, Cities ] = [ [  85, 45,  60 ]
                                     , [ 170, 95, 155 ]
                                     , [  60, 15,   5 ]
                                     ];
\end{verbatim}}
\noindent define two 2-dimensional arrays, \texttt{supply} and
\texttt{demand}, of non-negative floating-point numbers indexed over
the enumeration types \texttt{Products} and \texttt{Cities} and
initialized to the given matrices.
The construct,
{\small\begin{verbatim}
assert
 forall (p in Products)
   sum (o in Cities) supply[p,o] = sum(d in Cities) demand[p,d];
\end{verbatim}}
\noindent specifies a data integrity condition that must be verified
on the data contained in the arrays \texttt{supply} and \texttt{demand}.
once it has been initialized; \ie, that the total supply meet the
total demand. This shows two constructs: the \texttt{forall} and
\texttt{sum} \emph{aggregate operators}. They both use an identifier
ranging over a set (in this case, the enumerations \texttt{Products}
and \texttt{Cities}) and an expression. The expression of a
\texttt{forall} is of boolean type,\footnote{There are no such types
in \opl\ in fact. Instead, the integer $0$ and $1$ are used.} and
the expression of a \texttt{sum} is of numerical type. The value of
a \texttt{forall} is true if its expression is true for all its
range values. The value of a \texttt{sum} is the sum of values taken
by its expression for all its range values. This sort of computation
is at the core of \opl\ data definition and can be described a
(set) \emph{comprehension} in database query parlance. We shall see
that this is precisely how such expressions are to be formalized.

The declaration,
{\small\begin{verbatim}
float+ cost [ Products, Cities, Cities ] = [ [ [ 4, 6, 9 ]
                                             , [ 8, 4, 3 ]
                                             , [ 1, 6, 8 ]
                                             ]
                                           , [ [ 3, 6, 3 ]
                                             , [ 2, 5, 6 ]
                                             , [ 7, 8, 5 ]
                                             ]
                                           , [ [ 1, 2, 6 ]
                                             , [ 2, 3, 7 ]
                                             , [ 3, 8, 6 ]
                                             ]
                                           ];
\end{verbatim}}
\noindent defines a 3-dimensional array, \texttt{cost}, of non-negative
floating-point numbers indexed over the enumeration types
\texttt{Products}, \texttt{Cities}, and \texttt{Cities}, and
initialized to the  given array of matrices.

{\small\begin{verbatim}
var float+ trans [Products, Cities, Cities];

minimize
 sum (p in Products & o,d in Cities) cost[p,o,d] * trans[p,o,d]
subject to
 {
   forall (p in Products & o in Cities) 
      sum (d in Cities) trans[p,o,d] = supply[p,o];
   forall (p in Products & d in Cities) 
      sum (o in Cities) trans[p,o,d] = demand[p,d];
   forall (o, d in Cities)
      sum (p in Products) trans[p,o,d] <= limit;
 };
\end{verbatim}}}


\section{A review of object query language formalisms}
\label{review}

In this section, I review prominent formalisms, focusing mainly on two
recent proposals using the notion of comprehension syntax due to Peter
Buneman \etal~\cite{buneman-etal-94} with extensions to support
arrays---a data structure of prime importance for an language with
mathematical programming capabilities such as \opl. The first is due to
Leonidas Fegaras and David Maier~\cite{fegaras-maier-2000} and uses the
notion of {\em Monoid Comprehensions}; the second is due to Leonid
Libkin, Rona Machlin, and Limsoon Wong~\cite{libkin-etal-96} and proposes
a functional calculus of array objects. These two formalisms are very
similar, differing mostly in their treatment of arrays (as collections
in~\cite{fegaras-maier-2000}, and as functions
in~\cite{libkin-etal-96}). My intention is to try and merge ideas from
both for our purpose.

\subsection{Monoid homomorphisms and comprehensions}
\label{monhomcomp}

The formalism presented here is based on~\cite{fegaras-maier-2000} and
assumes familiarity with the notions and notations summarized in Appendix
Section~\ref{monoids}.
%on Page~\pageref{monoids}.
I will use the programming view of monoids exposed there using the
specific notation of monoid attributes, in particular for sets, bags, and
lists. I will also assume basic familiarity with naive $\lambda$-calculus
and associated typing as presented in Appendix Section~\ref{tplc}.
%on Page~\pageref{tplc}.

\subsubsection{Monoid homomorphisms}
\label{monhom}

Because many operations and data structures are monoids, it is
interesting to use the associated concepts as the computational building
block of an essential calculus. In particular, iteration over collection
types can be elegantly formulated as computing a \emph{monoid
homomorphism}. This notion coincides with the usual mathematical notion
of homomorphism, albeit given here from an operational standpoint and
biased toward collection monoids. Basically, a monoid homomorphism
\HOM{\oplus}{\odot} maps a function $f$ from a collection monoid $\oplus$
to \emph{any} monoid $\odot$ by collecting all the $f$-images of elements
of a $\oplus$-collection using the $\odot$ operation. For example, the
expression $\HOM{\conc}{\cup}[\abs{x}{x+1}]$ applied to the list
$[1,2,1,3,2]$ returns the set $\{2,3,4\}$. In other words, the monoid
homomorphism \HOM{\conc}{\cup} of a function $f$ applied to a list $L$
corresponds to the following \emph{loop} computation:
\[
\begin{array}{ll}
\t{result} \from \eset; \\
\b{foreach}\;\; x\;\; \b{in}\;\; L \;\;\b{do}\; \t{result} \from \t{result} \cup f(x); \\
\b{return}\;\; \t{result};
\end{array}
\]

This is formulated formally as follows:
\begin{definition}[Monoid Homomorphism]\label{monhomdef}
A \emph{Monoid Homomorphism} \HOM{\oplus}{\odot} defines a mapping from a
\emph{collection} homomorphism $\oplus$ to \emph{any} monoid $\odot$ such that
\subeq{\oplus}{\odot} by:
\[
\renewcommand{\arraystretch}{1.6}
\begin{array}{l@{\;\;\eqd\;\;}l}
\HOM{\oplus}{\odot}[f](\Z{\oplus})    & \Z{\odot} \\
\HOM{\oplus}{\odot}[f](\U{\oplus}(x)) & f(x) \\
\HOM{\oplus}{\odot}[f](x\oplus y)     & \HOM{\oplus}{\odot}[f](x) \odot
                                        \HOM{\oplus}{\odot}[f](y)
\end{array}
\]
for any function $f:\arr{\alpha}{\Ty{\odot}}$, $x:\alpha$, and $y:\alpha$,
where $\Ty{\oplus}=\Co{\oplus}(\alpha)$.
\end{definition}

Again, computationally, this amounts to executing the following
iteration:
\begin{equation}\label{loop}
\begin{array}{ll}
\t{result} \from \Z{\odot}; \\
\b{foreach}\;\; x_i\;\;\b{in}\;\;\U{\oplus}(x_1)\oplus\cdots\oplus\U{\oplus}(x_n)
\;\;\b{do}\; \t{result} \from \t{result} \odot f(x_i); \\
\b{return}\;\; \t{result};
\end{array}
\end{equation}

The reader may be puzzled by the condition \subeq{\oplus}{\odot} in
Definition~\ref{monhomdef}. It means that a monoid homomorphisms may only be
defined from a collection monoid to a monoid that has at least the same
equational theory. In other words, one can only go from an empty theory
monoid, to either a $\{C\}$-monoid or an $\{I\}$-monoid, or yet to a
$\{C,I\}$-monoid. This requirement is due to an algebraic technicality,
and relaxing it would enable a monoid homomorphism to be ill-defined.
To see this, consider going from, say, a commutative-idempotent monoid to
one that is commutative but not idempotent. Let us take, for example,
\HOM{\cup}{+}. Then, this entails:
\[
\renewcommand{\arraystretch}{1.6}
\begin{array}{l@{\;=\;}l}
1 & \HOM{\cup}{+}[\abs{x}{1}](\{a\}) \\
  & \HOM{\cup}{+}[\abs{x}{1}](\{a\}\cup\{a\}) \\
  & \HOM{\cup}{+}[\abs{x}{1}](\{a\}) \;+\;\HOM{\cup}{+}[\abs{x}{1}](\{a\}) \\
  & 1 + 1 \\
  & 2.
\end{array}
\]

The reader may have noticed that this restriction has the unfortunate
consequence of disallowing potentially useful computations, notable
examples being computing the cardinality of a set, or converting a set
into a list. However, this drawback can be easily overcome with a
suitable modification of the third clause in Definition~\ref{monhomdef},
and other expressions based on it, ensuring that anomalous cases such as
the above are dealt with by appropriate tests.

Also of importance for the consistency of Definition~\ref{monhomdef} is
the fact that a non-idempotent monoid must be anti-idempotent, and a
non-commutative monoid must be anti-commutative. Indeed, if $\oplus$ is
non-idempotent as well as non-anti-idempotent (say, $x_0\oplus x_0=x_0$
for some $x_0$), then this entails:
\[
\renewcommand{\arraystretch}{1.6}
\begin{array}{l@{\;=\;}l}
\HOM{\oplus}{\odot}[f](x_0) & \HOM{\oplus}{\odot}[f](x_0\oplus x_0) \\
 & \HOM{\oplus}{\odot}[f](x_0) \;\odot\; \HOM{\oplus}{\odot}[f](x_0)
\end{array}
\]
\noindent which is not necessarily true for non-idempotent $\odot$. A
similar argument may be given for commutativity. This consistency
condition is in fact not restrictive operationally as it is always
verified (\eg, a list will not allow partial commutation of any of its
element).

Here are a few familar functions expressed with well-defined monoid
homomorphisms:
\[
\renewcommand{\arraystretch}{1.6}
\begin{array}{l@{\;=\;}l}
\t{length}(l)   & \HOM{\conc}{+}[\abs{x}{1}](l) \\
e \in s         & \HOM{\cup}{\vee}[\abs{x}{x=e}](s) \\
s \times t      &
\HOM{\cup}{\cup}[\abs{x}{\HOM{\cup}{\cup}[\abs{y}{\{\pr{x}{y}\}}](t)}](s) \\
\t{map}(f,s)    & \HOM{\cup}{\cup}[\abs{x}{\{f(x)\}}](s) \\
\t{filter}(p,s) & \HOM{\cup}{\cup}[\abs{x}{\ite{p(x)}{\{x\}}{\eset}}](s).
\end{array}
\]


\subsubsection{Monoid comprehensions}
\label{moncomp}

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 $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 $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{loop})), 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.

Note that relational \emph{joins} are immediately expressible as monoid
comprehensions. Indeed, the join of two sets $S$ and $T$ using a function
$f$ and a predicate $p$ is simply:
\begin{equation}\label{setjoin}
S \Join_p^f T \;\eqd\; \comp{\cup}{f(x,y)}{x\from S, y\from T, p(x,y)}.
\end{equation}
Typically, a relational join will take $f$ to be a record constructor.
For example, if we write a record whose fields $\t{l}_i$ have values
$e_i$ for $i=1,\ldots,n$, as $\pr{\t{l}_1=e_1,}{\ldots,\t{l}_n=e_n}$,
then a standard relational join is obtained with, say, $f(x,y) =
\pr{\t{name}=y.\t{name}}{\t{age}=2*x.\t{age}}$, and $p(x,y)$ may be any
condition such as $x.\t{name}=y.\t{name}, x.\t{age}\geq 18$.

Clearly, monoid comprehensions can immediately express queries using all
usual relational operators (and, indeed, object queries as well) and most
usual functions. For example,
\[
\begin{array}{l@{\hskip2em}l}
\renewcommand{\arraystretch}{1.6}
\begin{array}{l@{\;\;\eqd\;\;}l}
\exists x\in s.e & \comp{\vee}{e}{x\from s} \\
\forall x\in s.e & \comp{\wedge}{e}{x\from s} \\
x \in s          & \comp{\vee}{x=y}{y\from s} \\
s \cap t         & \comp{\cup}{x}{x\from s, x\in t} \\
\t{count}(a,s)   & \comp{+}{1}{x\from s, x=a} \\
\end{array}
&
\renewcommand{\arraystretch}{1.6}
\begin{array}{l@{\;\;\eqd\;\;}l}
\t{length}(s)   & \comp{+}{1}{x\from s} \\
\t{sum}(s)      & \comp{+}{x}{x\from s} \\
\t{max}(s)      & \comp{\max}{x}{x\from s} \\
\t{filter}(p,s) & \comp{\cup}{x}{x\from s, p(x)} \\
\t{flatten}(s)  & \comp{\cup}{x}{t\from s, x\from t} \\
\end{array}
\end{array}
\]
Note that some of these functions will work only on appropriate types of
their arguments. For example, the type of the argument of $\t{sum}$ must
be a non-idempotent monoid, and so must the type of the second argument
of \t{count}. Thus, \t{sum} will add up the elements of a bag or a list,
and \t{count} will tally the number of occurrences of an element in a bag
or a list. Applying either \t{sum} or \t{count} to a set will be caught
as a type error.

\subsubsection{The monoid comprehension calculus}
\label{mcc}

We are now in a position to propose a programming calculus using monoid
comprehensions. Figure~\ref{mcc-syntax} defines an abstract grammar for
an expression $e$ of the \emph{Monoid Comprehension Calculus} and amounts
to adding comprehensions to an extended Typed Polymorphic
$\lambda$-Calculus. Figure~\ref{mcc-typing} gives the typing rules for
this calculus.

\begin{figure}
\begin{center}
\fbox{$\begin{array}{rrll}
e & ::= & \bot          & \mbox{null value} \\
  &   | & c             & \mbox{constant} \\
  &   | & x             & \mbox{symbol} \\
  &   | & \abs{x}{e}    & \mbox{abstraction} \\
  &   | & \app{e_1}{e_2}& \mbox{application} \\
  &   | & \tp{\t{l}_1=e_1}{\t{l}_n=e_n} & \mbox{record} \\
  &   | & \pj{e}{\t{l}} & \mbox{projection} \\
  &   | & \ite{e_1}{e_2}{e_3} & \mbox{conditional} \\
% &   | & \app{\fix}{e} & \mbox{recursion} \\
  &   | & \Z{\oplus}    & \mbox{monoid identity} \\
  &   | & \U{\oplus}(e) & \mbox{monoid unit injection} \\
  &   | & e_1\oplus e_2 & \mbox{monoid operation} \\
  &   | & \comp{\oplus}{e}{Q} & \mbox{monoid comprehension} \\
\end{array}$}
\end{center}
\caption{The monoid comprehension calculus}
\label{mcc-syntax}
\end{figure}


\begin{figure}
\begin{center}
\fbox{\begin{tabular}{rl}

$\typerule{}{\sequent{\Gamma}{\bot}{\alpha}}$
& for any $\Gamma$ \\ \\

$\typerule{}{\sequent{\Gamma}{c}{\tau}}$
& for any $\Gamma$, if $\type(a)=\tau$ \\ \\

$\typerule{}{\sequent{\Gamma}{x}{\tau}}$
& if $\Gamma(x)=\tau$ \\ \\

$\typerule{\sequent{\Gamma[x:\tau_1]}{e}{\tau_2}}
{\sequent{\Gamma}{\abs{x}{e}}{\arr{\tau_1}{\tau_2}}}$
& \\ \\

$\typerule{\sequent{\Gamma}{e_1}{\arr{\tau_1}{\tau_2}},
\          \sequent{\Gamma}{e_2}{\tau_1}}
{\sequent{\Gamma}{\app{e_1}{e_2}}{\tau_2}}$
& \\ \\

$\typerule{\sequent{\Gamma}{e_1}{\tau_1},
\          \cdots,
\          \sequent{\Gamma}{e_k}{\tau_k}}
{\sequent{\Gamma}
         {\tp{\t{l}_1=e_1}{\t{l}_k=e_k}}
         {\tp{\t{l}_1:\tau_1}{\t{l}_k:\tau_k}}}$
& \\ \\

$\typerule{\sequent{\Gamma}{e}{\tp{\t{l}_1:\tau_1}}{\t{l}_k:\tau_k}}
{\sequent{\Gamma}{\pj{e}{\t{l}}}{\tau}}$ 
& if $\t{l}\in\{\t{l}_1,\ldots,\t{l}_k\}$ \\ \\

$\typerule{\sequent{\Gamma}{e_1}{\bool},
\          \sequent{\Gamma}{e_2}{\tau},
\          \sequent{\Gamma}{e_3}{\tau}}
{\sequent{\Gamma}{\ite{e_1}{e_2}{e_3}}{\tau}}$
& \\ \\

%$\typerule{\sequent{\Gamma}{e}{\arr{\tau}{\tau}}}
%{\sequent{\Gamma}{\app{\fix}{e}}{\tau}}$
%& \\ \\

$\typerule{}{\sequent{\Gamma}{\Z{\oplus}}{\Ty{\oplus}}}$
& for any $\Gamma$ \\ \\

$\typerule{\sequent{\Gamma}{e}{\tau}}
{\sequent{\Gamma}{\U{\oplus}(e)}{\Co{\oplus}(\tau)}}$
& if $\oplus$ is a collection monoid \\ \\

$\typerule{\sequent{\Gamma}{e_1}{\Ty{\oplus}}
,\;        \sequent{\Gamma}{e_2}{\Ty{\oplus}}}
{\sequent{\Gamma}{e_1 \oplus e_2}{\Ty{\oplus}}}$
& if $\oplus$ is a primitive monoid \\ \\

$\typerule{\sequent{\Gamma}{e_1}{\Co{\oplus}(\tau)}
,\;        \sequent{\Gamma}{e_2}{\Co{\oplus}(\tau)}}
{\sequent{\Gamma}{e_1 \oplus e_2}{\Co{\oplus}(\tau)}}$
& if $\oplus$ is a collection monoid \\ \\

$\typerule{\sequent{\Gamma}{e}{\Ty{\oplus}}}
{\sequent{\Gamma}{\comp{\oplus}{e}{}}{\Ty{\oplus}}}$
& if $\oplus$ is a primitive monoid \\ \\

$\typerule{\sequent{\Gamma}{e}{\tau}}
{\sequent{\Gamma}{\comp{\oplus}{e}{}}{\Co{\oplus}(\tau)}}$
& if $\oplus$ is a collection monoid \\ \\

$\typerule{\sequent{\Gamma}{e_2}{\Co{\odot}(\tau_2)}
,\;        \sequent{\Gamma[x:\tau_2]}{\comp{\oplus}{e_1}{Q}}{\tau_1}}
{\sequent{\Gamma}{\comp{\oplus}{e_1}{x\from e_2,Q}}{\tau_1}}$
& if \subeq{\odot}{\oplus} \\ \\

$\typerule{\sequent{\Gamma}{e_2}{\bool}
,\;        \sequent{\Gamma}{\comp{\oplus}{e_1}{Q}}{\tau}}
{\sequent{\Gamma}{\comp{\oplus}{e_1}{e_2,Q}}{\tau}}$
& 

\end{tabular}}
\end{center}
\caption{Typing rules for the Monoid Comprehension Calculus}
\label{mcc-typing}
\end{figure}


\subsection{Multidimensional arrays as functions}

\section{Discussion}
\label{discussion}

\subsection{What types for \matisse?}

Before we delve into redesigning a new \opl, we need to ponder its
type particularities---indeed, peculiarities. The current \opl\ departs
from conventional programming langauges when it comes to types in
several respects. Figure~\ref{opl-types} shows the types supported by
\opl.
\begin{figure}

\begin{center}

\begin{tabular}{cccccccccc}
&&& \rnode{TYPE}{type} \\ [3cm]

\rnode{BASIC}{basic} &
\rnode{STRUCTURE}{structure} &
\rnode{RANGE}{range} &
\rnode{ENUM}{enum} &
\rnode{SETOF}{setof(type)} &
\rnode{ARRAY}{array[type]} \\

\end{tabular}
\ncline{-}{TYPE}{BASIC}
\ncline{-}{TYPE}{STRUCTURE}
\ncline{-}{TYPE}{RANGE}
\ncline{-}{TYPE}{ENUM}
\ncline{-}{TYPE}{SETOF}
\ncline{-}{TYPE}{ARRAY}
\end{center}

\caption{\opl\ types}
\label{opl-types}
\end{figure}

\subsubsection{Primitive types}

\subsubsection{Object types}

\subsubsection{Collections types}

\subsection{Array types}

\subsubsection{First-class indexing}

\textit{\textbf{HAK NOTE:} Discuss the ZPL-region
approach~\cite{zpl-regions} for use in \matisse, and their sparse
version~\cite{zpl-sparse-regions}.}

\subsubsection{Indexing types}

\subsection{Functional abstraction}

\section{Designing \matisse}
\label{redesign}

\subsection{Algebra}

\subsection{Semantics}

\subsection{Implementation}

\appendix\section*{Appendix}

In this part of the document, I summarize well-known notions that may be
needed by some readers lacking the appropriate background.  This is in
order to spare those who already know this material and unclutter the
main body of the text. The latter reason is also why
Section~\ref{transpmod} contains the complete listing of the
transportation model used in the discussion of Section~\ref{oplasoql}.

\section{Technical Background}

\subsection{The Relational Model}
\label{relmod}

\subsection{Monoids}
\label{monoids}

In this section, all notions and notations relating to monoids as they
are used in this paper are recalled and justified.

Mathematically, a monoid is a non-empty set equipped with an associative
internal binary operation and an identity element for this
operation. Formally, let $S$ be a set, $\star$ a function from $S\times
S$ to $S$, and $\epsilon\in S$; then, $\MON{S}{\star}{\epsilon}$
is a monoid iff, for any $x, y, z$ in $S$:
\begin{equation}\label{assoc}
x\star(y\star z) = (x\star y)\star z 
\end{equation}
and
\begin{equation}\label{neutral}
x\star\epsilon = \epsilon\star x = \epsilon.
\end{equation}

Most familiar mathematical binary operations define monoids. For
example, taking the set of natural numbers $\NN$, and the set of
boolean values $\BB=\{\true,\false\}$, the following are monoids:
\begin{itemize}
\item $\MON{\NN}{+}{0}$,
\item $\MON{\NN}{*}{1}$,
\item $\MON{\NN}{\max}{0}$,
\item $\MON{\BB}{\vee}{\false}$,
\item $\MON{\BB}{\wedge}{\true}$.
\end{itemize}
The operations of these monoids are so familiar that they need not
be explicated. For us, they have a ``built -in'' semantics that
allows us to compute with them since primary school. Indeed, we
shall refer to such readily interpreted monoids as \emph{primitive
monoids}.\footnote{We call these monoids ``primitive'' following the
presentation of Fegaras and Maier~\cite{fegaras-maier-2000} as it
adheres to a more operational (as opposed to mathematical) approach
more suitable to computer-scientists. Mathematically, however, these
should be called ``semantic'' monoids since they are interpreted by
the computation semantics of their operations.}

Note that the definition of a monoid does not preclude additional
algebraic structure. Such structure may be specified by other equations
augmenting the basic monoid equational theory given by the conjunction
of equations~(\ref{assoc}) and ~(\ref{neutral}). For example, all five
monoids listed above are \emph{commutative}; namely, they also obey
equation~(\ref{commut}):
\begin{equation}\label{commut}
x\star y = y\star x
\end{equation}
for any $x, y$. In addition, the three last ones (\ie, $\max$,
$\vee$, and $\wedge$) are also \emph{idempotent}; namely, they also obey
equation~(\ref{idem}):
\begin{equation}\label{idem}
x\star x = x
\end{equation}
for any $x$.

Not all monoids are primitive monoids. That is, one may define a monoid
purely syntactically whose operation only builds a syntactic structure
rather than being interpreted using some semantic computation. For
example, linear lists have such a structure: the operation is list
concatenation and builds a list out of two lists; its identity element
is the empty list.  A syntactic monoid may also have additional
algebraic structure.  For example, the monoid of bags is also defined as
a commutative syntactic monoid with the disjunct union operation and the
empty bag as identity. Or, the monoid of sets is a commutative and
idempotent syntactic monoid with the union operation and the empty set
as identity.

Because they are not interpreted, syntactic monoids pose a problem as
far as representation of its elements is concerned.  To illustrate this,
let us consider an empty-theory algebraic structure; that is, one
without any equations---not even associativity nor identity. Let us take
such a structure with one binary operation $\star$ on, say, the natural
numbers $\NN$. Saying that $\star$ is a ``syntactic'' operation means
that it constructs a syntactic term (\ie, an expression tree) by
composing two other syntactic terms. We thus can define the set
$T_{\star}$ of $\star$-terms on some base set, say the natural numbers,
inductively as the limit $\cup_{n\geq 0}T_n$ where,
\begin{equation}
\label{tstar}
T_n \;\eqd\; \left\{
\begin{array}{ll}
\NN & \makebox{if $n=0$} \\ \\
\{ t_1\star t_2 \;|\; t_i\in T_{n-1}, i=1,2 \} & \makebox{if $n>0$}
\end{array}\right.
\end{equation}
Clearly, the set $T_{\star}$ is well defined and so is the $\star$
operation over it. Indeed, $\star$ is a \emph{bona fide} function from
$T_{\star}\times T_{\star}$ to $T_{\star}$ mapping two terms $t_1$ and
$t_2$ in $T_{\star}$ into a unique term in $T_{\star}$---namely,
$t_1\star t_2$. This is why $T_{\star}$ is called the \emph{syntactic}
algebra.\footnote{For a fixed set of base elements and operations (which
constitute what is formally called a \emph{signature}), the syntactic
algebra is unique (up to isomorphism). This algebra is also called the
\emph{free}, or the \emph{initial}, algebra for its signature.}

Let us now assume that the $\star$ operation is associative---\ie, that
$\star$-terms verify Equation~(\ref{assoc}). Note that this equation
defines a (syntactic) \emph{congruence} on $T_{\star}$ which identifies
terms such as, say, $1\star(2\star3)$ and $(1\star2)\star3$. In fact,
for such an associative $\star$ operation, the set $T_{\star}$ defined
in Equation~(\ref{tstar}) is not the appropriate domain. Rather, the
right domain is the quotient set whose elements are (syntactic)
congruence classes modulo associativity of $\star$. Therefore, this
creates an ambiguity of representation of the syntactic
structures.\footnote{Note that this ambiguity never arises for semantic
algebras whose operations are interpreted into a unique result.}

Similarly, more algebraic structure defined by larger equational theories
induces coarser quotients of the empty-theory algebra by putting together
in common congruence classes all the syntactic expressions that can be
identified modulo the theory's equations.  The more equations, the more
ambiguous the syntactic structures of expressions. Mathematically, this
poses no problem as one can always abstract away from individuals to
congruence classes. However, operationally one must resort to some
concrete artifact to obtain a unique representation for all members of
the same congruence class.  One way is to devise a \emph{canonical}
representation into which to transform all terms. For example, an
associative operation could systematically ``move'' nested subtrees from
its left argument to its right argument---in effect using
Equation~(\ref{assoc}) as a one-way rewrite rule. However, while this is
possible for some equational theories, it is not so in general---\eg,
take commutativity.\footnote{Such are important considerations in the
field of \emph{term rewriting}~\cite{rewriting-taste}, where the problem
of finding canonical term representations for equational theories was
originally addressed by Donald Knuth and Peter Bendix in a seminal paper
proposing a general effective method---the so-called Knuth-Bendix
Completion Algorithm~\cite{k-b}. The problem, incidentally, is only
semi-decidable.  In other words, the Knuth-Bendix algorithm may diverge,
although several interesting variations have been proposed for a wide
extent of practical uses (see~\cite{rewriting-taste} for a good
introduction and bibliography).}

From a programming standpoint (which is ours), we can abstract away from
the ambiguity of canonical representations of syntactic monoid terms
using a flat notation. For example, in LISP and Prolog, a list is seen as
the (flat) sequence of its constituents.  Typically, a programmer writes
$[1,2,1]$ to represent the list whose elements are $1$, $2$ and $1$ in
this order, and does not care (nor need s/he be aware) of its concrete
representation.  A set---\ie, a commutative idempotent syntactic
monoid---is usually denoted by the usual mathematical notation $\{1,2\}$,
implicitly relying on disallowing duplicate elements, not minding the
order in which the elements appear. A bag, or multiset---\ie, a
commutative but non-idempotent syntactic monoid---uses a similar
notation, allowing duplicate elements but paying no heed to the order in
wich they appear; \ie, $\mset{1,2,1}$ is the bag containing $1$ twice,
and $2$ once.

Syntactic monoids are quite useful for programming as they provide
adquate data structures to represent collections of objects of a given
type. Thus, we refer to them as \emph{collection monoids}. Now, a
definition such as Equation~(\ref{tstar}) for a syntactic monoid,
although sound mathematically, is not quite adequate for programming
purposes. This is because it defines the $\star$ operations on two
distinct \emph{types} of elements; namely, the base elements (here
natural numbers) and constructed elements. In programming, it is
desirable that operations be given a crisp type. A way to achieve this is
by systematically ``wrapping'' each base element $x$ into a term such as
$x\star\epsilon$. This ``wrapping'' is achieve by associating to the
monoid a function $\U{\star}$ from the base set into the monoid domain
called its \emph{unit injection}. For example, if $\conc$ is the list
monoid operation for concatenating two lists, $\U{\conc}(x)=[x]$ and one
may view the list $[a,b,c]$ as $[a]\conc[b]\conc[c]$.  Similarly, the set
$\{a,b,c\}$ is viewed as $\{a\}\cup\{b\}\cup\{c\}$, and the bag
$\mset{a,b,c}$ as $\mset{a}\uplus\mset{b}\uplus\mset{c}$.  Clearly, this
bases the constructions on an isomorphic view of the base set rather than
the base set itself, while using a uniform type for the monoid operator.
Also, because the type of the base elements is irrelevant for the
construction other than imposing the constraint that all such elements be
of the same type, we present a collection monoid as a \emph{polymorphic}
data type. This justifies the formal view of monoids we give next using
the programming notion of type.

Because it is characterized by its operation $\oplus$, a monoid is often
simply referred to as $\oplus$. Thus, a monoid operation is used as a
subscript to denote its characteristic attributes.  Namely, for a monoid
$\oplus$,
\begin{itemize}
\item $\Ty{\oplus}$ is its type (\ie, $\oplus:
\arr{\Ty{\oplus}\times\Ty{\oplus}}{\Ty{\oplus}}$),

\item $\Z{\oplus} : \Ty{\oplus}$ is its identity element,

\item $\E{\oplus}$ is its equational theory (\ie, a subset of the set
$\{C,I\}$, where $C$ stands for ``commutative'' and $I$ for
``idempotent'');
\end{itemize}
and, if it is  a collection monoid,
\begin{itemize}
\item $\Co{\oplus}$ is its type constructor (\ie, $\Ty{\oplus} =
\Co{\oplus}(\alpha)$),

\item $\U{\oplus} : \arr{\alpha}{\Co{\oplus}(\alpha)}$ is its unit
injection.
\end{itemize}
Table~\ref{monatts} summarizes the monoid attributes of a few usual
monoids.
\begin{table}
\begin{center}
\begin{tabular}{c@{\hskip1.5cm}c}
\renewcommand{\arraystretch}{1.2}
\begin{tabular}[t]{|c|l|c|c|}
\hline
$\oplus$ & $\Ty{\oplus}$ & $\Z{\oplus}$ & $\E{\oplus}$  \\
\hline
$+$      & \integer     & $0$            & $\{C\}$ \\
$*$      & \integer     & $1$            & $\{C\}$ \\
$\max$   & \integer     & $0$            & $\{C,I\}$ \\
$\vee$   & \bool        & $\false$       & $\{C,I\}$ \\
$\wedge$ & \bool        & $\true$        & $\{C,I\}$  \\
\hline
\end{tabular}
&
\renewcommand{\arraystretch}{1.2}
\begin{tabular}[t]{|c|l|l|c|c|c|}
\hline
$\oplus$ & $\Co{\oplus}$   & $\Ty{\oplus}$   & $\Z{\oplus}$ & $\U{\oplus}(x)$ & $\E{\oplus}$  \\
\hline
$\cup$   & $\set$ & $\set(\alpha)$ &  $\eset$     & $\{x\}$         & $\{C,I\}$ \\
$\uplus$ & $\bag$ & $\bag(\alpha)$ &  $\ebag$     & $\mset{x}$      & $\{C\}$ \\
$\conc$  & $\lst$ & $\lst(\alpha)$ &  $\elst$     & $[x]$           & $\empty$  \\
\hline
\end{tabular}
\\ \\ [1ex]
Primitive monoids
&
Collection monoids
\end{tabular}
\end{center}
\caption{Attributes of a few common monoids}
\label{monatts}
\end{table}

\subsection{The Typed Polymorphic $\lambda$-Calculus}
\label{tplc}

We assume a set $\C$ of pregiven constants ususally denoted by $a, b
\ldots$, and a countably infinite set of variable symbols $\V$
usually denoted by $x, y, \ldots$.  The syntax of a term $t$ of the
$\lambda$-Calculus is given by the following grammar:
\begin{equation}
\label{lambda-terms}
\begin{array}{rrlll}
t & ::= & a          & (a\in\C) & \mbox{constant} \\
  &   | & x          & (x\in\V) & \mbox{symbol} \\
  &   | & \abs{x}{t} & (x\in\V) & \mbox{abstraction} \\
  &   | & \app{t}{t} &          & \mbox{application}
\end{array}
\end{equation}
We shall call $\T$ the set of terms $t$ defined by this grammar.
These terms are also called \emph{raw} terms.


An abstraction $\abs{x}{t}$ defines a \emph{lexical scope} for its
\emph{bound variable} $x$, whose extent is its \emph{body}
$t$. Thus, the notion of free occurrence of a variable in a term is
defined as usual, and so is the operation $\subst{t_2}{x}{t_1}$ of
substituting a term $t_2$ for all the free occurrences of a variable
$x$ in a term $t_1$. Thus, a bound variable may be renamed to a new
one in its scope without changing the abstraction.

The computation rule defined on $\lambda$-terms is the so-called
$\beta$-reduction:
\begin{equation}
\label{beta-reduction}
\begin{array}{rl}
\app{(\abs{x}{t_1})}{t_2} & \gives \subst{t_2}{x}{t_1}.
\end{array}
\end{equation}

We assume a set $\BT$ of basic type symbols denoted by $A, B,
\ldots$, and a countably infinite set of type variables $\VT$
denoted by $\alpha, \beta, \ldots$.  The syntax of a type $\tau$ of
the Typed Polymorphic $\lambda$-Calculus is given by the following
grammar:
\begin{equation}
\label{lambda-types}
\begin{array}{rrlll}
\tau & ::= & A                 & (A\in\BT)      & \mbox{basic type} \\
     &   | & \alpha            & (\alpha\in\VT) & \mbox{variable type} \\
     &   | & \arr{\tau}{\tau}  &                & \mbox{function type}
\end{array}
\end{equation}
We shall call $\TT$ the set of types $\tau$ defined by this grammar.
A \emph{monomorphic type} is a type that contains no variable types.
Any type containing at least one variable type is called a
\emph{polymorphic type}.

The terms of the Typed Polymorphic $\lambda$-Calculus are only those
raw terms in $\T$ that admit a well-defined type in $\TT$. Each
constant in $\C$ is assumed to have a unique type in $\TT$, and we
write $\type(a)=\tau$ to mean that constant $a$ has type $\tau$.

One may assign types to symbols using a \emph{type context}
$\Gamma$, which is a partial function from $V$ to $\TT$.  Given a
type context $\Gamma$, a variable $x\in\V$ and a type $\tau\in\TT$,
we define:
\begin{equation}
\label{type-extension}
\Gamma[x:\tau](y) \eqd \left\{
\begin{array}{ll}
\tau      & \mbox{if $x = y$}; \\ \\
\Gamma(y) & \mbox{if $x\neq y$}.
\end{array}\right.
\end{equation}
In other words, $\Gamma[x:\tau]$ coincides with $\Gamma$ everywhere
on $\V$ except at $x$, where it takes the value $\tau$. The
\emph{empty context} is the function noted $\empty$ defined
nowhere on $\V$.

To find out whether a term $t$ in $\T$ is well-typed, one must
exhibit a type assignment that constitutes a suitable typing context
for the variable symbols occurring in $t$, and from which one may
ascribe a (unique) type for the whole term.  Given a type context
$\Gamma$, a term $t$, and a type $\tau$, a \emph{type judgement} is
an expression of the form $\sequent{\Gamma}{t}{\tau}$, which stands
to mean that $t$ has been deemed to have type $\tau$ when the
symbols occurring in it have the types assigned to them by the
context $\Gamma$. Without a type context $\Gamma$, the expression
$t:\tau$ is used to mean that $\sequent{\Gamma}{t}{\tau}$ for some
$\Gamma$.

Deriving types for terms is done using \emph{typing rules} of the
form:
\[
\typerule%
{\sequent{\Gamma_1}{t_1}{\tau_n},\  \cdots\  \sequent{\Gamma_n}{t_n}{\tau_n}}
{\sequent{\Gamma}{t}{\tau}}
\]
which is read as follows: ``$t$ has type $\tau$ under $\Gamma$ if
$t_1$ has type $\tau_1$ under $\Gamma_1$, \ldots, and $t_n$ has type
$\tau_n$ under $\Gamma_n$.'' Note that it is possible that $n=0$, in
which case the rule is written:
\[
\typerule{}
{\sequent{\Gamma}{t}{\tau}}
\]
and it is called an \emph{axiom}.

The typing rules for the Typed Polymorphic $\lambda$-Calculus are
given in Figure~\ref{tplc-rules}.
\begin{figure}
\begin{center}
\fbox{\begin{tabular}{rl}

$\typerule{}{\sequent{\Gamma}{a}{\tau}}$
& for any $\Gamma$, if $\type(a)=\tau$ \\ \\

$\typerule{}{\sequent{\Gamma}{x}{\tau}}$
& if $\Gamma(x)=\tau$ \\ \\

$\typerule{\sequent{\Gamma[x:\tau_1]}{t}{\tau_2}}
{\sequent{\Gamma}{\abs{x}{t}}{\arr{\tau_1}{\tau_2}}}$
& \\ \\

$\typerule{\sequent{\Gamma}{t_1}{\arr{\tau_1}{\tau_2}}, \ \sequent{\Gamma}{t_2}{\tau_1}}
{\sequent{\Gamma}{\app{t_1}{t_2}}{\tau_2}}
$ &
\end{tabular}}
\end{center}
\caption{Typing rules for the Typed Polymorphic $\lambda$-Calculus}
\label{tplc-rules}
\end{figure}
These rules can be readily translated into a Logic Programming
language based on Horn-clauses such as Prolog, and used as an
effective means to infer the types of expressions based on the Typed
Polymorphic $\lambda$-Calculus.

The basic syntax of the Typed Polymorphic $\lambda$-Calculus may be
extended with other operators and convenient data structures as long
as typing rules for the new constructs are provided.  Typically, one
provides at least the set $\NN$ of integer constants and
$\BB=\{\true,\false\}$ of boolean constants, along with basic
arithmetic and boolean operators, pairing (or tupling), a
conditional operator, and a fix-point operator. The usual arithmetic
and boolean operators are denoted by constant symbols (\eg, $+, *,
-, /, \vee, \wedge,$ \etc). Let $\OP$ be this set.

The computation rules for these operators are based on their usual
semantics as one might expect, modulo transforming the usual binary
infix notation to a ``curryed'' application. For example, $t_1+t_2$
is implicitly taken to be the \emph{application}
$\app{(\app{+}{t_1})}{t_2}$. Note that this means that all such
operators are implicitly ``curryed.''\footnote{Recall that a curryed
form of an $n$-ary function $f$ is obtained when $f$ is applied to
less arguments than it expects; \ie, $f(t_1,\ldots,t_{k})$, for
$1\leq k < n$. In the $\lambda$-calculus, this form is simply
interpreted as the \emph{abstraction}
$\abs{x_1}{\ldots\abs{x_{n-k}}{f(t_1,\ldots,t_{k},x_1,\ldots,x_{n-k})}}$.
In their fully curried form, all $n$-ary functions can be seen as
unary functions; indeed, with this interpretation of curried forms,
it is clear that $f(t_1,\ldots,t_n) = \app{(\ldots(\app{f}{t_1})
\ldots t_{n-1})}{t_n}$.}

For example, we may augment the grammar for the terms given
in~(\ref{lambda-terms}) as follows:
\begin{equation}
\label{extended-lambda-terms}
\begin{array}{rrlll}
t & ::= & a          & (a\in\C=\NN\cup\BB\cup\OP) & \mbox{constant} \\
  &   | & x          & (x\in\V)                   & \mbox{symbol} \\
  &   | & \abs{x}{t} & (x\in\V)                   & \mbox{abstraction} \\
  &   | & \app{t}{t} &                            & \mbox{application} \\
  &   | & \tp{t}{t}  &                            & \mbox{tupling} \\
  &   | & \pj{t}{n}  & (n\in\NN)                  & \mbox{projection} \\
  &   | & \ite{t}{t}{t} &                         & \mbox{conditional} \\
  &   | & \app{\fix}{t} &                         & \mbox{recursion}
\end{array}
\end{equation}

The computation rules for the other new constructs are:
\begin{equation}
\label{extended-reductions}
\begin{array}{rl}
\pj{\tp{t_1}{t_k}}{i} & \gives \left\{
   \begin{array}{ll}
   t_i & \mbox{if $1\leq i\leq k$} \\ \\
   \mbox{undefined otherwise}
   \end{array}\right. \\ \\
\ite{c}{t_1}{t_2} & \gives \left\{
   \begin{array}{ll}
   t_1 & \mbox{if $c=\true$} \\ \\
   t_2 & \mbox{if $c=\false$} \\ \\
   \mbox{undefined otherwise}
   \end{array}\right. \\ \\
\app{\fix}{t} & \gives \app{t}{(\app{\fix}{t})}
\end{array}
\end{equation}

To account for the new constructs, the syntax of types is extended
accordingly to: 
\begin{equation}
\label{extended-lambda-types}
\begin{array}{rrlll}
\tau & ::= & \integer \;|\; \bool &                & \mbox{basic type} \\
     &   | & \alpha               & (\alpha\in\VT) & \mbox{variable type} \\
     &   | & \tp{\tau}{\tau}      &                & \mbox{tuple type} \\
     &   | & \arr{\tau}{\tau}     &                & \mbox{function type}
\end{array}
\end{equation}

We are given that $\type(n)=\integer$ for all $n\in\NN$ and that
$\type(\true)=\bool$ and $\type(\false)=\bool$. The (fully curried)
types of the built-in operators are given similarly; \ie,
$\type(+)=\arr{\integer}{(\arr{\integer}{\integer})}$,
$\type(\vee)=\arr{\bool}{(\arr{\bool}{\bool})}$, \etc, \ldots The
typing rules for this extended calculus are given in
Figure~\ref{extended-tplc-rules}.
\begin{figure}
\begin{center}
\fbox{\begin{tabular}{rl}

$\typerule{}{\sequent{\Gamma}{a}{\tau}}$
& for any $\Gamma$, if $\type(a)=\tau$ \\ \\

$\typerule{}{\sequent{\Gamma}{x}{\tau}}$
& if $\Gamma(x)=\tau$ \\ \\

$\typerule{\sequent{\Gamma[x:\tau_1]}{t}{\tau_2}}
{\sequent{\Gamma}{\abs{x}{t}}{\arr{\tau_1}{\tau_2}}}$
& \\ \\

$\typerule{\sequent{\Gamma}{t_1}{\arr{\tau_1}{\tau_2}},
\          \sequent{\Gamma}{t_2}{\tau_1}}
{\sequent{\Gamma}{\app{t_1}{t_2}}{\tau_2}}$
& \\ \\

$\typerule{\sequent{\Gamma}{t_1}{\tau_1},
\          \cdots,
\          \sequent{\Gamma}{t_k}{\tau_k}}
{\sequent{\Gamma}{\tp{t_1}{t_k}}{\tp{\tau_1}}{\tau_k}}$
& \\ \\

$\typerule{\sequent{\Gamma}{t}{\tp{\tau_1}}{\tau_k}}
{\sequent{\Gamma}{\pj{t}{n}}{\tau}}$ 
& if $1\leq n\leq k$ \\ \\

$\typerule{\sequent{\Gamma}{t_1}{\bool},
\          \sequent{\Gamma}{t_2}{\tau},
\          \sequent{\Gamma}{t_3}{\tau}}
{\sequent{\Gamma}{\ite{t_1}{t_2}{t_3}}{\tau}}$
& \\ \\

$\typerule{\sequent{\Gamma}{t}{\arr{\tau}{\tau}}}
{\sequent{\Gamma}{\app{\fix}{t}}{\tau}}$
& 

\end{tabular}}
\end{center}
\caption{Typing rules for an Extended Typed Polymorphic $\lambda$-Calculus}
\label{extended-tplc-rules}
\end{figure}

\section{A Transportation Model in \opl}
\label{transpmod}

{\small\begin{verbatim}
[01]    enum City ...;
[02]    enum Product ...;
[03]    float+ limit = ...;
[04]    
[05]    struct TableRoutesType
[06]       { Product p;
[07]         City o;
[08]         City d;
[09]         float+ cost;
[10]       };
[11]    
[12]    {TableRoutesType} TableRoutes = ...;
[13]    
[14]    struct Connection
[15]       { City o;
[16]         City d;
[17]       };
[18]    
[19]    struct Route
[20]       { Product p;
[21]         Connection e;
[22]       };
[23]    
[24]    {Route} Routes = { < p,<o,d> > | <p,o,d,c> in TableRoutes };
[25]    
[26]    {Connection} Connections = { c | <p,c> in Routes };
[27]    
[28]    struct Supply
[29]       { Product p;
[30]         City o;
[31]       };
[32]    
[33]    {Supply} Supplies = { <p,c.o> | <p,c> in Routes };
[34]    
[35]    float+ supply[Supplies] = ...;
[36]    
[37]    struct Customer
[38]       { Product p;
[39]         City d;
[40]       };
[41]    
[42]    {Customer} Customers = { <p,c.d> | <p,c> in Routes };
[43]    
[44]    float+ demand[Customers] = ...;
[45]    
[46]    float+ cost[Routes];
[47]    
[48]    initialize
[49]       { forall( <p,o,d,c> in TableRoutes)
[50]            cost[< p,<o,d> >] = c;
[51]       };
[52]    
[53]    {City} orig[p in Product] = { c.o | <p,c> in Routes };
[54]    {City} dest[p in Product] = { c.d | <p,c> in Routes };
[55]    
[56]    {Connection} CP[p in Product] = { c | <p,c> in Routes };
[57]    
[58]    assert
[59]       forall(p in Product) 
[60]         sum(o in orig[p]) supply[<p,o>] = sum(d in dest[p]) demand[<p,d>];
[61]    
[62]    var float+ trans[Routes];   
[63]    
[64]    minimize
[65]       sum(l in Routes) cost[l] * trans[l]
[66]    subject to
[67]       {
[68]         forall(p in Product, o in orig[p]) 
[69]            sum(<o,d> in CP[p]) trans[< p,<o,d> >] <= supply[<p,o>];
[70]    
[71]         forall(p in Product, d in dest[p]) 
[72]            sum(<o,d> in CP[p]) trans[< p,<o,d> >] >= demand[<p,d>];
[73]    
[74]         forall(c in Connections)
[75]            sum(<p,c> in Routes) trans[<p,c>] <= limit;
[77]       };
\end{verbatim}}


\bibliographystyle{plain}
\bibliography{main}

\end{document}
