Changeset 2519 for Papers/polymorphicvariants2012
 Timestamp:
 Dec 3, 2012, 12:29:42 PM (7 years ago)
 Location:
 Papers/polymorphicvariants2012
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/polymorphicvariants.tex
r2518 r2519 21 21 \newcommand{\rulefont}[1]{\ensuremath{(\mathbf{#1})}} 22 22 23 \lstset{basicstyle=\footnotesize\tt,columns=flexible,breaklines=false, 24 keywordstyle=\color{red}\bfseries, 25 keywordstyle=[2]\color{blue}, 26 commentstyle=\color{green}, 27 stringstyle=\color{blue}, 28 showspaces=false,showstringspaces=false, 29 xleftmargin=1em} 23 \renewcommand{\verb}{\lstinline} 24 \def\lstlanguagefiles{lstgrafite.tex} 25 \lstset{language=Grafite} 30 26 31 27 \bibliographystyle{spphys} … … 94 90 \begin{minipage}[b]{0.45\linewidth} 95 91 \begin{lstlisting} 92 \lstset{language=haskell} 96 93 data Term 97 94 = Lit Int … … 339 336 Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations. 340 337 341 Matita342 343 338 \subsection{Subtyping as instantiation vs subtyping as safe static cast} 344 339 345 \subsection{Syntax \&type checking rules}340 \subsection{Syntax and type checking rules} 346 341 The ones of Guarrigue + casts, but also for the bounded case? 347 342 Casts support both styles of subtyping. … … 385 380 (being isomorphic to the unit type) are simplified to the unit type and 386 381 possibly completely erased using the categorical properties of unit types 387 ($1 * T \s ymeq T$, $1 \to T \symeq T$, etc.). For more information, one can382 ($1 * T \simeq T$, $1 \to T \simeq T$, etc.). For more information, one can 388 383 read~\cite{berardi,christinemohring,letouzey}. 389 384 … … 554 549 \section{Appendix: interface of library functions used to implement everything} 555 550 551 We will explain our technique with a simple running example: a trivial language of arithmetic including numeric literals and two binary operations corresponding to addition and multiplication. 552 Our language is captured by the following inductive data type: 553 \begin{lstlisting} 554 inductive expression (E: Type[0]) : Type[0] := 555  Num : nat $\rightarrow$ expression E 556  Plus : E $\rightarrow$ E $\rightarrow$ expression E 557  Mul : E $\rightarrow$ E $\rightarrow$ expression E. 558 \end{lstlisting} 559 Here, \texttt{expression} is parameterised by a type, \texttt{E}. 560 We will say more about this later. 561 Paired with our inductive type representing the AST of natural number expressions, we have a type of tags: 562 \begin{lstlisting} 563 inductive tag_ : Type[0] := 564  num : tag_ 565  plus : tag_ 566  mul : tag_. 567 \end{lstlisting} 568 Tags, and the constructors of the inductive type they are shadowing, are kept in oneone correspondence with each other; for each constructor in the \texttt{expression} inductive type we have a single corresponding constructor in the \texttt{tag\_} inductive type, and \emph{vice versa}. 569 570 On the \texttt{tag\_} inductive type, we define the `obvious' decidable equality function: 571 \begin{lstlisting} 572 definition eq_tag\_: tag_ $\rightarrow$ tag_ $\rightarrow$ bool := 573 $\lambda$t1, t2. 574 match t1 with 575 [ num $\Rightarrow$ 576 match t2 with 577 [ num $\Rightarrow$ true 578  _ $\Rightarrow$ false 579 ] 580 $\ldots$ 581 ]. 582 \end{lstlisting} 583 Using \texttt{eq\_tag\_} we lift the \texttt{tag\_} inductive type into the Matita standard library's \texttt{DeqSet}. 584 The \texttt{DeqSet} abstraction represents types with a decidable equality. 585 Many generic functions in the Matita library are defined to work with this abstraction. 586 The lifting is straightforward: 587 \begin{lstlisting} 588 definition tag : DeqSet := 589 mk_DeqSet tag_ eq_tag ?. 590 * * normalize /2/ % 591 #abs destruct 592 qed. 593 \end{lstlisting} 594 Here, \texttt{mk\_DeqSet} is the constructor of the \texttt{DeqSet} record. 595 By convention in Matita, for a record type name \texttt{Foo}, there exists a constructor for that record type name \textt{mk\_Foo}. 596 We pass the constructor function three arguments: the type that possess a decidable equality, in this case \texttt{tag\_} 597 556 598 \bibliography{polymorphicvariants} 557 599
Note: See TracChangeset
for help on using the changeset viewer.