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

Last change on this file since 2414 was 2414, checked in by mulligan, 7 years ago

Added bib file, done a little bit of rearrangement.

File size: 7.4 KB
Line 
1\documentclass[smallextended]{svjour3}
2
3\smartqed
4
5\usepackage[english]{babel}
6\usepackage[colorlinks]{hyperref}
7\usepackage{listings}
8\usepackage{microtype}
9
10\lstset{basicstyle=\footnotesize\tt,columns=flexible,breaklines=false,
11        keywordstyle=\color{red}\bfseries,
12        keywordstyle=[2]\color{blue},
13        commentstyle=\color{green},
14        stringstyle=\color{blue},
15        showspaces=false,showstringspaces=false,
16        xleftmargin=1em}
17
18\bibliographystyle{spphys}
19
20\author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
21\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.}}
22
23\institute{
24  Dominic P. Mulligan \at
25  Computer Laboratory,\\
26  University of Cambridge.
27  \email{dominic.p.mulligan@gmail.com} \and
28  Claudio Sacerdoti Coen \at
29  Dipartimento di Scienze dell'Informazione,\\
30  Universit\`a di Bologna.
31  \email{sacerdot@cs.unibo.it}
32}
33
34\begin{document}
35
36\maketitle
37
38\begin{abstract}
39
40Big long abstract introducing the work
41
42\keywords{Polymorphic variants \and dependent type theory \and Matita theorem prover}
43
44\end{abstract}
45
46%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
47% Section
48%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
49\section{Introduction}
50\label{sect.introduction}
51
52%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
53% Section
54%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
55\section{Polymorphic variants}
56\label{sect.polymorphic.variants}
57
58In this section we will attempt to provide a self-contained \emph{pr\'ecis} of polymorphic variants for the unfamiliar reader.
59Those readers who wish to survey a more complete introduction to the subject are referred to Garrigue's original publications on the subject matter~\cite{garrigue:programming:1998,garrigue:code:2000}.
60
61Most mainstream functional programming languages, such as OCaml and Haskell, have mechanisms for defining new inductive types from old through the use of algebraic data type definitions.
62Each algebraic data type may be described as a sum-of-products.
63The programmer provides a fixed number of distinct \emph{constructors} with each constructor expects a (potentially empty) product of arguments.
64Values of a given inductive data type are built using a data type's constructors.
65Quotidian data structures---such as lists, trees, heaps, zippers, and so forth---can all be introduced using this now familiar mechanism.
66
67Having built data from various combinations of constructors, to complete the picture we now need some facility for picking said data apart, in order to build functions that operate over that data.
68Functional languages almost uniformly employ \emph{pattern matching} for this task.
69Given any inhabitant of an algebraic data type, by the aforementioned sum-of-products property, we know that it must consist of some constructor applied to various arguments.
70Using pattern matching we can therefore deconstruct algebraic data by performing a case analysis on the constructors of a given type.
71
72The combination of algebraic data types and pattern matching is powerful, and is arguably the main branching mechanism for most functional programming languages.
73Furthermore, 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 practically without bound.
74
75Unfortunately, in practical programming, we often want to expand a previously defined algebraic data type, adding more constructors.
76When it comes to extending algebraic data types with new constructors in this way, we hit a problem: these types are `closed'.
77In order to circumvent this restriction, we must introduce a new algebraic type with the additional constructor, lifting the old type---and any functions defined over it---into this type.
78
79\begin{figure}[ht]
80\begin{minipage}[b]{0.45\linewidth}
81\begin{lstlisting}
82data Term
83  = Lit Int
84  | Add Term Term
85  | Mul Term Term
86
87evaluate :: Term -> Int
88evaluate (Lit i)   = i
89evaluate (Add l r) = evaluate l + evaluate r
90evaluate (Mul l r) = evaluate l * evaluate r
91\end{lstlisting}
92\end{minipage}
93\hspace{0.5cm}
94\begin{minipage}[b]{0.45\linewidth}
95\begin{lstlisting}
96\end{lstlisting}
97\end{minipage}
98\label{fig.pattern-matching.vs.oop}
99\caption{A simple language of integer arithmetic embedded as an algebraic data type and as a class hierarchy.}
100\end{figure}
101
102We can compare and contrast functional programming languages' use of algebraic data and pattern matching with the approach taken by object-oriented languages (see Figure~\ref{fig.pattern-matching.vs.oop} for a concrete example).
103In mainstream object-oriented languages such as Java algebraic data types correspond to interfaces, or some base object.
104Constructors correspond to classes implementing this interface; branching by pattern matching is emulated using the language's dynamic dispatch mechanism.
105The base interface of the object hierarchy specifies the permitted operations defined for the type.
106
107As all operations
108it is hard to enlarge the set of operations defined over a given type without altering the entire class hierarchy.
109If the interface changes so must every class implementing it.
110However, note it is easy to extend the hierarchy to new cases, corresponding to the introduction of a new constructor in the functional world, by merely adding another class corresponding to that constructor implementing the interface.
111
112[dpm: reword the above --- hard to phrase precisely ]
113
114
115\begin{itemize}
116 \item General introduction, motivations
117 \item Bounded vs not-bounded.
118\end{itemize}
119
120%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
121% Section
122%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
123\subsection{Matita}
124\label{subsect.matita}
125
126\subsection{Subtyping as instantiation vs subtyping as safe static cast}
127
128\subsection{Syntax \& type checking rules}
129The ones of Guarrigue + casts, but also for the bounded case?
130Casts support both styles of subtyping.
131
132\subsection{Examples}
133The weird function types that only work in subtyping as instantiation
134
135\subsection{Solution to the expression problem}
136Our running example in pseudo-OCaml syntax
137
138\section{Bounded polymorphic variants via dependent types}
139Requirements (i.e. O(1) pattern-matching, natural extracted code, etc.)
140\subsection{Simulation (reduction + type checking)}
141\subsection{Examples}
142The weird function types redone
143\subsection{Subtyping as instantiation vs subtyping as safe static cast}
144Here we show/discuss how our approach supports both styles at once.
145\subsection{Solution to the expression problem, I}
146Using subtyping as cast, the file I have produced
147\subsection{Solution to the expression problem, II}
148Using subtyping as instantiation, comparisons, pros vs cons
149\subsection{Negative encoding (??)}
150The negative encoding and application to the expression problem
151\subsection{Other encodings (??)}
152Hints to other possible encodings
153
154\section{Extensible records (??)}
155
156\section{Comparison to related work and alternatives}
157\begin{itemize}
158 \item Disjoint unions: drawbacks
159 \item Encoding the unbounded case: drawbacks
160\end{itemize}
161
162\section{Appendix: interface of library functions used to implement everything}
163
164\bibliography{polymorphic-variants}
165
166\end{document}
Note: See TracBrowser for help on using the repository browser.