\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{\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 \}}
+\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{\mytesctx}{\
\newcommand{\mytelesyn}{\myse{telescope}}
\newcommand{\myrecs}{\mymeta{recs}}
+\newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
%% -----------------------------------------------------------------------------
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.}
\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{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{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}{ }{
}
\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
\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}
\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}
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 & ::= & \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}
+ \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
% \mysynsep \mytyc{D}.\myfun{f} \mysynsep
\mydesc{context validity:}{\myvalid{\myctx}}{
- \centering{
\begin{tabular}{ccc}
\AxiomC{\phantom{$\myjud{\mytya}{\mytyp_l}$}}
\UnaryInfC{$\myvalid{\myemptyctx}$}
\BinaryInfC{$\myvalid{\myctx ; \myfun{f} \mapsto \mytmt : \mytya}$}
\DisplayProof
\end{tabular}
- }
}
Now we can present the reduction rules, which are unsurprising. We have the
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}
\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
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{
+\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}$}
\AxiomC{$\mychkk{\myctx; \myb{x}: \mytyb}{\mytmt}{\myse{C}}$}
\BinaryInfC{$\mychk{\myabs{\myb{x}}{\mytmt}}{\mytya}$}
\DisplayProof
- }
}
\subsection{Elaboration}
$
}
+\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}}{
- \centering{
\begin{tabular}{cc}
\AxiomC{$\myjud{\mytmt}{\mytya}$}
\AxiomC{$\myfun{f} \not\in \myctx$}
\DisplayProof
\end{tabular}
}
-}
\subsubsection{User defined types}
$
}
+\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:}{\myelab{\mydeclsyn}{\mytmsyn ::= \cdots}}{
- \centering{
+ \mydesc{syntax elaboration:}{\mydeclsyn \myelabf \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@{\ }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
\end{array}
\end{array}
$
- }
}
\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
- \centering{
\AxiomC{$\myinf{\mytele \myarr \mytyp}{\mytyp}$}
\AxiomC{$\mytyc{D} \not\in \myctx$}
\noLine
\end{array}
$}
\DisplayProof
- }
}
- \mydesc{reduction elaboration:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
- \centering{
+ \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{$
\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{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.}
\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 } \\
\end{array}
\end{array}
$
- }
}
\mydesc{context elaboration:}{\myelab{\mydeclsyn}{\myctx}}{
- \centering{
\AxiomC{$\myinf{\mytele \myarr \mytyp}{\mytyp}$}
\AxiomC{$\mytyc{D} \not\in \myctx$}
\noLine
\end{array}
$}
\DisplayProof
- }
}
- \mydesc{reduction elaboration:}{\myctx \vdash \mytmsyn \myred \mytmsyn}{
- \centering{
+ \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.}
\subsection{Type hierarchy}
\label{sec:term-hierarchy}
-\subsection{Defined and postulated variables}
+\subsection{Observational equality, \mykant\ style}
-As mentioned, in \mykant\ we can defined top level variables, with or without
-a body. We call the variables
-
-\subsection{Observational equality}
+\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}
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
∀ {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 : ∀ {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
+
+ 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 / commitdiff