Changeset 2518 for Papers/polymorphic-variants-2012/polymorphic-variants.tex

Timestamp:

Dec 3, 2012, 12:28:11 PM (7 years ago)

Author:

sacerdot

Message:

...

File:

• Papers/polymorphic-variants-2012/polymorphic-variants.tex (modified) (1 diff)

Papers/polymorphic-variants-2012/polymorphic-variants.tex

@@ -481 +481 @@
 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 the same. 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$. This is just
+  a minor technicality of no importance.
+ \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 dual function that is the bridge from the deep to the shallow encoding.
+   We 
+\end{itemize}
+\end{definition}
 
 \subsection{Simulation (reduction + type checking)}