Changeset 2518

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


1 edited


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

    r2517 r2518  
    481481poor encodings that are generated by the syntactic universe.
     483\subsection{The encoding}
     484In order to encode bounded polymorphic variants in dependent type theory,
     485we encode 1) the universe; 2) the polymorphic variant types; 3) the
     486constructors of the polymorphic variant type; 4) the pattern matching operator;
     4875) an elimination proof principle for polymorphic variants. The pattern matching
     488operator and the elimination principle have the same behaviour, according to
     489the Curry-Howard isomorphism. We assume that the latter will be used to prove
     490statements without taking care of the computational content of the proof
     491(proof irrelevance). Thus only the pattern matching operator, and not the
     492elimination principle, will need to satisfy requirement 1.
     494The encoding is a careful mix of a deep and a shallow encodings, with user
     495provided connections between them. The shallow part of the encoding is there
     496for code extraction to satisfy requirements 1. In particular, the
     497shallow encoding of the universe is just an ordinary inductive type, which is
     498extracted to an algebraic type. The encoding of a polymorphic variant type is
     499just a $\Sigma$-type whose carrier is the universe, which is extracted
     500exactly as the universe (so satisfying requirement 2). The deep part of the
     501encoding allows to perform dependent computations on the list of fields that
     502are allowed in a polymorphic variant type. For example, from the list of fields
     503a dependently typed function can generate the type of the elimination principle.
     504The links between the two encodings are currently user provided, but it simple
     505to imagine a simple program that automates the task.
     507\begin{definition}[Universe encoding]
     508A 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
     509$T_1,\ldots,T_n$) is encoded by means of:
     511 \item Its shallow encoding, the corresponding inductive type
     512  $$inductive~u~(\alpha_1:Type[0],\ldots,\alpha_m:Type[0]) u : Type[0] :=
     513    K_1:T_1 \to u~\alpha_1~\ldots~\alpha_m ~|~ \ldots ~|~ K_n:T_n$ \to u~\alpha_1~\ldots~\alpha_m$$
     514 \item A disjoint sum (an inductive type) of names for the tags of $u$:
     515  $$inductive~tag_~ : Type[0] := k_1: tag_ ~|~ \ldots ~|~ k_n: tag_$$
     516 \item An equality test $eq_tag: tag_ \to tag_ \to bool$ that returns true
     517  iff the two tags are the same. This is boilerplate code that is often
     518  automatized by interactive theorem provers. We write $tag$ for the type
     519  the $tag_$ coupled with its decidable equality test $eq_tag$. This is just
     520  a minor technicality of no importance.
     521 \item A simple function $$tag_of_expr: \forall \alpha_1,\ldots,\alpha_m.
     522   u \alpha_1 \ldots \alpha_m \to  tag$$
     523   that performs a case analysis on the shallow encoding of a universe
     524   inhabitant and returns the name of the corresponding constructor.
     525   This boilerplate code is the bridge from the shallow to the deep
     526   encoding of the universe.
     527 \item A dual function that is the bridge from the deep to the shallow encoding.
     528   We
    484532\subsection{Simulation (reduction + type checking)}
Note: See TracChangeset for help on using the changeset viewer.