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}
+}
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
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}}$}
\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}
\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
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
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 :