\documentclass[report]{article}
+\usepackage{etex}
%% Narrow margins
% \usepackage{fullpage}
%% Symbols
\usepackage[fleqn]{amsmath}
+\usepackage{stmaryrd} %llbracket
%% Proof trees
\usepackage{bussproofs}
%% Diagrams
\usepackage[all]{xy}
+%% Quotations
+\usepackage{epigraph}
+
+%% Images
+\usepackage{graphicx}
+
+%% Subfigure
+\usepackage{subcaption}
+
+%% diagrams
+\usepackage{tikz}
+\usetikzlibrary{shapes,arrows,positioning}
+% \usepackage{tikz-cd}
+% \usepackage{pgfplots}
+
+
%% -----------------------------------------------------------------------------
%% Commands for Agda
\usepackage[english]{babel}
\FrameSep0.2cm
\newcommand{\mydesc}[3]{
- {\small
- \vspace{0.3cm}
- \hfill \textbf{#1} $#2$
- \vspace{-0.3cm}
- \begin{framed}
- #3
- \end{framed}
-}
+ \noindent
+ \mbox{
+ \parbox{\textwidth}{
+ {\small
+ \vspace{0.3cm}
+ \hfill \textbf{#1} $#2$
+
+ \framebox[\textwidth]{
+ \parbox{\textwidth}{
+ \vspace{0.1cm}
+ #3
+ \vspace{0.1cm}
+ }
+ }
+ }
+ }
+ }
}
% TODO is \mathbin the correct thing for arrow and times?
% TODO \mathbin or \mathrel here?
\newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
\newcommand{\mytt}{\mydc{$\langle\rangle$}}
-\newcommand{\myunit}{\mytyc{$\top$}}
+\newcommand{\myunit}{\mytyc{Unit}}
\newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
\newcommand{\myfst}{\myfld{fst}}
\newcommand{\mysnd}{\myfld{snd}}
\newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
\newcommand{\myleft}[1]{\mydc{left}_{#1}}
\newcommand{\myright}[1]{\mydc{right}_{#1}}
-\newcommand{\myempty}{\mytyc{$\bot$}}
+\newcommand{\myempty}{\mytyc{Empty}}
\newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
\newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
\newcommand{\myarg}{\_}
\newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
\newcommand{\mylub}{\sqcup}
\newcommand{\mydefeq}{\cong}
+\newcommand{\myrefl}{\mydc{refl}}
+\newcommand{\mypeq}[1]{\mathrel{\mytyc{=}_{#1}}}
+\newcommand{\myjeqq}{\myfun{=-elim}}
+\newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
+\newcommand{\mysubst}{\myfun{subst}}
+\newcommand{\myprsyn}{\myse{prop}}
+\newcommand{\myprdec}[1]{\llbracket #1 \rrbracket}
+\newcommand{\myand}{\wedge}
+\newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
+\newcommand{\mybot}{\bot}
+\newcommand{\mytop}{\top}
+\newcommand{\mycoe}{\myfun{coe}}
+\newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
+\newcommand{\mycoh}{\myfun{coh}}
+\newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
+\newcommand{\myjm}[4]{(#1 {:} #2) = (#3 {:} #4)}
+\newcommand{\myprop}{\mytyc{Prop}}
+\newcommand{\mytmup}{\mytmsyn\uparrow}
+\newcommand{\mydefs}{\Delta}
+\newcommand{\mynf}{\Downarrow}
+\newcommand{\myinff}[3]{#1 \vdash #2 \Rightarrow #3}
+\newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
+\newcommand{\mychkk}[3]{#1 \vdash #2 \Leftarrow #3}
+\newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
+\newcommand{\myann}[2]{#1 : #2}
+\newcommand{\mydeclsyn}{\myse{decl}}
+\newcommand{\myval}[3]{#1 : #2 \mapsto #3}
+\newcommand{\mypost}[2]{\mysyn{postulate}\ #1 : #2}
+\newcommand{\myadt}[4]{\mysyn{data}\ #1 : #2 \myarr \mytyp\ \mysyn{where}\ #3\{ #4 \}}
+\newcommand{\myreco}[4]{\mysyn{record}\ #1 : #2 \myarr \mytyp\ \mysyn{where}\ #3\ \{ #4 \}}
+% TODO change vdash
+\newcommand{\myelabt}{\vdash}
+\newcommand{\myelabf}{\rhd}
+\newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
+\newcommand{\mytele}{\Delta}
+\newcommand{\mytelee}{\delta}
+\newcommand{\mydcctx}{\Gamma}
+\newcommand{\mynamesyn}{\myse{name}}
+\newcommand{\myvec}{\overrightarrow}
+\newcommand{\mymeta}{\textsc}
+\newcommand{\myhyps}{\mymeta{hyps}}
+\newcommand{\mycc}{;}
+\newcommand{\myemptytele}{\cdot}
+\newcommand{\mymetagoes}{\Longrightarrow}
+% \newcommand{\mytesctx}{\
+\newcommand{\mytelesyn}{\myse{telescope}}
+\newcommand{\myrecs}{\mymeta{recs}}
%% -----------------------------------------------------------------------------
complete. As a corollary, we must be able to devise a term that reduces forever
(`loops' in imperative terms):
\[
- (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \dots\text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
+ (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \cdots \text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
\]
A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus
\noindent
\begin{minipage}{0.5\textwidth}
\mydesc{syntax}{ } {
- $ \mytmsyn ::= \dotsb \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
+ $ \mytmsyn ::= \cdots b \mysynsep \myfix{\myb{x}}{\mytysyn}{\mytmsyn} $
\vspace{0.4cm}
}
\end{minipage}
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \dots \\
+ \mytmsyn & ::= & \cdots \\
& | & \mytt \mysynsep \myapp{\myabsurd{\mytysyn}}{\mytmsyn} \\
& | & \myapp{\myleft{\mytysyn}}{\mytmsyn} \mysynsep
\myapp{\myright{\mytysyn}}{\mytmsyn} \mysynsep
\myapp{\mycase{\mytmsyn}{\mytmsyn}}{\mytmsyn} \\
& | & \mypair{\mytmsyn}{\mytmsyn} \mysynsep
\myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
- \mytysyn & ::= & \dots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
+ \mytysyn & ::= & \cdots \mysynsep \myunit \mysynsep \myempty \mysynsep \mytmsyn \mysum \mytmsyn \mysynsep \mytysyn \myprod \mytysyn
\end{array}
$
}
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \dots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
+ \mytmsyn & ::= & \cdots \mysynsep \mynil{\mytysyn} \mysynsep \mytmsyn \mycons \mytmsyn
\mysynsep
\myapp{\myapp{\myapp{\myfoldr}{\mytmsyn}}{\mytmsyn}}{\mytmsyn} \\
- \mytysyn & ::= & \dots \mysynsep \myapp{\mylist}{\mytysyn}
+ \mytysyn & ::= & \cdots \mysynsep \myapp{\mylist}{\mytysyn}
\end{array}
$
}
normalising. \cite{Coquand1986} further extended this line of work with the
Calculus of Constructions (CoC).
+Most widely used interactive theorem provers are based on ITT. Popular ones
+include Agda \citep{Norell2007, Bove2009}, Coq \citep{Coq}, and Epigram
+\citep{McBride2004, EpigramTut}.
+
+\subsection{A note on inference}
+
+% TODO do this, adding links to the sections about bidi type checking and
+% implicit universes.
+In the following text I will often omit explicit typing for abstractions or
+
+Moreover, I will use $\mytyp$ without bothering to specify a
+universe, with the silent assumption that the definition is consistent
+regarding to the hierarchy.
+
\subsection{A simple type theory}
\label{sec:core-tt}
& | & \mybool \mysynsep \mytrue \mysynsep \myfalse \mysynsep
\myitee{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
& | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
- \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \\
+ \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
+ (\myapp{\mytmsyn}{\mytmsyn}) \\
& | & \myexi{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
\mypairr{\mytmsyn}{\myb{x}}{\mytmsyn}{\mytmsyn} \\
& | & \myapp{\myfst}{\mytmsyn} \mysynsep \myapp{\mysnd}{\mytmsyn} \\
in the STLC is gone: values can appear in types, and the two are treated
uniformly in the syntax.
-While the usefulness of doing this will become clear soon, a consequence is that
-since types can be the result of computation, deciding type equality is not
-immediate as in the STLC. For this reason we define \emph{definitional
- equality}, $\mydefeq$, as the congruence relation extending $\myred$. Types
-that are definitionally equal can be used interchangeably. Here the
-`conversion' rule is not syntax directed, however we will see how it is possible
-to employ $\myred$ to decide term equality in a systematic way. % TODO add section
+While the usefulness of doing this will become clear soon, a consequence is
+that since types can be the result of computation, deciding type equality is
+not immediate as in the STLC. For this reason we define \emph{definitional
+ equality}, $\mydefeq$, as the congruence relation extending
+$\myred$---moreover, when comparing types syntactically we do it up to
+renaming of bound names ($\alpha$-renaming). For example under this
+discipline we will find that
+\[
+\myabss{\myb{x}}{\mytya}{\myb{x}} \mydefeq \myabss{\myb{y}}{\mytya}{\myb{y}}
+\]
+Types that are definitionally equal can be used interchangeably. Here the
+`conversion' rule is not syntax directed, however we will see how it is
+possible to employ $\myred$ to decide term equality in a systematic
+way. % TODO add section
Another thing to notice is that considering the need to reduce terms to decide
equality, it is essential for a dependently type system to be terminating and
confluent for type checking to be decidable.
Moreover, we specify a \emph{type hierarchy} to talk about `large' types:
$\mytyp_0$ will be the type of types inhabited by data: $\mybool$, $\mynat$,
$\mylist$, etc. $\mytyp_1$ will be the type of $\mytyp_0$, and so on---for
-example we have $\mytrue : \mybool : \mytyp_0 : \mytyp_1 : \dots$. Each type
-`level' is often called a universe in the literature. While it is possible, to
-simplify things by having only one universe $\mytyp$ with $\mytyp : \mytyp$,
-this plan is inconsistent for much the same reason that impredicative na\"{\i}ve
-set theory is \citep{Hurkens1995}. Moreover, various techniques can be employed
-to lift the burden of explicitly handling universes.
+example we have $\mytrue : \mybool : \mytyp_0 : \mytyp_1 : \cdots$. Each type
+`level' is often called a universe in the literature. While it is possible,
+to simplify things by having only one universe $\mytyp$ with $\mytyp :
+\mytyp$, this plan is inconsistent for much the same reason that impredicative
+na\"{\i}ve set theory is \citep{Hurkens1995}. Moreover, various techniques
+can be employed to lift the burden of explicitly handling universes.
% TODO add sectioon about universes
\subsubsection{Contexts}
}
}
-
\section{The struggle for equality}
\label{sec:equality}
-\subsection{Propositional equality...}
+In the previous section we saw how a type checker (or a human) needs a notion of
+\emph{definitional equality}. Beyond this meta-theoretic notion, in this
+section we will explore the ways of expressing equality \emph{inside} the
+theory, as a reasoning tool available to the user. This area is the main
+concern of this thesis, and in general a very active research topic, since we do
+not have a fully satisfactory solution, yet.
+
+\subsection{Propositional equality}
+
+\noindent
+\begin{minipage}{0.5\textwidth}
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \cdots \\
+ & | & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep
+ \myapp{\myrefl}{\mytmsyn} \\
+ & | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
+ \end{array}
+ $
+}
+\end{minipage}
+\begin{minipage}{0.5\textwidth}
+\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
+ \centering{
+ $
+ \myjeq{\myse{P}}{(\myapp{\myrefl}{\mytmm})}{\mytmn} \myred \mytmn
+ $
+ }
+ \vspace{0.9cm}
+}
+\end{minipage}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \AxiomC{$\myjud{\mytya}{\mytyp_l}$}
+ \AxiomC{$\myjud{\mytmm}{\mytya}$}
+ \AxiomC{$\myjud{\mytmn}{\mytya}$}
+ \TrinaryInfC{$\myjud{\mytmm \mypeq{\mytya} \mytmn}{\mytyp_l}$}
+ \DisplayProof
+
+ \myderivsp
+
+ \begin{tabular}{cc}
+ \AxiomC{\phantom{$\myctx P \mytyp_l$}}
+ \noLine
+ \UnaryInfC{$\myjud{\mytmt}{\mytya}$}
+ \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\mytmt \mypeq{\mytya} \mytmt}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{P}}{\myfora{\myb{x}\ \myb{y}}{\mytya}{\myfora{q}{\myb{x} \mypeq{\mytya} \myb{y}}{\mytyp_l}}}$}
+ \noLine
+ \UnaryInfC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.2cm}\myjud{\myse{p}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}}$}
+ \UnaryInfC{$\myjud{\myjeq{\myse{P}}{\myse{q}}{\myse{p}}}{\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmn}}{q}}$}
+ \DisplayProof
+ \end{tabular}
+ }
+}
+
+To express equality between two terms inside ITT, the obvious way to do so is
+to have the equality construction to be a type-former. Here we present what
+has survived as the dominating form of equality in systems based on ITT up to
+the present day.
+
+Our type former is $\mypeq{\mytya}$, which given a type (in this case
+$\mytya$) relates equal terms of that type. $\mypeq{}$ has one introduction
+rule, $\myrefl$, which introduces an equality relation between definitionally
+equal terms---in the typing rule we display the term as `the same', meaning
+`the same up to $\mydefeq$'. % TODO maybe mention this earlier
+
+Finally, we have one eliminator for $\mypeq{}$, $\myjeqq$. $\myjeq{\myse{P}}{\myse{q}}{\myse{p}}$ takes
+\begin{itemize}
+\item $\myse{P}$, a predicate working with two terms of a certain type (say
+ $\mytya$) and a proof of their equality
+\item $\myse{q}$, a proof that two terms in $\mytya$ (say $\myse{m}$ and
+ $\myse{n}$) are equal
+\item and $\myse{p}$, an inhabitant of $\myse{P}$ applied to $\myse{m}$, plus
+ the trivial proof by reflexivity showing that $\myse{m}$ is equal to itself
+\end{itemize}
+Given these ingredients, $\myjeqq$ retuns a member of $\myse{P}$ applied to
+$\mytmm$, $\mytmn$, and $\myse{q}$. In other words $\myjeqq$ takes a
+witness that $\myse{P}$ works with \emph{definitionally equal} terms, and
+returns a witness of $\myse{P}$ working with \emph{propositionally equal}
+terms. Invokations of $\myjeqq$ will vanish when the equality proofs will
+reduce to invocations to reflexivity, at which point the arguments must be
+definitionally equal, and thus the provided
+$\myapp{\myapp{\myapp{\myse{P}}{\mytmm}}{\mytmm}}{(\myapp{\myrefl}{\mytmm})}$
+can be returned.
+
+While the $\myjeqq$ rule is slightly convoluted, ve can derive many more
+`friendly' rules from it, for example a more obvious `substitution' rule, that
+replaces equal for equal in predicates:
+\[
+\begin{array}{l}
+(\myabs{\myb{A}\ \myb{P}\ \myb{x}\ \myb{y}\ \myb{q}\ \myb{p}}{
+ \myjeq{(\myabs{\myb{x}\ \myb{y}\ \myb{q}}{\myapp{\myb{P}}{\myb{y}}})}{\myb{q}}{\myb{p}}}) : \\
+\myind{1} \myfora{\myb{A}}{\mytyp}{\myfora{\myb{P}}{\myb{A} \myarr \mytyp}{\myfora{\myb{x}\ \myb{y}}{\myb{A}}{\myb{x} \mypeq{\myb{A}} \myb{y} \myarr \myapp{\myb{P}}{\myb{x}} \myarr \myapp{\myb{P}}{\myb{y}}}}}
+\end{array}
+\]
+This rule is often called $\myfun{subst}$---here we will invoke it without
+specifying the type ($\myb{A}$) and the sides of the equality
+($\myb{x},\myb{y}$).
+
+Once we have $\myfun{subst}$, we can easily prove more familiar laws regarding
+equality, such as symmetry, transitivity, and a congruence law:
-\subsection{...and its limitations}
+% TODO finish this
+
+\subsection{Common extensions}
eta law
UIP
+\subsection{Limitations}
+
+\epigraph{\emph{Half of my time spent doing research involves thinking up clever
+ schemes to avoid needing functional extensionality.}}{@larrytheliquid}
+
+However, propositional equality as described is quite restricted when
+reasoning about equality beyond the term structure, which is what definitional
+equality gives us (extension notwithstanding).
+
+The problem is best exemplified by \emph{function extensionality}. In
+mathematics, we would expect to be able to treat functions that give equal
+output for equal input as the same. When reasoning in a mechanised framework
+we ought to be able to do the same: in the end, without considering the
+operational behaviour, all functions equal extensionally are going to be
+replaceable with one another.
+
+However this is not the case, or in other words with the tools we have we have
+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}
+ }
+}
+\]
+To see why this is the case, consider the functions
+\[\myabs{\myb{x}}{0 \mathrel{\myfun{+}} \myb{x}}$ and $\myabs{\myb{x}}{\myb{x} \mathrel{\myfun{+}} 0}\]
+where $\myfun{+}$ is defined by recursion on the first argument, gradually
+destructing it to build up successors of the second argument. The two
+functions are clearly denotationally the same, and we can in fact prove that
+\[
+\myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{+}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{+}} 0)}
+\]
+By analysis on the $\myb{x}$. However, the two functions are not
+definitionally equal, and thus we won't be able to get rid of the
+quantification.
+
+For the reasons above, theories that offer a propositional equality similar to
+what we presented are called \emph{intensional}, as opposed to
+\emph{extensional}. Most systems in wide use today (such as Agda, Coq and
+Epigram) are of this kind.
+
+This is quite an annoyance that often makes reasoning awkward to execute. It
+also extends to other fields, for example proving bisimulation between
+processes specified by coinduction, or in general proving equivalences based
+on the behaviour on a term.
+
\subsection{Equality reflection}
+One way to `solve' this problem is by identifying propositional equality with
+definitional equality:
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+ \centering{
+ \AxiomC{$\myjud{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}$}
+ \UnaryInfC{$\myjud{\mytmm \mydefeq \mytmn}{\mytya}$}
+ \DisplayProof
+ }
+}
+
+This rule takes the name of \emph{equality reflection}, and is a very
+different rule from the ones we saw up to now: it links a typing judgement
+internal to the type theory to a meta-theoretic judgement that the type
+checker uses to work with terms. It is easy to see the dangerous consequences
+that this causes:
+\begin{itemize}
+\item The rule is syntax directed, and the type checker is presumably expected
+ to come up with equality proofs when needed.
+\item More worryingly, type checking becomes undecidable also because
+ computing under false assumptions becomes unsafe.
+ Consider for example
+ \[
+ \myabss{\myb{q}}{\mytya \mypeq{\mytyp} (\mytya \myarr \mytya)}{\myhole{?}}
+ \]
+ Using the assumed proof in tandem with equality reflection we could easily
+ write a classic Y combinator, sending the compiler into a loop.
+\end{itemize}
+
+Given these facts theories employing equality reflection, like NuPRL
+\citep{NuPRL}, carry the derivations that gave rise to each typing judgement
+to keep the systems manageable. % TODO more info, problems with that.
+
+For all its faults, equality reflection does allow us to prove extensionality,
+using the extensions we gave above. Assuming that $\myctx$ contains
+\[\myb{A}, \myb{B} : \mytyp; \myb{f}, \myb{g} : \myb{A} \myarr \myb{B}; \myb{q} : \myfora{\myb{x}}{\myb{A}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\]
+We can then derive
+\begin{prooftree}
+ \AxiomC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{q}}{\myb{x}}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}$}
+ \RightLabel{equality reflection}
+ \UnaryInfC{$\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{f}}{\myb{x}} \mydefeq \myapp{\myb{g}}{\myb{x}}}{\myb{B}}$}
+ \RightLabel{congruence for $\lambda$s}
+ \UnaryInfC{$\myjud{(\myabs{\myb{x}}{\myapp{\myb{f}}{\myb{x}}}) \mydefeq (\myabs{\myb{x}}{\myapp{\myb{g}}{\myb{x}}})}{\myb{A} \myarr \myb{B}}$}
+ \RightLabel{$\eta$-law for $\lambda$}
+ \UnaryInfC{$\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}$}
+ \RightLabel{$\myrefl$}
+ \UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
+\end{prooftree}
+
+Now, the question is: do we need to give up well-behavedness of our theory to
+gain extensionality?
+
+\subsection{Observational equality}
+\label{sec:ott}
+
+% TODO should we explain this in detail?
+A recent development by \citet{Altenkirch2007}, \emph{Observational Type
+ Theory} (OTT), promises to keep the well behavedness of ITT while being able
+to gain many useful equality proofs\footnote{It is suspected that OTT gains
+ \emph{all} the equality proofs of ETT, but no proof exists yet.}, including
+function extensionality. The main idea is to give the user the possibility to
+\emph{coerce} (or transport) values from a type $\mytya$ to a type $\mytyb$,
+if the type checker can prove structurally that $\mytya$ and $\mytya$ are
+equal; and providing a value-level equality based on similar principles. A
+brief overview is given below,
+
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \cdots \\
+ & | & \myprdec{\myprsyn} \mysynsep
+ \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
+ \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+ \myprsyn & ::= & \mybot \mysynsep \mytop \mysynsep \myprsyn \myand \myprsyn
+ \mysynsep \myprfora{\myb{x}}{\mytmsyn}{\myprsyn} \\\
+ & | & \mytmsyn = \mytmsyn \mysynsep
+ \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
+ \end{array}
+ $
+}
+\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
+ \centering{
+ }
+}
+
+The original presentation of OTT employs the theory presented above. It is
+close to the one presented in section \ref{sec:itt}, with the additions
+presented above, and the change that only one the `first' universe, the type
+of small types ($\mytyp_0$), is present.
+
+The propositional universe is meant to be where equality proofs live in. The
+equality proofs are respectively between types ($\mytya = \mytyb$), and
+between values
+
+
+
+However, only one universe is present ($\mytyp_0$), and a \emph{propositional}
+universe is isolated, intended to be the universe where equality proofs live
+in. Propositions (as long as our system is consistent) are inhabited only by
+one element, and thus can all be treated as definitionally equal.
+
+
+
+% \section{Augmenting ITT}
+% \label{sec:practical}
+
+% \subsection{A more liberal hierarchy}
+
+% \subsection{Type inference}
+
+% \subsubsection{Bidirectional type checking}
+
+% \subsubsection{Pattern unification}
+
+% \subsection{Pattern matching and explicit fixpoints}
+
+% \subsection{Induction-recursion}
+
+% \subsection{Coinduction}
+
+% \subsection{Dealing with partiality}
+
+% \subsection{Type holes}
+
+\section{\mykant : the theory}
+\label{sec:kant-theory}
+
+\mykant\ is an interactive theorem prover developed as part of this thesis.
+The plan is to present a core language which would be capable of serving as
+the basis for a more featureful system, while still presenting interesting
+features and more importantly observational equality.
+
+The author learnt the hard way the implementations challenges for such a
+project, and while there is a solid and working base to work on, observational
+equality is not currently implemented. However, a detailed plan on how to add
+it this functionality is provided, and should not prove to be too much work.
+
+The features currently implemented in \mykant\ are:
+
+\begin{description}
+\item[Full dependent types] As we would expect, we have dependent a system
+ which is as expressive as the `best' corner in the lambda cube described in
+ section \ref{sec:itt}.
+
+\item[Implicit, cumulative universe hierarchy] The user does not need to
+ specify universe level explicitly, and universes are \emph{cumulative}.
+
+\item[User defined data types and records] Instead of forcing the user to
+ choose from a restricted toolbox, we let her define inductive data types,
+ with associated primitive recursion operators; or records, with associated
+ projections for each field.
+
+\item[Bidirectional type checking] While no `fancy' inference via unification
+ is present, we take advantage of an type synthesis system in the style of
+ \cite{Pierce2000}, extending the concept for user defined data types.
+
+\item[Type holes] When building up programs interactively, it is useful to
+ leave parts unfinished while exploring the current context. This is what
+ type holes are for.
+\end{description}
+
+The planned features are:
+
+\begin{description}
+\item[Observational equality] As described in section \ref{sec:ott} but
+ extended to work with the type hierarchy and to admit equality between
+ arbitrary data types.
+
+\item[Coinductive data] ...
+\end{description}
+
+We will analyse the features one by one, along with motivations and tradeoffs
+for the design decisions made.
+
+\subsection{Bidirectional type checking}
+
+We start by describing bidirectional type checking since it calls for fairly
+different typing rules that what we have seen up to now. The idea is to have
+two kind of terms: terms for which a type can always be inferred, and terms
+that need to be checked against a type. A nice observation is that this
+duality runs through the semantics of the terms: data destructors (function
+application, record projections, primitive re cursors) \emph{infer} types,
+while data constructors (abstractions, record/data types data constructors)
+need to be checked. In the literature these terms are respectively known as
+
+To introduce the concept and notation, we will revisit the STLC in a
+bidirectional style. The presentation follows \cite{Loh2010}.
+
+% TODO do this --- is it even necessary
+
+% \subsubsection{Declarations and contexts}
+
+% A \mykant declaration can be one of 4 kinds:
+
+% \begin{description}
+% \item[Value] A declared variable, together with a type and a body.
+% \item[Postulate] An abstract variable, with a type but no body.
+% \item[Inductive data] A datatype, with a type constructor and various data
+% constructors---somewhat similar to what we find in Haskell. A primitive
+% recursor (or `destructor') will be generated automatically.
+% \item[Record] A record, which consists of one data constructor and various
+% fields, with no recursive occurrences. We will explain the need for records
+% later.
+% \end{description}
+
+% The syntax of
+
+\subsection{Base terms and types}
+
+Let us begin by describing the primitives available without the user defining
+any data types, and without equality. The syntax given here is the one of the
+core (`desugared') terms, and the way we handle variables and substitution is
+left unspecified, and explained in section \ref{sec:term-repr}, along with
+other implementation issues. We are also going to give an account of the
+implicit type hierarchy separately in section \ref{sec:term-hierarchy}, so as
+not to clutter derivation rules too much, and just treat types as
+impredicative for the time being.
+
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \mynamesyn \mysynsep \mytyp \\
+ & | & \myfora{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
+ \myabss{\myb{x}}{\mytmsyn}{\mytmsyn} \mysynsep
+ (\myapp{\mytmsyn}{\mytmsyn}) \mysynsep
+ (\myann{\mytmsyn}{\mytmsyn}) \\
+ \mynamesyn & ::= & \myb{x} \mysynsep \myfun{f}
+ \end{array}
+ $
+}
+
+The syntax for our calculus includes just two basic constructs: abstractions
+and $\mytyp$s. Everything else will be provided by user-definable constructs.
+Since we let the user define values, we will need a context capable of
+carrying the body of variables along with their type. We also want to make
+sure not to have duplicate top names, so we enforce that.
+
+% \mytyc{D} \mysynsep \mytyc{D}.\mydc{c}
+% \mysynsep \mytyc{D}.\myfun{f} \mysynsep
+
+\mydesc{context validity:}{\myvalid{\myctx}}{
+ \centering{
+ \begin{tabular}{ccc}
+ \AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
+ \UnaryInfC{$\myvalid{\myemptyctx}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytya}{\mytyp}$}
+ \AxiomC{$\mynamesyn \not\in \myctx$}
+ \BinaryInfC{$\myvalid{\myctx ; \mynamesyn : \mytya}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \AxiomC{$\myfun{f} \not\in \myctx$}
+ \BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
+ \DisplayProof
+ \end{tabular}
+ }
+}
+
+Now we can present the reduction rules, which are unsurprising. We have the
+usual functional application ($\beta$-reduction), but also a rule to replace
+names with their bodies, if in the context ($\delta$-reduction), and one to
+discard type annotations. For this reason the new reduction rules are
+dependent on the context:
+
+\mydesc{reduction:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
+ \centering{
+ \begin{tabular}{ccc}
+ \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
+ \UnaryInfC{$\myctx \vdash \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn}
+ \myred \mysub{\mytmm}{\myb{x}}{\mytmn}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myfun{f} \mapsto \mytmt : \mytya \in \myctx$}
+ \UnaryInfC{$\myctx \vdash \myfun{f} \myred \mytmt$}
+ \DisplayProof
+ &
+ \AxiomC{\phantom{$\myb{x} \mapsto \mytmt : \mytya \in \myctx$}}
+ \UnaryInfC{$\myctx \vdash \myann{\mytmm}{\mytya} \myred \mytmm$}
+ \DisplayProof
+ \end{tabular}
+ }
+}
+
+We want to define a \emph{weak head normal form} (WHNF) for our terms, to give
+a syntax directed presentation of type rules with no `conversion' rule. We
+will consider all \emph{canonical} forms (abstractions and data constructors)
+to be in weak head normal form... % TODO finish
+
+We can now give types to our terms. Using our definition of WHNF, I will use
+$\mytmm \mynf \mytmn$ to indicate that $\mytmm$'s normal form is $\mytmn$.
+This way, we can avoid the non syntax-directed conversion rule, giving a more
+algorithmic presentation of type checking.
+
+\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytysyn}{
+ \centering{
+ \begin{tabular}{ccc}
+ \AxiomC{$\myb{x} : A \in \myctx$ or $\myb{x} \mapsto \mytmt : A \in \myctx$}
+ \UnaryInfC{$\myinf{\myb{x}}{A}$}
+ \DisplayProof
+ &
+ \AxiomC{$\mychk{\mytmt}{\mytya}$}
+ \UnaryInfC{$\myinf{\myann{\mytmt}{\mytya}}{\mytya}$}
+ \DisplayProof
+ \end{tabular}
+ \myderivsp
+
+ \AxiomC{$\myinf{\mytmm}{\mytya}$}
+ \AxiomC{$\myctx \vdash \mytya \mynf \myfora{\myb{x}}{\mytyb}{\myse{C}}$}
+ \AxiomC{$\mychk{\mytmn}{\mytyb}$}
+ \TrinaryInfC{$\myinf{\myapp{\mytmm}{\mytmn}}{\mysub{\myse{C}}{\myb{x}}{\mytmn}}$}
+ \DisplayProof
+
+ \myderivsp
+
+ \AxiomC{$\myctx \vdash \mytya \mynf \myfora{\myb{x}}{\mytyb}{\myse{C}}$}
+ \AxiomC{$\mychkk{\myctx; \myb{x}: \mytyb}{\mytmt}{\myse{C}}$}
+ \BinaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\mytya}$}
+ \DisplayProof
+ }
+}
+
+\subsection{Elaboration}
+
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mydeclsyn & ::= & \myval{\myb{x}}{\mytmsyn}{\mytmsyn} \\
+ & | & \mypost{\myb{x}}{\mytmsyn} \\
+ & | & \myadt{\mytyc{D}}{\mytelesyn}{}{\mydc{c} : \mytelesyn\ |\ \cdots } \\
+ & | & \myreco{\mytyc{D}}{\mytelesyn}{}{\myfun{f} : \mytmsyn,\ \cdots } \\
+
+ \mytelesyn & ::= & \myemptytele \mysynsep \mytelesyn \mycc (\myb{x} {:} \mytmsyn)
+ \end{array}
+ $
+}
+
+\subsubsection{Values and postulated variables}
+
+\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
+ \centering{
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\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{$\myfun{f} \not\in \myctx$}
+ \BinaryInfC{
+ $
+ \myctx \myelabt \mypost{\myfun{f}}{\mytya}
+ \ \ \myelabf\ \ \myctx; \myfun{f} : \mytya
+ $
+ }
+ \DisplayProof
+ \end{tabular}
+}
+}
+
+\subsubsection{User defined types}
+
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{l}
+ \mynamesyn ::= \cdots \mysynsep \mytyc{D} \mysynsep \mytyc{D}.\mydc{c} \mysynsep \mytyc{D}.\myfun{f}
+ \end{array}
+ $
+}
+
+\subsubsection{Data types}
+
+\begin{figure}[t]
+ \mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
+ \centering{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \myvec{(\myb{x} {:} \mytya)} \ |\ \cdots } \\
+ & \myelabf &
+
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\myvec{\mytmsyn}} \mysynsep
+ \mytyc{D}.\mydc{c}_n \myappsp \myvec{\mytmsyn} \mysynsep \cdots \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
+ \end{array}
+ \end{array}
+ $
+ }
+ }
+
+ \mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
+ \centering{
+ \AxiomC{$\myinf{\mytele \myarr \mytyp}{\mytyp}$}
+ \AxiomC{$\mytyc{D} \not\in \myctx$}
+ \noLine
+ \BinaryInfC{$\myinff{\myctx;\ \mytyc{D} : \mytele \myarr \mytyp}{\mytele \mycc \mytele_i \myarr \myapp{\mytyc{D}}{\mytelee}}{\mytyp}\ \ \ (1 \leq i \leq n)$}
+ \noLine
+ \UnaryInfC{For each $(\myb{x} {:} \mytya)$ in each $\mytele_i$, if $\mytyc{D} \in \mytya$, then $\mytya = \myapp{\mytyc{D}}{\vec{\mytmt}}$.}
+ \UnaryInfC{$
+ \begin{array}{r@{\ }c@{\ }l}
+ \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{ \mydc{c} : \mytele_1 \ |\ \cdots \ |\ \mydc{c}_n : \mytele_n } \\
+ & & \vspace{-0.2cm} \\
+ & \myelabf & \myctx;\ \mytyc{D} : \mytele \mycc \mytyp;\ \mytyc{D}.\mydc{c}_1 : \mytele \mycc \mytele_1 \myarr \myapp{\mytyc{D}}{\mytelee};\ \cdots;\ \mytyc{D}.\mydc{c}_n : \mytele \mycc \mytele_n \myarr \myapp{\mytyc{D}}{\mytelee}; \\
+ & &
+ \begin{array}{@{}r@{\ }l l}
+ \mytyc{D}.\myfun{elim} : & \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr & \textbf{target} \\
+ & (\myb{P} {:} \myapp{\mytyc{D}}{\mytelee} \myarr \mytyp) \myarr & \textbf{motive} \\
+ & \left.
+ \begin{array}{@{}l}
+ (\mytele_1 \mycc \myhyps(\myb{P}, \mytele_1) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_1}{\mytelee_1})}) \myarr \\
+ \myind{3} \vdots \\
+ (\mytele_n \mycc \myhyps(\myb{P}, \mytele_n) \myarr \myapp{\myb{P}}{(\myapp{\mytyc{D}.\mydc{c}_n}{\mytelee_n})}) \myarr
+ \end{array} \right \}
+ & \textbf{methods} \\
+ & \myapp{\myb{P}}{\myb{x}} &
+ \end{array} \\
+ \\
+ \multicolumn{3}{l}{
+ \begin{array}{@{}l l@{\ } l@{} r c l}
+ \textbf{where} & \myhyps(\myb{P}, & \myemptytele &) & \mymetagoes & \myemptytele \\
+ & \myhyps(\myb{P}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{\mytmt}}) \mycc \mytele &) & \mymetagoes & (\myb{r'} {:} \myapp{\myb{P}}{\myb{r}}) \mycc \myhyps(\myb{P}, \mytele) \\
+ & \myhyps(\myb{P}, & (\myb{x} {:} \mytya) \mycc \mytele & ) & \mymetagoes & \myhyps(\myb{P}, \mytele)
+ \end{array}
+ }
+ \end{array}
+ $}
+ \DisplayProof
+ }
+ }
+
+ \mydesc{reduction elaboration:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
+ \centering{
+ \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
+ \AxiomC{$\mytyc{D}.\mydc{c}_i : \mytele;\mytele_i \myarr \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
+ \BinaryInfC{$
+ \begin{array}{c}
+ \myctx \vdash \myapp{\myapp{\myapp{\mytyc{D}.\myfun{elim}}{(\myapp{\mytyc{D}.\mydc{c}_i}{\vec{\myse{t}}})}}{\myse{P}}}{\vec{\myse{m}}} \myred \myapp{\myapp{\myse{m}_i}{\vec{\mytmt}}}{\myrecs(\myse{P}, \vec{m}, \mytele_i)} \\ \\
+ \begin{array}{@{}l l@{\ } l@{} r c l}
+ \textbf{where} & \myrecs(\myse{P}, \vec{m}, & \myemptytele &) & \mymetagoes & \myemptytele \\
+ & \myrecs(\myse{P}, \vec{m}, & (\myb{r} {:} \myapp{\mytyc{D}}{\vec{t}}); \mytele & ) & \mymetagoes & (\mytyc{D}.\myfun{elim} \myappsp \myb{r} \myappsp \myse{P} \myappsp \vec{m}); \myrecs(\myse{P}, \vec{m}, \mytele) \\
+ & \myrecs(\myse{P}, \vec{m}, & (\myb{x} {:} \mytya); \mytele &) & \mymetagoes & \myrecs(\myse{P}, \vec{m}, \mytele)
+ \end{array}
+ \end{array}
+ $}
+ \DisplayProof
+ }
+ }
+
+ \caption{Elaborations for data types.}
+ \label{fig:elab-adt}
+\end{figure}
+
+
+\subsubsection{Records}
+
+\begin{figure}[t]
+\mydesc{syntax elaboration:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
+ \centering{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \myctx & \myelabt & \myadt{\mytyc{D}}{\mytele}{}{\cdots\ |\ \mydc{c}_n : \myvec{(\myb{x} {:} \mytya)} \ |\ \cdots } \\
+ & \myelabf &
+
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \cdots \mysynsep \myapp{\mytyc{D}}{\myvec{\mytmsyn}} \mysynsep
+ \mytyc{D}.\mydc{c}_n \myappsp \myvec{\mytmsyn} \mysynsep \cdots \mysynsep \mytyc{D}.\myfun{elim} \myappsp \mytmsyn \\
+ \end{array}
+ \end{array}
+ $
+ }
+}
+
+
+\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
+ \centering{
+ \AxiomC{$\myinf{\mytele \myarr \mytyp}{\mytyp}$}
+ \AxiomC{$\mytyc{D} \not\in \myctx$}
+ \noLine
+ \BinaryInfC{$\myinff{\myctx; \mytele; (\myb{f}_j : \myse{F}_j)_{j=1}^{i - 1}}{F_i}{\mytyp} \myind{3} (1 \le i \le n)$}
+ \UnaryInfC{$
+ \begin{array}{r@{\ }c@{\ }l}
+ \myctx & \myelabt & \myreco{\mytyc{D}}{\mytele}{}{ \myfun{f}_1 : \myse{F}_1, \cdots, \myfun{f}_n : \myse{F}_n } \\
+ & & \vspace{-0.2cm} \\
+ & \myelabf & \myctx;\ \mytyc{D} : \mytele \myarr \mytyp;\\
+ & & \mytyc{D}.\myfun{f}_1 : \mytele \myarr \myapp{\mytyc{D}}{\mytelee} \myarr \myse{F}_1;\ \cdots;\ \mytyc{D}.\myfun{f}_n : \mytele \myarr (\myb{x} {:} \myapp{\mytyc{D}}{\mytelee}) \myarr \mysub{\myse{F}_n}{\myb{f}_i}{\myapp{\myfun{f}_i}{\myb{x}}}_{i = 1}^{n-1}; \\
+ & & \mytyc{D}.\mydc{constr} : \mytele \myarr \myse{F}_1 \myarr \cdots \myarr \myse{F}_n \myarr \myapp{\mytyc{D}}{\mytelee};
+ \end{array}
+ $}
+ \DisplayProof
+ }
+}
+
+ \mydesc{reduction elaboration:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
+ \centering{
+ \AxiomC{$\mytyc{D} \in \myctx$}
+ \UnaryInfC{$\myctx \vdash \myapp{\mytyc{D}.\myfun{f}_i}{(\mytyc{D}.\mydc{constr} \myappsp \vec{t})} \myred t_i$}
+ \DisplayProof
+ }
+ }
+
+ \caption{Elaborations for records.}
+ \label{fig:elab-adt}
+\end{figure}
+
+
+\subsection{Type hierarchy}
+\label{sec:term-hierarchy}
+
+\subsection{Defined and postulated variables}
+
+As mentioned, in \mykant\ we can defined top level variables, with or without
+a body. We call the variables
+
\subsection{Observational equality}
-\subsection{Univalence foundations}
+\section{\mykant : The practice}
+\label{sec:kant-practice}
-\section{Augmenting ITT}
-\label{sec:practical}
+The codebase consists of around 2500 lines of Haskell, as reported by the
+\texttt{cloc} utility. The high level design is heavily inspired by Conor
+McBride's work on various incarnations of Epigram, and specifically by the
+first version as described \citep{McBride2004} and the codebase for the new
+version \footnote{Available intermittently as a \texttt{darcs} repository at
+ \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.}. In many ways \mykant\ is
+something in between the first and second version of Epigram.
-\subsection{A more liberal hierarchy}
+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}.
-\subsection{Type inference}
+\begin{figure}
+ \centering{
+ \includegraphics[scale=1.0]{kant-web.png}
+ }
+ \caption{The \mykant\ web prompt.}
+ \label{fig:kant-web}
+\end{figure}
-\subsubsection{Bidirectional type checking}
+The interaction with the user takes place in a loop living in and updating a
+context \mykant\ declarations. The user inputs a new declaration that goes
+through various stages 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}:
-\subsubsection{Pattern unification}
+\begin{description}
+\item[Parse] In this phase the text input gets converted to a sugared
+ version of the core language.
-\subsection{Pattern matching and explicit fixpoints}
+\item[Desugar] The sugared declaration is converted to a core term.
-\subsection{Induction-recursion}
+\item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
+ which is necessary to implement the type hierarchy check.
-\subsection{Coinduction}
+\item[Elaborate] Convert the declaration to some context item, which might be
+ a value declaration (type and body) or a data type declaration (constructors
+ and destructors). This phase works in tandem with \textbf{Typechecking},
+ which in turns needs to \textbf{Evaluate} terms.
-\subsection{Dealing with partiality}
+\item[Distill] and report the result. `Distilling' refers to the process of
+ converting a core term back to a sugared version that the user can
+ visualise. This can be necessary both to display errors including terms or
+ to display result of evaluations or type checking that the user has
+ requested.
-\subsection{Type holes}
+\item[Pretty print] Format the terms in a nice way, and display the result to
+ the user.
-\section{\mykant}
-\label{sec:kant}
+\end{description}
+The details of each phase will be described in section % TODO insert section
+
+\begin{figure}
+ \centering{\small
+ \tikzstyle{block} = [rectangle, draw, text width=5em, text centered, rounded
+ corners, minimum height=2.5em, node distance=0.7cm]
+
+ \tikzstyle{decision} = [diamond, draw, text width=4.5em, text badly
+ centered, inner sep=0pt, node distance=0.7cm]
+
+ \tikzstyle{line} = [draw, -latex']
+
+ \tikzstyle{cloud} = [draw, ellipse, minimum height=2em, text width=5em, text
+ centered, node distance=1.5cm]
+
+
+ \begin{tikzpicture}[auto]
+ \node [cloud] (user) {User};
+ \node [block, below left=1cm and 0.1cm of user] (parse) {Parse};
+ \node [block, below=of parse] (desugar) {Desugar};
+ \node [block, below=of desugar] (reference) {Reference};
+ \node [block, below=of reference] (elaborate) {Elaborate};
+ \node [block, left=of elaborate] (tycheck) {Typecheck};
+ \node [block, left=of tycheck] (evaluate) {Evaluate};
+ \node [decision, right=of elaborate] (error) {Error?};
+ \node [block, right=of parse] (distill) {Distill};
+ \node [block, right=of desugar] (update) {Update context};
+
+ \path [line] (user) -- (parse);
+ \path [line] (parse) -- (desugar);
+ \path [line] (desugar) -- (reference);
+ \path [line] (reference) -- (elaborate);
+ \path [line] (elaborate) edge[bend right] (tycheck);
+ \path [line] (tycheck) edge[bend right] (elaborate);
+ \path [line] (elaborate) -- (error);
+ \path [line] (error) edge[out=0,in=0] node [near start] {yes} (distill);
+ \path [line] (error) -- node [near start] {no} (update);
+ \path [line] (update) -- (distill);
+ \path [line] (distill) -- (user);
+ \path [line] (tycheck) edge[bend right] (evaluate);
+ \path [line] (evaluate) edge[bend right] (tycheck);
+ \end{tikzpicture}
+ }
+ \caption{High level overview of the life of a \mykant\ prompt cycle.}
+ \label{fig:kant-process}
+\end{figure}
+
+\subsection{Term representation}
+\label{sec:term-repr}
+
+\subsection{Type hierarchy}
+
+\subsection{Elaboration}
+
+\section{Evaluation}
+
+\section{Future work}
\appendix
for example
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
- Typing derivations here.
+ \centering{Typing derivations here.}
}
In the languages presented and Agda code samples I also highlight the syntax,
(x : W S P) → -- If so, ...
C x -- ...C always holds.
rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
+
+ data _≡_ {a} {A : Set a} : A → A → Set a where
+ refl : ∀ x → x ≡ x
+
+ ≡-elim : ∀ {a b} {A : Set a}
+ (P : (x y : A) → x ≡ y → Set b) →
+ ∀ {x y} → P x x (refl x) → (x≡y : x ≡ y) → P x y x≡y
+ ≡-elim P p (refl x) = p
+
+ subst : ∀ {a b} {A : Set a}
+ (P : A → Set b) →
+ ∀ {x y} → (x≡y : x ≡ y) → P x → P y
+ subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
\end{code}
\nocite{*}
projects / bitonic-mengthesis.git / blobdiff