- Timestamp:
- Dec 3, 2012, 12:28:11 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/polymorphic-variants-2012/polymorphic-variants.tex
r2517 r2518 481 481 poor encodings that are generated by the syntactic universe. 482 482 483 \subsection{The encoding} 484 In order to encode bounded polymorphic variants in dependent type theory, 485 we encode 1) the universe; 2) the polymorphic variant types; 3) the 486 constructors of the polymorphic variant type; 4) the pattern matching operator; 487 5) an elimination proof principle for polymorphic variants. The pattern matching 488 operator and the elimination principle have the same behaviour, according to 489 the Curry-Howard isomorphism. We assume that the latter will be used to prove 490 statements without taking care of the computational content of the proof 491 (proof irrelevance). Thus only the pattern matching operator, and not the 492 elimination principle, will need to satisfy requirement 1. 493 494 The encoding is a careful mix of a deep and a shallow encodings, with user 495 provided connections between them. The shallow part of the encoding is there 496 for code extraction to satisfy requirements 1. In particular, the 497 shallow encoding of the universe is just an ordinary inductive type, which is 498 extracted to an algebraic type. The encoding of a polymorphic variant type is 499 just a $\Sigma$-type whose carrier is the universe, which is extracted 500 exactly as the universe (so satisfying requirement 2). The deep part of the 501 encoding allows to perform dependent computations on the list of fields that 502 are allowed in a polymorphic variant type. For example, from the list of fields 503 a dependently typed function can generate the type of the elimination principle. 504 The links between the two encodings are currently user provided, but it simple 505 to imagine a simple program that automates the task. 506 507 \begin{definition}[Universe encoding] 508 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 509 $T_1,\ldots,T_n$) is encoded by means of: 510 \begin{itemize} 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 529 \end{itemize} 530 \end{definition} 483 531 484 532 \subsection{Simulation (reduction + type checking)}
Note: See TracChangeset
for help on using the changeset viewer.