From d37afb396d71260f1cd1490f0031ea0fd49422c8 Mon Sep 17 00:00:00 2001
From: Francesco Mazzoli <f@mazzo.li>
Date: Mon, 17 Dec 2012 18:49:37 +0000
Subject: [PATCH] more background

---
 docs/background.tex | 38 ++++++++++++++++++++++++++++++++++----
 1 file changed, 34 insertions(+), 4 deletions(-)

diff --git a/docs/background.tex b/docs/background.tex
index 6e40d44..507dbf8 100644
--- a/docs/background.tex
+++ b/docs/background.tex
@@ -193,7 +193,6 @@ types\footnote{Actually, we don't need to: computers can infer the right type
 \begin{equation*}
   \termt ::= \dots \separ (\abs{x : \tya}{\termt})
 \end{equation*}
-
 Now we are ready to give the typing judgements:
 
 \begin{center}
@@ -216,6 +215,7 @@ This typing system takes the name of ``simply typed lambda calculus'' (STLC),
 and enjoys a number of properties.  Two of them are expected in most type
 systems: %TODO add credit to pierce
 \begin{description}
+  % TODO the definition of "stuck" thing is wrong
 \item[Progress] A well-typed term is not stuck.  With stuck, we mean a compound
   term (not a variable or a value) that cannot be reduced further.  In the raw
   $\lambda$-calculus all we have is functions, but if we add other primitive
@@ -269,7 +269,7 @@ That is, function composition.  We might want extend our bare lambda calculus
 with a couple of terms to make our natural deduction more pleasant to use.  For
 example, tagged unions (\texttt{Either} in Haskell) are disjunctions, and tuples
 are conjunctions.  We also want to be able to express falsity, and that is done
-by introduced a type ``inhabited'' by no terms.  If evidence of such a type is
+by introducing a type inhabited by no terms.  If evidence of such a type is
 presented, then we can derive any type, which expresses absurdity.
 
 \newcommand{\lcinl}{\mathsf{inl}\appspace}
@@ -349,10 +349,14 @@ the foundation of the STLC.
 
 \subsection{Extending the STLC}
 
+\newcommand{\lctype}{\mathsf{Type}}
+\newcommand{\lcite}[3]{\mathsf{if}\appspace#1\appspace\mathsf{then}\appspace#2\appspace\mathsf{else}\appspace#3}
+\newcommand{\lcbool}{\mathsf{Bool}}
+
 The STLC can be made more expressive in various ways.  Henk Barendregt
-succinctly expressed geometrically in what ``direction'' we can expand our type
-system:
+succinctly expressed geometrically how we can expand our type system:
 
+\begin{equation*}
 \xymatrix@!0@=1.5cm{
   & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
   & & \lambda C \ar@{-}[dd]
@@ -366,5 +370,31 @@ system:
   \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
   & & \lambda P \ar@{-}[ur]
 }
+\end{equation*}
+Here $\lambda{\to}$, in the bottom left, is the STLC.  From there can move along
+3 dimensions:
+\begin{description}
+\item[Terms depending on types (towards $\lambda{2}$)] In other words, we can
+  quantify over types in our type signatures: $(\lambda A : \lctype. \lambda x :
+  A. x) : \forall A. A \to A$.  The first and most famous instance of this idea
+  has been System F.  This gives us a form of polymorphism and has been wildly
+  successful, also thanks to a well known inference algorithm for a restricted
+  version of System F known as Hindley-Milner.  Languages like Haskell and SML
+  are based on this discipline.
+\item[Types depending on types (towards $\lambda{\underline{\omega}}$)] In other
+  words, we have type operators: $(\lambda A : \lctype. \lambda R : \lctype. (A \to R) \to R) : \lctype \to \lctype \to \lctype$.
+\item[Types depending on terms (towards $\lambda{P}$)] Also known as ``dependent
+  types'', give great expressive power: $(\lambda x :
+  \lcbool. \lcite{x}{\mathbb{N}}{\mathbb{Q}}) : \lcbool \to \lctype$.
+\end{description}
+
+All the systems preserve the properties that make the STLC well behaved (some of
+which I haven't mentioned yet).  The system we are going to focus on,
+Intuitionistic Type Theory, has all of the above additions, and thus would sit
+where $\lambda{C}$ sits in the ``$\lambda$-cube'' above.
+
+\section{Intuitionistic Type Theory}
+
+In this section I will describe 
 
 \end{document}
-- 
2.30.2