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

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

Garrigue's stuff completely added to the paper. Need to explain the typing relation properly.

File size: 11.2 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.
91
92\begin{figure}[ht]
93\begin{minipage}[b]{0.45\linewidth}
94\begin{lstlisting}
95data Term
96  = Lit Int
97  | Add Term Term
98  | Mul Term Term
99
100evaluate :: Term -> Int
101evaluate (Lit i)   = i
102evaluate (Add l r) = evaluate l + evaluate r
103evaluate (Mul l r) = evaluate l * evaluate r
104\end{lstlisting}
105\end{minipage}
106\hspace{0.5cm}
107\begin{minipage}[b]{0.45\linewidth}
108\begin{lstlisting}
109
110\end{lstlisting}
111\end{minipage}
112\label{fig.pattern-matching.vs.oop}
113\caption{A simple language of integer arithmetic embedded as an algebraic data type and as a class hierarchy.}
114\end{figure}
115
116We 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).
117In mainstream object-oriented languages such as Java algebraic data types correspond to interfaces, or some base object.
118Constructors correspond to classes implementing this interface; branching by pattern matching is emulated using the language's dynamic dispatch mechanism.
119The base interface of the object hierarchy specifies the permitted operations defined for the type.
120
121As all operations
122it is hard to enlarge the set of operations defined over a given type without altering the entire class hierarchy.
123If the interface changes so must every class implementing it.
124However, 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.
125
126[dpm: reword the above --- hard to phrase precisely ]
127
128
129\begin{itemize}
130 \item General introduction, motivations
131 \item Bounded vs not-bounded.
132\end{itemize}
133
134\begin{figure}
135\begin{gather*}
136\begin{prooftree}
137(\Gamma(x) = \sigma)
138\justifies
139K; \Gamma \ent x : \sigma
140\using\rulefont{{\Gamma}x}
141\end{prooftree}
142\qquad
143\begin{prooftree}
144K; \Gamma, x : \phi \ent r : \psi
145\justifies
146K; \Gamma \ent \lam{x}r : \phi \funarr \psi
147\using\rulefont{{\Gamma}\lambda}
148\end{prooftree}
149\qquad
150\begin{prooftree}
151K;\Gamma \ent r : \phi \funarr \psi \quad K;\Gamma \ent s : \phi
152\justifies
153K;\Gamma \ent rs : \psi
154\using\rulefont{{\Gamma}rs}
155\end{prooftree}
156\\[1.5ex]
157\begin{prooftree}
158K; \Gamma \ent r : \sigma \quad K; \Gamma, x:\sigma \ent s : \psi
159\justifies
160K; \Gamma \ent \letin{x}{r}{s} : \psi
161\using\rulefont{{\Gamma}{:=}}
162\end{prooftree}
163\qquad
164\begin{prooftree}
165K;\Gamma \ent r : \sigma \quad (a \not\in ftv(\Gamma))
166\justifies
167K;\Gamma \ent r : \fall{a}{\sigma}
168\using\rulefont{{\Gamma}{\forall}{a}}
169\end{prooftree}
170\\[1.5ex]
171\begin{prooftree}
172K;\Gamma \ent r : \fall{a}{\sigma} \quad K;\Gamma \ent s : \psi
173\justifies
174K;\Gamma \ent rs : \sigma[a := \psi]
175\using\rulefont{{\Gamma}inst{a}}
176\end{prooftree}
177\\[1.5ex]
178\begin{prooftree}
179(L \subseteq L' \quad H \subseteq H')
180\justifies
181K \oplus i_{{\geq \pair{L}{U}}} \ent i \geq \pair{L'}{H'}
182\using\rulefont{{K}i}
183\end{prooftree}
184\qquad
185\begin{prooftree}
186K;\Gamma \ent r : \phi \quad K \ent i \geq \pair{tag}{\top}
187\justifies
188K;\Gamma \ent \polytag{tag(r)} : [ i \mid tag : \phi \cons T ]
189\using\rulefont{{K}variant}
190\end{prooftree}
191\\[1.5ex]
192\begin{prooftree}
193K;\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
194K;\Gamma, x_k : \phi_k \ent r_k : \psi \quad (1 \leq k \leq n)
195\justifies
196K;\Gamma \ent \mathbf{match}\ r\ \mathbf{with}\ \{ \polytag{tag_k(x_k)} \Rightarrow r_k \}^n_1 : \psi
197\using\rulefont{{K}match}
198\end{prooftree}
199\\[1.5ex]
200\begin{prooftree}
201K;\Gamma \ent r : \sigma \quad (\rho \not\in ftv(\Gamma))
202\justifies
203K;\Gamma \ent r : \fall{\rho}{\sigma}
204\using\rulefont{{K}{\forall}{\rho}}
205\end{prooftree}
206\qquad
207\begin{prooftree}
208K;\Gamma \ent r : \fall{\rho}{\sigma} \quad K;\Gamma \ent s : T
209\justifies
210K;\Gamma \ent rs : \sigma[\rho := T]
211\using\rulefont{{K}inst{\rho}}
212\end{prooftree}
213\\[1.5ex]
214\begin{prooftree}
215K \oplus i_{\geq \pair{L}{U}};\Gamma \ent r : \sigma
216\justifies
217K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma}
218\using\rulefont{{K}{\forall}{i}}
219\end{prooftree}
220\qquad
221\begin{prooftree}
222K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma} \quad K \ent i' \geq \pair{L, U}
223\justifies
224K;\Gamma \ent r : \sigma[i := i']
225\using\rulefont{{K}inst{i}}
226\end{prooftree}
227\end{gather*}
228\caption{Garrigue's typing relation for polymorphic variants}
229\label{fig.garrigue.typing.relation}
230\end{figure}
231
232%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
233% Section
234%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
235\subsection{Matita}
236\label{subsect.matita}
237
238Matita~\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.
239Throughout this paper, all running examples are provided in Matita's proof script vernacular.
240This vernacular, similar to the syntax of OCaml or Coq, should be mostly straightforward.
241
242One possible source of confusion is our use of $?$ and $\ldots$, which correspond to a term, or terms, to be inferred automatically by unification, respectively.
243Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations.
244
245Matita
246
247\subsection{Subtyping as instantiation vs subtyping as safe static cast}
248
249\subsection{Syntax \& type checking rules}
250The ones of Guarrigue + casts, but also for the bounded case?
251Casts support both styles of subtyping.
252
253\subsection{Examples}
254The weird function types that only work in subtyping as instantiation
255
256\subsection{Solution to the expression problem}
257Our running example in pseudo-OCaml syntax
258
259\section{Bounded polymorphic variants via dependent types}
260Requirements (i.e. O(1) pattern-matching, natural extracted code, etc.)
261\subsection{Simulation (reduction + type checking)}
262\subsection{Examples}
263The weird function types redone
264\subsection{Subtyping as instantiation vs subtyping as safe static cast}
265Here we show/discuss how our approach supports both styles at once.
266\subsection{Solution to the expression problem, I}
267Using subtyping as cast, the file I have produced
268\subsection{Solution to the expression problem, II}
269Using subtyping as instantiation, comparisons, pros vs cons
270\subsection{Negative encoding (??)}
271The negative encoding and application to the expression problem
272\subsection{Other encodings (??)}
273Hints to other possible encodings
274
275\section{Extensible records (??)}
276
277\section{Comparison to related work and alternatives}
278\begin{itemize}
279 \item Disjoint unions: drawbacks
280 \item Encoding the unbounded case: drawbacks
281\end{itemize}
282
283\section{Appendix: interface of library functions used to implement everything}
284
285\bibliography{polymorphic-variants}
286
287\end{document}
Note: See TracBrowser for help on using the repository browser.