Changeset 2519


Ignore:
Timestamp:
Dec 3, 2012, 12:29:42 PM (7 years ago)
Author:
mulligan
Message:

To prevent conflicts

Location:
Papers/polymorphic-variants-2012
Files:
1 added
1 edited

Legend:

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

    r2518 r2519  
    2121\newcommand{\rulefont}[1]{\ensuremath{(\mathbf{#1})}}
    2222
    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{lst-grafite.tex}
     25\lstset{language=Grafite}
    3026
    3127\bibliographystyle{spphys}
     
    9490\begin{minipage}[b]{0.45\linewidth}
    9591\begin{lstlisting}
     92\lstset{language=haskell}
    9693data Term
    9794  = Lit Int
     
    339336Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations.
    340337
    341 Matita
    342 
    343338\subsection{Subtyping as instantiation vs subtyping as safe static cast}
    344339
    345 \subsection{Syntax \& type checking rules}
     340\subsection{Syntax and type checking rules}
    346341The ones of Guarrigue + casts, but also for the bounded case?
    347342Casts support both styles of subtyping.
     
    385380(being isomorphic to the unit type) are simplified to the unit type and
    386381possibly completely erased using the categorical properties of unit types
    387 ($1 * T \symeq T$, $1 \to T \symeq T$, etc.). For more information, one can
     382($1 * T \simeq T$, $1 \to T \simeq T$, etc.). For more information, one can
    388383read~\cite{berardi,christine-mohring,letouzey}.
    389384
     
    554549\section{Appendix: interface of library functions used to implement everything}
    555550
     551We 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.
     552Our language is captured by the following inductive data type:
     553\begin{lstlisting}
     554inductive 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}
     559Here, \texttt{expression} is parameterised by a type, \texttt{E}.
     560We will say more about this later.
     561Paired with our inductive type representing the AST of natural number expressions, we have a type of tags:
     562\begin{lstlisting}
     563inductive tag_ : Type[0] :=
     564  | num : tag_
     565  | plus : tag_
     566  | mul : tag_.
     567\end{lstlisting}
     568Tags, and the constructors of the inductive type they are shadowing, are kept in one-one 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
     570On the \texttt{tag\_} inductive type, we define the `obvious' decidable equality function:
     571\begin{lstlisting}
     572definition 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}
     583Using \texttt{eq\_tag\_} we lift the \texttt{tag\_} inductive type into the Matita standard library's \texttt{DeqSet}.
     584The \texttt{DeqSet} abstraction represents types with a decidable equality.
     585Many generic functions in the Matita library are defined to work with this abstraction.
     586The lifting is straightforward:
     587\begin{lstlisting}
     588definition tag : DeqSet :=
     589  mk_DeqSet tag_ eq_tag ?.
     590  * * normalize /2/ %
     591  #abs destruct
     592qed.
     593\end{lstlisting}
     594Here, \texttt{mk\_DeqSet} is the constructor of the \texttt{DeqSet} record.
     595By convention in Matita, for a record type name \texttt{Foo}, there exists a constructor for that record type name \textt{mk\_Foo}.
     596We pass the constructor function three arguments: the type that possess a decidable equality, in this case \texttt{tag\_}
     597
    556598\bibliography{polymorphic-variants}
    557599
Note: See TracChangeset for help on using the changeset viewer.