%% diagrams
\usepackage{tikz}
\usetikzlibrary{shapes,arrows,positioning}
+\usetikzlibrary{intersections}
% \usepackage{tikz-cd}
% \usepackage{pgfplots}
\newtheoremstyle{named}{}{}{\itshape}{}{\bfseries}{}{.5em}{\textsc{#1}}
\theoremstyle{named}
+\pgfdeclarelayer{background}
+\pgfdeclarelayer{foreground}
+\pgfsetlayers{background,main,foreground}
+
%% -----------------------------------------------------------------------------
\title{\mykant: Implementing Observational Equality}
\[
\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}
}
}
\]
\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.
\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}
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
\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}
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{]}){*} \\
\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}
\subsubsection{Context}
-Given the parmetrised type,
+Given our term type parametrised on the type of the variables,
% TODO finish
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$.
\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}
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}
projects / bitonic-mengthesis.git / commitdiff