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

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

Changes to Section 2.

File size: 5.9 KB
Line 
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
30Big 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
48In this section we provide a self-contained \emph{pr\'ecis} of polymorphic variants.
49For a more complete summary, we refer the reader to Garrigue's publications on the subject~\cite{dpm: todo}.
50
51Most mainstream functional programming languages, such as OCaml and Haskell, have mechanisms for inductively defining types through the use of \emph{algebraic data types}.
52Each 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.
53Inductive data, modelled as an algebraic data type, is built incrementally from the ground-up using the constructors of that type.
54Quotidian data structures---such as lists, trees, heaps, zippers, and so forth---can all be introduced using this now familiar mechanism.
55
56Having built data using constructors, to complete the picture we now need some facility for picking said data apart.
57Functional languages employ \emph{pattern matching} for this task.
58Given 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.
59Using pattern matching we can therefore deconstruct algebraic data by performing a case analysis on the constructors of a given type.
60
61The combination of algebraic data types and pattern matching is powerful, and is arguably the main branching mechanism for most functional programming languages.
62Further, 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.
63Unfortunately, when it comes to extending algebraic data types with new constructors these types are essentially `closed'.
64We cannot simply extend an algebraic type with a new constructor.
65We must introduce a new algebraic type with the additional constructor, lifting the old type---and any functions defined over it---into this type.
66
67Moving 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, or extending the root object.
68In mainstream object-oriented languages such as Java algebraic data types correspond to interfaces, or some base object.
69Constructors correspond to classes implementing this interface; pattern matching is emulated using the language's dynamic dispatch mechanism.
70The interface specifies the permitted operations defined for the type.
71In contrast to the functional approach, it is hard to enlarge the set of operations defined over a given type without altering the entire class hierarchy.
72If the interface changes so must every class implementing it.
73However, 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.
74
75[dpm: reword the above --- hard to phrase precisely ]
76
77
78\begin{itemize}
79 \item General introduction, motivations
80 \item Bounded vs not-bounded.
81\end{itemize}
82
83\subsection{Subtyping as instantiation vs subtyping as safe static cast}
84
85\subsection{Syntax \& type checking rules}
86The ones of Guarrigue + casts, but also for the bounded case?
87Casts support both styles of subtyping.
88
89\subsection{Examples}
90The weird function types that only work in subtyping as instantiation
91
92\subsection{Solution to the expression problem}
93Our running example in pseudo-OCaml syntax
94
95\section{Bounded polymorphic variants via dependent types}
96Requirements (i.e. O(1) pattern-matching, natural extracted code, etc.)
97\subsection{Simulation (reduction + type checking)}
98\subsection{Examples}
99The weird function types redone
100\subsection{Subtyping as instantiation vs subtyping as safe static cast}
101Here we show/discuss how our approach supports both styles at once.
102\subsection{Solution to the expression problem, I}
103Using subtyping as cast, the file I have produced
104\subsection{Solution to the expression problem, II}
105Using subtyping as instantiation, comparisons, pros vs cons
106\subsection{Negative encoding (??)}
107The negative encoding and application to the expression problem
108\subsection{Other encodings (??)}
109Hints to other possible encodings
110
111\section{Extensible records (??)}
112
113\section{Comparison to related work and alternatives}
114\begin{itemize}
115 \item Disjoint unions: drawbacks
116 \item Encoding the unbounded case: drawbacks
117\end{itemize}
118
119\section{Appendix: interface of library functions used to implement everything}
120
121\end{document}
Note: See TracBrowser for help on using the repository browser.