Changeset 2525
 Timestamp:
 Dec 3, 2012, 5:39:42 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/polymorphicvariants.tex
r2524 r2525 540 540 541 541 \begin{example}[The universe for our running example] 542 The following lines of Matita code implement the universe encoding for our 543 running example. They constitute the file~\texttt{test.ma}. 542 544 \begin{lstlisting} 543 545 inductive expr (E: Type[0]) : Type[0] ≝ … … 582 584 \end{lstlisting} 583 585 \end{example} 586 587 We are now ready to lift the universe encoding to the encoding of polymorphic 588 variant types, constructors, case analysis and elimination principle. 589 590 The idea consists in following quite litteraly the description of the syntax 591 of bounded polymorphic variants: a bounded polymorphic variant is deeply 592 encoded by the list of constructors that are allowed. Row polymorphism is 593 achieved by quantifying over the list, which can be bounded from above and 594 below using normal hypotheses. A dependently typed semantic function coerces 595 the deep encoding to the shallow one, that we will soon describe. We will 596 handle the function has an implicit coercion, so that we will simply write 597 $i$ to represent both the list of tag names $i$ and the type former which is 598 the polymorphic variant type described by $i$. The context always allow to 599 disambiguate between the two uses and insert the coercion every time that 600 a list $i$ is used in a type former. 601 For example, the list $[num;plus]$ for our 602 running example will represent the polymorphic variant type 603 $[i_{\geq \pair{[num;plus]}{[num;plus]}}]$ and a function that expects at 604 least $num$ but that does not handle $mul$ will be typed as either 605 $f : \forall E. \forall i. [num] \subseteq i \subseteq [num;plus] \to i~E \to \ldots$ 606 or $f: \forall E. \forall i. i \subseteq [plus] \to (num::i)~E \to \ldots$. 607 608 We defined the shallow encoding of the bounded polymorphic variant type 609 specified by a list $i$ of constructors as a $\Sigma$type whose carrier 610 is the universe data type $u$ and whose property rules out all constructors 611 whose tag is not in $i$. Code extraction will simplify the $\Sigma$type to 612 its carrier, satisfying both requirements 1 and 2. 613 614 \begin{definition}[Polymorphic variant type encoding] 615 A bounded polymorphic variant $i$ where $i_{\geq \pair{L}{U}}$ is deeply encoded 616 by a variable $i$ of type list of tags ($i: list~tag$) under the hypothesis 617 that $L \subseteq i \subseteq U$. 618 The corresponding shallow encoding is 619 $\Sigma x:u~\alpha_1~\ldots~\alpha_n. tag\_of\_expr \ldots x \in i$. 620 An implicit coercion maps $i : list~tag \mapsto \Sigma x:u~\alpha_1~\ldots~\alpha_n. tag\_of\_expr \ldots x \in i$. 621 \end{definition} 622 623 Subtyping is not necessary for polymorphic variants \`a la Guarrigue~\cite{???}: 624 the slogan, borrowed by~\cite{???}, is \emph{structural subtyping as 625 instantitation}. 626 Subtyping as instantiation fits very well with the HindleyMilner type system 627 because it supports type inference. Since we work with a type system more 628 expressive than HindleyMilner where type inference is undecidable, we are 629 not restricted to subtyping as instantiation, but we can also exploit the 630 natural subtyping rule between polymorphic variants types~\ref{???}. 631 632 \begin{definition}[Subtyping] 633 There exists a coercion of type 634 $\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 635 i_2~\alpha_1~\ldots~\alpha_n$ 636 \end{definition} 637 In the encoding of the universe we required an equality test over tags. 638 The test is exploited here to implement a computational version of the 639 $\subseteq$ relation between list of tags. I.e. it is possible to define 640 $\subseteq$ in such a way that for closed terms $i_1$ and $i_2$, 641 $i_1 \subseteq i_2$ reduces to $True$. As we will see, this suggests a different 642 style where polymorphic variant types are represented using the less number 643 of row quantifications and type membership and subtyping are automatically 644 decided by mere computation, without any user intervention. 645 646 The subtyping coercion takes apart the inhabitant of the polymorphic variant 647 $i_1$, obtaining both an inhabitant $x$ of the universe and a proof that its 648 constructors are all in $i_1$. Then it builds an inhabitant of the polymorphic 649 variant $i_2$ by coupling $x$ with the proof that all of its constructors are 650 in $i_2 \superseteq i_1$. The computational content of the coercion is just 651 the identity function and code extraction erases it: requirement 2 is satisfied. 652 653 \begin{definition}[Constructor encoding] 654 A constructor $K_i : T_i \to u~\alpha_1~\ldots~\alpha_m$ of the universe is 655 lifted to a polymorphic variant constructor 656 $T_i \to i~\alpha_1~\ldots~\alpha_m$ when 657 $\forall x:T_i. tag\_of\_expr (K_i x) \in i$. 658 The lifting is obtained by inhabiting the sigma type 659 $\Sigma x:u~\alpha_1~\ldots~\alpha_n. tag\_of\_expr \ldots x \in i$ 660 with a pair whose first component is the applied constructor and the second 661 component the proof of the condition above. 662 \end{definition} 663 We can exploit again the equality test over tag types to implement a 664 computational version of the predicate $tag\_of\_expr (K_i x) \in i$. 665 Therefore, when $i$ is a closed term, all tests reduce to $True$. 666 Matita implements a generalized system of coercions that allow to declare 667 the lifting of polymorphic variant as an implicit coercion. Since the coercion 668 requires a proof of the condition, a new proof obligation is opened. 669 The proof obligation is just $True$ when $i$ is closed. 670 671 The computational content of the lifted constructor is just the identity 672 function: the $n$th constructor of a polymorphic variant type is represented 673 after code extraction by the $n$th constructor of the unvierse inductive type, 674 satisfying requirement 1. 584 675 585 676 \subsection{Simulation (reduction + type checking)}
Note: See TracChangeset
for help on using the changeset viewer.