From 4a595ccd130b5954a103a66f2941ab2ed711ee6a Mon Sep 17 00:00:00 2001 From: Francesco Mazzoli Date: Fri, 14 Jun 2013 17:38:59 +0100 Subject: [PATCH] ... --- thesis.bib | 58 +++++++++++- thesis.lagda | 249 ++++++++++++++++++++++++++++++++++++--------------- 2 files changed, 235 insertions(+), 72 deletions(-) diff --git a/thesis.bib b/thesis.bib index 468ba5c..58bfa89 100644 --- a/thesis.bib +++ b/thesis.bib @@ -30,7 +30,7 @@ @online{GHC, author = {{The GHC Team}}, title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.1}, - url = {http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/}, + url = {http://www.haskell.org/ghc/docs/latest/html/users_guide/}, howpublished = {\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}}, year = 2012 } @@ -513,4 +513,60 @@ year = {2012} pages={525--549}, year={2000}, publisher={JSTOR} +} + +@inproceedings{chakravarty2005associated, + title={Associated types with class}, + author={Chakravarty, Manuel MT and Keller, Gabriele and Jones, Simon Peyton and Marlow, Simon}, + booktitle={ACM SIGPLAN Notices}, + volume={40}, + number={1}, + pages={1--13}, + year={2005}, + organization={ACM} +} + +@article{miller1992unification, + title={Unification under a mixed prefix}, + author={Miller, Dale}, + journal={Journal of symbolic computation}, + volume={14}, + number={4}, + pages={321--358}, + year={1992}, + publisher={Elsevier} +} + +@UNPUBLISHED{gundrytutorial, + title={A tutorial implementation of dynamic pattern unification}, + author={Gundry, Adam and McBride, Conor}, + note= {Unpublished draft}, + year={2013} +} + +@techreport{cockett1992charity, + title={About charity}, + author={Cockett, Robin and Fukushima, Tom}, + year={1992}, + journal={Yellow Series Report} +} + +@incollection{mcbride2009let, + title={Let’s see how things unfold: Reconciling the infinite with the intensional}, + author={McBride, Conor}, + booktitle={Algebra and Coalgebra in Computer Science}, + pages={113--126}, + year={2009}, + publisher={Springer} +} + +@article{huet1973undecidability, + title={The undecidability of unification in third order logic}, + author={Huet, Gerard P}, + journal={Information and Control}, + volume={22}, + number={3}, + pages={257--267}, + year={1973}, + publisher={Elsevier} } \ No newline at end of file diff --git a/thesis.lagda b/thesis.lagda index f664a13..74dfe88 100644 --- a/thesis.lagda +++ b/thesis.lagda @@ -62,6 +62,7 @@ %% diagrams \usepackage{tikz} \usetikzlibrary{shapes,arrows,positioning} +\usetikzlibrary{intersections} % \usepackage{tikz-cd} % \usepackage{pgfplots} @@ -274,6 +275,10 @@ \newtheoremstyle{named}{}{}{\itshape}{}{\bfseries}{}{.5em}{\textsc{#1}} \theoremstyle{named} +\pgfdeclarelayer{background} +\pgfdeclarelayer{foreground} +\pgfsetlayers{background,main,foreground} + %% ----------------------------------------------------------------------------- \title{\mykant: Implementing Observational Equality} @@ -1529,8 +1534,8 @@ no term of type \[ \myfun{ext} : \myfora{\myb{A}\ \myb{B}}{\mytyp}{\myfora{\myb{f}\ \myb{g}}{ \myb{A} \myarr \myb{B}}{ - (\myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{\myb{B}} \myapp{\myb{g}}{\myb{x}}}) \myarr - \myb{f} \mypeq{\myb{A} \myarr \myb{B}} \myb{g} + (\myfora{\myb{x}}{\myb{A}}{\mypeq \myappsp \myb{B} \myappsp (\myapp{\myb{f}}{\myb{x}}) \myappsp (\myapp{\myb{g}}{\myb{x}})}) \myarr + \mypeq \myappsp (\myb{A} \myarr \myb{B}) \myappsp \myb{f} \myappsp \myb{g} } } \] @@ -2903,7 +2908,7 @@ instantiate when due: \DisplayProof } -\subsubsection{Why user defined types? Why eliminators? Why no inductive families?} +\subsubsection{Why user defined types? Why eliminators?} The hardest design choice when designing $\mykant$\ was to decide whether user defined types should be included, and how to handle them. @@ -2933,37 +2938,9 @@ schools of thought regarding how to manipulate them: \end{description} We chose the safer and easier to implement path, given the time -constraints and the higher confidence of correctnes. - -Beyond normal inductive data types, \mykant\ also does not venture in -more sophisticated notions. A popular improvements on basic data types -are such as inductive families, where the parameters for the type -constructors change based on the data constructors. This choice was -motivated by the fact that inductive families can be represented by -adding equalities concerning the parameters as arguments to the data -constructor, in much the same way that GADTs are handled in Haskell -\citep{Sulzmann2007}. - -Another popular extension introduced by \cite{dybjer2000general} is -induction-recursion, where we define a data type in tandem with a -function on that type. This technique has proven extremely useful to -define embeddings of other calculi in an host language, by defining the -representation of the embedded language as a data type and at the same -time a function decoding from the representation to a type in the host -language. - -It is also worth mentionning that in recent times there has been work by -\cite{dagand2012elaborating, chapman2010gentle} to show how to define a -set of primitives that data types can be elaborated into, with the -additional advantage of having the possibility of having a very powerful -notion of generic programming by writing functions working on the -`primitive' types as to be workable by all `compatible' user-defined -data types. This has been a considerable problem in the dependently -type world, where we often define types which are more `strongly typed' -version of similar structures,\footnote{For example the $\mytyc{OList}$ - presented in Section \ref{sec:user-type} being a `more typed' version - of an ordinary list.} and then find ourselves forced to redefine -identical operations on both types. +constraints and the higher confidence of correctness. See also Section +\ref{sec:future-work} for a brief overview of ways to extend or treat +user defined types. \subsection{Cumulative hierarchy and typical ambiguity} \label{sec:term-hierarchy} @@ -3673,15 +3650,24 @@ ways \mykant\ is something in between the first and second version of Epigram. The author learnt the hard way the implementation challenges for such a -project, and while there is a solid and working base to work on, the -implementation of observational equality is not currently complete. -However, given the detailed plan in the previous section, doing so -should not prove to be too much work. +project, and ran out of time while implementing observational equality. +While the constructs and typing rules are present, the machinery to make +it happen (equality reduction, coercions, quotation, etc.) is not +present yet. Everything else presented is implemented and working +reasonably well, and given the detailed plan in the previous section, +finishing off should not prove too much work. + +The interaction with the user takes place in a loop living in and +updating a context of \mykant\ declarations, which presents itself as in +Figure \ref{fig:kant-web}. Files with lists of declarations can also be +loaded. The REPL is a available both as a commandline application and in +a web interface, which is available at \url{bertus.mazzo.li}. -The interaction happens in a read-eval-print loop (REPL), which presents -itself as in Fiure \ref{fig:kant-web}. The REPL is a available both as -a commandline application and in a web interface, which is available at -\url{bertus.mazzo.li}. +A REPL cycle starts with the user inputing a \mykant\ +declaration or another REPL command, which then goes through various +stages that can end up in a context update, or in failures of various +kind. The process is described diagrammatically in figure +\ref{fig:kant-process}. \begin{figure}[t] {\small\begin{verbatim}B E R T U S @@ -3707,12 +3693,6 @@ Type: Nat\end{verbatim} \label{fig:kant-web} \end{figure} -The interaction with the user takes place in a loop living in and -updating a context of \mykant\ declarations. A REPL cycle starts with -the user inputing a \mykant\ declaration or another REPL command, which -then goes through various stages that can end up in a context update, or -in failures of various kind. The process is described diagrammatically -in figure \ref{fig:kant-process}: \begin{description} @@ -3805,22 +3785,19 @@ Here we will review only a sampling of the more interesting implementation challenges present when implementing an interactive theorem prover. -\subsection{What is done, what is missing} - -Sadly the author ran out of time while implementing observational -equality, and while the constructs and typing rules are present, the -machinery to make it happen (equality reduction, coercions, quotation, -etc.) is not present yet. Everything else presented is implemented and -working reasonably well. - \subsection{Syntax} +The syntax of \mykant\ is presented in Figure \ref{fig:syntax}. +Examples showing the usage of most of the constructs are present in +Appendices \ref{app:kant-itt}, \ref{app:kant-examples}, and +\ref{app:hurkens}. + \begin{figure}[p] $ \begin{array}{@{\ \ }l@{\ }c@{\ }l} \multicolumn{3}{@{}l}{\text{A name, in regexp notation.}} \\ \mysee{name} & ::= & \texttt{[a-zA-Z] [a-zA-Z0-9'\_-]*} \\ - \multicolumn{3}{@{}l}{\text{A binder might or might not (\texttt{\_}) bind.}} \\ + \multicolumn{3}{@{}l}{\text{A binder might or might not (\texttt{\_}) bind a name.}} \\ \mysee{binder} & ::= & \mytermi{\_} \mysynsep \mysee{name} \\ \multicolumn{3}{@{}l}{\text{A series of typed bindings.}} \\ \mysee{telescope}\, \ \ \ & ::= & (\mytermi{[}\ \mysee{binder}\ \mytermi{:}\ \mysee{term}\ \mytermi{]}){*} \\ @@ -3874,11 +3851,6 @@ working reasonably well. \label{fig:syntax} \end{figure} -The syntax of \mykant\ is presented in Figure \ref{fig:syntax}. -Examples showing the usage of most of the constructs are present in -Appendices \ref{app:kant-itt}, \ref{app:kant-examples}, and -\ref{app:hurkens}. - \subsection{Term and context representation} \label{sec:term-repr} @@ -4117,7 +4089,7 @@ terms to compare them---a useful tutorial on this technique is given by \subsubsection{Context} -Given the parmetrised type, +Given our term type parametrised on the type of the variables, % TODO finish @@ -4138,7 +4110,7 @@ denote with $x, y, z, \dots$. and are of two kinds: Predictably, $\le$ expresses a reflexive order, and $<$ expresses an irreflexive order, both working with the same notion of equality, where -$x < y$ implies $x \le y$---they behave like $\le$ and $<$ do on natural +$x < y$ implies $x \le y$---they behave like $\le$ and $<$ do for natural numbers (or in our case, levels in a type hierarchy). We also need an equality constraint ($x = y$), which can be reduced to two constraints $x \le y$ and $y \le x$. @@ -4158,17 +4130,88 @@ library is implemented as a modification of the code described by \cite{King1995}. We represent the set by building a graph where vertices are variables, -and edges are constraints between them. The edges are labelled with the -constraint type ($<$ or $\le$). As we add constraints, $\le$ -constraints are replaced by $<$ constraints, so that if we started with -an empty set and added +and edges are constraints between them, labelled with the appropriate +constraint: $x < y$ gives rise to a $<$-labelled edge from $x$ to $y$< +and $x \le y$ to a $\le$-labelled edge from $x$ to $y$. As we add +constraints, $\le$ constraints are replaced by $<$ constraints, so that +if we started with an empty set and added \[ - x \le y,\ y < z,\ z \le k,\ k \le j,\ x < y,\ j \le y + x < y,\ y \le z,\ z \le k,\ k < j,\ j \le y\, z < k \] it would generate the graph shown in Figure \ref{fig:graph-one}. \begin{figure}[t] - + \centering + \begin{subfigure}[b]{0.3\textwidth} + \begin{tikzpicture}[node distance=1.5cm] + % Place nodes + \node (x) {$x$}; + \node [right of=x] (y) {$y$}; + \node [right of=y] (z) {$z$}; + \node [below of=z] (k) {$k$}; + \node [left of=k] (j) {$j$}; + %% Lines + \path[->] + (x) edge node [above] {$<$} (y) + (y) edge node [above] {$\le$} (z) + (z) edge node [right] {$<$} (k) + (k) edge node [below] {$\le$} (j) + (j) edge node [left ] {$\le$} (y); + \end{tikzpicture} + \caption{Before $z < k$.} + \label{fig:graph-one-before} + \end{subfigure}% + ~ + \begin{subfigure}[b]{0.3\textwidth} + \begin{tikzpicture}[node distance=1.5cm] + % Place nodes + \node (x) {$x$}; + \node [right of=x] (y) {$y$}; + \node [right of=y] (z) {$z$}; + \node [below of=z] (k) {$k$}; + \node [left of=k] (j) {$j$}; + %% Lines + \path[->] + (x) edge node [above] {$<$} (y) + (y) edge node [above] {$\le$} (z) + (z) edge node [right] {$<$} (k) + (k) edge node [below] {$\le$} (j) + (j) edge node [left ] {$\le$} (y); + \end{tikzpicture} + \caption{After $z < k$.} + \label{fig:graph-one-after} + \end{subfigure}% + ~ + \begin{subfigure}[b]{0.3\textwidth} + \begin{tikzpicture}[remember picture, node distance=1.5cm] + \begin{pgfonlayer}{foreground} + % Place nodes + \node (x) {$x$}; + \node [right of=x] (y) {$y$}; + \node [right of=y] (z) {$z$}; + \node [below of=z] (k) {$k$}; + \node [left of=k] (j) {$j$}; + %% Lines + \path[->] + (x) edge node [above] {$<$} (y) + (y) edge node [above] {$\le$} (z) + (z) edge node [right] {$<$} (k) + (k) edge node [below] {$\le$} (j) + (j) edge node [left ] {$\le$} (y); + \end{pgfonlayer}{foreground} + \end{tikzpicture} + \begin{tikzpicture}[remember picture, overlay] + \begin{pgfonlayer}{background} + \fill [red, opacity=0.3] + (-2.5,2.4) rectangle (-0.4,0.2) + (-4,2.4) rectangle (-3.3,1.6); + \end{pgfonlayer}{background} + \end{tikzpicture} + \caption{SCCs.} + \label{fig:graph-one-scc} + \end{subfigure}% + \caption{Strong constraints overrule weak constraints.} + \label{fig:graph-one} \end{figure} \subsection{Type holes} @@ -4184,12 +4227,76 @@ sorroundings. In \mykant\ -\subsection{Web prompt} +\subsection{Web REPL} \section{Evaluation} \section{Future work} +\label{sec:future-work} + +As mentioned, the first move that the author plans to make is to work +towards a simple but powerful term representation, and then adjust +\mykant\ to this new representation. A good plan seems to be to +associate each type (terms, telescopes, etc.) with what we can +substitute variables with, so that the term type will be associated with +itself, while telescopes and propositions will be associated to terms. +This can probably be accomplished elegantly with Haskell's \emph{type + families} \citep{chakravarty2005associated}. After achieving a more +solid machinery for terms, implementing observational equality fully +should prove relatively easy. + +Beyond this steps, \mykant\ would still need many additions to compete +as a reasonable alternative to the existing systems: + +\begin{description} +\item[Pattern matching] Eliminators are very clumsy to use, and + +\item[More powerful data types] Beyond normal inductive data types, + \mykant\ does not in more sophisticated notions. A popular + improvements on basic data types are inductive families, where the + parameters for the type constructors change based on the data + constructors, which lets us express naturally types such as + $\mytyc{Vec} : \mynat \myarr \mytyp$, which given a number returns the + type of lists of that length, or $\mytyc{Fin} : \mynat \myarr \mytyp$, + which given a number $n$ gives the type of numbers less than $n$. + This apparent omission was motivated by the fact that inductive + families can be represented by adding equalities concerning the + parameters of the type constructors as arguments to the data + constructor, in much the same way that Generalised Abstract Data Types + \citep{GHC} are handled in Haskell, where interestingly the modified + version of System F that lies at the core of recent versions of GHC + features coercions similar to those found in OTT \citep{Sulzmann2007}. + + Another popular extension introduced by \cite{dybjer2000general} is + induction-recursion, where we define a data type in tandem with a + function on that type. This technique has proven extremely useful to + define embeddings of other calculi in an host language, by defining + the representation of the embedded language as a data type and at the + same time a function decoding from the representation to a type in the + host language. + + It is also worth mentionning that in recent times there has been work + by \cite{dagand2012elaborating, chapman2010gentle} to show how to + define a set of primitives that data types can be elaborated into, + with the additional advantage of having the possibility of having a + very powerful notion of generic programming by writing functions + working on the `primitive' types as to be workable by all `compatible' + user-defined data types. This has been a considerable problem in the + dependently type world, where we often define types which are more + `strongly typed' version of similar structures,\footnote{For example + the $\mytyc{OList}$ presented in Section \ref{sec:user-type} being a + `more typed' version of an ordinary list.} and then find ourselves + forced to redefine identical operations on both types. + +\item[Type inference] While bidirectional type checking helps, for a + syts \cite{miller1992unification} \cite{gundrytutorial} + \cite{huet1973undecidability}. + +\item[Coinduction] \cite{cockett1992charity} \cite{mcbride2009let}. +\end{description} + + \subsection{Coinduction} -- 2.30.2