From 798a3023430d620ec17004b4d9d68235bed97e28 Mon Sep 17 00:00:00 2001
From: Francesco Mazzoli <f@mazzo.li>
Date: Mon, 10 Jun 2013 19:47:42 +0100
Subject: [PATCH] ...

---
 thesis.bib   | 44 ++++++++++++++++++++++++++++++++++++++++++++
 thesis.lagda | 25 +++++++++++++++----------
 2 files changed, 59 insertions(+), 10 deletions(-)

diff --git a/thesis.bib b/thesis.bib
index 74ff54f..f46fb3d 100644
--- 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 51c7e6b..d7a4864 100644
--- 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 :
-- 
2.30.2