1 | \documentclass[smallextended]{svjour3} |
---|
2 | |
---|
3 | \smartqed |
---|
4 | |
---|
5 | \usepackage[english]{babel} |
---|
6 | \usepackage[colorlinks]{hyperref} |
---|
7 | \usepackage{microtype} |
---|
8 | |
---|
9 | |
---|
10 | \author{Dominic P. Mulligan \and Claudio Sacerdoti Coen} |
---|
11 | \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.}} |
---|
12 | |
---|
13 | \institute{ |
---|
14 | Dominic P. Mulligan \at |
---|
15 | Computer Laboratory,\\ |
---|
16 | University of Cambridge. |
---|
17 | \email{dominic.p.mulligan@gmail.com} \and |
---|
18 | Claudio Sacerdoti Coen \at |
---|
19 | Dipartimento di Scienze dell'Informazione,\\ |
---|
20 | Universit\`a di Bologna. |
---|
21 | \email{sacerdot@cs.unibo.it} |
---|
22 | } |
---|
23 | |
---|
24 | \begin{document} |
---|
25 | |
---|
26 | \maketitle |
---|
27 | |
---|
28 | \begin{abstract} |
---|
29 | |
---|
30 | Big long abstract introducing the work |
---|
31 | |
---|
32 | \keywords{Polymorphic variants \and dependent type theory \and Matita theorem prover} |
---|
33 | |
---|
34 | \end{abstract} |
---|
35 | |
---|
36 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
37 | % Section |
---|
38 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
39 | \section{Introduction} |
---|
40 | \label{sect.introduction} |
---|
41 | |
---|
42 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
43 | % Section |
---|
44 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
---|
45 | \section{Polymorphic variants} |
---|
46 | \label{sect.polymorphic.variants} |
---|
47 | |
---|
48 | In this section we provide a self-contained \emph{pr\'ecis} of polymorphic variants. |
---|
49 | For a more complete summary, we refer the reader to Garrigue's publications on the subject~\cite{dpm: todo}. |
---|
50 | |
---|
51 | Most mainstream functional programming languages, such as OCaml and Haskell, have mechanisms for inductively defining types through the use of \emph{algebraic data types}. |
---|
52 | Each algebraic data type can be described as a sum-of-products, wherein we associate a fixed number of distinct \emph{constructors} to the type being introduced, all of whom expect a product of arguments. |
---|
53 | Inductive data, modelled as an algebraic data type, is built incrementally from the ground-up using the constructors of that type. |
---|
54 | Quotidian data structures---such as lists, trees, heaps, zippers, and so forth---can all be introduced using this now familiar mechanism. |
---|
55 | |
---|
56 | Having built data using constructors, to complete the picture we now need some facility for picking said data apart. |
---|
57 | Functional languages employ \emph{pattern matching} for this task. |
---|
58 | Given any inhabitant of an inductive type, by the aforementioned sum-of-products property, we know that it must consist of some constructor of that type applied to various arguments. |
---|
59 | Using pattern matching we can therefore deconstruct algebraic data by performing a case analysis on the constructors of a given type. |
---|
60 | |
---|
61 | The combination of algebraic data types and pattern matching is powerful, and is arguably the main branching mechanism for most functional programming languages. |
---|
62 | Further, 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 unbounded. |
---|
63 | Unfortunately, when it comes to extending algebraic data types with new constructors these types are essentially `closed'. |
---|
64 | We cannot simply extend an algebraic type with a new constructor. |
---|
65 | We must introduce a new algebraic type with the additional constructor, lifting the old type---and any functions defined over it---into this type. |
---|
66 | |
---|
67 | Moving sideways, we can compare and contrast functional programming languages' use of algebraic data paired with pattern matching with the approach taken by object-oriented languages. |
---|
68 | In mainstream object-oriented languages such as Java algebraic data types correspond to class hierarchies, each constructor corresponding to a subclass in this hierarchy. |
---|
69 | Pattern matching is emulated using a dynamic dispatch mechanism. |
---|
70 | Using the object-oriented approach it is easy to add a new `case' to a given hierarchy: just introduce a new subclass. |
---|
71 | |
---|
72 | [dpm: reword the above --- hard to phrase precisely ] |
---|
73 | |
---|
74 | |
---|
75 | \begin{itemize} |
---|
76 | \item General introduction, motivations |
---|
77 | \item Bounded vs not-bounded. |
---|
78 | \end{itemize} |
---|
79 | |
---|
80 | \subsection{Subtyping as instantiation vs subtyping as safe static cast} |
---|
81 | |
---|
82 | \subsection{Syntax \& type checking rules} |
---|
83 | The ones of Guarrigue + casts, but also for the bounded case? |
---|
84 | Casts support both styles of subtyping. |
---|
85 | |
---|
86 | \subsection{Examples} |
---|
87 | The weird function types that only work in subtyping as instantiation |
---|
88 | |
---|
89 | \subsection{Solution to the expression problem} |
---|
90 | Our running example in pseudo-OCaml syntax |
---|
91 | |
---|
92 | \section{Bounded polymorphic variants via dependent types} |
---|
93 | Requirements (i.e. O(1) pattern-matching, natural extracted code, etc.) |
---|
94 | \subsection{Simulation (reduction + type checking)} |
---|
95 | \subsection{Examples} |
---|
96 | The weird function types redone |
---|
97 | \subsection{Subtyping as instantiation vs subtyping as safe static cast} |
---|
98 | Here we show/discuss how our approach supports both styles at once. |
---|
99 | \subsection{Solution to the expression problem, I} |
---|
100 | Using subtyping as cast, the file I have produced |
---|
101 | \subsection{Solution to the expression problem, II} |
---|
102 | Using subtyping as instantiation, comparisons, pros vs cons |
---|
103 | \subsection{Negative encoding (??)} |
---|
104 | The negative encoding and application to the expression problem |
---|
105 | \subsection{Other encodings (??)} |
---|
106 | Hints to other possible encodings |
---|
107 | |
---|
108 | \section{Extensible records (??)} |
---|
109 | |
---|
110 | \section{Comparison to related work and alternatives} |
---|
111 | \begin{itemize} |
---|
112 | \item Disjoint unions: drawbacks |
---|
113 | \item Encoding the unbounded case: drawbacks |
---|
114 | \end{itemize} |
---|
115 | |
---|
116 | \section{Appendix: interface of library functions used to implement everything} |
---|
117 | |
---|
118 | \end{document} |
---|