%% diagrams
\usepackage{tikz}
\usetikzlibrary{shapes,arrows,positioning}
+\usetikzlibrary{intersections}
% \usepackage{tikz-cd}
% \usepackage{pgfplots}
\newcommand{\mynegder}{\vspace{-0.3cm}}
\newcommand{\myquot}{\Uparrow}
\newcommand{\mynquot}{\, \Downarrow}
-\newcommand{\mycanquot}{\ensuremath{\textsc{quote}{\Uparrow}}}
-\newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Downarrow}}}
+\newcommand{\mycanquot}{\ensuremath{\textsc{quote}{\Downarrow}}}
+\newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Uparrow}}}
\newcommand{\mymetaguard}{\ |\ }
\newcommand{\mybox}{\Box}
+\newcommand{\mytermi}[1]{\text{\texttt{#1}}}
+\newcommand{\mysee}[1]{\langle\myse{#1}\rangle}
\renewcommand{\[}{\begin{equation*}}
\renewcommand{\]}{\end{equation*}}
\newtheoremstyle{named}{}{}{\itshape}{}{\bfseries}{}{.5em}{\textsc{#1}}
\theoremstyle{named}
+\pgfdeclarelayer{background}
+\pgfdeclarelayer{foreground}
+\pgfsetlayers{background,main,foreground}
+
%% -----------------------------------------------------------------------------
\title{\mykant: Implementing Observational Equality}
\section{Introduction}
+
+
\section{Simple and not-so-simple types}
\label{sec:types}
\subsection{The untyped $\lambda$-calculus}
\label{sec:untyped}
-Along with Turing's machines, the earliest attempts to formalise computation
-lead to the $\lambda$-calculus \citep{Church1936}. This early programming
-language encodes computation with a minimal syntax and no `data' in the
-traditional sense, but just functions. Here we give a brief overview of the
-language, which will give the chance to introduce concepts central to the
-analysis of all the following calculi. The exposition follows the one found in
-chapter 5 of \cite{Queinnec2003}.
+Along with Turing's machines, the earliest attempts to formalise
+computation lead to the definition of the $\lambda$-calculus
+\citep{Church1936}. This early programming language encodes computation
+with a minimal syntax and no `data' in the traditional sense, but just
+functions. Here we give a brief overview of the language, which will
+give the chance to introduce concepts central to the analysis of all the
+following calculi. The exposition follows the one found in chapter 5 of
+\cite{Queinnec2003}.
\begin{mydef}[$\lambda$-terms]
Syntax of the $\lambda$-calculus: variables, abstractions, and
the updated knowledge on the value of $\myb{x}$.
\subsubsection{$\myarr$, or dependent function}
+\label{rec:depprod}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
\AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
\[
\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}
}
}
\]
Now, the question is: do we need to give up well-behavedness of our theory to
gain extensionality?
-\subsection{Some alternatives}
-
-% TODO finish
-% TODO add `extentional axioms' (Hoffman), setoid models (Thorsten)
-
\section{The observational approach}
\label{sec:ott}
\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
\begin{tabular}{cc}
- \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \AxiomC{$\mychk{\mytmt}{\mytya}$}
\AxiomC{$\myfun{f} \not\in \myctx$}
\BinaryInfC{
$\myctx \myelabt \myval{\myfun{f}}{\mytya}{\mytmt} \ \ \myelabf\ \ \myctx; \myfun{f} \mapsto \mytmt : \mytya$
}
\DisplayProof
&
- \AxiomC{$\myjud{\mytya}{\mytyp}$}
+ \AxiomC{$\mychk{\mytya}{\mytyp}$}
\AxiomC{$\myfun{f} \not\in \myctx$}
\BinaryInfC{
$
\subsubsection{Why user defined types? Why eliminators?}
-The `hardest' design choice when designing $\mykant$\ was to decide
-whether user defined types should be included. In the end, we can
-devise
+The hardest design choice when designing $\mykant$\ was to decide
+whether user defined types should be included, and how to handle them.
+In the end, as we saw, we can devise general structures like $\mytyc{W}$
+that can express all inductive structures. However, using those tools
+beyond very simple examples is near-impossible for a human user. Thus
+all theorem provers in use provide some mean for the user to define
+structures tailored to specific uses.
-% TODO reference levitated theories, indexed containers
+Even if we take user defined data types for granted, there are two broad
+schools of thought regarding how to manipulate them:
+\begin{description}
+\item[Fixed points and pattern matching] The road chose by Agda and Coq.
+ Functions are written like in Haskell---matching on the input and with
+ explicit recursion. An external check on the recursive arguments
+ ensures that they are decreasing, and thus that all functions
+ terminate. This approach is the best in terms of user usability, but
+ it is tricky to implement correctly.
+
+\item[Elaboration into eliminators] The road chose by \mykant, and
+ pioneered by the Epigram line of work. The advantage is that we can
+ reduce every data type to simple definitions which guarantee
+ termination and are simple to reduce and type. It is however more
+ cumbersome to use than pattern maching, although \cite{McBride2004}
+ has shown how to implement a pattern matching interface on top of a
+ larger set of combinators of those provided by \mykant.
+\end{description}
-foobar
+We chose the safer and easier to implement path, given the time
+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}
Having a well founded type hierarchy is crucial if we want to retain
consistency, otherwise we can break our type systems by proving bottom,
-as shown in Appendix \ref{sec:hurkens}.
+as shown in Appendix \ref{app:hurkens}.
However, hierarchy as presented in section \label{sec:itt} is a
considerable burden on the user, on various levels. Consider for
\begin{figure}[b!]
- % TODO finish
\mydesc{cumulativity:}{\myctx \vdash \mytmsyn \mycumul \mytmsyn}{
\begin{tabular}{ccc}
\AxiomC{$\myctx \vdash \mytya \mydefeq \mytyb$}
are currently subject of research. We chose less flexible but more
concise way, since it is easier to implement and better understood.
-% \begin{figure}[t]
-% % TODO do this
-% \caption{Constraints generated by the typical ambiguity engine. We
-% assume some global set of constraints with the ability of generating
-% fresh references.}
-% \label{fig:hierarchy}
-% \end{figure}
-
\subsection{Observational equality, \mykant\ style}
There are two correlated differences between $\mykant$\ and the theory
sums' in the literature, referring to the interpretation that
identifies the first element as a `tag' deciding the type of the
second element, which lets us recover sum types (disjuctions), as we
- saw in Section \ref{sec:user-type}. Thus, $\mysigma$.} to
+ saw in Section \ref{sec:depprod}. Thus, $\mysigma$.} to
avoid confusion with the $\mytyc{Prod}$ in the prelude:
\[
\begin{array}{@{}l}
\subsubsection{Coercions}
-% \begin{figure}[t]
-% \mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
-
-% }
-% \caption{Coercions in \mykant.}
-% \label{fig:kant-coe}
-% \end{figure}
-
% TODO finish
\subsubsection{$\myprop$ and the hierarchy}
type checking we define two mutually recursive functions, one quoting
canonical terms against their types (since we need the type to typecheck
canonical terms), one quoting neutral terms while recovering their
-types.
+types. The full procedure for quotation is shown in Figure
+\ref{fig:kant-quot}. We $\boxed{\text{box}}$ the neutral proofs and
+neutral members of empty types, following the notation in
+\cite{Altenkirch2007}, and we make use of $\mydefeq_{\mybox}$ which
+compares terms syntactically up to $\alpha$-renaming, but also up to
+equivalent proofs: we consider all boxed content as equal.
Our quotation will work on normalised terms, so that all defined values
will have been replaced. Moreover, we match on datatype eliminators and
-all their arguments, so that $\mynat.\myfun{elim} \myappsp \vec{\mytmt}$
-will stand for $\mynat.\myfun{elim}$ applied to the scrutinised
-$\mynat$, plus its three arguments. This measure can be easily
-implemented by checking the head of applications and `consuming' the
-needed terms.
+all their arguments, so that $\mynat.\myfun{elim} \myappsp \mytmm
+\myappsp \myse{P} \myappsp \vec{\mytmn}$ will stand for
+$\mynat.\myfun{elim}$ applied to the scrutinised $\mynat$, the
+predicate, and the two cases. This measure can be easily implemented by
+checking the head of applications and `consuming' the needed terms.
-% TODO finish this
\begin{figure}[t]
\mydesc{canonical quotation:}{\mycanquot(\myctx, \mytmsyn : \mytmsyn) \mymetagoes \mytmsyn}{
\small
$
- \begin{array}{@{}l}
- \mycanquot(\myctx, \mytmt : \mytyc{D} \myappsp \vec{A}) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \boxed{\mytmt} \\
- \mycanquot(\myctx, \mytmt : \mytyc{D} \myappsp \vec{A}) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \\ \myind{2} \mytyc{D}.\mydc{constr} \myappsp \cdots \myappsp \mycanquot(\myctx, \mytyc{D}.\myfun{f}_n : (\myctx(\mytyc{D}.\myfun{f}_n))(\vec{A};\mytmt)) \\
- \mycanquot(\myctx, \mytyc{D}.\mydc{c} \myappsp \vec{t} : \mytyc{D} \myappsp \vec{A}) \mymetagoes \cdots \\
- \mycanquot(\myctx, \myse{f} : \myfora{\myb{x}}{\mytya}{\mytyb}) \mymetagoes \myabs{\myb{x}}{\mycanquot(\myctx; \myb{x} : \mytya, \myapp{\myse{f}}{\myb{x}} : \mytyb)} \\
- \mycanquot(\myctx, \myse{p} : \myprdec{\myse{P}}) \mymetagoes \boxed{\myse{p}}
+ \begin{array}{@{}l@{}l}
+ \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \boxed{\mytmt} \\
+ \mycanquot(\myctx,\ \mytmt : \mytyc{D} \myappsp \vec{A} &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\mydc{constr} \myappsp \cdots \myappsp \mycanquot(\myctx, \mytyc{D}.\myfun{f}_n : (\myctx(\mytyc{D}.\myfun{f}_n))(\vec{A};\mytmt)) \\
+ \mycanquot(\myctx,\ \mytyc{D}.\mydc{c} \myappsp \vec{t} : \mytyc{D} \myappsp \vec{A} &) \mymetagoes \cdots \\
+ \mycanquot(\myctx,\ \myse{f} : \myfora{\myb{x}}{\mytya}{\mytyb} &) \mymetagoes \myabs{\myb{x}}{\mycanquot(\myctx; \myb{x} : \mytya, \myapp{\myse{f}}{\myb{x}} : \mytyb)} \\
+ \mycanquot(\myctx,\ \myse{p} : \myprdec{\myse{P}} &) \mymetagoes \boxed{\myse{p}}
\\
- \mycanquot(\myctx, \mytmt : \mytya) \mymetagoes \mytmt'\text{, where}\ \mytmt' : \myarg = \myneuquot(\myctx, \mytmt)
+ \mycanquot(\myctx,\ \mytmt : \mytya &) \mymetagoes \mytmt'\ \text{\textbf{where}}\ \mytmt' : \myarg = \myneuquot(\myctx, \mytmt)
\end{array}
$
}
\myfora{\myb{x}}{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx; \myb{x} : \mytya, \mytyb)} : \mytyp \\
\myneuquot(\myctx,\ \mytyc{D} \myappsp \vec{A} &) \mymetagoes \mytyc{D} \myappsp \cdots \mycanquot(\myctx, \mymeta{head}((\myctx(\mytyc{D}))(\mytya_1 \cdots \mytya_{n-1}))) : \mytyp \\
\myneuquot(\myctx,\ \myprdec{\myjm{\mytmm}{\mytya}{\mytmn}{\mytyb}} &) \mymetagoes \myprdec{\myjm{\mycanquot(\myctx, \mytmm : \mytya)}{\mytya'}{\mycanquot(\myctx, \mytmn : \mytyb)}{\mytyb'}} : \mytyp \\
- \multicolumn{2}{@{}l}{\myind{2}\text{where}\ \mytya' : \myarg = \myneuquot(\myctx, \mytya)\text{, and}\ \mytyb' : \myarg = \myneuquot(\myctx, \mytyb)} \\
- \myneuquot(\myctx,\ \mytyc{D}.\myfun{f} \myappsp \mytmt &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \\
- \multicolumn{2}{@{}l}{\myind{2} \mytyc{D}.\myfun{f} \myappsp \mytmt' : (\myctx(\mytyc{D}.\myfun{f}))(\vec{A};\mytmt)\text{, where}\ \mytmt' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmt)} \\
- \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmt \myappsp \myse{P} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\myfun{elim} \myappsp \boxed{\mytmt} \myappsp \myneuquot(\myctx, \myse{P} \myappsp \mytmt) \\
- \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmm \myappsp \myse{P} \myappsp \vec{\mytmn} &) \mymetagoes \cdots \\
- \myneuquot(\myctx,\ \myapp{\myse{f}}{\mytmt} &) \mymetagoes \\
- \multicolumn{2}{@{}l}{\myind{2} \myapp{\myse{f'}}{\mycanquot(\myctx, \mytmt : \mytya)} : \mysub{\mytyb}{\myb{x}}{\mytmt}\text{, where}\ \myse{f'} : \myfora{\myb{x}}{\mytya}{\mytyb} = \myneuquot(\myctx, \myse{f})} \\
+ \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytya' : \myarg = \myneuquot(\myctx, \mytya)} \\
+ \multicolumn{2}{@{}l}{\myind{2}\phantom{\text{\textbf{where}}}\ \mytyb' : \myarg = \myneuquot(\myctx, \mytyb)} \\
+ \myneuquot(\myctx,\ \mytyc{D}.\myfun{f} \myappsp \mytmt &) \mymetaguard \mymeta{record}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\myfun{f} \myappsp \mytmt' : (\myctx(\mytyc{D}.\myfun{f}))(\vec{A};\mytmt) \\
+ \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytmt' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmt)} \\
+ \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmt \myappsp \myse{P} &) \mymetaguard \mymeta{empty}(\myctx, \mytyc{D}) \mymetagoes \mytyc{D}.\myfun{elim} \myappsp \boxed{\mytmt} \myappsp \myneuquot(\myctx, \myse{P}) : \myse{P} \myappsp \mytmt \\
+ \myneuquot(\myctx,\ \mytyc{D}.\myfun{elim} \myappsp \mytmm \myappsp \myse{P} \myappsp \vec{\mytmn} &) \mymetagoes \mytyc{D}.\myfun{elim} \myappsp \mytmm' \myappsp \myneuquot(\myctx, \myse{P}) \cdots : \myse{P} \myappsp \mytmm\\
+ \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \mytmm' : \mytyc{D} \myappsp \vec{A} = \myneuquot(\myctx, \mytmm)} \\
+ \myneuquot(\myctx,\ \myapp{\myse{f}}{\mytmt} &) \mymetagoes \myapp{\myse{f'}}{\mycanquot(\myctx, \mytmt : \mytya)} : \mysub{\mytyb}{\myb{x}}{\mytmt} \\
+ \multicolumn{2}{@{}l}{\myind{2}\text{\textbf{where}}\ \myse{f'} : \myfora{\myb{x}}{\mytya}{\mytyb} = \myneuquot(\myctx, \myse{f})} \\
\myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetaguard \myneuquot(\myctx, \mytya) \mydefeq_{\mybox} \myneuquot(\myctx, \mytyb) \mymetagoes \myneuquot(\myctx, \mytmt) \\
\myneuquot(\myctx,\ \mycoee{\mytya}{\mytyb}{\myse{Q}}{\mytmt} &) \mymetagoes
\mycoee{\myneuquot(\myctx, \mytya)}{\myneuquot(\myctx, \mytyb)}{\boxed{\myse{Q}}}{\myneuquot(\myctx, \mytmt)}
\end{array}
$
}
- \caption{Quotation in \mykant.}
+ \caption{Quotation in \mykant. Along the already used
+ $\mymeta{record}$ meta-operation on the context we make use of
+ $\mymeta{empty}$, which checks if a certain type constructor has
+ zero data constructor. The `data constructor' cases for non-record,
+ non-empty, data types are omitted for brevity.}
\label{fig:kant-quot}
\end{figure}
-% TODO finish
-
\subsubsection{Why $\myprop$?}
It is worth to ask if $\myprop$ is needed at all. It is perfectly
propositional, a fact which prevented the use of quotients in dependent
type theories \citep{Jacobs1994}.
-% TODO finish
-
\section{\mykant : The practice}
\label{sec:kant-practice}
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 happens in a read-eval-print loop (REPL). The REPL is a
-available both as a commandline application and in a web interface,
-which is available at \url{kant.mazzo.li} and presents itself as in
-figure \ref{fig:kant-web}.
+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}.
+
+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{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 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{]}){*} \\
+ \multicolumn{3}{@{}l}{\text{Terms, including propositions.}} \\
+ \multicolumn{3}{@{}l}{
+ \begin{array}{@{\ \ }l@{\ }c@{\ }l@{\ \ \ \ \ }l}
+ \mysee{term} & ::= & \mysee{name} & \text{A variable.} \\
+ & | & \mytermi{*} & \text{\mytyc{Type}.} \\
+ & | & \mytermi{\{|}\ \mysee{term}{*}\ \mytermi{|\}} & \text{Type holes.} \\
+ & | & \mytermi{Prop} & \text{\mytyc{Prop}.} \\
+ & | & \mytermi{Top} \mysynsep \mytermi{Bot} & \text{$\mytop$ and $\mybot$.} \\
+ & | & \mysee{term}\ \mytermi{/\textbackslash}\ \mysee{term} & \text{Conjuctions.} \\
+ & | & \mytermi{[|}\ \mysee{term}\ \mytermi{|]} & \text{Proposition decoding.} \\
+ & | & \mytermi{coe}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coercion.} \\
+ & | & \mytermi{coh}\ \mysee{term}\ \mysee{term}\ \mysee{term}\ \mysee{term} & \text{Coherence.} \\
+ & | & \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)}\ \mytermi{=}\ \mytermi{(}\ \mysee{term}\ \mytermi{:}\ \mysee{term}\ \mytermi{)} & \text{Heterogeneous equality.} \\
+ & | & \mytermi{(}\ \mysee{compound}\ \mytermi{)} & \text{Parenthesised term.} \\
+ \mysee{compound} & ::= & \mytermi{\textbackslash}\ \mysee{binder}{*}\ \mytermi{=>}\ \mysee{term} & \text{Untyped abstraction.} \\
+ & | & \mytermi{\textbackslash}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} & \text{Typed abstraction.} \\
+ & | & \mytermi{forall}\ \mysee{telescope}\ \mysee{term} & \text{Universal quantification.} \\
+ & | & \mysee{arr} \\
+ \mysee{arr} & ::= & \mysee{telescope}\ \mytermi{->}\ \mysee{arr} & \text{Dependent function.} \\
+ & | & \mysee{term}\ \mytermi{->}\ \mysee{arr} & \text{Non-dependent function.} \\
+ & | & \mysee{term}{+} & \text {Application.}
+ \end{array}
+ } \\
+ \multicolumn{3}{@{}l}{\text{Typed names.}} \\
+ \mysee{typed} & ::= & \mysee{name}\ \mytermi{:}\ \mysee{term} \\
+ \multicolumn{3}{@{}l}{\text{Declarations.}} \\
+ \mysee{decl}& ::= & \mysee{value} \mysynsep \mysee{abstract} \mysynsep \mysee{data} \mysynsep \mysee{record} \\
+ \multicolumn{3}{@{}l}{\text{Defined values. The telescope specifies named arguments.}} \\
+ \mysee{value} & ::= & \mysee{name}\ \mysee{telescope}\ \mytermi{:}\ \mysee{term}\ \mytermi{=>}\ \mysee{term} \\
+ \multicolumn{3}{@{}l}{\text{Abstracted variables.}} \\
+ \mysee{abstract} & ::= & \mytermi{postulate}\ \mysee{typed} \\
+ \multicolumn{3}{@{}l}{\text{Data types, and their constructors.}} \\
+ \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\
+ \mysee{constrs} & ::= & \mysee{typed} \\
+ & | & \mysee{typed}\ \mytermi{|}\ \mysee{constrs} \\
+ \multicolumn{3}{@{}l}{\text{Records, and their projections. The $\mysee{name}$ before the projections is the constructor name.}} \\
+ \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
+ \mysee{projs} & ::= & \mysee{typed} \\
+ & | & \mysee{typed}\ \mytermi{,}\ \mysee{projs}
+ \end{array}
+ $
+
+ \caption{\mykant' syntax. The non-terminals are marked with
+ $\langle\text{angle brackets}\rangle$ for greater clarity. The
+ syntax in the implementation is actually more liberal, for example
+ giving the possibility of using arrow types directly in
+ constructor/projection declarations.}
+ \label{fig:syntax}
+\end{figure}
+
\subsection{Term and context representation}
\label{sec:term-repr}
Another source of contention related to term representation is dealing
with evaluation. Here \mykant\ does not make bold moves, and simply
-employs substitution. Before
-Moreover, when elaborating user defined types,
-all
+employs substitution. When type checking we match types by reducing
+them to their wheak head normal form, as to avoid unnecessary evaluation.
+
+We treat data types eliminators and record projections in an uniform
+way, by elaborating declarations in a series of \emph{rewriting rules}:
+\begin{Verbatim}
+type Rewr =
+ forall v.
+ TmRef v -> -- Term to which the destructor is applied
+ [TmRef v] -> -- List of other arguments
+ -- The result of the rewriting, if the eliminator reduces.
+ Maybe [TmRef v]
+\end{Verbatim}
+A rewriting rule is polymorphic in the variable type, guaranteeing that
+it just pattern matches on terms structure and rearranges them in some
+way, and making it possible to apply it at any level in the term. When
+reducing a series of applications we match the first term and check if
+it is a destructor, and if that's the case we apply the reduction rule
+and reduce further if it yields a new list of terms.
+
+This has the advantage of being very simple, but has the disadvantage of
+being quite poor in terms of performance and that we need to do
+quotation manually. An alternative that solves both of these is the
+already mentioned \emph{normalization by evaluation}, where we would
+compute by turning terms into Haskell values, and then reify back to
+terms to compare them---a useful tutorial on this technique is given by
+\cite{Loh2010}.
\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}
(\myb{x} {:} \mytya)(\myb{y} {:} \mytyb) \myarr \cdots =
(\myb{x} {:} \mytya) \myarr (\myb{y} {:} \mytyb) \myarr \cdots
\]
+Meta operations names will be displayed in $\mymeta{smallcaps}$ and
+written in a pattern matching style, also making use of boolean guards.
+For example, a meta operation operating on a context and terms might
+look like this:
+\[
+\begin{array}{@{}l}
+ \mymeta{quux}(\myctx, \myb{x}) \mymetaguard \myb{x} \in \myctx \mymetagoes \myctx(\myb{x}) \\
+ \mymeta{quux}(\myctx, \myb{x}) \mymetagoes \mymeta{outofbounds} \\
+ \myind{2} \vdots
+\end{array}
+\]
\section{Code}
\end{code}
\subsubsection{\mykant}
+\label{app:kant-itt}
The following things are missing: $\mytyc{W}$-types, since our
positivity check is overly strict, and equality, since we haven't
}
\subsection{\mykant\ examples}
+\label{app:kant-examples}
{\small
\verbatiminput{examples.ka}
}
\subsection{\mykant' hierachy}
-\label{sec:hurkens}
+\label{app:hurkens}
This rendition of the Hurken's paradox does not type check with the
hierachy enabled, type checks and loops without it. Adapted from an
projects / bitonic-mengthesis.git / blobdiff