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

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/polymorphic-variants-2012/polymorphic-variants.tex

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