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

\documentclass[smallextended]{svjour3}

\smartqed

\usepackage{amsmath}
\usepackage[english]{babel}
\usepackage[colorlinks]{hyperref}
\usepackage{listings}
\usepackage{microtype}
\usepackage{prooftree}

\newcommand{\cons}{{::}}
\newcommand{\ent}{\vdash}
\newcommand{\fall}[2]{\forall{#1}.#2}
\newcommand{\funarr}{\rightarrow}
\newcommand{\lam}[2]{\lambda{#1}.{#2}}
\newcommand{\letin}[3]{\mathbf{let}\ {#1}\ {:=}\ {#2}\ \mathbf{in}\ {#3}}
\newcommand{\match}[3]{\mathbf{match}\ #1\ \mathbf{with}\ #2\ \Rightarrow #3}
\newcommand{\pair}[2]{\langle #1, #2 \rangle}
\newcommand{\polytag}[1]{{`}#1}
\newcommand{\rulefont}[1]{\ensuremath{(\mathbf{#1})}}

\renewcommand{\verb}{\lstinline}
\def\lstlanguagefiles{lst-grafite.tex}
\lstset{language=Grafite}

\bibliographystyle{spphys}

\author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
\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.}}

\institute{
  Dominic P. Mulligan \at
  Computer Laboratory,\\
  University of Cambridge.
  \email{dominic.p.mulligan@gmail.com} \and
  Claudio Sacerdoti Coen \at
  Dipartimento di Scienze dell'Informazione,\\
  Universit\`a di Bologna.
  \email{sacerdot@cs.unibo.it}
}

\begin{document}

\maketitle

\begin{abstract}

Big long abstract introducing the work

\keywords{Polymorphic variants \and dependent type theory \and Matita theorem prover}

\end{abstract}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Section
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
\label{sect.introduction}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Section
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Polymorphic variants}
\label{sect.polymorphic.variants}

In this section we will attempt to provide a self-contained \emph{pr\'ecis} of polymorphic variants for the unfamiliar reader.
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}.

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.
Each algebraic data type may be described as a sum-of-products.
The programmer provides a fixed number of distinct \emph{constructors} with each constructor expects a (potentially empty) product of arguments.
Values of a given inductive data type are built using a data type's constructors.
Quotidian data structures---such as lists, trees, heaps, zippers, and so forth---can all be introduced using this now familiar mechanism.

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.
Functional languages almost uniformly employ \emph{pattern matching} for this task.
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.
Using pattern matching we can therefore deconstruct algebraic data by performing a case analysis on the constructors of a given type.

The combination of algebraic data types and pattern matching is powerful, and is arguably the main branching mechanism for most functional programming languages.
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.

Unfortunately, in practical programming, we often want to expand a previously defined algebraic data type, adding more constructors.
When it comes to extending algebraic data types with new constructors in this way, we hit a problem: these types are `closed'.
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.
This manual extension, coupled with the lifting of any existing functions into the new type, is cumbersome and error-prone.

\begin{figure}[ht]
\begin{minipage}[b]{0.45\linewidth}
\begin{lstlisting}
\lstset{language=haskell}
data Term
  = Lit Int
  | Add Term Term

eval :: Term -> Int
eval (Lit i)   = i
eval (Add l r) = eval l + eval r
\end{lstlisting}
\end{minipage}
\hspace{0.5cm}
\begin{minipage}[b]{0.45\linewidth}
\begin{lstlisting}
interface Term {
  int eval();
}

class Lit implements Term {
  private int v = 0;
  ...
  int eval() { return v; }
}

class Add implements Term {
  private Term left, right = null;
  ...
  int eval() {
    return left.eval() + right.eval();
  }
}
\end{lstlisting}
\end{minipage}
\label{fig.pattern-matching.vs.oop}
\caption{A simple language of integer arithmetic embedded as an algebraic data type and as a class hierarchy.}
\end{figure}

However, we can look abroad to see what other families of programming languages do to solve this problem.
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).
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.
The base interface of the object hierarchy specifies the permitted operations defined for the type.
Branching by pattern matching is emulated using the language's dynamic dispatch mechanism.

As all permitted operations on 
it is hard to enlarge the set of operations defined over a given type without altering the entire class hierarchy.
If the interface changes so must every class implementing it.
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.

\begin{figure}[ht]
\begin{minipage}[b]{0.45\linewidth}
\begin{lstlisting}
...
data Term'
  = Lift Term
  | Mul Term' Term'

eval' :: Term' -> Int
eval' (Lift t)  = eval t
eval' (Mul l r) = eval' l * eval ' r
\end{lstlisting}
\end{minipage}
\hspace{0.5cm}
\begin{minipage}[b]{0.45\linewidth}
\begin{lstlisting}
...
class Mul implements Term {
  private Term left, right = null;
  ...
  int eval() {
    return left.eval() * right.eval();
  }
}
\end{lstlisting}
\end{minipage}
\label{fig.extending.base.type}
\caption{Extending our simple language of arithmetic with a new grammatical element.}
\end{figure}

\begin{figure}[ht]
\begin{minipage}[b]{0.45\linewidth}
\begin{lstlisting}
...
show :: Term -> String
show (Lit i)   = show i
show (Add l r) =
  show l ++ " + " ++ show r
\end{lstlisting}
\end{minipage}
\hspace{0.5cm}
\begin{minipage}[b]{0.45\linewidth}
\begin{lstlisting}
interface Term {
  int eval();
  String show();
}

class Lit implements Term {
  private int v = 0;
  ...
  int eval() { return v; }
  String show() {
    return Int.toString(v);
  }
}

class Add implements Term {
  private Term left, right = null;
  ...
  int eval() {
    return left.eval() + right.eval();
  }
  ...
  String show() {
    return left.show() + \
      " + " + right.show();
  }
}
\end{lstlisting}
\end{minipage}
\label{fig.extending.base.type}
\caption{Extending the permitted operations over our simple language of arithmetic.}
\end{figure}

[dpm: reword the above --- hard to phrase precisely ]


\begin{itemize}
 \item General introduction, motivations
 \item Bounded vs not-bounded.
\end{itemize}

\begin{definition}
\label{defn.garrigues.calculus}
Inductively define a 
\end{definition}

\begin{figure}
\begin{gather*}
\begin{prooftree}
(\Gamma(x) = \sigma)
\justifies
K; \Gamma \ent x : \sigma
\using\rulefont{{\Gamma}x}
\end{prooftree}
\qquad
\begin{prooftree}
K; \Gamma, x : \phi \ent r : \psi
\justifies
K; \Gamma \ent \lam{x}r : \phi \funarr \psi
\using\rulefont{{\Gamma}\lambda}
\end{prooftree}
\qquad
\begin{prooftree}
K;\Gamma \ent r : \phi \funarr \psi \quad K;\Gamma \ent s : \phi
\justifies
K;\Gamma \ent rs : \psi
\using\rulefont{{\Gamma}rs}
\end{prooftree}
\\[1.5ex]
\begin{prooftree}
K; \Gamma \ent r : \sigma \quad K; \Gamma, x:\sigma \ent s : \psi
\justifies
K; \Gamma \ent \letin{x}{r}{s} : \psi
\using\rulefont{{\Gamma}{:=}}
\end{prooftree}
\qquad
\begin{prooftree}
K;\Gamma \ent r : \sigma \quad (a \not\in ftv(\Gamma))
\justifies
K;\Gamma \ent r : \fall{a}{\sigma}
\using\rulefont{{\Gamma}{\forall}{a}}
\end{prooftree}
\\[1.5ex]
\begin{prooftree}
K;\Gamma \ent r : \fall{a}{\sigma} \quad K;\Gamma \ent s : \psi
\justifies
K;\Gamma \ent rs : \sigma[a := \psi]
\using\rulefont{{\Gamma}inst{a}}
\end{prooftree}
\\[1.5ex]
\begin{prooftree}
(L \subseteq L' \quad H \subseteq H')
\justifies
K \oplus i_{{\geq \pair{L}{U}}} \ent i \geq \pair{L'}{H'}
\using\rulefont{{K}i}
\end{prooftree}
\qquad
\begin{prooftree}
K;\Gamma \ent r : \phi \quad K \ent i \geq \pair{tag}{\top}
\justifies
K;\Gamma \ent \polytag{tag(r)} : [ i \mid tag : \phi \cons T ]
\using\rulefont{{K}variant}
\end{prooftree}
\\[1.5ex]
\begin{prooftree}
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
K;\Gamma, x_k : \phi_k \ent r_k : \psi \quad (1 \leq k \leq n)
\justifies
K;\Gamma \ent \mathbf{match}\ r\ \mathbf{with}\ \{ \polytag{tag_k(x_k)} \Rightarrow r_k \}^n_1 : \psi
\using\rulefont{{K}match}
\end{prooftree}
\\[1.5ex]
\begin{prooftree}
K;\Gamma \ent r : \sigma \quad (\rho \not\in ftv(\Gamma))
\justifies
K;\Gamma \ent r : \fall{\rho}{\sigma}
\using\rulefont{{K}{\forall}{\rho}}
\end{prooftree}
\qquad
\begin{prooftree}
K;\Gamma \ent r : \fall{\rho}{\sigma} \quad K;\Gamma \ent s : T
\justifies
K;\Gamma \ent rs : \sigma[\rho := T]
\using\rulefont{{K}inst{\rho}}
\end{prooftree}
\\[1.5ex]
\begin{prooftree}
K \oplus i_{\geq \pair{L}{U}};\Gamma \ent r : \sigma
\justifies
K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma}
\using\rulefont{{K}{\forall}{i}}
\end{prooftree}
\qquad
\begin{prooftree}
K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma} \quad K \ent i' \geq \pair{L, U}
\justifies
K;\Gamma \ent r : \sigma[i := i']
\using\rulefont{{K}inst{i}}
\end{prooftree}
\end{gather*}
\caption{Garrigue's typing relation for polymorphic variants}
\label{fig.garrigue.typing.relation}
\end{figure}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Section
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Matita}
\label{subsect.matita}

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.
Throughout this paper, all running examples are provided in Matita's proof script vernacular.
This vernacular, similar to the syntax of OCaml or Coq, should be mostly straightforward.

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.
Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations.

\subsection{Subtyping as instantiation \emph{vs} subtyping as a safe static cast}

\subsection{Syntax and type checking rules}
The ones of Guarrigue + casts, but also for the bounded case?
Casts support both styles of subtyping.

\subsection{Examples}
The weird function types that only work in subtyping as instantiation

\subsection{Solution to the expression problem}
Our running example in pseudo-OCaml syntax

\section{Bounded polymorphic variants via dependent types}
The topic of this paper, and this section in particular, is to present an
\emph{encoding} of a subclass of polymorphic variants into dependent type
theory. The final aim is to provide a solution to the expression problem
that is implementable in user space into interactive theorem provers
based on dependent type theories, in particular Coq, Agda and Matita.
Moreover, we are only interested into an encoding that satisfies a number
of constraints listed below. Essentially, the constraints ask that code
automatically extracted from the system should be compiled efficiently
without any change to the extraction machine. The encoding has been tested
in the interactive theorem prover Matita, but we believe that it should be
easily ported to the other cited systems.

\subsection{Code extraction}
Since our requirements have code extraction in mind, we briefly recall here
what code extraction is in our context.

Code extraction, as implemented in Coq, Matita and other systems, is the
procedure that, given a proof term, extracts a program in a functional
programming language that implements the computational content of the proof
term. In particular, all proof parts that only establish correctness of the
answer, totality of functions, etc. are to be erased. In particular, given
a precondition $P$ and a postcondition $Q$, from a
constructive proof of a $\forall x:A.P(x) \to \exists y:B. Q(x,y)$ statement
one extracts a (partial) function $f$ from the encoding of $A$ to the encoding
of $B$ that satisfies $\forall x. P(x) \to Q(x,f(x))$.

Code extraction, as implemented by the above systems, does not attempt any
optimization of the representation of data types. The only modification allowed
is that parts of the data that are propositional and thus bare no content
(being isomorphic to the unit type) are simplified to the unit type and
possibly completely erased using the categorical properties of unit types
($1 * T \simeq T$, $1 \to T \simeq T$, etc.). For more information, one can
read~\cite{berardi,christine-mohring,letouzey}.

Thus, if a polymorphic variant is encoded in type theory as an n-ary sum of
n-ary products, these being inefficiently represented using binary sums and
products, the same holds for the extracted code.

\subsection{The requirements}

We list the following requirements.
\begin{enumerate}
 \item The representation of a polymorphic variant type in the extracted code
   should be as efficient, in memory and time, as the isomorphic inductive
   type. Efficiency should here be considered up to constants, and not
   asymptotic.
 \item Polymorphic types in the subtyping relation should be encoded using
   data types that, once extracted, are in the subtyping relation too.
   Before code extraction, instead, it is allowed to use explicit non identity
   functions to coerce inhabitants of the sub-type into the super-type.
   What matters is that the computational content of these coercions should be
   the identity.
\end{enumerate}
The first requirements prevents the encoding of polymorphic variants
using binary sums and products. For example, a constructor of an inductive
type with four constructors requires one memory cell, but the same constructor
for a binary sum of binary sums requires two memory cells, and twice the time
to inhabit the data type. The solution is to force the code extracted from the
polymorphic variant $\tau$ to be an inductive type. In turn this forces the
encoding of polymorphic variants to be based on inductive types.

The second requirement is in contrast with the possibility to extend a
polymorphic variant type: when a type $\tau$ is extended to $\tau + a:T$,
an inhabitant of the extraction of $\tau$ should already be an inhabitant of
the extraction of $\tau + a:T$. This is possible if polymorphic variants were
extracted to polymorphic variants in the target language, but this is not
actually the case in any of the considered systems (e.g. Coq or Matita).
Indeed, because of the first requirement, $\tau$ and $\tau + a:T$ are to be
extracted to two inductive types. The only way to obtain subtyping is to
already use the same representation: we need to anticipate or \emph{bound}
the extension.

Thus we accept the following limitation, together with an additional requirement
to mitigate the limitation:
\begin{enumerate}
 \item[3] We only encode \emph{bounded polymorphic variants}, whose typing
  rules are given in Figure~\ref{???}.
 \item[4] Bounded polymorphic variants are characterized by a universe, i.e.
  a set of fields together with their type. Every bounded polymorphic variant
  is a sub-variant of the universe, obtained by selecting only certain fields.
  We ask that adding a new field to the universe should have no impact on
  pre-existing code that does not use it. More precisely, it should be possible
  to add a field to the universe and recompile all pre-existing developments
  without further modifications.
\end{enumerate}

\subsection{Discussion on the requirements and alternative approaches}
The set of requirements we have imposed drastically restrict the set of possible
solutions for the encoding. Moreover, they clearly represent a trade off between
flexibility and efficiency. We discuss here alternative approaches based on
different set of requirements.

Maximal flexibility is only obtained dropping the boundedness limitation.
One of the benefits or open polymorphic variants is separate compilation:
the developers of libraries can use their own set of constructors and the
user can freely mix them when the types of the different fields are coherent.
Moreover, separate compilation can be made efficient if one accepts that
correct programs can be rejected with very low probability at linking
time~\cite{guarriguexxx}.

Requirement 4 has been imposed to recover the flexibility of open variants.
Suppose that every library starts with a file that declares its own universe.
Then, to mix two libraries, one needs to merge the two universe declarations
together, which is only possible if the universes are coherent. Once this is
done, the library files will keep compiling because of the requirement. What
is irremediably lost is separate compilation. We believe that this loss can
be withstood in many practical situations, because 1) merging of different
libraries that need to share at least some constructor is rare and needs to
be done just once; 2) the addition of new fields to the universe of a library
under development usually requires a significant effort to fix the library that
should make the recompilation time of the other libraries negligible.

If separate compilation is considered fundamental, then the only possible
approach seems that of introducing a syntactic data type (a universe) of
descriptions of polymorphic variants type, which is then interpreted by
dependent functions (type formers) to the appropriate sums of types.
The problem, generalized to that of giving a universe to the full syntax of
inductive types, is being studied by the groups of Altenkirch and
Ghani~\cite{aa,bb,cc,dd}. This approach, which is mathematically
very elegant, is in conflict with requirements 1 and 2. The conflict can be
solved by devising an ad-hoc extraction procedure which targets a programming
language that already implements polymorphic variants efficiently. As far as
we know, this has not been done yet. The next generation of Epigram, however,
is supposed to be implemented around this idea. Instead of an ad-hoc extraction
procedure, Epigram will be directly compiled to executable code, optimizing the
poor encodings that are generated by the syntactic universe.

\subsection{The encoding}
In order to encode bounded polymorphic variants in dependent type theory,
we encode 1) the universe; 2) the polymorphic variant types; 3) the
constructors of the polymorphic variant type; 4) the pattern matching operator;
5) an elimination proof principle for polymorphic variants. The pattern matching
operator and the elimination principle have the same behaviour, according to
the Curry-Howard isomorphism. We assume that the latter will be used to prove
statements without taking care of the computational content of the proof
(proof irrelevance). Thus only the pattern matching operator, and not the
elimination principle, will need to satisfy requirement 1.

The encoding is a careful mix of a deep and a shallow encodings, with user
provided connections between them. The shallow part of the encoding is there
for code extraction to satisfy requirements 1. In particular, the
shallow encoding of the universe is just an ordinary inductive type, which is
extracted to an algebraic type. The encoding of a polymorphic variant type is
just a $\Sigma$-type whose carrier is the universe, which is extracted
exactly as the universe (so satisfying requirement 2). The deep part of the
encoding allows to perform dependent computations on the list of fields that
are allowed in a polymorphic variant type. For example, from the list of fields
a dependently typed function can generate the type of the elimination principle.
The links between the two encodings are currently user provided, but it simple
to imagine a simple program that automates the task.

\begin{definition}[Universe encoding]
A parametric universe
$$(\alpha_1,\ldots,\alpha_m) u := K_1:T_1 ~|~ \ldots ~|~ K_n:T_n$$
(where $\alpha_1,\ldots, \alpha_m$ are type variables bound in
$T_1,\ldots,T_n$) is encoded by means of:
\begin{itemize}
 \item Its shallow encoding, the corresponding inductive type
  $$inductive~u~(\alpha_1:Type[0],\ldots,\alpha_m:Type[0]) u : Type[0] :=
    K_1:T_1 \to u~\alpha_1~\ldots~\alpha_m ~|~ \ldots ~|~ K_n:T_n \to u~\alpha_1~\ldots~\alpha_m$$
 \item A disjoint sum (an inductive type) of names for the tags of $u$:
  $$inductive~tag\_~ : Type[0] := k_1: tag\_ ~|~ \ldots ~|~ k_n: tag\_$$
 \item An equality test $eq\_tag: tag\_ \to tag\_ \to bool$ that returns true
  iff the two tags are equal. This is boilerplate code that is often
  automatized by interactive theorem provers. We write $tag$ for the type
  the $tag\_$ coupled with its decidable equality test $eq\_tag$ and
  a user provided proof that $\forall x,y:tag. eq\_tag x y = true \iff x=y$.
 \item A simple function $$tag\_of\_expr: \forall \alpha_1,\ldots,\alpha_m.
   u \alpha_1 \ldots \alpha_m \to  tag$$
   that performs a case analysis on the shallow encoding of a universe
   inhabitant and returns the name of the corresponding constructor.
   This boilerplate code is the bridge from the shallow to the deep
   encoding of the universe.
 \item A type former
   $$Q\_holds\_for\_tag: \forall \alpha_1,\ldots,\alpha_m.
      \forall Q: u~\alpha_1~\ldots~\alpha_n \to Prop.
       \forall t:tag. Prop$$
   that performs pattern matching over the tag and returns the proof obligation
   for the proof of $Q$ in the case corresponding to the tag.
 \item A proof of exhaustivity of pattern matching over the tag. This
   boilerplate proof is the bridge from the deep to the shallow encoding of the
   universe. The statement is:
   $$Q\_holds\_for\_tag\_spec:
    \forall \alpha_1,\ldots,\alpha_m.
     \forall Q: u~\alpha_1~\ldots~\alpha_m \to Prop.
      \forall x: u~\alpha_1~\ldots~\alpha_m.
       Q\_holds\_for\_tag~\ldots~Q~\ldots~(tag\_of\_expr~\ldots~x) \to Q x$$
\end{itemize}
\end{definition}

\begin{example}[The universe for our running example]
The following lines of Matita code implement the universe encoding for our
running example. They constitute the file~\texttt{test.ma}.
\begin{lstlisting}
inductive expr (E: Type[0]) : Type[0] ≝
   Num : nat -> expr E
 | Plus : E -> E -> expr E
 | Mul : E -> E -> expr E.

inductive tag_ : Type[0] := num : tag_ | plus : tag_ | mul : tag_.

definition eq_tag : tag_ -> tag_ -> bool :=
 λt1,t2.
  match t1 with
  [ num => match t2 with [num => true | _ => false]
  | plus => match t2 with [plus => true | _ => false]
  | mul => match t2 with [mul => true | _ => false]].

definition tag : DeqSet ≝ mk_DeqSet tag_ eq_tag ?.
 ** normalize /2/ % #abs destruct
qed.

definition tag_of_expr : ∀E:Type[0]. expr E -> tag :=
 λE,e.
   match e with
   [ Num _ => num
   | Plus _ _ => plus
   | Mul _ _ => mul ].

definition Q_holds_for_tag:
 ∀E:Type[0]. ∀Q: expr E → Prop. ∀t:tag. Prop ≝
 λE,Q,t.
  match t with
    [ num  ⇒ ∀n.   Q (Num … n)
    | plus ⇒ ∀x,y. Q (Plus … x y)
    | mul  ⇒ ∀x,y. Q (Mul … x y)
    ].

theorem Q_holds_for_tag_spec:
 ∀E:Type[0]. ∀Q: expr E → Prop.
  ∀x: expr E. Q_holds_for_tag … Q … (tag_of_expr … x) → Q x.
#E #Q * normalize //
qed.
\end{lstlisting}
\end{example}

We are now ready to lift the universe encoding to the encoding of polymorphic
variant types, constructors, case analysis and elimination principle.

The idea consists in following quite litteraly the description of the syntax
of bounded polymorphic variants: a bounded polymorphic variant is deeply
encoded by the list of constructors that are allowed. Row polymorphism is
achieved by quantifying over the list, which can be bounded from above and
below using normal hypotheses. A dependently typed semantic function coerces
the deep encoding to the shallow one, that we will soon describe. We will
handle the function has an implicit coercion, so that we will simply write
$i$ to represent both the list of tag names $i$ and the type former which is
the polymorphic variant type described by $i$. The context always allow to
disambiguate between the two uses and insert the coercion every time that
a list $i$ is used in a type former.
For example, the list $[num;plus]$ for our
running example will represent the polymorphic variant type
$[i_{\geq \pair{[num;plus]}{[num;plus]}}]$ and a function that expects at
least $num$ but that does not handle $mul$ will be typed as either
$f : \forall E. \forall i. [num] \subseteq i \subseteq [num;plus] \to i~E \to \ldots$
or $f: \forall E. \forall i. i \subseteq [plus] \to (num::i)~E \to \ldots$.

We defined the shallow encoding of the bounded polymorphic variant type
specified by a list $i$ of constructors as a $\Sigma$-type whose carrier
is the universe data type $u$ and whose property rules out all constructors
whose tag is not in $i$. Code extraction will simplify the $\Sigma$-type to
its carrier, satisfying both requirements 1 and 2.

\begin{definition}[Polymorphic variant type encoding]
A bounded polymorphic variant $i$ where $i_{\geq \pair{L}{U}}$ is deeply encoded
by a variable $i$ of type list of tags ($i: list~tag$) under the hypothesis
that $L \subseteq i \subseteq U$.
The corresponding shallow encoding is
$\Sigma x:u~\alpha_1~\ldots~\alpha_n. tag\_of\_expr \ldots x \in i$.
An implicit coercion maps $i : list~tag \mapsto \Sigma x:u~\alpha_1~\ldots~\alpha_n. tag\_of\_expr \ldots x \in i$.
\end{definition}

Subtyping is not necessary for polymorphic variants \`a la Guarrigue~\cite{???}:
the slogan, borrowed by~\cite{???}, is \emph{structural subtyping as
instantitation}.
Subtyping as instantiation fits very well with the Hindley-Milner type system
because it supports type inference. Since we work with a type system more
expressive than Hindley-Milner where type inference is undecidable, we are
not restricted to subtyping as instantiation, but we can also exploit the
natural subtyping rule between polymorphic variants types~\ref{???}.

\begin{definition}[Subtyping]
There exists a coercion of type
$\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
 i_2~\alpha_1~\ldots~\alpha_n$
\end{definition}
In the encoding of the universe we required an equality test over tags.
The test is exploited here to implement a computational version of the
$\subseteq$ relation between list of tags. I.e. it is possible to define
$\subseteq$ in such a way that for closed terms $i_1$ and $i_2$,
$i_1 \subseteq i_2$ reduces to $True$. As we will see, this suggests a different
style where polymorphic variant types are represented using the less number
of row quantifications and type membership and subtyping are automatically
decided by mere computation, without any user intervention.

The subtyping coercion takes apart the inhabitant of the polymorphic variant
$i_1$, obtaining both an inhabitant $x$ of the universe and a proof that its
constructors are all in $i_1$. Then it builds an inhabitant of the polymorphic
variant $i_2$ by coupling $x$ with the proof that all of its constructors are
in $i_2 \superseteq i_1$. The computational content of the coercion is just
the identity function and code extraction erases it: requirement 2 is satisfied.

\begin{definition}[Constructor encoding]
A constructor $K_i : T_i \to u~\alpha_1~\ldots~\alpha_m$ of the universe is
lifted to a polymorphic variant constructor
$T_i \to i~\alpha_1~\ldots~\alpha_m$ when
$\forall x:T_i.  tag\_of\_expr (K_i x) \in i$.
The lifting is obtained by inhabiting the sigma type
$\Sigma x:u~\alpha_1~\ldots~\alpha_n. tag\_of\_expr \ldots x \in i$
with a pair whose first component is the applied constructor and the second
component the proof of the condition above.
\end{definition}
We can exploit again the equality test over tag types to implement a
computational version of the predicate $tag\_of\_expr (K_i x) \in i$.
Therefore, when $i$ is a closed term, all tests reduce to $True$.
Matita implements a generalized system of coercions that allow to declare
the lifting of polymorphic variant as an implicit coercion. Since the coercion
requires a proof of the condition, a new proof obligation is opened.
The proof obligation is just $True$ when $i$ is closed.

The computational content of the lifted constructor is just the identity
function: the $n$-th constructor of a polymorphic variant type is represented
after code extraction by the $n$-th constructor of the unvierse inductive type,
satisfying requirement 1.

\subsection{Simulation (reduction + type checking)}
\subsection{Examples}
The weird function types redone
\subsection{Subtyping as instantiation vs subtyping as safe static cast}
Here we show/discuss how our approach supports both styles at once.
\subsection{Solution to the expression problem, I}
Using subtyping as cast, the file I have produced
\subsection{Solution to the expression problem, II}
Using subtyping as instantiation, comparisons, pros vs cons
\subsection{Negative encoding (??)}
The negative encoding and application to the expression problem
\subsection{Other encodings (??)}
Hints to other possible encodings

\section{Extensible records (??)}

\section{Comparison to related work and alternatives}
\begin{itemize}
 \item Disjoint unions: drawbacks
 \item Encoding the unbounded case: drawbacks
\end{itemize}

\section{Appendix: interface of library functions used to implement everything}

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.
Our language is captured by the following inductive data type:
\begin{lstlisting}
inductive expression (E: Type[0]) : Type[0] :=
 | Num : nat $\rightarrow$ expression E
 | Plus : E $\rightarrow$ E $\rightarrow$ expression E
 | Mul : E $\rightarrow$ E $\rightarrow$ expression E.
\end{lstlisting}
Here, \texttt{expression} is parameterised by a type, \texttt{E}.
We will say more about this later.
Paired with our inductive type representing the AST of natural number expressions, we have a type of tags:
\begin{lstlisting}
inductive tag_ : Type[0] :=
  | num : tag_ 
  | plus : tag_ 
  | mul : tag_.
\end{lstlisting}
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}.

On the \texttt{tag\_} inductive type, we define the `obvious' decidable equality function:
\begin{lstlisting}
definition eq_tag_: tag_ $\rightarrow$ tag_ $\rightarrow$ bool :=
  $\lambda$t1, t2.
    match t1 with
    [ num $\Rightarrow$
      match t2 with
      [ num $\Rightarrow$ true
      | _ $\Rightarrow$ false
      ]
    $\ldots$
    ].
\end{lstlisting}
Using \texttt{eq\_tag\_} we lift the \texttt{tag\_} inductive type into the Matita standard library's \texttt{DeqSet}.
The \texttt{DeqSet} abstraction represents types with a decidable equality.
Many generic functions in the Matita library are defined to work with this abstraction.
The lifting is straightforward:
\begin{lstlisting}
definition tag : DeqSet :=
  mk_DeqSet tag_ eq_tag ?.
  * * normalize /2/ %
  #abs destruct
qed.
\end{lstlisting}
Here, \texttt{mk\_DeqSet} is the constructor of the \texttt{DeqSet} record.
By convention in Matita, for a record type name \texttt{Foo}, there exists a constructor for that record type name \texttt{mk\_Foo}.
We pass the constructor function three arguments: the type that possess a decidable equality, in this case \texttt{tag\_}

\bibliography{polymorphic-variants}

\end{document}