\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*}}
\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}}$}
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{
$
\DisplayProof
}
-\subsubsection{Why user defined types? Why eliminators?}
+\subsubsection{Why user defined types? Why eliminators? Why no inductive families?}
-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 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.
\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}
However, given the detailed plan in the previous section, doing so
should not prove to be 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 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}.
\begin{figure}[t]
{\small\begin{verbatim}B E R T U S
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}
+
+\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.}} \\
+ \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}
+
+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}
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}
it would generate the graph shown in Figure \ref{fig:graph-one}.
\begin{figure}[t]
-
+
\end{figure}
\subsection{Type holes}
(\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 / commitdiff