...

diff --git a/thesis.bib b/thesis.bib
index 74ff54f218395c2ac4a83605f8a91ea9a952247a..f46fb3dc2c1dbdde13aec10ccd5cbbe963fe0786 100644 (file)
--- a/thesis.bib
+++ b/thesis.bib
@@ -342,3 +342,47 @@ year = {2012}
   file = {:home/bitonic/docs/papers/simply-easy.pdf:pdf},
   owner = {bitonic}
 }
+
+@ARTICLE{Bruijn91,
+  author = {de Bruijn, Nicolaas Govert},
+  title = {Telescopic mappings in typed lambda calculus},
+  journal = {Information and Computation},
+  year = {1991},
+  volume = {91},
+  pages = {189--204},
+  number = {2},
+  file = {:/home/bitonic/docs/papers/telescopes.pdf:PDF},
+  publisher = {Elsevier}
+}
+
+@UNPUBLISHED{Huet1988,
+  author = {Huet, Gerard},
+  title = {Extending The Calculus of Constructions with Type:Type},
+  note = {Unpublished draft},
+  year = {1988},
+  file = {:home/bitonic/docs/papers/huet-typtyp.pdf:pdf},
+  owner = {bitonic},
+  timestamp = {2013.06.10}
+}
+
+@ARTICLE{Harper1991,
+  author = {Harper, Robert and Pollack, Robert},
+  title = {Type checking with universes},
+  journal = {Theoretical computer science},
+  year = {1991},
+  volume = {89},
+  pages = {107--136},
+  number = {1},
+  file = {:/home/bitonic/docs/papers/type-checking-universes.ps.gz:PostScript},
+  publisher = {Elsevier}
+}
+
+@ARTICLE{Jacobs1994,
+  author = {Jacobs, Bart},
+  title = {Quotients in simple type theory},
+  journal = {available from the Hypatia Electronic Library: http://hypatia. dcs.
+       qmw. ac. uk},
+  year = {1994},
+  file = {:/home/bitonic/docs/papers/jacobs-quotients.pdf:PDF},
+  publisher = {Citeseer}
+}

diff --git a/thesis.lagda b/thesis.lagda
index 51c7e6be9c2c964eb4ed49fce8d2657b4af331a4..d7a4864e0c926b3b091b24b9379c9cb553ebb7a0 100644 (file)
--- a/thesis.lagda
+++ b/thesis.lagda
@@ -993,9 +993,7 @@ be of the same type, to preserve subject reduction, since execution
 could take both paths.  This is a pity, since the type system does not
 reflect the fact that in each branch we gain knowledge on the term we
 are branching on.  Which means that programs along the lines of
-{\small
-\begin{verbatim}if null xs then head xs else 0
-\end{verbatim}}
+{\small\[\text{\texttt{if null xs then head xs else 0}}\]}
 are a necessary, well typed, danger.
 
 However, in a more expressive system, we can do better: the branches' type can
@@ -1064,7 +1062,7 @@ levels of argument and return type.  This trend will continue with the other
 type-level binders, $\myprod$ and $\mytyc{W}$.
 
 \subsubsection{$\myprod$, or dependent product}
-\ref{sec:disju}
+\label{sec:disju}
 
 \mydesc{typing:}{\myjud{\mytmsyn}{\mytmsyn}}{
      \AxiomC{$\myjud{\mytya}{\mytyp_{l_1}}$}
@@ -2264,9 +2262,7 @@ what we can defined, with some examples.
   \end{array}
   \]}
   This is very similar to what we would write in Haskell:
-  {\small
-  \begin{verbatim}data Nat = Zero | Suc Nat
-  \end{verbatim}}
+  {\small\[\text{\texttt{data Nat = Zero | Suc Nat}}\]}
   Once the data type is defined, $\mykant$\ will generate syntactic
   constructs for the type and data constructors, so that we will have
   \begin{center}
@@ -2334,6 +2330,15 @@ what we can defined, with some examples.
     \mytyc{\mynat}.\myfun{elim} \myappsp (\mydc{suc} \myappsp \mytmt) & \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps} \myred \myse{ps} \myappsp \mytmt \myappsp (\mynat.\myfun{elim} \myappsp \mytmt \myappsp \myse{P} \myappsp \myse{pz} \myappsp \myse{ps})
   \end{array}
   \]}
+  The Haskell equivalent would be
+  {\small\[
+    \begin{array}{@{}l}
+      \text{\texttt{elim :: Nat -> a -> (Nat -> a -> a) -> a}}\\
+      \text{\texttt{elim Zero    pz ps = pz}}\\
+      \text{\texttt{elim (Suc n) pz ps = ps n (elim n pz ps)}}
+    \end{array}
+    \]}
+  Which buys us the computational behaviour, but not the reasoning power.
   % TODO maybe more examples, e.g. Haskell eliminator and fibonacci
 
 \item[Binary trees] Now for a polymorphic data type: binary trees, since
@@ -2469,8 +2474,8 @@ Following the intuition given by the examples, the mechanised
 elaboration is presented in figure \ref{fig:elab}, which is essentially
 a modification of figure 9 of \citep{McBride2004}\footnote{However, our
   datatypes do not have indices, we do bidirectional typechecking by
-  treating constructors/destructors are syntactic constructors, and we
-  have records.}.
+  treating constructors/destructors as syntactic constructs, and we have
+  records.}.
 
 In data types declarations we allow recursive occurrences as long as
 they are \emph{strictly positive}, employing a syntactic check to make
@@ -2525,7 +2530,7 @@ foobar
 
 A type hierarchy as presented in section \label{sec:itt} is a
 considerable burden on the user, on various levels.  Consider for
-example how we recovered disjunctions in section \label{sec:disju}: we
+example how we recovered disjunctions in section \ref{sec:disju}: we
 have a function that takes two $\mytyp_0$ and forms a new $\mytyp_0$.
 What if we wanted to form a disjunction containing two $\mytyp_0$, or
 $\mytyp_{42}$?  Our definition would fail us, since $\mytyp_0 :