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

Last change on this file since 2427 was 2427, checked in by mulligan, 8 years ago

More work on explanation.

File size: 13.1 KB
Line 
1\documentclass[smallextended]{svjour3}
2
3\smartqed
4
5\usepackage{amsmath}
6\usepackage[english]{babel}
7\usepackage[colorlinks]{hyperref}
8\usepackage{listings}
9\usepackage{microtype}
10\usepackage{prooftree}
11
12\newcommand{\cons}{{::}}
13\newcommand{\ent}{\vdash}
14\newcommand{\fall}[2]{\forall{#1}.#2}
15\newcommand{\funarr}{\rightarrow}
16\newcommand{\lam}[2]{\lambda{#1}.{#2}}
17\newcommand{\letin}[3]{\mathbf{let}\ {#1}\ {:=}\ {#2}\ \mathbf{in}\ {#3}}
18\newcommand{\match}[3]{\mathbf{match}\ #1\ \mathbf{with}\ #2\ \Rightarrow #3}
19\newcommand{\pair}[2]{\langle #1, #2 \rangle}
20\newcommand{\polytag}[1]{{`}#1}
21\newcommand{\rulefont}[1]{\ensuremath{(\mathbf{#1})}}
22
23\lstset{basicstyle=\footnotesize\tt,columns=flexible,breaklines=false,
24        keywordstyle=\color{red}\bfseries,
25        keywordstyle=[2]\color{blue},
26        commentstyle=\color{green},
27        stringstyle=\color{blue},
28        showspaces=false,showstringspaces=false,
29        xleftmargin=1em}
30
31\bibliographystyle{spphys}
32
33\author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
34\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.}}
35
36\institute{
37  Dominic P. Mulligan \at
38  Computer Laboratory,\\
39  University of Cambridge.
40  \email{dominic.p.mulligan@gmail.com} \and
41  Claudio Sacerdoti Coen \at
42  Dipartimento di Scienze dell'Informazione,\\
43  Universit\`a di Bologna.
44  \email{sacerdot@cs.unibo.it}
45}
46
47\begin{document}
48
49\maketitle
50
51\begin{abstract}
52
53Big long abstract introducing the work
54
55\keywords{Polymorphic variants \and dependent type theory \and Matita theorem prover}
56
57\end{abstract}
58
59%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
60% Section
61%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
62\section{Introduction}
63\label{sect.introduction}
64
65%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
66% Section
67%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
68\section{Polymorphic variants}
69\label{sect.polymorphic.variants}
70
71In this section we will attempt to provide a self-contained \emph{pr\'ecis} of polymorphic variants for the unfamiliar reader.
72Those 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}.
73
74Most 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.
75Each algebraic data type may be described as a sum-of-products.
76The programmer provides a fixed number of distinct \emph{constructors} with each constructor expects a (potentially empty) product of arguments.
77Values of a given inductive data type are built using a data type's constructors.
78Quotidian data structures---such as lists, trees, heaps, zippers, and so forth---can all be introduced using this now familiar mechanism.
79
80Having 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.
81Functional languages almost uniformly employ \emph{pattern matching} for this task.
82Given 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.
83Using pattern matching we can therefore deconstruct algebraic data by performing a case analysis on the constructors of a given type.
84
85The combination of algebraic data types and pattern matching is powerful, and is arguably the main branching mechanism for most functional programming languages.
86Furthermore, 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.
87
88Unfortunately, in practical programming, we often want to expand a previously defined algebraic data type, adding more constructors.
89When it comes to extending algebraic data types with new constructors in this way, we hit a problem: these types are `closed'.
90In 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.
91This manual extension, coupled with the lifting of any existing functions into the new type, is cumbersome and error-prone.
92
93\begin{figure}[ht]
94\begin{minipage}[b]{0.45\linewidth}
95\begin{lstlisting}
96data Term
97  = Lit Int
98  | Add Term Term
99
100eval :: Term -> Int
101eval (Lit i)   = i
102eval (Add l r) = eval l + eval r
103\end{lstlisting}
104\end{minipage}
105\hspace{0.5cm}
106\begin{minipage}[b]{0.45\linewidth}
107\begin{lstlisting}
108interface Term {
109  int eval();
110}
111
112class Lit implements Term {
113  private int v = 0;
114  ...
115  int eval() { return v; }
116}
117
118class Add implements Term {
119  private Term left, right = null;
120  ...
121  int eval() {
122    return left.eval() + right.eval();
123  }
124}
125\end{lstlisting}
126\end{minipage}
127\label{fig.pattern-matching.vs.oop}
128\caption{A simple language of integer arithmetic embedded as an algebraic data type and as a class hierarchy.}
129\end{figure}
130
131However, we can look abroad to see what other families of programming languages do to solve this problem.
132For instance, we 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).
133In mainstream, class-based object-oriented languages---such as Java, for example---algebraic data types can be emulated by interfaces, coupled with a number of subclasses corresponding to constructors, implementing the `root' interface.
134The base interface of the object hierarchy specifies the permitted operations defined for the type.
135Branching by pattern matching is emulated using the language's dynamic dispatch mechanism.
136
137As all permitted operations on
138it is hard to enlarge the set of operations defined over a given type without altering the entire class hierarchy.
139If the interface changes so must every class implementing it.
140However, 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.
141
142\begin{figure}[ht]
143\begin{minipage}[b]{0.45\linewidth}
144\begin{lstlisting}
145...
146data Term'
147  = Lift Term
148  | Mul Term' Term'
149
150eval' :: Term' -> Int
151eval' (Lift t)  = eval t
152eval' (Mul l r) = eval' l * eval ' r
153\end{lstlisting}
154\end{minipage}
155\hspace{0.5cm}
156\begin{minipage}[b]{0.45\linewidth}
157\begin{lstlisting}
158...
159class Mul implements Term {
160  private Term left, right = null;
161  ...
162  int eval() {
163    return left.eval() * right.eval();
164  }
165}
166\end{lstlisting}
167\end{minipage}
168\label{fig.extending.base.type}
169\caption{Extending our simple language of arithmetic with a new grammatical element.}
170\end{figure}
171
172\begin{figure}[ht]
173\begin{minipage}[b]{0.45\linewidth}
174\begin{lstlisting}
175...
176show :: Term -> String
177show (Lit i)   = show i
178show (Add l r) =
179  show l ++ " + " ++ show r
180\end{lstlisting}
181\end{minipage}
182\hspace{0.5cm}
183\begin{minipage}[b]{0.45\linewidth}
184\begin{lstlisting}
185interface Term {
186  int eval();
187  String show();
188}
189
190class Lit implements Term {
191  private int v = 0;
192  ...
193  int eval() { return v; }
194  String show() {
195    return Int.toString(v);
196  }
197}
198
199class Add implements Term {
200  private Term left, right = null;
201  ...
202  int eval() {
203    return left.eval() + right.eval();
204  }
205  ...
206  String show() {
207    return left.show() + \
208      " + " + right.show();
209  }
210}
211\end{lstlisting}
212\end{minipage}
213\label{fig.extending.base.type}
214\caption{Extending the permitted operations over our simple language of arithmetic.}
215\end{figure}
216
217[dpm: reword the above --- hard to phrase precisely ]
218
219
220\begin{itemize}
221 \item General introduction, motivations
222 \item Bounded vs not-bounded.
223\end{itemize}
224
225\begin{definition}
226\label{defn.garrigues.calculus}
227Inductively define a
228\end{definition}
229
230\begin{figure}
231\begin{gather*}
232\begin{prooftree}
233(\Gamma(x) = \sigma)
234\justifies
235K; \Gamma \ent x : \sigma
236\using\rulefont{{\Gamma}x}
237\end{prooftree}
238\qquad
239\begin{prooftree}
240K; \Gamma, x : \phi \ent r : \psi
241\justifies
242K; \Gamma \ent \lam{x}r : \phi \funarr \psi
243\using\rulefont{{\Gamma}\lambda}
244\end{prooftree}
245\qquad
246\begin{prooftree}
247K;\Gamma \ent r : \phi \funarr \psi \quad K;\Gamma \ent s : \phi
248\justifies
249K;\Gamma \ent rs : \psi
250\using\rulefont{{\Gamma}rs}
251\end{prooftree}
252\\[1.5ex]
253\begin{prooftree}
254K; \Gamma \ent r : \sigma \quad K; \Gamma, x:\sigma \ent s : \psi
255\justifies
256K; \Gamma \ent \letin{x}{r}{s} : \psi
257\using\rulefont{{\Gamma}{:=}}
258\end{prooftree}
259\qquad
260\begin{prooftree}
261K;\Gamma \ent r : \sigma \quad (a \not\in ftv(\Gamma))
262\justifies
263K;\Gamma \ent r : \fall{a}{\sigma}
264\using\rulefont{{\Gamma}{\forall}{a}}
265\end{prooftree}
266\\[1.5ex]
267\begin{prooftree}
268K;\Gamma \ent r : \fall{a}{\sigma} \quad K;\Gamma \ent s : \psi
269\justifies
270K;\Gamma \ent rs : \sigma[a := \psi]
271\using\rulefont{{\Gamma}inst{a}}
272\end{prooftree}
273\\[1.5ex]
274\begin{prooftree}
275(L \subseteq L' \quad H \subseteq H')
276\justifies
277K \oplus i_{{\geq \pair{L}{U}}} \ent i \geq \pair{L'}{H'}
278\using\rulefont{{K}i}
279\end{prooftree}
280\qquad
281\begin{prooftree}
282K;\Gamma \ent r : \phi \quad K \ent i \geq \pair{tag}{\top}
283\justifies
284K;\Gamma \ent \polytag{tag(r)} : [ i \mid tag : \phi \cons T ]
285\using\rulefont{{K}variant}
286\end{prooftree}
287\\[1.5ex]
288\begin{prooftree}
289K;\Gamma \ent r : [ i \mid \{ tag_k : \phi_k \}^n_1 \cons T ] \quad K \ent i \geq \pair{\bot}{\{tag_k\}^n_1} \quad
290K;\Gamma, x_k : \phi_k \ent r_k : \psi \quad (1 \leq k \leq n)
291\justifies
292K;\Gamma \ent \mathbf{match}\ r\ \mathbf{with}\ \{ \polytag{tag_k(x_k)} \Rightarrow r_k \}^n_1 : \psi
293\using\rulefont{{K}match}
294\end{prooftree}
295\\[1.5ex]
296\begin{prooftree}
297K;\Gamma \ent r : \sigma \quad (\rho \not\in ftv(\Gamma))
298\justifies
299K;\Gamma \ent r : \fall{\rho}{\sigma}
300\using\rulefont{{K}{\forall}{\rho}}
301\end{prooftree}
302\qquad
303\begin{prooftree}
304K;\Gamma \ent r : \fall{\rho}{\sigma} \quad K;\Gamma \ent s : T
305\justifies
306K;\Gamma \ent rs : \sigma[\rho := T]
307\using\rulefont{{K}inst{\rho}}
308\end{prooftree}
309\\[1.5ex]
310\begin{prooftree}
311K \oplus i_{\geq \pair{L}{U}};\Gamma \ent r : \sigma
312\justifies
313K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma}
314\using\rulefont{{K}{\forall}{i}}
315\end{prooftree}
316\qquad
317\begin{prooftree}
318K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma} \quad K \ent i' \geq \pair{L, U}
319\justifies
320K;\Gamma \ent r : \sigma[i := i']
321\using\rulefont{{K}inst{i}}
322\end{prooftree}
323\end{gather*}
324\caption{Garrigue's typing relation for polymorphic variants}
325\label{fig.garrigue.typing.relation}
326\end{figure}
327
328%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
329% Section
330%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
331\subsection{Matita}
332\label{subsect.matita}
333
334Matita~\cite{asperti:user:2007} is a dependently-typed proof assistant developed in Bologna, implementing the Calculus of (Co)inductive Constructions, a type theory similar to that of Coq.
335Throughout this paper, all running examples are provided in Matita's proof script vernacular.
336This vernacular, similar to the syntax of OCaml or Coq, should be mostly straightforward.
337
338One possible source of confusion is our use of $?$ and $\ldots$, which correspond to a term, or terms, to be inferred automatically by unification, respectively.
339Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations.
340
341Matita
342
343\subsection{Subtyping as instantiation vs subtyping as safe static cast}
344
345\subsection{Syntax \& type checking rules}
346The ones of Guarrigue + casts, but also for the bounded case?
347Casts support both styles of subtyping.
348
349\subsection{Examples}
350The weird function types that only work in subtyping as instantiation
351
352\subsection{Solution to the expression problem}
353Our running example in pseudo-OCaml syntax
354
355\section{Bounded polymorphic variants via dependent types}
356Requirements (i.e. O(1) pattern-matching, natural extracted code, etc.)
357\subsection{Simulation (reduction + type checking)}
358\subsection{Examples}
359The weird function types redone
360\subsection{Subtyping as instantiation vs subtyping as safe static cast}
361Here we show/discuss how our approach supports both styles at once.
362\subsection{Solution to the expression problem, I}
363Using subtyping as cast, the file I have produced
364\subsection{Solution to the expression problem, II}
365Using subtyping as instantiation, comparisons, pros vs cons
366\subsection{Negative encoding (??)}
367The negative encoding and application to the expression problem
368\subsection{Other encodings (??)}
369Hints to other possible encodings
370
371\section{Extensible records (??)}
372
373\section{Comparison to related work and alternatives}
374\begin{itemize}
375 \item Disjoint unions: drawbacks
376 \item Encoding the unbounded case: drawbacks
377\end{itemize}
378
379\section{Appendix: interface of library functions used to implement everything}
380
381\bibliography{polymorphic-variants}
382
383\end{document}
Note: See TracBrowser for help on using the repository browser.