# Changeset 2525

Ignore:
Timestamp:
Dec 3, 2012, 5:39:42 PM (7 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2524 \begin{example}[The universe for our running example] The following lines of Matita code implement the universe encoding for our running example. They constitute the file~\texttt{test.ma}. \begin{lstlisting} inductive expr (E: Type[0]) : Type[0] ≝ \end{lstlisting} \end{example} We are now ready to lift the universe encoding to the encoding of polymorphic variant types, constructors, case analysis and elimination principle. The idea consists in following quite litteraly the description of the syntax of bounded polymorphic variants: a bounded polymorphic variant is deeply encoded by the list of constructors that are allowed. Row polymorphism is achieved by quantifying over the list, which can be bounded from above and below using normal hypotheses. A dependently typed semantic function coerces the deep encoding to the shallow one, that we will soon describe. We will handle the function has an implicit coercion, so that we will simply write $i$ to represent both the list of tag names $i$ and the type former which is the polymorphic variant type described by $i$. The context always allow to disambiguate between the two uses and insert the coercion every time that a list $i$ is used in a type former. For example, the list $[num;plus]$ for our running example will represent the polymorphic variant type $[i_{\geq \pair{[num;plus]}{[num;plus]}}]$ and a function that expects at least $num$ but that does not handle $mul$ will be typed as either $f : \forall E. \forall i. [num] \subseteq i \subseteq [num;plus] \to i~E \to \ldots$ or $f: \forall E. \forall i. i \subseteq [plus] \to (num::i)~E \to \ldots$. We defined the shallow encoding of the bounded polymorphic variant type specified by a list $i$ of constructors as a $\Sigma$-type whose carrier is the universe data type $u$ and whose property rules out all constructors whose tag is not in $i$. Code extraction will simplify the $\Sigma$-type to its carrier, satisfying both requirements 1 and 2. \begin{definition}[Polymorphic variant type encoding] A bounded polymorphic variant $i$ where $i_{\geq \pair{L}{U}}$ is deeply encoded by a variable $i$ of type list of tags ($i: list~tag$) under the hypothesis that $L \subseteq i \subseteq U$. The corresponding shallow encoding is $\Sigma x:u~\alpha_1~\ldots~\alpha_n. tag\_of\_expr \ldots x \in i$. An implicit coercion maps $i : list~tag \mapsto \Sigma x:u~\alpha_1~\ldots~\alpha_n. tag\_of\_expr \ldots x \in i$. \end{definition} Subtyping is not necessary for polymorphic variants \`a la Guarrigue~\cite{???}: the slogan, borrowed by~\cite{???}, is \emph{structural subtyping as instantitation}. Subtyping as instantiation fits very well with the Hindley-Milner type system because it supports type inference. Since we work with a type system more expressive than Hindley-Milner where type inference is undecidable, we are not restricted to subtyping as instantiation, but we can also exploit the natural subtyping rule between polymorphic variants types~\ref{???}. \begin{definition}[Subtyping] There exists a coercion of type $\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 i_2~\alpha_1~\ldots~\alpha_n$ \end{definition} In the encoding of the universe we required an equality test over tags. The test is exploited here to implement a computational version of the $\subseteq$ relation between list of tags. I.e. it is possible to define $\subseteq$ in such a way that for closed terms $i_1$ and $i_2$, $i_1 \subseteq i_2$ reduces to $True$. As we will see, this suggests a different style where polymorphic variant types are represented using the less number of row quantifications and type membership and subtyping are automatically decided by mere computation, without any user intervention. The subtyping coercion takes apart the inhabitant of the polymorphic variant $i_1$, obtaining both an inhabitant $x$ of the universe and a proof that its constructors are all in $i_1$. Then it builds an inhabitant of the polymorphic variant $i_2$ by coupling $x$ with the proof that all of its constructors are in $i_2 \superseteq i_1$. The computational content of the coercion is just the identity function and code extraction erases it: requirement 2 is satisfied. \begin{definition}[Constructor encoding] A constructor $K_i : T_i \to u~\alpha_1~\ldots~\alpha_m$ of the universe is lifted to a polymorphic variant constructor $T_i \to i~\alpha_1~\ldots~\alpha_m$ when $\forall x:T_i. tag\_of\_expr (K_i x) \in i$. The lifting is obtained by inhabiting the sigma type $\Sigma x:u~\alpha_1~\ldots~\alpha_n. tag\_of\_expr \ldots x \in i$ with a pair whose first component is the applied constructor and the second component the proof of the condition above. \end{definition} We can exploit again the equality test over tag types to implement a computational version of the predicate $tag\_of\_expr (K_i x) \in i$. Therefore, when $i$ is a closed term, all tests reduce to $True$. Matita implements a generalized system of coercions that allow to declare the lifting of polymorphic variant as an implicit coercion. Since the coercion requires a proof of the condition, a new proof obligation is opened. The proof obligation is just $True$ when $i$ is closed. The computational content of the lifted constructor is just the identity function: the $n$-th constructor of a polymorphic variant type is represented after code extraction by the $n$-th constructor of the unvierse inductive type, satisfying requirement 1. \subsection{Simulation (reduction + type checking)}