\documentclass[report]{article}
+\usepackage{etex}
%% Narrow margins
% \usepackage{fullpage}
%% Images
\usepackage{graphicx}
+%% Subfigure
+\usepackage{subcaption}
+
%% diagrams
\usepackage{tikz}
\usetikzlibrary{shapes,arrows,positioning}
\newcommand{\mysyn}{\AgdaKeyword}
\newcommand{\mytyc}{\AgdaDatatype}
+% TODO have this with math mode so I can have subscripts
\newcommand{\mydc}{\AgdaInductiveConstructor}
\newcommand{\myfld}{\AgdaField}
\newcommand{\myfun}{\AgdaFunction}
-% TODO make this use AgdaBound
-\newcommand{\myb}[1]{\AgdaBound{#1}}
+\newcommand{\myb}[1]{\AgdaBound{$#1$}}
\newcommand{\myfield}{\AgdaField}
\newcommand{\myind}{\AgdaIndent}
\newcommand{\mykant}{\textsc{Kant}}
\newcommand{\myse}{\mysynel}
\newcommand{\mytmsyn}{\mysynel{term}}
\newcommand{\mysp}{\ }
-% TODO \mathbin or \mathre here?
\newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
\newcommand{\myappsp}{\hspace{0.07cm}}
\newcommand{\myapp}[2]{#1 \myappsp #2}
\framebox[\textwidth]{
\parbox{\textwidth}{
\vspace{0.1cm}
- #3
+ \centering{
+ #3
+ }
\vspace{0.1cm}
}
}
\newcommand{\myempty}{\mytyc{Empty}}
\newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
\newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
-\newcommand{\myarg}{\_}
+\newcommand{\myarg}{-}
\newcommand{\myderivsp}{\vspace{0.3cm}}
\newcommand{\mytyp}{\mytyc{Type}}
\newcommand{\myneg}{\myfun{$\neg$}}
\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{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathopen{\mytyc{$\rrbracket$}}}
+\newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
\newcommand{\myprfora}[3]{\forall #1 {:} #2. #3}
-\newcommand{\mybot}{\bot}
-\newcommand{\mytop}{\top}
+\newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
+\newcommand{\mybot}{\mytyc{$\bot$}}
+\newcommand{\mytop}{\mytyc{$\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{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
+\newcommand{\myeq}{\mathrel{\mytyc{=}}}
\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\ \mysyn{where}\ #3\{ #4 \}}
+\newcommand{\myreco}[4]{\mysyn{record}\ #1 : #2\ \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}}
+\newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
%% -----------------------------------------------------------------------------
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
of this idea takes the name of \emph{simply typed $\lambda$ calculus}, whose
rules are shown in figure \ref{fig:stlc}.
-Our types contain a set of \emph{type variables} $\Phi$, which might correspond
-to some `primitive' types; and $\myarr$, the type former for `arrow' types, the
-types of functions. The language is explicitly typed: when we bring a variable
-into scope with an abstraction, we explicitly declare its type. $\mytya$,
-$\mytyb$, $\mytycc$, will be used to refer to a generic type. Reduction is
-unchanged from the untyped $\lambda$-calculus.
+Our types contain a set of \emph{type variables} $\Phi$, which might
+correspond to some `primitive' types; and $\myarr$, the type former for
+`arrow' types, the types of functions. The language is explicitly
+typed: when we bring a variable into scope with an abstraction, we
+explicitly declare its type. Reduction is unchanged from the untyped
+$\lambda$-calculus.
\begin{figure}[t]
\mydesc{syntax}{ }{
}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
- \centering{
\begin{tabular}{ccc}
\AxiomC{$\myctx(x) = A$}
\UnaryInfC{$\myjud{\myb{x}}{A}$}
\BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
\DisplayProof
\end{tabular}
- }
}
\caption{Syntax and typing rules for the STLC. Reduction is unchanged from
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}
\begin{minipage}{0.5\textwidth}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}} {
- \centering{
\AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\mytmt}{\mytya}$}
\UnaryInfC{$\myjud{\myfix{\myb{x}}{\mytya}{\mytmt}}{\mytya}$}
\DisplayProof
- }
}
\end{minipage}
\mydesc{reduction:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
$ \myfix{\myb{x}}{\mytya}{\mytmt} \myred \mysub{\mytmt}{\myb{x}}{(\myfix{\myb{x}}{\mytya}{\mytmt})}$
- }
}
This will deprive us of normalisation, which is a particularly bad thing if we
\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{reduction:}{\mytmsyn \myred \mytmsyn}{
- \centering{
\begin{tabular}{cc}
$
\begin{array}{l@{ }l@{\ }c@{\ }l}
\end{array}
$
\end{tabular}
- }
}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
- \centering{
\begin{tabular}{cc}
\AxiomC{\phantom{$\myjud{\mytmt}{\myempty}$}}
\UnaryInfC{$\myjud{\mytt}{\myunit}$}
\UnaryInfC{$\myjud{\myapp{\myabsurd{\mytya}}{\mytmt}}{\mytya}$}
\DisplayProof
\end{tabular}
- }
+
\myderivsp
- \centering{
+
\begin{tabular}{cc}
\AxiomC{$\myjud{\mytmt}{\mytya}$}
\UnaryInfC{$\myjud{\myapp{\myleft{\mytyb}}{\mytmt}}{\mytya \mysum \mytyb}$}
\DisplayProof
\end{tabular}
- }
+
\myderivsp
- \centering{
+
\begin{tabular}{cc}
\AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
\AxiomC{$\myjud{\mytmn}{\mytya \myarr \mytycc}$}
\TrinaryInfC{$\myjud{\myapp{\mycase{\mytmm}{\mytmn}}{\mytmt}}{\mytycc}$}
\DisplayProof
\end{tabular}
- }
+
\myderivsp
- \centering{
+
\begin{tabular}{ccc}
\AxiomC{$\myjud{\mytmm}{\mytya}$}
\AxiomC{$\myjud{\mytmn}{\mytyb}$}
\UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
\DisplayProof
\end{tabular}
- }
}
\caption{Rules for the extendend STLC. Only the new features are shown, all the
rules and syntax for the STLC apply here too.}
\label{fig:natded}
\end{figure}
-Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either} in
-Haskell) correspond to disjunctions, and dually tuples (or pairs, or
-products---$\myprod$ here, tuples in Haskell) correspond to conjunctions. This
-is apparent looking at the ways to construct and destruct the values inhabiting
-those types: for $\mysum$ $\myleft{ }$ and $\myright{ }$ correspond to $\vee$
-introduction, and $\mycase{\_}{\_}$ to $\vee$ elimination; for $\myprod$
-$\mypair{\_}{\_}$ corresponds to $\wedge$ introduction, $\myfst$ and $\mysnd$ to
-$\wedge$ elimination.
+Tagged unions (or sums, or coproducts---$\mysum$ here, \texttt{Either}
+in Haskell) correspond to disjunctions, and dually tuples (or pairs, or
+products---$\myprod$ here, tuples in Haskell) correspond to
+conjunctions. This is apparent looking at the ways to construct and
+destruct the values inhabiting those types: for $\mysum$ $\myleft{ }$
+and $\myright{ }$ correspond to $\vee$ introduction, and
+$\mycase{\myarg}{\myarg}$ to $\vee$ elimination; for $\myprod$
+$\mypair{\myarg}{\myarg}$ corresponds to $\wedge$ introduction, $\myfst$
+and $\mysnd$ to $\wedge$ elimination.
The trivial type $\myunit$ corresponds to the logical $\top$, and dually
$\myempty$ corresponds to the logical $\bot$. $\myunit$ has one introduction
rule ($\mytt$), and thus one inhabitant; and no eliminators. $\myempty$ has no
introduction rules, and thus no inhabitants; and one eliminator ($\myabsurd{
-}$), corresponding to the logical \emph{ex falso quodlibet}. Note that in the
-constructors for the sums and the destructor for $\myempty$ we need to include
-some type information to keep type checking decidable.
+}$), corresponding to the logical \emph{ex falso quodlibet}.
With these rules, our STLC now looks remarkably similar in power and use to the
natural deduction we already know. $\myneg \mytya$ can be expressed as $\mytya
\]
\subsection{Inductive data}
+\label{sec:ind-data}
To make the STLC more useful as a programming language or reasoning tool it is
common to include (or let the user define) inductive data types. These comprise
\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}
$
}
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
- \centering{
$
\begin{array}{l@{\ }c@{\ }l}
\myapp{\myapp{\myapp{\myfoldr}{\myse{f}}}{\mytmt}}{\mynil{\mytya}} & \myred & \mytmt \\
\end{array}
$
}
-}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
- \centering{
\begin{tabular}{cc}
\AxiomC{\phantom{$\myjud{\mytmm}{\mytya}$}}
\UnaryInfC{$\myjud{\mynil{\mytya}}{\myapp{\mylist}{\mytya}}$}
\BinaryInfC{$\myjud{\mytmm \mycons \mytmn}{\myapp{\mylist}{\mytya}}$}
\DisplayProof
\end{tabular}
- }
\myderivsp
- \centering{
+
\AxiomC{$\myjud{\mysynel{f}}{\mytya \myarr \mytyb \myarr \mytyb}$}
\AxiomC{$\myjud{\mytmm}{\mytyb}$}
\AxiomC{$\myjud{\mytmn}{\myapp{\mylist}{\mytya}}$}
\TrinaryInfC{$\myjud{\myapp{\myapp{\myapp{\myfoldr}{\mysynel{f}}}{\mytmm}}{\mytmn}}{\mytyb}$}
\DisplayProof
- }
}
\caption{Rules for lists in the STLC.}
\label{fig:list}
\subsection{A simple type theory}
\label{sec:core-tt}
-The calculus I present follows the exposition in \citep{Thompson1991}, and is
-quite close to the original formulation of predicative ITT as found in
-\citep{Martin-Lof1984}. The system's syntax and reduction rules are presented
-in their entirety in figure \ref{fig:core-tt-syn}. The typing rules are
-presented piece by piece. An Agda rendition of the presented theory is
-reproduced in appendix \ref{app:agda-code}.
+The calculus I present follows the exposition in \citep{Thompson1991},
+and is quite close to the original formulation of predicative ITT as
+found in \citep{Martin-Lof1984}. The system's syntax and reduction
+rules are presented in their entirety in figure \ref{fig:core-tt-syn}.
+The typing rules are presented piece by piece. An Agda rendition of the
+presented theory and all the examples is reproduced in appendix
+\ref{app:agda-itt}.
\begin{figure}[t]
\mydesc{syntax}{ }{
& | & \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} \\
}
\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
- \centering{
- \begin{tabular}{cc}
+ \begin{tabular}{ccc}
$
\begin{array}{l@{ }l@{\ }c@{\ }l}
\myitee{\mytrue &}{\myb{x}}{\myse{P}}{\mytmm}{\mytmn} & \myred & \mytmm \\
$
\myapp{(\myabss{\myb{x}}{\mytya}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{\myb{x}}{\mytmn}
$
- \myderivsp
- \end{tabular}
+ &
$
\begin{array}{l@{ }l@{\ }c@{\ }l}
\myapp{\myfst &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
\myapp{\mysnd &}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
\end{array}
$
+ \end{tabular}
+
\myderivsp
$
\myrec{\myapp{\myse{f}}{\myb{t}}}{\myb{y}}{\myse{P}}{\mytmt}
})}
$
- }
}
\caption{Syntax and reduction rules for our type theory.}
\label{fig:core-tt-syn}
\label{sec:term-types}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\begin{tabular}{cc}
\AxiomC{$\myjud{\mytmt}{\mytya}$}
\AxiomC{$\mytya \mydefeq \mytyb$}
\UnaryInfC{$\myjud{\mytyp_l}{\mytyp_{l + 1}}$}
\DisplayProof
\end{tabular}
- }
}
The first thing to notice is that a barrier between values and types that we had
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
+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
\begin{minipage}{0.5\textwidth}
\mydesc{context validity:}{\myvalid{\myctx}}{
- \centering{
\begin{tabular}{cc}
\AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
\UnaryInfC{$\myvalid{\myemptyctx}$}
\UnaryInfC{$\myvalid{\myctx ; \myb{x} : \mytya}$}
\DisplayProof
\end{tabular}
- }
}
\end{minipage}
\begin{minipage}{0.5\textwidth}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\AxiomC{$\myctx(x) = \mytya$}
\UnaryInfC{$\myjud{\myb{x}}{\mytya}$}
\DisplayProof
- }
}
\end{minipage}
\vspace{0.1cm}
\subsubsection{$\myunit$, $\myempty$}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\begin{tabular}{ccc}
\AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
\UnaryInfC{$\myjud{\myunit}{\mytyp_0}$}
\UnaryInfC{\phantom{$\myjud{\myempty}{\mytyp_0}$}}
\DisplayProof
\end{tabular}
- }
}
Nothing surprising here: $\myunit$ and $\myempty$ are unchanged from the STLC,
\subsubsection{$\mybool$, and dependent $\myfun{if}$}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\begin{tabular}{ccc}
\AxiomC{}
\UnaryInfC{$\myjud{\mybool}{\mytyp_0}$}
\BinaryInfC{$\myjud{\mytmm}{\mysub{\mytya}{x}{\mytrue}}$ \hspace{0.7cm} $\myjud{\mytmn}{\mysub{\mytya}{x}{\myfalse}}$}
\UnaryInfC{$\myjud{\myitee{\mytmt}{\myb{x}}{\mytya}{\mytmm}{\mytmn}}{\mysub{\mytya}{\myb{x}}{\mytmt}}$}
\DisplayProof
-
- }
}
With booleans we get the first taste of `dependent' in `dependent types'. While
\subsubsection{$\myarr$, or dependent function}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
\AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
\BinaryInfC{$\myjud{\myfora{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
\BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mysub{\mytyb}{\myb{x}}{\mytmn}}$}
\DisplayProof
\end{tabular}
- }
}
Dependent functions are one of the two key features that perhaps most
characterise dependent types---the other being dependent products. With
-dependent functions, the result type can depend on the value of the argument.
-This feature, together with the fact that the result type might be a type
-itself, brings a lot of interesting possibilities. Keeping the correspondence
-with logic alive, dependent functions are much like universal quantifiers
-($\forall$) in logic.
+dependent functions, the result type can depend on the value of the
+argument. This feature, together with the fact that the result type
+might be a type itself, brings a lot of interesting possibilities.
+Following this intuition, in the introduction rule, the return type is
+typechecked in a context with an abstracted variable of lhs' type, and
+in the elimination rule the actual argument is substituted in the return
+type. Keeping the correspondence with logic alive, dependent functions
+are much like universal quantifiers ($\forall$) in logic.
+
+For example, assuming that we have lists and natural numbers in our
+language, using dependent functions we would be able to
+write:
+\[
+\begin{array}{c@{\ }c@{\ }l@{\ }}
+\myfun{length} & : & (\myb{A} {:} \mytyp_0) \myarr \myapp{\mylist}{\myb{A}} \myarr \mynat \\
+\myarg \myfun{$>$} \myarg & : & \mynat \myarr \mynat \myarr \mytyp_0 \\
+\myfun{head} & : & (\myb{A} {:} \mytyp_0) \myarr (\myb{l} {:} \myapp{\mylist}{\myb{A}})
+ \myarr \myapp{\myapp{\myfun{length}}{\myb{A}}}{\myb{l}} \mathrel{\myfun{>}} 0 \myarr
+ \myb{A}
+\end{array}
+\]
+
+\myfun{length} is the usual polymorphic length function. $\myfun{>}$ is
+a function that takes two naturals and returns a type: if the lhs is
+greater then the rhs, $\myunit$ is returned, $\myempty$ otherwise. This
+way, we can express a `non-emptyness' condition in $\myfun{head}$, by
+including a proof that the length of the list argument is non-zero.
+This allows us to rule out the `empty list' case, so that we can safely
+return the first element.
Again, we need to make sure that the type hierarchy is respected, which is the
reason why a type formed by $\myarr$ will live in the least upper bound of the
levels of argument and return type. This trend will continue with the other
type-level binders, $\myprod$ and $\mytyc{W}$.
-% TODO maybe examples?
-
\subsubsection{$\myprod$, or dependent product}
-
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
\AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
\BinaryInfC{$\myjud{\myexi{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
\UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mysub{\mytyb}{\myb{x}}{\myapp{\myfst}{\mytmt}}}$}
\DisplayProof
\end{tabular}
-
- }
}
+If dependent functions are a generalisation of $\myarr$ in the STLC,
+dependent products are a generalisation of $\myprod$ in the STLC. The
+improvement is that the second element's type can depend on the value of
+the first element. The corrispondence with logic is through the
+existential quantifier: $\exists x \in \mathbb{N}. even(x)$ can be
+expressed as $\myexi{\myb{x}}{\mynat}{\myapp{\myfun{even}}{\myb{x}}}$.
+The first element will be a number, and the second evidence that the
+number is even. This highlights the fact that we are working in a
+constructive logic: if we have an existence proof, we can always ask for
+a witness. This means, for instance, that $\neg \forall \neg$ is not
+equivalent to $\exists$.
\subsubsection{$\mytyc{W}$, or well-order}
\label{sec:well-order}
\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
- \centering{
\AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
\AxiomC{$\myjudd{\myctx;\myb{x} : \mytya}{\mytyb}{\mytyp_{l_2}}$}
\BinaryInfC{$\myjud{\myw{\myb{x}}{\mytya}{\mytyb}}{\mytyp_{l_1 \mylub l_2}}$}
}$}
\UnaryInfC{$\myjud{\myrec{\myse{u}}{\myb{w}}{\myse{P}}{\myse{p}}}{\mysub{\myse{P}}{\myb{w}}{\myse{u}}}$}
\DisplayProof
- }
}
\section{The struggle for equality}
\label{sec: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.
+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. As in the previous section, everything presented is
+formalised in Agda in appendix \ref{app:agda-code}.
\subsection{Propositional equality}
\mydesc{syntax}{ }{
$
\begin{array}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \dots \\
+ \mytmsyn & ::= & \cdots \\
& | & \mytmsyn \mypeq{\mytmsyn} \mytmsyn \mysynsep
\myapp{\myrefl}{\mytmsyn} \\
& | & \myjeq{\mytmsyn}{\mytmsyn}{\mytmsyn}
\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}$}
\begin{tabular}{cc}
\AxiomC{\phantom{$\myctx P \mytyp_l$}}
\noLine
- \UnaryInfC{$\myjud{\mytmt}{\mytya}$}
- \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmt}}{\mytmt \mypeq{\mytya} \mytmt}$}
+ \UnaryInfC{$\myjud{\mytmm}{\mytya}\hspace{1.1cm}\mytmm \mydefeq \mytmn$}
+ \UnaryInfC{$\myjud{\myapp{\myrefl}{\mytmm}}{\mytmm \mypeq{\mytya} \mytmn}$}
\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{\myse{q}}{\mytmm \mypeq{\mytya} \mytmn}\hspace{1.1cm}\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 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
+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 extensionally equal, and we can in fact
+prove that
\[
\myfora{\myb{x}}{\mynat}{(0 \mathrel{\myfun{+}} \myb{x}) \mypeq{\mynat} (\myb{x} \mathrel{\myfun{+}} 0)}
\]
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
\[\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}}}$}
+ \AxiomC{$\hspace{1.1cm}\myjudd{\myctx; \myb{x} : \myb{A}}{\myapp{\myb{q}}{\myb{x}}}{\myapp{\myb{f}}{\myb{x}} \mypeq{} \myapp{\myb{g}}{\myb{x}}}\hspace{1.1cm}$}
\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}}$}
+ \UnaryInfC{$\hspace{1.4cm}\myjud{\myb{f} \mydefeq \myb{g}}{\myb{A} \myarr \myb{B}}\hspace{1.4cm}$}
\RightLabel{$\myrefl$}
\UnaryInfC{$\myjud{\myapp{\myrefl}{\myb{f}}}{\myb{f} \mypeq{} \myb{g}}$}
\end{prooftree}
gain extensionality?
\subsection{Observational equality}
-\ref{sec:ott}
+\label{sec:ott}
% TODO should we explain this in detail?
A recent development by \citet{Altenkirch2007}, \emph{Observational Type
brief overview is given below,
\mydesc{syntax}{ }{
+ $\mytyp_l$ is replaced by $\mytyp$. \\
+ $
+ \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 \myeq \mytmsyn \mysynsep
+ \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
+ \end{array}
+ $
+}
+
+\mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
+
+ There is only $\mytyp$, which corresponds to $\mytyp_0$. \\ Thus all
+ the type-formers take $\mytyp$ arguments and form a $\mytyp$. \\ \ \\
+
+ % TODO insert large eliminator
+
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\myse{P}}{\myprop}$}
+ \UnaryInfC{$\myjud{\myprdec{\myse{P}}}{\mytyp}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \BinaryInfC{$\myjud{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}$}
+ \DisplayProof
+ \end{tabular}
+
+ \myderivsp
+
+ \AxiomC{$\myjud{\myse{P}}{\myprdec{\mytya \myeq \mytyb}}$}
+ \AxiomC{$\myjud{\mytmt}{\mytya}$}
+ \BinaryInfC{$\myjud{\mycohh{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\myprdec{\myjm{\mytmt}{\mytya}{\mycoee{\mytya}{\mytyb}{\myse{P}}{\mytmt}}{\mytyb}}}$}
+ \DisplayProof
+}
+
+\mydesc{propositions:}{\myjud{\myprsyn}{\myprop}}{
+ \begin{tabular}{cc}
+ \AxiomC{\phantom{$\myjud{\myse{P}}{\myprop}$}}
+ \UnaryInfC{$\myjud{\mytop}{\myprop}$}
+ \noLine
+ \UnaryInfC{$\myjud{\mybot}{\myprop}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{P}}{\myprop}$}
+ \AxiomC{$\myjud{\myse{Q}}{\myprop}$}
+ \BinaryInfC{$\myjud{\myse{P} \myand \myse{Q}}{\myprop}$}
+ \noLine
+ \UnaryInfC{\phantom{$\myjud{\mybot}{\myprop}$}}
+ \DisplayProof
+ \end{tabular}
+
+ \myderivsp
+
+ \begin{tabular}{cc}
+ \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
+ \AxiomC{$\myjudd{\myctx; \myb{x} : \mytya}{\myse{P}}{\myprop}$}
+ \BinaryInfC{$\myjud{\myprfora{\myb{x}}{\mytya}{\myse{P}}}{\myprop}$}
+ \DisplayProof
+ &
+ \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
+ \AxiomC{$\myjud{\myse{B}}{\mytyp}$}
+ \BinaryInfC{$\myjud{\mytya \myeq \mytyb}{\myprop}$}
+ \DisplayProof
+ \end{tabular}
+
+ \myderivsp
+
+ \AxiomC{$\myjud{\myse{A}}{\mytyp}$}
+ \AxiomC{$\myjud{\mytmm}{\myse{A}}$}
+ \AxiomC{$\myjud{\myse{B}}{\mytyp}$}
+ \AxiomC{$\myjud{\mytmn}{\myse{B}}$}
+ \QuaternaryInfC{$\myjud{\myjm{\mytmm}{\myse{A}}{\mytmn}{\myse{B}}}{\myprop}$}
+ \DisplayProof
+}
+
+\mydesc{proposition decoding:}{\myprdec{\mytmsyn} \myred \mytmsyn}{
+ \begin{tabular}{cc}
+ $
+ \begin{array}{l@{\ }c@{\ }l}
+ \myprdec{\mybot} & \myred & \myempty \\
+ \myprdec{\mytop} & \myred & \myunit
+ \end{array}
+ $
+ &
+ $
+ \begin{array}{r@{ }c@{ }l@{\ }c@{\ }l}
+ \myprdec{&\myse{P} \myand \myse{Q} &} & \myred & \myprdec{\myse{P}} \myprod \myprdec{\myse{Q}} \\
+ \myprdec{&\myprfora{\myb{x}}{\mytya}{\myse{P}} &} & \myred &
+ \myfora{\myb{x}}{\mytya}{\myprdec{\myse{P}}}
+ \end{array}
+ $
+ \end{tabular}
+}
+
+\mydesc{equality reduction:}{\myprsyn \myred \myprsyn}{
+ $
+ \begin{array}{c@{\ }c@{\ }c@{\ }l}
+ \myempty & \myeq & \myempty & \myred \mytop \\
+ \myunit & \myeq & \myunit & \myred \mytop \\
+ \mybool & \myeq & \mybool & \myred \mytop \\
+ \myexi{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myexi{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \\
+ \multicolumn{4}{l}{
+ \myind{2} \mytya_1 \myeq \mytyb_1 \myand
+ \myprfora{\myb{x_1}}{\mytya_1}{\myprfora{\myb{x_2}}{\mytya_2}{\myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2}} \myimpl \mytyb_1 \myeq \mytyb_2}
+ } \\
+ \myfora{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myfora{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
+ \myw{\myb{x_1}}{\mytya_1}{\mytyb_1} & \myeq & \myw{\myb{x_2}}{\mytya_2}{\mytyb_2} & \myred \cdots \\
+ \mytya & \myeq & \mytyb & \myred \mybot\ \text{for other canonical types.}
+ \end{array}
+ $
+}
+
+\mydesc{reduction}{\mytmsyn \myred \mytmsyn}{
$
- \begin{array}{r@{\ }c@{\ }l}
- \mytmsyn & ::= & \dots \\
- & | & \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}
+ \begin{array}{l@{\ }l@{\ }l@{\ }l@{\ }l@{\ }c@{\ }l@{\ }}
+ \mycoe & \myempty & \myempty & \myse{Q} & \myse{t} & \myred & \myse{t} \\
+ \mycoe & \myunit & \myunit & \myse{Q} & \mytt & \myred & \mytt \\
+ \mycoe & \mybool & \mybool & \myse{Q} & \mytrue & \myred & \mytrue \\
+ \mycoe & \mybool & \mybool & \myse{Q} & \myfalse & \myred & \myfalse \\
+ \mycoe & (\myexi{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
+ (\myexi{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
+ \mytmt_1 & \myred &
+ foo \\
+ \mycoe & (\myfora{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
+ (\myfora{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
+ \mytmt_1 & \myred &
+ \cdots \\
+
+ \mycoe & (\myw{\myb{x_1}}{\mytya_1}{\mytyb_1}) &
+ (\myw{\myb{x_2}}{\mytya_2}{\mytyb_2}) & \myse{Q} &
+ \mytmt_1 & \myred &
+ \cdots \\
+
+ \mycoe & \mytya & \mytyb & \myse{Q} & \mytmt & \myred & \myapp{\myabsurd{\mytyb}}{\myse{Q}}
\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
-\section{Augmenting ITT}
-\label{sec:practical}
+% \section{Augmenting ITT}
+% \label{sec:practical}
-\subsection{A more liberal hierarchy}
+% \subsection{A more liberal hierarchy}
-\subsection{Type inference}
+% \subsection{Type inference}
-\subsubsection{Bidirectional type checking}
+% \subsubsection{Bidirectional type checking}
-\subsubsection{Pattern unification}
+% \subsubsection{Pattern unification}
-\subsection{Pattern matching and explicit fixpoints}
+% \subsection{Pattern matching and explicit fixpoints}
-\subsection{Induction-recursion}
+% \subsection{Induction-recursion}
-\subsection{Coinduction}
+% \subsection{Coinduction}
-\subsection{Dealing with partiality}
+% \subsection{Dealing with partiality}
-\subsection{Type holes}
+% \subsection{Type holes}
-\section{\mykant}
-\label{sec:kant}
+\section{\mykant : the theory}
+\label{sec:kant-theory}
-\mykant is an interactive theorem prover developed as part of this thesis.
+\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.
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.
-\subsection{High level overview}
-
-\subsubsection{Features}
-
-The features currently implemented in \mykant are:
+The features currently implemented in \mykant\ are:
\begin{description}
\item[Full dependent types] As we would expect, we have dependent a system
The planned features are:
\begin{description}
-\item[Observational equality] As described in section \label{sec:ott} but
+\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.
We will analyse the features one by one, along with motivations and tradeoffs
for the design decisions made.
-\subsubsection{Implementation}
+\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}}{
+ \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}{
+ \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 \mytmsyn}{
+ \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}
+ $
+}
+
+\mydesc{typing:}{\myctx \vdash \mytmsyn \Leftrightarrow \mytmsyn}{
+
+}
+
+\subsubsection{Values and postulated variables}
+
+As mentioned, in \mykant\ we can defined top level variables, with or without
+a body. We call the variables
+
+\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
+ \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}
+ $
+}
+
+\mydesc{typing:}{ }{
+ \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
+ \AxiomC{$\mytyc{D}.\mydc{c} : \mytele \mycc \mytele' \myarr
+ \myapp{\mytyc{D}}{\mytelee} \in \myctx$}
+ \BinaryInfC{$\mychk{\myapp{\mytyc{D}.\mydc{c}}{\vec{t}}}{\myapp{\mytyc{D}}{\vec{A}}}$}
+ \DisplayProof
+ % TODO
+
+ \myderivsp
+
+ \AxiomC{$\mytyc{D} : \mytele \myarr \mytyp \in \myctx$}
+ \AxiomC{$\mytyc{D}.\myfun{f} : \mytele \myarr
+ \myapp{\mytyc{D}}{\mytelee} \myarr \myse{F}$}
+ \AxiomC{$\myjud{\mytmt}{\myapp{\mytyc{D}}{\vec{A}}}$}
+ \TrinaryInfC{$\myinf{\myapp{\mytyc{D}.\myfun{f}}{\mytmt}}{TODO}$}
+ \DisplayProof
+}
+
+\subsubsection{Data types}
+
+\begin{figure}[t]
+ \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \mytmsyn ::= \cdots}{
+ $
+ \begin{array}{r@{\ }l}
+ & \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}}{
+ \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:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
+ \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{A}}); \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}}{
+ $
+ \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}}{
+ \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:}{\mydeclsyn \myelabf \myctx \vdash \mytmsyn \myred \mytmsyn}{
+ \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{Observational equality, \mykant\ style}
+
+\mydesc{syntax}{ }{
+ $
+ \begin{array}{r@{\ }c@{\ }l}
+ \mytmsyn & ::= & \mytmsyn \myeq \mytmsyn \mysynsep \myjm{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \\
+ & | & \mycoee{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn} \mysynsep
+ \mycohh{\mytmsyn}{\mytmsyn}{\mytmsyn}{\mytmsyn}
+ \end{array}
+ $
+}
+
+\section{\mykant : The practice}
+\label{sec:kant-practice}
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
+ \url{http://sneezy.cs.nott.ac.uk/darcs/Pig09}.}. In many ways \mykant\ is
something in between the first and second version of Epigram.
The interaction happens in a read-eval-print loop (REPL). The repl is a
\centering{
\includegraphics[scale=1.0]{kant-web.png}
}
- \caption{The \mykant web prompt.}
+ \caption{The \mykant\ web prompt.}
\label{fig:kant-web}
\end{figure}
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,
-which then goes through various stages that can end up in a context update, or
-in failures of various kind. The process is described in figure
-\ref{fig:kant-process}. The workings of each phase will be illustrated in the
-next sections.
+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}:
+
+\begin{description}
+\item[Parse] In this phase the text input gets converted to a sugared
+ version of the core language.
+
+\item[Desugar] The sugared declaration is converted to a core term.
+
+\item[Reference] Occurrences of $\mytyp$ get decorated by a unique reference,
+ which is necessary to implement the type hierarchy check.
+
+\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.
+
+\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.
+
+\item[Pretty print] Format the terms in a nice way, and display the result to
+ the user.
+
+\end{description}
+The details of each phase will be described in section % TODO insert section
+
\begin{figure}
- {\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, below=of elaborate] (tycheck) {Typecheck};
- \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);
-
-
- \end{tikzpicture}
+ \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.}
+ \caption{High level overview of the life of a \mykant\ prompt cycle.}
\label{fig:kant-process}
\end{figure}
-\subsection{Bidirectional type checking}
+\subsection{Term representation}
+\label{sec:term-repr}
-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 recursors) \emph{infer} types,
-while data constructors (abstractions, record/data types data constructors)
-need to be checked.
+\subsection{Type hierarchy}
-To introduce the concept and notation, we will revisit the STLC in a
-bidirectional style.
+\subsection{Elaboration}
+
+\section{Evaluation}
+
+\section{Future work}
\appendix
for example
\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
- \centering{Typing derivations here.}
+ Typing derivations here.
}
In the languages presented and Agda code samples I also highlight the syntax,
\UnaryInfC{$\myjud{\myapp{\mysnd}{\mytmt}}{\mytyb}$}
\end{prooftree}
-\section{Agda rendition of core ITT}
-\label{app:agda-code}
+\section{Agda rendition of ITT}
+\label{app:agda-itt}
+
+Note that in what follows rules for `base' types are
+universe-polymorphic, to reflect the exposition. Derived definitions,
+on the other hand, mostly work with \mytyc{Set}, reflecting the fact
+that in the theory presented we don't have universe polymorphism.
\begin{code}
module ITT where
open import Level
- data ⊥ : Set where
+ data Empty : Set where
- absurd : ∀ {a} {A : Set a} → ⊥ → A
+ absurd : ∀ {a} {A : Set a} → Empty → A
absurd ()
- record ⊤ : Set where
+ ¬_ : ∀ {a} → (A : Set a) → Set a
+ ¬ A = A → Empty
+
+ record Unit : Set where
constructor tt
record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
C x -- ...C always holds.
rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
+module Examples-→ where
+ open ITT
+
+ data ℕ : Set where
+ zero : ℕ
+ suc : ℕ → ℕ
+
+ -- These pragmas are needed so we can use number literals.
+ {-# BUILTIN NATURAL ℕ #-}
+ {-# BUILTIN ZERO zero #-}
+ {-# BUILTIN SUC suc #-}
+
+ data List (A : Set) : Set where
+ [] : List A
+ _∷_ : A → List A → List A
+
+ length : ∀ {A} → List A → ℕ
+ length [] = zero
+ length (_ ∷ l) = suc (length l)
+
+ _>_ : ℕ → ℕ → Set
+ zero > _ = Empty
+ suc _ > zero = Unit
+ suc x > suc y = x > y
+
+ head : ∀ {A} → (l : List A) → length l > 0 → A
+ head [] p = absurd p
+ head (x ∷ _) _ = x
+
+module Examples-× where
+ open ITT
+ open Examples-→
+
+ even : ℕ → Set
+ even zero = Unit
+ even (suc zero) = Empty
+ even (suc (suc n)) = even n
+
+ 6-is-even : even 6
+ 6-is-even = tt
+
+ 5-is-not-even : ¬ (even 5)
+ 5-is-not-even = absurd
+
+ there-is-an-even-number : ℕ × even
+ there-is-an-even-number = 6 , 6-is-even
+
+module Equality where
+ open ITT
+
data _≡_ {a} {A : Set a} : A → A → Set a where
refl : ∀ x → x ≡ x
- J : ∀ {a b} {A : Set a}
+ ≡-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
- J P p (refl x) = p
+ ≡-elim P p (refl x) = p
+
+ subst : ∀ {A : Set} (P : A → Set) → ∀ {x y} → (x≡y : x ≡ y) → P x → P y
+ subst P x≡y p = ≡-elim (λ _ y _ → P y) p x≡y
+
+ sym : ∀ {A : Set} (x y : A) → x ≡ y → y ≡ x
+ sym x y p = subst (λ y′ → y′ ≡ x) p (refl x)
+
+ trans : ∀ {A : Set} (x y z : A) → x ≡ y → y ≡ z → x ≡ z
+ trans x y z p q = subst (λ z′ → x ≡ z′) q p
- subst : ∀ {a b} {A : Set a}
- (P : A → Set b) →
- ∀ {x y} → (x≡y : x ≡ y) → P x → P y
- subst P q p = J (λ _ y _ → P y) p q
+ cong : ∀ {A B : Set} (x y : A) → x ≡ y → (f : A → B) → f x ≡ f y
+ cong x y p f = subst (λ y′ → f x ≡ f y′) p (refl (f x))
\end{code}
\nocite{*}
projects / bitonic-mengthesis.git / blobdiff