source: Papers/polymorphic-variants-2012/polymorphic-variants.tex @ 2409

\documentclass[smallextended]{svjour3}

\smartqed

\usepackage[english]{babel}
\usepackage[colorlinks]{hyperref}
\usepackage{microtype}


\author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
\title{Polymorphic variants in dependent type theory\thanks{The project CerCo acknowledges the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number: 243881.}}

\institute{
  Dominic P. Mulligan \at
  Computer Laboratory,\\
  University of Cambridge.
  \email{dominic.p.mulligan@gmail.com} \and
  Claudio Sacerdoti Coen \at
  Dipartimento di Scienze dell'Informazione,\\
  Universit\`a di Bologna.
  \email{sacerdot@cs.unibo.it}
}

\begin{document}

\maketitle

\begin{abstract}

Big long abstract introducing the work

\keywords{Polymorphic variants \and dependent type theory \and Matita theorem prover}

\end{abstract}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Section
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
\label{sect.introduction}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Section
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Polymorphic variants}
\label{sect.polymorphic.variants}

In this section we provide a self-contained \emph{pr\'ecis} of polymorphic variants.
For a more complete summary, we refer the reader to Garrigue's publications on the subject~\cite{dpm: todo}.

Most mainstream functional programming languages, such as OCaml and Haskell, have mechanisms for inductively defining types through the use of \emph{algebraic data types}.
Each algebraic data type can be described as a sum-of-products, wherein we associate a fixed number of distinct \emph{constructors} to the type being introduced, all of whom expect a product of arguments.
Inductive data, modelled as an algebraic data type, is built incrementally from the ground-up using the constructors of that type.
Quotidian data structures---such as lists, trees, heaps, zippers, and so forth---can all be introduced using this now familiar mechanism.

Having built data using constructors, to complete the picture we now need some facility for picking said data apart.
Functional languages employ \emph{pattern matching} for this task.
Given any inhabitant of an inductive type, by the aforementioned sum-of-products property, we know that it must consist of some constructor of that type applied to various arguments.
Using pattern matching we can therefore deconstruct algebraic data by performing a case analysis on the constructors of a given type.

The combination of algebraic data types and pattern matching is powerful, and is arguably the main branching mechanism for most functional programming languages.
Further, using pattern matching it is easy to define new functions that consume algebraic data---the set of operations that can be defined for any given algebraic type is unbounded.
Unfortunately, when it comes to extending algebraic data types with new constructors these types are essentially `closed'.
We cannot simply extend an algebraic type with a new constructor.
We must introduce a new algebraic type with the additional constructor, lifting the old type---and any functions defined over it---into this type.

Moving sideways, we can compare and contrast functional programming languages' use of algebraic data paired with pattern matching with the approach taken by object-oriented languages.
In mainstream object-oriented languages such as Java algebraic data types correspond to class hierarchies, each constructor corresponding to a subclass in this hierarchy.
Pattern matching is emulated using a dynamic dispatch mechanism.
Using the object-oriented approach it is easy to add a new `case' to a given hierarchy: just introduce a new subclass.

[dpm: reword the above --- hard to phrase precisely ]


\begin{itemize}
 \item General introduction, motivations
 \item Bounded vs not-bounded.
\end{itemize}

\subsection{Subtyping as instantiation vs subtyping as safe static cast}

\subsection{Syntax \& type checking rules}
The ones of Guarrigue + casts, but also for the bounded case?
Casts support both styles of subtyping.

\subsection{Examples}
The weird function types that only work in subtyping as instantiation

\subsection{Solution to the expression problem}
Our running example in pseudo-OCaml syntax

\section{Bounded polymorphic variants via dependent types}
Requirements (i.e. O(1) pattern-matching, natural extracted code, etc.)
\subsection{Simulation (reduction + type checking)}
\subsection{Examples}
The weird function types redone
\subsection{Subtyping as instantiation vs subtyping as safe static cast}
Here we show/discuss how our approach supports both styles at once.
\subsection{Solution to the expression problem, I}
Using subtyping as cast, the file I have produced
\subsection{Solution to the expression problem, II}
Using subtyping as instantiation, comparisons, pros vs cons
\subsection{Negative encoding (??)}
The negative encoding and application to the expression problem
\subsection{Other encodings (??)}
Hints to other possible encodings

\section{Extensible records (??)}

\section{Comparison to related work and alternatives}
\begin{itemize}
 \item Disjoint unions: drawbacks
 \item Encoding the unbounded case: drawbacks
\end{itemize}

\section{Appendix: interface of library functions used to implement everything}

\end{document}