# Changeset 2518 for Papers

Ignore:
Timestamp:
Dec 3, 2012, 12:28:11 PM (9 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2517 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)}