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 | \renewcommand{\verb}{\lstinline} |
---|
24 | \def\lstlanguagefiles{lst-grafite.tex} |
---|
25 | \lstset{language=Grafite} |
---|
26 | |
---|
27 | \bibliographystyle{spphys} |
---|
28 | |
---|
29 | \author{Dominic P. Mulligan \and Claudio Sacerdoti Coen} |
---|
30 | \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.}} |
---|
31 | |
---|
32 | \institute{ |
---|
33 | Dominic P. Mulligan \at |
---|
34 | Computer Laboratory,\\ |
---|
35 | University of Cambridge. |
---|
36 | \email{dominic.p.mulligan@gmail.com} \and |
---|
37 | Claudio Sacerdoti Coen \at |
---|
38 | Dipartimento di Scienze dell'Informazione,\\ |
---|
39 | Universit\`a di Bologna. |
---|
40 | \email{sacerdot@cs.unibo.it} |
---|
41 | } |
---|
42 | |
---|
43 | \begin{document} |
---|
44 | |
---|
45 | \maketitle |
---|
46 | |
---|
47 | \begin{abstract} |
---|
48 | |
---|
49 | Big long abstract introducing the work |
---|
50 | |
---|
51 | \keywords{Polymorphic variants \and dependent type theory \and Matita theorem prover} |
---|
52 | |
---|
53 | \end{abstract} |
---|
54 | |
---|
55 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
56 | % Section |
---|
57 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
58 | \section{Introduction} |
---|
59 | \label{sect.introduction} |
---|
60 | |
---|
61 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
62 | % Section |
---|
63 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
64 | \section{Polymorphic variants} |
---|
65 | \label{sect.polymorphic.variants} |
---|
66 | |
---|
67 | In this section we will attempt to provide a self-contained \emph{pr\'ecis} of polymorphic variants for the unfamiliar reader. |
---|
68 | 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}. |
---|
69 | |
---|
70 | 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. |
---|
71 | Each algebraic data type may be described as a sum-of-products. |
---|
72 | The programmer provides a fixed number of distinct \emph{constructors} with each constructor expects a (potentially empty) product of arguments. |
---|
73 | Values of a given inductive data type are built using a data type's constructors. |
---|
74 | Quotidian data structures---such as lists, trees, heaps, zippers, and so forth---can all be introduced using this now familiar mechanism. |
---|
75 | |
---|
76 | 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. |
---|
77 | Functional languages almost uniformly employ \emph{pattern matching} for this task. |
---|
78 | 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. |
---|
79 | Using pattern matching we can therefore deconstruct algebraic data by performing a case analysis on the constructors of a given type. |
---|
80 | |
---|
81 | The combination of algebraic data types and pattern matching is powerful, and is arguably the main branching mechanism for most functional programming languages. |
---|
82 | 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. |
---|
83 | |
---|
84 | Unfortunately, in practical programming, we often want to expand a previously defined algebraic data type, adding more constructors. |
---|
85 | When it comes to extending algebraic data types with new constructors in this way, we hit a problem: these types are `closed'. |
---|
86 | 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. |
---|
87 | This manual extension, coupled with the lifting of any existing functions into the new type, is cumbersome and error-prone. |
---|
88 | |
---|
89 | \begin{figure}[ht] |
---|
90 | \begin{minipage}[b]{0.45\linewidth} |
---|
91 | \begin{lstlisting} |
---|
92 | \lstset{language=haskell} |
---|
93 | data Term |
---|
94 | = Lit Int |
---|
95 | | Add Term Term |
---|
96 | |
---|
97 | eval :: Term -> Int |
---|
98 | eval (Lit i) = i |
---|
99 | eval (Add l r) = eval l + eval r |
---|
100 | \end{lstlisting} |
---|
101 | \end{minipage} |
---|
102 | \hspace{0.5cm} |
---|
103 | \begin{minipage}[b]{0.45\linewidth} |
---|
104 | \begin{lstlisting} |
---|
105 | interface Term { |
---|
106 | int eval(); |
---|
107 | } |
---|
108 | |
---|
109 | class Lit implements Term { |
---|
110 | private int v = 0; |
---|
111 | ... |
---|
112 | int eval() { return v; } |
---|
113 | } |
---|
114 | |
---|
115 | class Add implements Term { |
---|
116 | private Term left, right = null; |
---|
117 | ... |
---|
118 | int eval() { |
---|
119 | return left.eval() + right.eval(); |
---|
120 | } |
---|
121 | } |
---|
122 | \end{lstlisting} |
---|
123 | \end{minipage} |
---|
124 | \label{fig.pattern-matching.vs.oop} |
---|
125 | \caption{A simple language of integer arithmetic embedded as an algebraic data type and as a class hierarchy.} |
---|
126 | \end{figure} |
---|
127 | |
---|
128 | However, we can look abroad to see what other families of programming languages do to solve this problem. |
---|
129 | 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). |
---|
130 | 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. |
---|
131 | The base interface of the object hierarchy specifies the permitted operations defined for the type. |
---|
132 | Branching by pattern matching is emulated using the language's dynamic dispatch mechanism. |
---|
133 | |
---|
134 | As all permitted operations on |
---|
135 | it is hard to enlarge the set of operations defined over a given type without altering the entire class hierarchy. |
---|
136 | If the interface changes so must every class implementing it. |
---|
137 | 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. |
---|
138 | |
---|
139 | \begin{figure}[ht] |
---|
140 | \begin{minipage}[b]{0.45\linewidth} |
---|
141 | \begin{lstlisting} |
---|
142 | ... |
---|
143 | data Term' |
---|
144 | = Lift Term |
---|
145 | | Mul Term' Term' |
---|
146 | |
---|
147 | eval' :: Term' -> Int |
---|
148 | eval' (Lift t) = eval t |
---|
149 | eval' (Mul l r) = eval' l * eval ' r |
---|
150 | \end{lstlisting} |
---|
151 | \end{minipage} |
---|
152 | \hspace{0.5cm} |
---|
153 | \begin{minipage}[b]{0.45\linewidth} |
---|
154 | \begin{lstlisting} |
---|
155 | ... |
---|
156 | class Mul implements Term { |
---|
157 | private Term left, right = null; |
---|
158 | ... |
---|
159 | int eval() { |
---|
160 | return left.eval() * right.eval(); |
---|
161 | } |
---|
162 | } |
---|
163 | \end{lstlisting} |
---|
164 | \end{minipage} |
---|
165 | \label{fig.extending.base.type} |
---|
166 | \caption{Extending our simple language of arithmetic with a new grammatical element.} |
---|
167 | \end{figure} |
---|
168 | |
---|
169 | \begin{figure}[ht] |
---|
170 | \begin{minipage}[b]{0.45\linewidth} |
---|
171 | \begin{lstlisting} |
---|
172 | ... |
---|
173 | show :: Term -> String |
---|
174 | show (Lit i) = show i |
---|
175 | show (Add l r) = |
---|
176 | show l ++ " + " ++ show r |
---|
177 | \end{lstlisting} |
---|
178 | \end{minipage} |
---|
179 | \hspace{0.5cm} |
---|
180 | \begin{minipage}[b]{0.45\linewidth} |
---|
181 | \begin{lstlisting} |
---|
182 | interface Term { |
---|
183 | int eval(); |
---|
184 | String show(); |
---|
185 | } |
---|
186 | |
---|
187 | class Lit implements Term { |
---|
188 | private int v = 0; |
---|
189 | ... |
---|
190 | int eval() { return v; } |
---|
191 | String show() { |
---|
192 | return Int.toString(v); |
---|
193 | } |
---|
194 | } |
---|
195 | |
---|
196 | class Add implements Term { |
---|
197 | private Term left, right = null; |
---|
198 | ... |
---|
199 | int eval() { |
---|
200 | return left.eval() + right.eval(); |
---|
201 | } |
---|
202 | ... |
---|
203 | String show() { |
---|
204 | return left.show() + \ |
---|
205 | " + " + right.show(); |
---|
206 | } |
---|
207 | } |
---|
208 | \end{lstlisting} |
---|
209 | \end{minipage} |
---|
210 | \label{fig.extending.base.type} |
---|
211 | \caption{Extending the permitted operations over our simple language of arithmetic.} |
---|
212 | \end{figure} |
---|
213 | |
---|
214 | [dpm: reword the above --- hard to phrase precisely ] |
---|
215 | |
---|
216 | |
---|
217 | \begin{itemize} |
---|
218 | \item General introduction, motivations |
---|
219 | \item Bounded vs not-bounded. |
---|
220 | \end{itemize} |
---|
221 | |
---|
222 | \begin{definition} |
---|
223 | \label{defn.garrigues.calculus} |
---|
224 | Inductively define a |
---|
225 | \end{definition} |
---|
226 | |
---|
227 | \begin{figure} |
---|
228 | \begin{gather*} |
---|
229 | \begin{prooftree} |
---|
230 | (\Gamma(x) = \sigma) |
---|
231 | \justifies |
---|
232 | K; \Gamma \ent x : \sigma |
---|
233 | \using\rulefont{{\Gamma}x} |
---|
234 | \end{prooftree} |
---|
235 | \qquad |
---|
236 | \begin{prooftree} |
---|
237 | K; \Gamma, x : \phi \ent r : \psi |
---|
238 | \justifies |
---|
239 | K; \Gamma \ent \lam{x}r : \phi \funarr \psi |
---|
240 | \using\rulefont{{\Gamma}\lambda} |
---|
241 | \end{prooftree} |
---|
242 | \qquad |
---|
243 | \begin{prooftree} |
---|
244 | K;\Gamma \ent r : \phi \funarr \psi \quad K;\Gamma \ent s : \phi |
---|
245 | \justifies |
---|
246 | K;\Gamma \ent rs : \psi |
---|
247 | \using\rulefont{{\Gamma}rs} |
---|
248 | \end{prooftree} |
---|
249 | \\[1.5ex] |
---|
250 | \begin{prooftree} |
---|
251 | K; \Gamma \ent r : \sigma \quad K; \Gamma, x:\sigma \ent s : \psi |
---|
252 | \justifies |
---|
253 | K; \Gamma \ent \letin{x}{r}{s} : \psi |
---|
254 | \using\rulefont{{\Gamma}{:=}} |
---|
255 | \end{prooftree} |
---|
256 | \qquad |
---|
257 | \begin{prooftree} |
---|
258 | K;\Gamma \ent r : \sigma \quad (a \not\in ftv(\Gamma)) |
---|
259 | \justifies |
---|
260 | K;\Gamma \ent r : \fall{a}{\sigma} |
---|
261 | \using\rulefont{{\Gamma}{\forall}{a}} |
---|
262 | \end{prooftree} |
---|
263 | \\[1.5ex] |
---|
264 | \begin{prooftree} |
---|
265 | K;\Gamma \ent r : \fall{a}{\sigma} \quad K;\Gamma \ent s : \psi |
---|
266 | \justifies |
---|
267 | K;\Gamma \ent rs : \sigma[a := \psi] |
---|
268 | \using\rulefont{{\Gamma}inst{a}} |
---|
269 | \end{prooftree} |
---|
270 | \\[1.5ex] |
---|
271 | \begin{prooftree} |
---|
272 | (L \subseteq L' \quad H \subseteq H') |
---|
273 | \justifies |
---|
274 | K \oplus i_{{\geq \pair{L}{U}}} \ent i \geq \pair{L'}{H'} |
---|
275 | \using\rulefont{{K}i} |
---|
276 | \end{prooftree} |
---|
277 | \qquad |
---|
278 | \begin{prooftree} |
---|
279 | K;\Gamma \ent r : \phi \quad K \ent i \geq \pair{tag}{\top} |
---|
280 | \justifies |
---|
281 | K;\Gamma \ent \polytag{tag(r)} : [ i \mid tag : \phi \cons T ] |
---|
282 | \using\rulefont{{K}variant} |
---|
283 | \end{prooftree} |
---|
284 | \\[1.5ex] |
---|
285 | \begin{prooftree} |
---|
286 | 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 |
---|
287 | K;\Gamma, x_k : \phi_k \ent r_k : \psi \quad (1 \leq k \leq n) |
---|
288 | \justifies |
---|
289 | K;\Gamma \ent \mathbf{match}\ r\ \mathbf{with}\ \{ \polytag{tag_k(x_k)} \Rightarrow r_k \}^n_1 : \psi |
---|
290 | \using\rulefont{{K}match} |
---|
291 | \end{prooftree} |
---|
292 | \\[1.5ex] |
---|
293 | \begin{prooftree} |
---|
294 | K;\Gamma \ent r : \sigma \quad (\rho \not\in ftv(\Gamma)) |
---|
295 | \justifies |
---|
296 | K;\Gamma \ent r : \fall{\rho}{\sigma} |
---|
297 | \using\rulefont{{K}{\forall}{\rho}} |
---|
298 | \end{prooftree} |
---|
299 | \qquad |
---|
300 | \begin{prooftree} |
---|
301 | K;\Gamma \ent r : \fall{\rho}{\sigma} \quad K;\Gamma \ent s : T |
---|
302 | \justifies |
---|
303 | K;\Gamma \ent rs : \sigma[\rho := T] |
---|
304 | \using\rulefont{{K}inst{\rho}} |
---|
305 | \end{prooftree} |
---|
306 | \\[1.5ex] |
---|
307 | \begin{prooftree} |
---|
308 | K \oplus i_{\geq \pair{L}{U}};\Gamma \ent r : \sigma |
---|
309 | \justifies |
---|
310 | K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma} |
---|
311 | \using\rulefont{{K}{\forall}{i}} |
---|
312 | \end{prooftree} |
---|
313 | \qquad |
---|
314 | \begin{prooftree} |
---|
315 | K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma} \quad K \ent i' \geq \pair{L, U} |
---|
316 | \justifies |
---|
317 | K;\Gamma \ent r : \sigma[i := i'] |
---|
318 | \using\rulefont{{K}inst{i}} |
---|
319 | \end{prooftree} |
---|
320 | \end{gather*} |
---|
321 | \caption{Garrigue's typing relation for polymorphic variants} |
---|
322 | \label{fig.garrigue.typing.relation} |
---|
323 | \end{figure} |
---|
324 | |
---|
325 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
326 | % Section |
---|
327 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
328 | \subsection{Matita} |
---|
329 | \label{subsect.matita} |
---|
330 | |
---|
331 | 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. |
---|
332 | Throughout this paper, all running examples are provided in Matita's proof script vernacular. |
---|
333 | This vernacular, similar to the syntax of OCaml or Coq, should be mostly straightforward. |
---|
334 | |
---|
335 | 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. |
---|
336 | Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations. |
---|
337 | |
---|
338 | \subsection{Subtyping as instantiation \emph{vs} subtyping as a safe static cast} |
---|
339 | |
---|
340 | \subsection{Syntax and type checking rules} |
---|
341 | The ones of Guarrigue + casts, but also for the bounded case? |
---|
342 | Casts support both styles of subtyping. |
---|
343 | |
---|
344 | \subsection{Examples} |
---|
345 | The weird function types that only work in subtyping as instantiation |
---|
346 | |
---|
347 | \subsection{Solution to the expression problem} |
---|
348 | Our running example in pseudo-OCaml syntax |
---|
349 | |
---|
350 | \section{Bounded polymorphic variants via dependent types} |
---|
351 | The topic of this paper, and this section in particular, is to present an |
---|
352 | \emph{encoding} of a subclass of polymorphic variants into dependent type |
---|
353 | theory. The final aim is to provide a solution to the expression problem |
---|
354 | that is implementable in user space into interactive theorem provers |
---|
355 | based on dependent type theories, in particular Coq, Agda and Matita. |
---|
356 | Moreover, we are only interested into an encoding that satisfies a number |
---|
357 | of constraints listed below. Essentially, the constraints ask that code |
---|
358 | automatically extracted from the system should be compiled efficiently |
---|
359 | without any change to the extraction machine. The encoding has been tested |
---|
360 | in the interactive theorem prover Matita, but we believe that it should be |
---|
361 | easily ported to the other cited systems. |
---|
362 | |
---|
363 | \subsection{Code extraction} |
---|
364 | Since our requirements have code extraction in mind, we briefly recall here |
---|
365 | what code extraction is in our context. |
---|
366 | |
---|
367 | Code extraction, as implemented in Coq, Matita and other systems, is the |
---|
368 | procedure that, given a proof term, extracts a program in a functional |
---|
369 | programming language that implements the computational content of the proof |
---|
370 | term. In particular, all proof parts that only establish correctness of the |
---|
371 | answer, totality of functions, etc. are to be erased. In particular, given |
---|
372 | a precondition $P$ and a postcondition $Q$, from a |
---|
373 | constructive proof of a $\forall x:A.P(x) \to \exists y:B. Q(x,y)$ statement |
---|
374 | one extracts a (partial) function $f$ from the encoding of $A$ to the encoding |
---|
375 | of $B$ that satisfies $\forall x. P(x) \to Q(x,f(x))$. |
---|
376 | |
---|
377 | Code extraction, as implemented by the above systems, does not attempt any |
---|
378 | optimization of the representation of data types. The only modification allowed |
---|
379 | is that parts of the data that are propositional and thus bare no content |
---|
380 | (being isomorphic to the unit type) are simplified to the unit type and |
---|
381 | possibly completely erased using the categorical properties of unit types |
---|
382 | ($1 * T \simeq T$, $1 \to T \simeq T$, etc.). For more information, one can |
---|
383 | read~\cite{berardi,christine-mohring,letouzey}. |
---|
384 | |
---|
385 | Thus, if a polymorphic variant is encoded in type theory as an n-ary sum of |
---|
386 | n-ary products, these being inefficiently represented using binary sums and |
---|
387 | products, the same holds for the extracted code. |
---|
388 | |
---|
389 | \subsection{The requirements} |
---|
390 | |
---|
391 | We list the following requirements. |
---|
392 | \begin{enumerate} |
---|
393 | \item The representation of a polymorphic variant type in the extracted code |
---|
394 | should be as efficient, in memory and time, as the isomorphic inductive |
---|
395 | type. Efficiency should here be considered up to constants, and not |
---|
396 | asymptotic. |
---|
397 | \item Polymorphic types in the subtyping relation should be encoded using |
---|
398 | data types that, once extracted, are in the subtyping relation too. |
---|
399 | Before code extraction, instead, it is allowed to use explicit non identity |
---|
400 | functions to coerce inhabitants of the sub-type into the super-type. |
---|
401 | What matters is that the computational content of these coercions should be |
---|
402 | the identity. |
---|
403 | \end{enumerate} |
---|
404 | The first requirements prevents the encoding of polymorphic variants |
---|
405 | using binary sums and products. For example, a constructor of an inductive |
---|
406 | type with four constructors requires one memory cell, but the same constructor |
---|
407 | for a binary sum of binary sums requires two memory cells, and twice the time |
---|
408 | to inhabit the data type. The solution is to force the code extracted from the |
---|
409 | polymorphic variant $\tau$ to be an inductive type. In turn this forces the |
---|
410 | encoding of polymorphic variants to be based on inductive types. |
---|
411 | |
---|
412 | The second requirement is in contrast with the possibility to extend a |
---|
413 | polymorphic variant type: when a type $\tau$ is extended to $\tau + a:T$, |
---|
414 | an inhabitant of the extraction of $\tau$ should already be an inhabitant of |
---|
415 | the extraction of $\tau + a:T$. This is possible if polymorphic variants were |
---|
416 | extracted to polymorphic variants in the target language, but this is not |
---|
417 | actually the case in any of the considered systems (e.g. Coq or Matita). |
---|
418 | Indeed, because of the first requirement, $\tau$ and $\tau + a:T$ are to be |
---|
419 | extracted to two inductive types. The only way to obtain subtyping is to |
---|
420 | already use the same representation: we need to anticipate or \emph{bound} |
---|
421 | the extension. |
---|
422 | |
---|
423 | Thus we accept the following limitation, together with an additional requirement |
---|
424 | to mitigate the limitation: |
---|
425 | \begin{enumerate} |
---|
426 | \item[3] We only encode \emph{bounded polymorphic variants}, whose typing |
---|
427 | rules are given in Figure~\ref{???}. |
---|
428 | \item[4] Bounded polymorphic variants are characterized by a universe, i.e. |
---|
429 | a set of fields together with their type. Every bounded polymorphic variant |
---|
430 | is a sub-variant of the universe, obtained by selecting only certain fields. |
---|
431 | We ask that adding a new field to the universe should have no impact on |
---|
432 | pre-existing code that does not use it. More precisely, it should be possible |
---|
433 | to add a field to the universe and recompile all pre-existing developments |
---|
434 | without further modifications. |
---|
435 | \end{enumerate} |
---|
436 | |
---|
437 | \subsection{Discussion on the requirements and alternative approaches} |
---|
438 | The set of requirements we have imposed drastically restrict the set of possible |
---|
439 | solutions for the encoding. Moreover, they clearly represent a trade off between |
---|
440 | flexibility and efficiency. We discuss here alternative approaches based on |
---|
441 | different set of requirements. |
---|
442 | |
---|
443 | Maximal flexibility is only obtained dropping the boundedness limitation. |
---|
444 | One of the benefits or open polymorphic variants is separate compilation: |
---|
445 | the developers of libraries can use their own set of constructors and the |
---|
446 | user can freely mix them when the types of the different fields are coherent. |
---|
447 | Moreover, separate compilation can be made efficient if one accepts that |
---|
448 | correct programs can be rejected with very low probability at linking |
---|
449 | time~\cite{guarriguexxx}. |
---|
450 | |
---|
451 | Requirement 4 has been imposed to recover the flexibility of open variants. |
---|
452 | Suppose that every library starts with a file that declares its own universe. |
---|
453 | Then, to mix two libraries, one needs to merge the two universe declarations |
---|
454 | together, which is only possible if the universes are coherent. Once this is |
---|
455 | done, the library files will keep compiling because of the requirement. What |
---|
456 | is irremediably lost is separate compilation. We believe that this loss can |
---|
457 | be withstood in many practical situations, because 1) merging of different |
---|
458 | libraries that need to share at least some constructor is rare and needs to |
---|
459 | be done just once; 2) the addition of new fields to the universe of a library |
---|
460 | under development usually requires a significant effort to fix the library that |
---|
461 | should make the recompilation time of the other libraries negligible. |
---|
462 | |
---|
463 | If separate compilation is considered fundamental, then the only possible |
---|
464 | approach seems that of introducing a syntactic data type (a universe) of |
---|
465 | descriptions of polymorphic variants type, which is then interpreted by |
---|
466 | dependent functions (type formers) to the appropriate sums of types. |
---|
467 | The problem, generalized to that of giving a universe to the full syntax of |
---|
468 | inductive types, is being studied by the groups of Altenkirch and |
---|
469 | Ghani~\cite{aa,bb,cc,dd}. This approach, which is mathematically |
---|
470 | very elegant, is in conflict with requirements 1 and 2. The conflict can be |
---|
471 | solved by devising an ad-hoc extraction procedure which targets a programming |
---|
472 | language that already implements polymorphic variants efficiently. As far as |
---|
473 | we know, this has not been done yet. The next generation of Epigram, however, |
---|
474 | is supposed to be implemented around this idea. Instead of an ad-hoc extraction |
---|
475 | procedure, Epigram will be directly compiled to executable code, optimizing the |
---|
476 | poor encodings that are generated by the syntactic universe. |
---|
477 | |
---|
478 | \subsection{The encoding} |
---|
479 | In order to encode bounded polymorphic variants in dependent type theory, |
---|
480 | we encode 1) the universe; 2) the polymorphic variant types; 3) the |
---|
481 | constructors of the polymorphic variant type; 4) the pattern matching operator; |
---|
482 | 5) an elimination proof principle for polymorphic variants. The pattern matching |
---|
483 | operator and the elimination principle have the same behaviour, according to |
---|
484 | the Curry-Howard isomorphism. We assume that the latter will be used to prove |
---|
485 | statements without taking care of the computational content of the proof |
---|
486 | (proof irrelevance). Thus only the pattern matching operator, and not the |
---|
487 | elimination principle, will need to satisfy requirement 1. |
---|
488 | |
---|
489 | The encoding is a careful mix of a deep and a shallow encodings, with user |
---|
490 | provided connections between them. The shallow part of the encoding is there |
---|
491 | for code extraction to satisfy requirements 1. In particular, the |
---|
492 | shallow encoding of the universe is just an ordinary inductive type, which is |
---|
493 | extracted to an algebraic type. The encoding of a polymorphic variant type is |
---|
494 | just a $\Sigma$-type whose carrier is the universe, which is extracted |
---|
495 | exactly as the universe (so satisfying requirement 2). The deep part of the |
---|
496 | encoding allows to perform dependent computations on the list of fields that |
---|
497 | are allowed in a polymorphic variant type. For example, from the list of fields |
---|
498 | a dependently typed function can generate the type of the elimination principle. |
---|
499 | The links between the two encodings are currently user provided, but it simple |
---|
500 | to imagine a simple program that automates the task. |
---|
501 | |
---|
502 | \begin{definition}[Universe encoding] |
---|
503 | A parametric universe |
---|
504 | $$(\alpha_1,\ldots,\alpha_m) u := K_1:T_1 ~|~ \ldots ~|~ K_n:T_n$$ |
---|
505 | (where $\alpha_1,\ldots, \alpha_m$ are type variables bound in |
---|
506 | $T_1,\ldots,T_n$) is encoded by means of: |
---|
507 | \begin{itemize} |
---|
508 | \item Its shallow encoding, the corresponding inductive type |
---|
509 | $$inductive~u~(\alpha_1:Type[0],\ldots,\alpha_m:Type[0]) u : Type[0] := |
---|
510 | K_1:T_1 \to u~\alpha_1~\ldots~\alpha_m ~|~ \ldots ~|~ K_n:T_n \to u~\alpha_1~\ldots~\alpha_m$$ |
---|
511 | \item A disjoint sum (an inductive type) of names for the tags of $u$: |
---|
512 | $$inductive~tag\_~ : Type[0] := k_1: tag\_ ~|~ \ldots ~|~ k_n: tag\_$$ |
---|
513 | \item An equality test $eq\_tag: tag\_ \to tag\_ \to bool$ that returns true |
---|
514 | iff the two tags are equal. This is boilerplate code that is often |
---|
515 | automatized by interactive theorem provers. We write $tag$ for the type |
---|
516 | the $tag\_$ coupled with its decidable equality test $eq\_tag$ and |
---|
517 | a user provided proof that $\forall x,y:tag. eq\_tag x y = true \iff x=y$. |
---|
518 | \item A simple function $$tag\_of\_expr: \forall \alpha_1,\ldots,\alpha_m. |
---|
519 | u \alpha_1 \ldots \alpha_m \to tag$$ |
---|
520 | that performs a case analysis on the shallow encoding of a universe |
---|
521 | inhabitant and returns the name of the corresponding constructor. |
---|
522 | This boilerplate code is the bridge from the shallow to the deep |
---|
523 | encoding of the universe. |
---|
524 | \item A type former |
---|
525 | $$Q\_holds\_for\_tag: \forall \alpha_1,\ldots,\alpha_m. |
---|
526 | \forall Q: u~\alpha_1~\ldots~\alpha_n \to Prop. |
---|
527 | \forall t:tag. Prop$$ |
---|
528 | that performs pattern matching over the tag and returns the proof obligation |
---|
529 | for the proof of $Q$ in the case corresponding to the tag. |
---|
530 | \item A proof of exhaustivity of pattern matching over the tag. This |
---|
531 | boilerplate proof is the bridge from the deep to the shallow encoding of the |
---|
532 | universe. The statement is: |
---|
533 | $$Q\_holds\_for\_tag\_spec: |
---|
534 | \forall \alpha_1,\ldots,\alpha_m. |
---|
535 | \forall Q: u~\alpha_1~\ldots~\alpha_m \to Prop. |
---|
536 | \forall x: u~\alpha_1~\ldots~\alpha_m. |
---|
537 | Q\_holds\_for\_tag~\ldots~Q~\ldots~(tag\_of\_expr~\ldots~x) \to Q x$$ |
---|
538 | \end{itemize} |
---|
539 | \end{definition} |
---|
540 | |
---|
541 | \begin{example}[The universe for our running example] |
---|
542 | The following lines of Matita code implement the universe encoding for our |
---|
543 | running example. They constitute the file~\texttt{test.ma}. |
---|
544 | \begin{lstlisting} |
---|
545 | inductive expr (E: Type[0]) : Type[0] ≝ |
---|
546 | Num : nat -> expr E |
---|
547 | | Plus : E -> E -> expr E |
---|
548 | | Mul : E -> E -> expr E. |
---|
549 | |
---|
550 | inductive tag_ : Type[0] := num : tag_ | plus : tag_ | mul : tag_. |
---|
551 | |
---|
552 | definition eq_tag : tag_ -> tag_ -> bool := |
---|
553 | λt1,t2. |
---|
554 | match t1 with |
---|
555 | [ num => match t2 with [num => true | _ => false] |
---|
556 | | plus => match t2 with [plus => true | _ => false] |
---|
557 | | mul => match t2 with [mul => true | _ => false]]. |
---|
558 | |
---|
559 | definition tag : DeqSet ≝ mk_DeqSet tag_ eq_tag ?. |
---|
560 | ** normalize /2/ % #abs destruct |
---|
561 | qed. |
---|
562 | |
---|
563 | definition tag_of_expr : ∀E:Type[0]. expr E -> tag := |
---|
564 | λE,e. |
---|
565 | match e with |
---|
566 | [ Num _ => num |
---|
567 | | Plus _ _ => plus |
---|
568 | | Mul _ _ => mul ]. |
---|
569 | |
---|
570 | definition Q_holds_for_tag: |
---|
571 | ∀E:Type[0]. ∀Q: expr E → Prop. ∀t:tag. Prop ≝ |
---|
572 | λE,Q,t. |
---|
573 | match t with |
---|
574 | [ num ⇒ ∀n. Q (Num … n) |
---|
575 | | plus ⇒ ∀x,y. Q (Plus … x y) |
---|
576 | | mul ⇒ ∀x,y. Q (Mul … x y) |
---|
577 | ]. |
---|
578 | |
---|
579 | theorem Q_holds_for_tag_spec: |
---|
580 | ∀E:Type[0]. ∀Q: expr E → Prop. |
---|
581 | ∀x: expr E. Q_holds_for_tag … Q … (tag_of_expr … x) → Q x. |
---|
582 | #E #Q * normalize // |
---|
583 | qed. |
---|
584 | \end{lstlisting} |
---|
585 | \end{example} |
---|
586 | |
---|
587 | We are now ready to lift the universe encoding to the encoding of polymorphic |
---|
588 | variant types, constructors, case analysis and elimination principle. |
---|
589 | |
---|
590 | The idea consists in following quite litteraly the description of the syntax |
---|
591 | of bounded polymorphic variants: a bounded polymorphic variant is deeply |
---|
592 | encoded by the list of constructors that are allowed. Row polymorphism is |
---|
593 | achieved by quantifying over the list, which can be bounded from above and |
---|
594 | below using normal hypotheses. A dependently typed semantic function coerces |
---|
595 | the deep encoding to the shallow one, that we will soon describe. We will |
---|
596 | handle the function has an implicit coercion, so that we will simply write |
---|
597 | $i$ to represent both the list of tag names $i$ and the type former which is |
---|
598 | the polymorphic variant type described by $i$. The context always allow to |
---|
599 | disambiguate between the two uses and insert the coercion every time that |
---|
600 | a list $i$ is used in a type former. |
---|
601 | For example, the list $[num;plus]$ for our |
---|
602 | running example will represent the polymorphic variant type |
---|
603 | $[i_{\geq \pair{[num;plus]}{[num;plus]}}]$ and a function that expects at |
---|
604 | least $num$ but that does not handle $mul$ will be typed as either |
---|
605 | $f : \forall E. \forall i. [num] \subseteq i \subseteq [num;plus] \to i~E \to \ldots$ |
---|
606 | or $f: \forall E. \forall i. i \subseteq [plus] \to (num::i)~E \to \ldots$. |
---|
607 | |
---|
608 | We defined the shallow encoding of the bounded polymorphic variant type |
---|
609 | specified by a list $i$ of constructors as a $\Sigma$-type whose carrier |
---|
610 | is the universe data type $u$ and whose property rules out all constructors |
---|
611 | whose tag is not in $i$. Code extraction will simplify the $\Sigma$-type to |
---|
612 | its carrier, satisfying both requirements 1 and 2. |
---|
613 | |
---|
614 | \begin{definition}[Polymorphic variant type encoding] |
---|
615 | A bounded polymorphic variant $i$ where $i_{\geq \pair{L}{U}}$ is deeply encoded |
---|
616 | by a variable $i$ of type list of tags ($i: list~tag$) under the hypothesis |
---|
617 | that $L \subseteq i \subseteq U$. |
---|
618 | The corresponding shallow encoding is |
---|
619 | $\Sigma x:u~\alpha_1~\ldots~\alpha_n. tag\_of\_expr \ldots x \in i$. |
---|
620 | An implicit coercion maps $i : list~tag \mapsto \Sigma x:u~\alpha_1~\ldots~\alpha_n. tag\_of\_expr \ldots x \in i$. |
---|
621 | \end{definition} |
---|
622 | |
---|
623 | Subtyping is not necessary for polymorphic variants \`a la Guarrigue~\cite{???}: |
---|
624 | the slogan, borrowed by~\cite{???}, is \emph{structural subtyping as |
---|
625 | instantitation}. |
---|
626 | Subtyping as instantiation fits very well with the Hindley-Milner type system |
---|
627 | because it supports type inference. Since we work with a type system more |
---|
628 | expressive than Hindley-Milner where type inference is undecidable, we are |
---|
629 | not restricted to subtyping as instantiation, but we can also exploit the |
---|
630 | natural subtyping rule between polymorphic variants types~\ref{???}. |
---|
631 | |
---|
632 | \begin{definition}[Subtyping] |
---|
633 | There exists a coercion of type |
---|
634 | $\forall i_1,i_2: list~tag. i_1 \subseteq i_2 \to \forall \alpha_1,\ldots,\alpha_m. i_1~\alpha_1~\ldots~\alpha_n \to |
---|
635 | i_2~\alpha_1~\ldots~\alpha_n$ |
---|
636 | \end{definition} |
---|
637 | In the encoding of the universe we required an equality test over tags. |
---|
638 | The test is exploited here to implement a computational version of the |
---|
639 | $\subseteq$ relation between list of tags. I.e. it is possible to define |
---|
640 | $\subseteq$ in such a way that for closed terms $i_1$ and $i_2$, |
---|
641 | $i_1 \subseteq i_2$ reduces to $True$. As we will see, this suggests a different |
---|
642 | style where polymorphic variant types are represented using the less number |
---|
643 | of row quantifications and type membership and subtyping are automatically |
---|
644 | decided by mere computation, without any user intervention. |
---|
645 | |
---|
646 | The subtyping coercion takes apart the inhabitant of the polymorphic variant |
---|
647 | $i_1$, obtaining both an inhabitant $x$ of the universe and a proof that its |
---|
648 | constructors are all in $i_1$. Then it builds an inhabitant of the polymorphic |
---|
649 | variant $i_2$ by coupling $x$ with the proof that all of its constructors are |
---|
650 | in $i_2 \superseteq i_1$. The computational content of the coercion is just |
---|
651 | the identity function and code extraction erases it: requirement 2 is satisfied. |
---|
652 | |
---|
653 | \begin{definition}[Constructor encoding] |
---|
654 | A constructor $K_i : T_i \to u~\alpha_1~\ldots~\alpha_m$ of the universe is |
---|
655 | lifted to a polymorphic variant constructor |
---|
656 | $T_i \to i~\alpha_1~\ldots~\alpha_m$ when |
---|
657 | $\forall x:T_i. tag\_of\_expr (K_i x) \in i$. |
---|
658 | The lifting is obtained by inhabiting the sigma type |
---|
659 | $\Sigma x:u~\alpha_1~\ldots~\alpha_n. tag\_of\_expr \ldots x \in i$ |
---|
660 | with a pair whose first component is the applied constructor and the second |
---|
661 | component the proof of the condition above. |
---|
662 | \end{definition} |
---|
663 | We can exploit again the equality test over tag types to implement a |
---|
664 | computational version of the predicate $tag\_of\_expr (K_i x) \in i$. |
---|
665 | Therefore, when $i$ is a closed term, all tests reduce to $True$. |
---|
666 | Matita implements a generalized system of coercions that allow to declare |
---|
667 | the lifting of polymorphic variant as an implicit coercion. Since the coercion |
---|
668 | requires a proof of the condition, a new proof obligation is opened. |
---|
669 | The proof obligation is just $True$ when $i$ is closed. |
---|
670 | |
---|
671 | The computational content of the lifted constructor is just the identity |
---|
672 | function: the $n$-th constructor of a polymorphic variant type is represented |
---|
673 | after code extraction by the $n$-th constructor of the unvierse inductive type, |
---|
674 | satisfying requirement 1. |
---|
675 | |
---|
676 | \begin{definition}[Pattern matching encoding] |
---|
677 | A pattern match $match~t~with \{K_{n_j} \Rightarrow M_{n_j}\}^r_1$ that only considers a superset of the constructors listed in the polymorphic variant type |
---|
678 | $i$ is encoded as |
---|
679 | $match~t~with \{K_i \Rightarrow k_i \in i \to M'_i\}$ |
---|
680 | where $M'_{n_j} = M_{n_j}$ for all $j \in [1,\ldots,r]$ and |
---|
681 | $M'_{n_j}$ is obtained by elimination of $False$ in all other cases. |
---|
682 | The proofs of $False$ required to perform the elimination are obtained from |
---|
683 | the hypotheses $k_i \in i$ which contradicts the fact that $k_i$ was not |
---|
684 | listed in a superset of $i$. |
---|
685 | \end{definition} |
---|
686 | Again, for closed types $i$, the test $k_i \in i$ can be implemented in such |
---|
687 | a way that it reduces to $False$ in all cases where a proof of $False$ is |
---|
688 | required. In the remaining case proof automation can be used to automatically |
---|
689 | find the proofs of absurdity. |
---|
690 | |
---|
691 | \subsection{Simulation (reduction + type checking)} |
---|
692 | \subsection{Examples} |
---|
693 | The weird function types redone |
---|
694 | \subsection{Subtyping as instantiation vs subtyping as safe static cast} |
---|
695 | Here we show/discuss how our approach supports both styles at once. |
---|
696 | \subsection{Solution to the expression problem, I} |
---|
697 | Using subtyping as cast, the file I have produced |
---|
698 | \subsection{Solution to the expression problem, II} |
---|
699 | Using subtyping as instantiation, comparisons, pros vs cons |
---|
700 | \subsection{Negative encoding (??)} |
---|
701 | The negative encoding and application to the expression problem |
---|
702 | \subsection{Other encodings (??)} |
---|
703 | Hints to other possible encodings |
---|
704 | |
---|
705 | \section{Extensible records (??)} |
---|
706 | |
---|
707 | \section{Comparison to related work and alternatives} |
---|
708 | \begin{itemize} |
---|
709 | \item Disjoint unions: drawbacks |
---|
710 | \item Encoding the unbounded case: drawbacks |
---|
711 | \end{itemize} |
---|
712 | |
---|
713 | \section{Appendix: interface of library functions used to implement everything} |
---|
714 | |
---|
715 | We will explain our technique with a simple running example: a trivial language of arithmetic including numeric literals and two binary operations corresponding to addition and multiplication. |
---|
716 | Our language is captured by the following inductive data type: |
---|
717 | \begin{lstlisting} |
---|
718 | inductive expression (E: Type[0]) : Type[0] := |
---|
719 | | Num : nat $\rightarrow$ expression E |
---|
720 | | Plus : E $\rightarrow$ E $\rightarrow$ expression E |
---|
721 | | Mul : E $\rightarrow$ E $\rightarrow$ expression E. |
---|
722 | \end{lstlisting} |
---|
723 | Here, \texttt{expression} is parameterised by a type, \texttt{E}. |
---|
724 | We will say more about this later. |
---|
725 | Paired with our inductive type representing the AST of natural number expressions, we have a type of tags: |
---|
726 | \begin{lstlisting} |
---|
727 | inductive tag_ : Type[0] := |
---|
728 | | num : tag_ |
---|
729 | | plus : tag_ |
---|
730 | | mul : tag_. |
---|
731 | \end{lstlisting} |
---|
732 | Tags, and the constructors of the inductive type they are shadowing, are kept in one-one correspondence with each other; for each constructor in the \texttt{expression} inductive type we have a single corresponding constructor in the \texttt{tag\_} inductive type, and \emph{vice versa}. |
---|
733 | |
---|
734 | On the \texttt{tag\_} inductive type, we define the `obvious' decidable equality function: |
---|
735 | \begin{lstlisting} |
---|
736 | definition eq_tag_: tag_ $\rightarrow$ tag_ $\rightarrow$ bool := |
---|
737 | $\lambda$t1, t2. |
---|
738 | match t1 with |
---|
739 | [ num $\Rightarrow$ |
---|
740 | match t2 with |
---|
741 | [ num $\Rightarrow$ true |
---|
742 | | _ $\Rightarrow$ false |
---|
743 | ] |
---|
744 | $\ldots$ |
---|
745 | ]. |
---|
746 | \end{lstlisting} |
---|
747 | Using \texttt{eq\_tag\_} we lift the \texttt{tag\_} inductive type into the Matita standard library's \texttt{DeqSet}. |
---|
748 | The \texttt{DeqSet} abstraction represents types with a decidable equality. |
---|
749 | Many generic functions in the Matita library are defined to work with this abstraction. |
---|
750 | The lifting is straightforward: |
---|
751 | \begin{lstlisting} |
---|
752 | definition tag : DeqSet := |
---|
753 | mk_DeqSet tag_ eq_tag ?. |
---|
754 | * * normalize /2/ % |
---|
755 | #abs destruct |
---|
756 | qed. |
---|
757 | \end{lstlisting} |
---|
758 | Here, \texttt{mk\_DeqSet} is the constructor of the \texttt{DeqSet} record. |
---|
759 | By convention in Matita, for a record type name \texttt{Foo}, there exists a constructor for that record type name \texttt{mk\_Foo}. |
---|
760 | We pass the constructor function three arguments: the type that possess a decidable equality---in this case \texttt{tag\_}---the equality function itself, and a proof that propositional equality and decidable equality co-incide for this type. |
---|
761 | In this case, the final argument to \texttt{mk\_DeqSet} is posed as a proof obligation (marked by `\texttt{?}'), which is closed via Matita's tactic interface below the definition. |
---|
762 | |
---|
763 | \bibliography{polymorphic-variants} |
---|
764 | |
---|
765 | \end{document} |
---|