diff options
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/background.tex | 38 |
1 files 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} |