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

Last change on this file since 2424 was 2424, checked in by mulligan, 7 years ago

Changes to the file including making a start on incorporating Garrigue's typing rules in to the paper. Also added prooftree.sty to get the paper to compile.

File size: 9.3 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{\ent}{\vdash}
13\newcommand{\funarr}{\rightarrow}
14\newcommand{\lam}[2]{\lambda{#1}.{#2}}
15\newcommand{\letin}[3]{\mathbf{let}\ {#1}\ {:=}\ {#2}\ \mathbf{in}\ {#3}}
16\newcommand{\pair}[2]{\langle #1, #2 \rangle}
17\newcommand{\rulefont}[1]{\ensuremath{(\mathbf{#1})}}
18
19\lstset{basicstyle=\footnotesize\tt,columns=flexible,breaklines=false,
20        keywordstyle=\color{red}\bfseries,
21        keywordstyle=[2]\color{blue},
22        commentstyle=\color{green},
23        stringstyle=\color{blue},
24        showspaces=false,showstringspaces=false,
25        xleftmargin=1em}
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
49Big 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
67In this section we will attempt to provide a self-contained \emph{pr\'ecis} of polymorphic variants for the unfamiliar reader.
68Those 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
70Most 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.
71Each algebraic data type may be described as a sum-of-products.
72The programmer provides a fixed number of distinct \emph{constructors} with each constructor expects a (potentially empty) product of arguments.
73Values of a given inductive data type are built using a data type's constructors.
74Quotidian data structures---such as lists, trees, heaps, zippers, and so forth---can all be introduced using this now familiar mechanism.
75
76Having 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.
77Functional languages almost uniformly employ \emph{pattern matching} for this task.
78Given 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.
79Using pattern matching we can therefore deconstruct algebraic data by performing a case analysis on the constructors of a given type.
80
81The combination of algebraic data types and pattern matching is powerful, and is arguably the main branching mechanism for most functional programming languages.
82Furthermore, 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
84Unfortunately, in practical programming, we often want to expand a previously defined algebraic data type, adding more constructors.
85When it comes to extending algebraic data types with new constructors in this way, we hit a problem: these types are `closed'.
86In 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
88\begin{figure}[ht]
89\begin{minipage}[b]{0.45\linewidth}
90\begin{lstlisting}
91data Term
92  = Lit Int
93  | Add Term Term
94  | Mul Term Term
95
96evaluate :: Term -> Int
97evaluate (Lit i)   = i
98evaluate (Add l r) = evaluate l + evaluate r
99evaluate (Mul l r) = evaluate l * evaluate r
100\end{lstlisting}
101\end{minipage}
102\hspace{0.5cm}
103\begin{minipage}[b]{0.45\linewidth}
104\begin{lstlisting}
105
106\end{lstlisting}
107\end{minipage}
108\label{fig.pattern-matching.vs.oop}
109\caption{A simple language of integer arithmetic embedded as an algebraic data type and as a class hierarchy.}
110\end{figure}
111
112We 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).
113In mainstream object-oriented languages such as Java algebraic data types correspond to interfaces, or some base object.
114Constructors correspond to classes implementing this interface; branching by pattern matching is emulated using the language's dynamic dispatch mechanism.
115The base interface of the object hierarchy specifies the permitted operations defined for the type.
116
117As all operations
118it is hard to enlarge the set of operations defined over a given type without altering the entire class hierarchy.
119If the interface changes so must every class implementing it.
120However, 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.
121
122[dpm: reword the above --- hard to phrase precisely ]
123
124
125\begin{itemize}
126 \item General introduction, motivations
127 \item Bounded vs not-bounded.
128\end{itemize}
129
130\begin{figure}
131\begin{gather*}
132\begin{prooftree}
133(\Gamma(x) = \phi)
134\justifies
135K; \Gamma \ent x : \phi
136\using\rulefont{{\Gamma}x}
137\end{prooftree}
138\qquad
139\begin{prooftree}
140K; \Gamma, x : \phi \ent r : \psi
141\justifies
142K; \Gamma \ent \lam{x}r : \phi \funarr \psi
143\using\rulefont{{\Gamma}\lambda}
144\end{prooftree}
145\qquad
146\begin{prooftree}
147K;\Gamma \ent r : \phi \funarr \psi \quad K;\Gamma \ent s : \phi
148\justifies
149K;\Gamma \ent rs : \psi
150\using\rulefont{{\Gamma}rs}
151\end{prooftree}
152\\[1.5ex]
153\begin{prooftree}
154K; \Gamma \ent r : \phi \quad K; \Gamma, x:\phi \ent s : \psi
155\justifies
156K; \Gamma \ent \letin{x}{r}{s} : \psi
157\using\rulefont{{\Gamma}{:=}}
158\end{prooftree}
159\qquad
160\begin{prooftree}
161(L \subseteq L' \quad H \subseteq H')
162\justifies
163K \oplus i_{{\geq \pair{L}{U}}} \ent i \geq \pair{L'}{H'}
164\using\rulefont{{K}i}
165\end{prooftree}
166\end{gather*}
167\caption{Garrigue's typing relation for polymorphic variants}
168\label{fig.garrigue.typing.relation}
169\end{figure}
170
171%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
172% Section
173%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
174\subsection{Matita}
175\label{subsect.matita}
176
177Matita~\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.
178Throughout this paper, all running examples are provided in Matita's proof script vernacular.
179This vernacular, similar to the syntax of OCaml or Coq, should be mostly straightforward.
180
181One possible source of confusion is our use of $?$ and $\ldots$, which correspond to a term, or terms, to be inferred automatically by unification, respectively.
182Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations.
183
184Matita
185
186\subsection{Subtyping as instantiation vs subtyping as safe static cast}
187
188\subsection{Syntax \& type checking rules}
189The ones of Guarrigue + casts, but also for the bounded case?
190Casts support both styles of subtyping.
191
192\subsection{Examples}
193The weird function types that only work in subtyping as instantiation
194
195\subsection{Solution to the expression problem}
196Our running example in pseudo-OCaml syntax
197
198\section{Bounded polymorphic variants via dependent types}
199Requirements (i.e. O(1) pattern-matching, natural extracted code, etc.)
200\subsection{Simulation (reduction + type checking)}
201\subsection{Examples}
202The weird function types redone
203\subsection{Subtyping as instantiation vs subtyping as safe static cast}
204Here we show/discuss how our approach supports both styles at once.
205\subsection{Solution to the expression problem, I}
206Using subtyping as cast, the file I have produced
207\subsection{Solution to the expression problem, II}
208Using subtyping as instantiation, comparisons, pros vs cons
209\subsection{Negative encoding (??)}
210The negative encoding and application to the expression problem
211\subsection{Other encodings (??)}
212Hints to other possible encodings
213
214\section{Extensible records (??)}
215
216\section{Comparison to related work and alternatives}
217\begin{itemize}
218 \item Disjoint unions: drawbacks
219 \item Encoding the unbounded case: drawbacks
220\end{itemize}
221
222\section{Appendix: interface of library functions used to implement everything}
223
224\bibliography{polymorphic-variants}
225
226\end{document}
Note: See TracBrowser for help on using the repository browser.