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 | |
---|
53 | Big 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 | |
---|
71 | In this section we will attempt to provide a self-contained \emph{pr\'ecis} of polymorphic variants for the unfamiliar reader. |
---|
72 | Those 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 | |
---|
74 | Most 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. |
---|
75 | Each algebraic data type may be described as a sum-of-products. |
---|
76 | The programmer provides a fixed number of distinct \emph{constructors} with each constructor expects a (potentially empty) product of arguments. |
---|
77 | Values of a given inductive data type are built using a data type's constructors. |
---|
78 | Quotidian data structures---such as lists, trees, heaps, zippers, and so forth---can all be introduced using this now familiar mechanism. |
---|
79 | |
---|
80 | Having 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. |
---|
81 | Functional languages almost uniformly employ \emph{pattern matching} for this task. |
---|
82 | Given 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. |
---|
83 | Using pattern matching we can therefore deconstruct algebraic data by performing a case analysis on the constructors of a given type. |
---|
84 | |
---|
85 | The combination of algebraic data types and pattern matching is powerful, and is arguably the main branching mechanism for most functional programming languages. |
---|
86 | Furthermore, 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 | |
---|
88 | Unfortunately, in practical programming, we often want to expand a previously defined algebraic data type, adding more constructors. |
---|
89 | When it comes to extending algebraic data types with new constructors in this way, we hit a problem: these types are `closed'. |
---|
90 | In 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 | This 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} |
---|
96 | data Term |
---|
97 | = Lit Int |
---|
98 | | Add Term Term |
---|
99 | |
---|
100 | eval :: Term -> Int |
---|
101 | eval (Lit i) = i |
---|
102 | eval (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} |
---|
108 | interface Term { |
---|
109 | int eval(); |
---|
110 | } |
---|
111 | |
---|
112 | class Lit implements Term { |
---|
113 | private int v = 0; |
---|
114 | ... |
---|
115 | int eval() { return v; } |
---|
116 | } |
---|
117 | |
---|
118 | class 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 | |
---|
131 | However, we can look abroad to see what other families of programming languages do to solve this problem. |
---|
132 | For 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). |
---|
133 | In 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. |
---|
134 | The base interface of the object hierarchy specifies the permitted operations defined for the type. |
---|
135 | Branching by pattern matching is emulated using the language's dynamic dispatch mechanism. |
---|
136 | |
---|
137 | As all permitted operations on |
---|
138 | it is hard to enlarge the set of operations defined over a given type without altering the entire class hierarchy. |
---|
139 | If the interface changes so must every class implementing it. |
---|
140 | However, 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 | ... |
---|
146 | data Term' |
---|
147 | = Lift Term |
---|
148 | | Mul Term' Term' |
---|
149 | |
---|
150 | eval' :: Term' -> Int |
---|
151 | eval' (Lift t) = eval t |
---|
152 | eval' (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 | ... |
---|
159 | class 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 | ... |
---|
176 | show :: Term -> String |
---|
177 | show (Lit i) = show i |
---|
178 | show (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} |
---|
185 | interface Term { |
---|
186 | int eval(); |
---|
187 | String show(); |
---|
188 | } |
---|
189 | |
---|
190 | class 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 | |
---|
199 | class 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} |
---|
227 | Inductively define a |
---|
228 | \end{definition} |
---|
229 | |
---|
230 | \begin{figure} |
---|
231 | \begin{gather*} |
---|
232 | \begin{prooftree} |
---|
233 | (\Gamma(x) = \sigma) |
---|
234 | \justifies |
---|
235 | K; \Gamma \ent x : \sigma |
---|
236 | \using\rulefont{{\Gamma}x} |
---|
237 | \end{prooftree} |
---|
238 | \qquad |
---|
239 | \begin{prooftree} |
---|
240 | K; \Gamma, x : \phi \ent r : \psi |
---|
241 | \justifies |
---|
242 | K; \Gamma \ent \lam{x}r : \phi \funarr \psi |
---|
243 | \using\rulefont{{\Gamma}\lambda} |
---|
244 | \end{prooftree} |
---|
245 | \qquad |
---|
246 | \begin{prooftree} |
---|
247 | K;\Gamma \ent r : \phi \funarr \psi \quad K;\Gamma \ent s : \phi |
---|
248 | \justifies |
---|
249 | K;\Gamma \ent rs : \psi |
---|
250 | \using\rulefont{{\Gamma}rs} |
---|
251 | \end{prooftree} |
---|
252 | \\[1.5ex] |
---|
253 | \begin{prooftree} |
---|
254 | K; \Gamma \ent r : \sigma \quad K; \Gamma, x:\sigma \ent s : \psi |
---|
255 | \justifies |
---|
256 | K; \Gamma \ent \letin{x}{r}{s} : \psi |
---|
257 | \using\rulefont{{\Gamma}{:=}} |
---|
258 | \end{prooftree} |
---|
259 | \qquad |
---|
260 | \begin{prooftree} |
---|
261 | K;\Gamma \ent r : \sigma \quad (a \not\in ftv(\Gamma)) |
---|
262 | \justifies |
---|
263 | K;\Gamma \ent r : \fall{a}{\sigma} |
---|
264 | \using\rulefont{{\Gamma}{\forall}{a}} |
---|
265 | \end{prooftree} |
---|
266 | \\[1.5ex] |
---|
267 | \begin{prooftree} |
---|
268 | K;\Gamma \ent r : \fall{a}{\sigma} \quad K;\Gamma \ent s : \psi |
---|
269 | \justifies |
---|
270 | K;\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 |
---|
277 | K \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} |
---|
282 | K;\Gamma \ent r : \phi \quad K \ent i \geq \pair{tag}{\top} |
---|
283 | \justifies |
---|
284 | K;\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} |
---|
289 | K;\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 |
---|
290 | K;\Gamma, x_k : \phi_k \ent r_k : \psi \quad (1 \leq k \leq n) |
---|
291 | \justifies |
---|
292 | K;\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} |
---|
297 | K;\Gamma \ent r : \sigma \quad (\rho \not\in ftv(\Gamma)) |
---|
298 | \justifies |
---|
299 | K;\Gamma \ent r : \fall{\rho}{\sigma} |
---|
300 | \using\rulefont{{K}{\forall}{\rho}} |
---|
301 | \end{prooftree} |
---|
302 | \qquad |
---|
303 | \begin{prooftree} |
---|
304 | K;\Gamma \ent r : \fall{\rho}{\sigma} \quad K;\Gamma \ent s : T |
---|
305 | \justifies |
---|
306 | K;\Gamma \ent rs : \sigma[\rho := T] |
---|
307 | \using\rulefont{{K}inst{\rho}} |
---|
308 | \end{prooftree} |
---|
309 | \\[1.5ex] |
---|
310 | \begin{prooftree} |
---|
311 | K \oplus i_{\geq \pair{L}{U}};\Gamma \ent r : \sigma |
---|
312 | \justifies |
---|
313 | K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma} |
---|
314 | \using\rulefont{{K}{\forall}{i}} |
---|
315 | \end{prooftree} |
---|
316 | \qquad |
---|
317 | \begin{prooftree} |
---|
318 | K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma} \quad K \ent i' \geq \pair{L, U} |
---|
319 | \justifies |
---|
320 | K;\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 | |
---|
334 | Matita~\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. |
---|
335 | Throughout this paper, all running examples are provided in Matita's proof script vernacular. |
---|
336 | This vernacular, similar to the syntax of OCaml or Coq, should be mostly straightforward. |
---|
337 | |
---|
338 | One possible source of confusion is our use of $?$ and $\ldots$, which correspond to a term, or terms, to be inferred automatically by unification, respectively. |
---|
339 | Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations. |
---|
340 | |
---|
341 | Matita |
---|
342 | |
---|
343 | \subsection{Subtyping as instantiation vs subtyping as safe static cast} |
---|
344 | |
---|
345 | \subsection{Syntax \& type checking rules} |
---|
346 | The ones of Guarrigue + casts, but also for the bounded case? |
---|
347 | Casts support both styles of subtyping. |
---|
348 | |
---|
349 | \subsection{Examples} |
---|
350 | The weird function types that only work in subtyping as instantiation |
---|
351 | |
---|
352 | \subsection{Solution to the expression problem} |
---|
353 | Our running example in pseudo-OCaml syntax |
---|
354 | |
---|
355 | \section{Bounded polymorphic variants via dependent types} |
---|
356 | Requirements (i.e. O(1) pattern-matching, natural extracted code, etc.) |
---|
357 | \subsection{Simulation (reduction + type checking)} |
---|
358 | \subsection{Examples} |
---|
359 | The weird function types redone |
---|
360 | \subsection{Subtyping as instantiation vs subtyping as safe static cast} |
---|
361 | Here we show/discuss how our approach supports both styles at once. |
---|
362 | \subsection{Solution to the expression problem, I} |
---|
363 | Using subtyping as cast, the file I have produced |
---|
364 | \subsection{Solution to the expression problem, II} |
---|
365 | Using subtyping as instantiation, comparisons, pros vs cons |
---|
366 | \subsection{Negative encoding (??)} |
---|
367 | The negative encoding and application to the expression problem |
---|
368 | \subsection{Other encodings (??)} |
---|
369 | Hints 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} |
---|