...

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}