# source:Papers/polymorphic-variants-2012/polymorphic-variants.tex@2517

Last change on this file since 2517 was 2517, checked in by sacerdot, 7 years ago

...

File size: 20.5 KB
Line
1\documentclass[smallextended]{svjour3}
2
3\smartqed
4
5\usepackage{amsmath}
6\usepackage[english]{babel}
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},
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
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
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
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
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}
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}
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}
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}
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}
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}
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}
356The topic of this paper, and this section in particular, is to present an
357\emph{encoding} of a subclass of polymorphic variants into dependent type
358theory. The final aim is to provide a solution to the expression problem
359that is implementable in user space into interactive theorem provers
360based on dependent type theories, in particular Coq, Agda and Matita.
361Moreover, we are only interested into an encoding that satisfies a number
362of constraints listed below. Essentially, the constraints ask that code
363automatically extracted from the system should be compiled efficiently
364without any change to the extraction machine. The encoding has been tested
365in the interactive theorem prover Matita, but we believe that it should be
366easily ported to the other cited systems.
367
368\subsection{Code extraction}
369Since our requirements have code extraction in mind, we briefly recall here
370what code extraction is in our context.
371
372Code extraction, as implemented in Coq, Matita and other systems, is the
373procedure that, given a proof term, extracts a program in a functional
374programming language that implements the computational content of the proof
375term. In particular, all proof parts that only establish correctness of the
376answer, totality of functions, etc. are to be erased. In particular, given
377a precondition $P$ and a postcondition $Q$, from a
378constructive proof of a $\forall x:A.P(x) \to \exists y:B. Q(x,y)$ statement
379one extracts a (partial) function $f$ from the encoding of $A$ to the encoding
380of $B$ that satisfies $\forall x. P(x) \to Q(x,f(x))$.
381
382Code extraction, as implemented by the above systems, does not attempt any
383optimization of the representation of data types. The only modification allowed
384is that parts of the data that are propositional and thus bare no content
385(being isomorphic to the unit type) are simplified to the unit type and
386possibly completely erased using the categorical properties of unit types
387($1 * T \symeq T$, $1 \to T \symeq T$, etc.). For more information, one can
389
390Thus, if a polymorphic variant is encoded in type theory as an n-ary sum of
391n-ary products, these being inefficiently represented using binary sums and
392products, the same holds for the extracted code.
393
394\subsection{The requirements}
395
396We list the following requirements.
397\begin{enumerate}
398 \item The representation of a polymorphic variant type in the extracted code
399   should be as efficient, in memory and time, as the isomorphic inductive
400   type. Efficiency should here be considered up to constants, and not
401   asymptotic.
402 \item Polymorphic types in the subtyping relation should be encoded using
403   data types that, once extracted, are in the subtyping relation too.
404   Before code extraction, instead, it is allowed to use explicit non identity
405   functions to coerce inhabitants of the sub-type into the super-type.
406   What matters is that the computational content of these coercions should be
407   the identity.
408\end{enumerate}
409The first requirements prevents the encoding of polymorphic variants
410using binary sums and products. For example, a constructor of an inductive
411type with four constructors requires one memory cell, but the same constructor
412for a binary sum of binary sums requires two memory cells, and twice the time
413to inhabit the data type. The solution is to force the code extracted from the
414polymorphic variant $\tau$ to be an inductive type. In turn this forces the
415encoding of polymorphic variants to be based on inductive types.
416
417The second requirement is in contrast with the possibility to extend a
418polymorphic variant type: when a type $\tau$ is extended to $\tau + a:T$,
419an inhabitant of the extraction of $\tau$ should already be an inhabitant of
420the extraction of $\tau + a:T$. This is possible if polymorphic variants were
421extracted to polymorphic variants in the target language, but this is not
422actually the case in any of the considered systems (e.g. Coq or Matita).
423Indeed, because of the first requirement, $\tau$ and $\tau + a:T$ are to be
424extracted to two inductive types. The only way to obtain subtyping is to
425already use the same representation: we need to anticipate or \emph{bound}
426the extension.
427
428Thus we accept the following limitation, together with an additional requirement
429to mitigate the limitation:
430\begin{enumerate}
431 \item[3] We only encode \emph{bounded polymorphic variants}, whose typing
432  rules are given in Figure~\ref{???}.
433 \item[4] Bounded polymorphic variants are characterized by a universe, i.e.
434  a set of fields together with their type. Every bounded polymorphic variant
435  is a sub-variant of the universe, obtained by selecting only certain fields.
436  We ask that adding a new field to the universe should have no impact on
437  pre-existing code that does not use it. More precisely, it should be possible
438  to add a field to the universe and recompile all pre-existing developments
439  without further modifications.
440\end{enumerate}
441
442\subsection{Discussion on the requirements and alternative approaches}
443The set of requirements we have imposed drastically restrict the set of possible
444solutions for the encoding. Moreover, they clearly represent a trade off between
445flexibility and efficiency. We discuss here alternative approaches based on
446different set of requirements.
447
448Maximal flexibility is only obtained dropping the boundedness limitation.
449One of the benefits or open polymorphic variants is separate compilation:
450the developers of libraries can use their own set of constructors and the
451user can freely mix them when the types of the different fields are coherent.
452Moreover, separate compilation can be made efficient if one accepts that
453correct programs can be rejected with very low probability at linking
454time~\cite{guarriguexxx}.
455
456Requirement 4 has been imposed to recover the flexibility of open variants.
457Suppose that every library starts with a file that declares its own universe.
458Then, to mix two libraries, one needs to merge the two universe declarations
459together, which is only possible if the universes are coherent. Once this is
460done, the library files will keep compiling because of the requirement. What
461is irremediably lost is separate compilation. We believe that this loss can
462be withstood in many practical situations, because 1) merging of different
463libraries that need to share at least some constructor is rare and needs to
464be done just once; 2) the addition of new fields to the universe of a library
465under development usually requires a significant effort to fix the library that
466should make the recompilation time of the other libraries negligible.
467
468If separate compilation is considered fundamental, then the only possible
469approach seems that of introducing a syntactic data type (a universe) of
470descriptions of polymorphic variants type, which is then interpreted by
471dependent functions (type formers) to the appropriate sums of types.
472The problem, generalized to that of giving a universe to the full syntax of
473inductive types, is being studied by the groups of Altenkirch and
474Ghani~\cite{aa,bb,cc,dd}. This approach, which is mathematically
475very elegant, is in conflict with requirements 1 and 2. The conflict can be
476solved by devising an ad-hoc extraction procedure which targets a programming
477language that already implements polymorphic variants efficiently. As far as
478we know, this has not been done yet. The next generation of Epigram, however,
479is supposed to be implemented around this idea. Instead of an ad-hoc extraction
480procedure, Epigram will be directly compiled to executable code, optimizing the
481poor encodings that are generated by the syntactic universe.
482
483
484\subsection{Simulation (reduction + type checking)}
485\subsection{Examples}
486The weird function types redone
487\subsection{Subtyping as instantiation vs subtyping as safe static cast}
488Here we show/discuss how our approach supports both styles at once.
489\subsection{Solution to the expression problem, I}
490Using subtyping as cast, the file I have produced
491\subsection{Solution to the expression problem, II}
492Using subtyping as instantiation, comparisons, pros vs cons
493\subsection{Negative encoding (??)}
494The negative encoding and application to the expression problem
495\subsection{Other encodings (??)}
496Hints to other possible encodings
497
498\section{Extensible records (??)}
499
500\section{Comparison to related work and alternatives}
501\begin{itemize}
502 \item Disjoint unions: drawbacks
503 \item Encoding the unbounded case: drawbacks
504\end{itemize}
505
506\section{Appendix: interface of library functions used to implement everything}
507
508\bibliography{polymorphic-variants}
509
510\end{document}
Note: See TracBrowser for help on using the repository browser.