\usepackage{turnstile}
\usepackage{centernot}
\usepackage{stmaryrd}
+\usepackage{bm}
%% -----------------------------------------------------------------------------
%% Utils
Moreover, I will from time to time give examples in the Haskell programming
language as defined in \citep{Haskell2010}, which I will typeset in
-\texttt{typewriter} font. I assume that the reader is already familiar with
+\texttt{teletype} font. I assume that the reader is already familiar with
Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
\subsection{Untyped $\lambda$-calculus}
\app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \dotsb
\]
Terms that can be reduced only a finite number of times (the non-looping ones)
-are said to be \emph{normalising}, and the `final' term (where no reductions are
-possible on the term or on its subterms) is called \emph{normal form}.
+are said to be \emph{strongly normalising}, and the `final' term (where no
+reductions are possible on the term or on its subterms) is called \emph{normal
+ form}.
+
+From now on I will omit the `strongly' in `strongly normalising', however weaker
+notions of normalisation have been described. More generally, it is often
+convenient not to reduce subterms indiscriminately, and have a more principled
+approach to evaluation, or `evaluation strategy'. Common evaluation strategies
+include `call by value' (or `strict'), where arguments of abstractions are
+reduced before being applied to the abstraction; and conversely `call by name'
+(or `lazy'), where we reduce only when we need to do so to proceed - in other
+words when we have an application where the function is still not a $\lambda$.
+In both these reduction strategies we never reduce under an abstraction, and a
+different notion of normalisation (`weak head normal form') if often used, where
+every abstraction is a weak head normal form.
\subsection{The simply typed $\lambda$-calculus}
\label{sec:stlc}
\begin{center}
\axname{syntax}
- $$\tysyn ::= x \separ \tysyn \tyarr \tysyn$$
+$$
+\begin{array}{rcl}
+ \tysyn & ::= & \alpha \separ \tysyn \tyarr \tysyn \\
+ \alpha & \in & \text{A set of base types provided by the language}
+\end{array}
+$$
\end{center}
-I will use $\tya,\tyb,\dots$ to indicate a generic type.
+I will use $\tya,\tyb,\dots$ to indicate a generic type, carrying the convention
+from set theory of denoting member of sets with lowercase letters and sets
+themselves with capitals.
A context $\Gamma$ is a map from variables to types. I will use the notation
$\Gamma; x : \tya$ to augment it and to `extract' pairs from it.
Predictably, $\tya \tyarr \tyb$ is the type of a function from $\tya$ to
-$\tyb$. We need to be able to decorate our abstractions with
-types\footnote{Actually, we don't need to: computers can infer the right type
- easily, but that is another story.}:
+$\tyb$. We extend the syntax and allow to decorate our abstractions with
+types:
\begin{center}
\axname{syntax}
- $$\termsyn ::= x \separ (\abs{x : \tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$
+ $$\termsyn ::= x \separ (\abs{x{:}\tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$
\end{center}
Now we are ready to give the typing judgements:
\DisplayProof
&
\AxiomC{$\Gamma; x : \tya \vdash \termt : \tyb$}
- \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \tya \tyarr \tyb$}
+ \UnaryInfC{$\Gamma \vdash \abs{x{:}\tya}{\termt} : \tya \tyarr \tyb$}
\DisplayProof
\end{tabular}
with a couple of terms former to make our natural deduction more pleasant to
use. For example, tagged unions (\texttt{Either} in Haskell) are disjunctions,
and tuples (or products) are conjunctions. We also want to be able to express
-falsity ($\bot$): that can done 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. Conversely, truth ($\top$) is the type with just one
-trivial element ($\lcunit$).
+falsity ($\bot$): that can done by introducing a type inhabited by no closed
+terms. If evidence of such a type is presented (necessarily under an
+abstraction), then we can derive any type, which expresses absurdity.
+Conversely, truth ($\top$) is the type with just one trivial element
+($\lcunit$).
\newcommand{\lcinl}{\lccon{inl}\appsp}
\newcommand{\lcinr}{\lccon{inr}\appsp}
\newcommand{\lcabsurd}{\lcfun{absurd}\appsp}
\newcommand{\lcabsurdd}[1]{\lcfun{absurd}_{#1}\appsp}
-
+% TODO make parens bold with \bm
\begin{center}
\axname{syntax}
$$
Logic frameworks and programming languages based on type theory have a long
history. Per Martin-L\"{o}f described the first version of his theory in 1971,
-but then revised it since the original version was too impredicative and thus
-inconsistent\footnote{In the early version $\lcsetz : \lcsetz$, see section
- \ref{sec:core-tt} for an explanation on why this causes problems.}. For this
-reason he gave a revised and consistent definition later \citep{Martin-Lof1984}.
+but then revised it since the original version was inconsistent due to its
+impredicativity\footnote{In the early version there was only one universe
+ $\lcsetz$ and $\lcsetz : \lcsetz$, see section \ref{sec:core-tt} for an
+ explanation on why this causes problems.}. For this reason he gave a revised
+and consistent definition later \citep{Martin-Lof1984}.
A related development is the polymorphic $\lambda$-calculus, and specifically
the previously mentioned System F, which was developed independently by Girard
\begin{description}
\item[`forall' ($\tyarr$)] is a generalisation of $\tyarr$ in the STLC and
- expresses universal quantification in our logic. It is often written with a
- syntax closer to logic, e.g. $\forall x : \tya. \tyb$. In the
- literature this is also known as `dependent product' and shown as $\Pi$,
- following the interpretation of functions as infinitary products. I will just
- call it `dependent function', reserving `product' for $\exists$.
+ expresses universal quantification in our logic, where $A \tyarr B$ can be
+ expressed as $(- : A) \tyarr B$. It is often written with a syntax closer to
+ logic, e.g. $\forall x : \tya. \tyb$. In the literature this is also known as
+ `dependent product' and shown as $\Pi$, following the interpretation of
+ functions as infinitary products. I will just call it `dependent function',
+ reserving `product' for $\exists$.
\item[`exists' ($\times$)] is a generalisation of $\wedge$ in the extended STLC
of section \ref{sec:curry-howard}, and thus I will call it `dependent
logic, it represents existential quantification. Similarly to $\tyarr$, it is
often written as $\exists x : \tya. \tyb$.
- For added confusion, in the literature that calls $\tyarr$ $\Pi$, $\times$ is
- often named `dependent sum' and shown as $\Sigma$. This is following the
+ For added confusion, in the literature that uses $\Pi$ for $\tyarr$, $\times$
+ is often named `dependent sum' and shown as $\Sigma$. This is following the
interpretation of $\exists$ as a generalised, infinitary $\vee$, where the
first element of the pair is the `tag' that determines which type the second
element will have.
$\defeq$ as the smallest equivalence relation extending $\bredc$, where $\bredc$
is the reflexive transitive closure of $\bred$; and we treat types that are
related according to $\defeq$ as the same. Another way of seeing $\defeq$ is
-this: when we want to compare two types for equality, we reduce them as far as
+this: when we want to compare two terms for equality, we reduce them as far as
possible and then check if they are equal\footnote{Note that when comparing
- terms we do it up to $\alpha$-renaming. That is, we do not consider
- relabelling of variables as a difference - for example $\abs{x : A}{x} \defeq
- \abs{y : A}{y}$.}. This works since not only each term has a normal form (ITT
-is strongly normalising), but the normal form is also unique; or in other words
+ terms we do it up to $\alpha$-renaming. That is, we do not consider renaming
+ of bound variables as a difference - for example $\abs{x : A}{x} \defeq \abs{y
+ : A}{y}$.}. This works since not only each term has a normal form (ITT is
+strongly normalising), but the normal form is also unique; or in other words
$\bred$ is confluent (if $\termt \bredc \termm$ and $\termt \bredc \termn$, then
there is a $p$ such that $\termm \bredc \termp$ and $\termn \bredc \termp$).
This measure makes sure that, for instance, $\app{(\abs{x :
The theory presented is \emph{stratified}. We have a hierarchy of types
$\lcset{0} : \lcset{1} : \lcset{2} : \dots$, so that there is no `type of all
-types', and our theory is predicative. Type-formers like $\tyarr$ and $\times$
+types', and our theory is predicative. Constructors like $\tyarr$ and $\times$
take the least upper bound $\sqcup$ of the contained types. The layers of the
hierarchy are called `universes'. Theories where $\lcsetz : \lcsetz$ are
inconsistent due to Girard's paradox \citep{Hurkens1995}, and thus lose their
-well-behavedness. Some impredicativity sometimes has its place, either because
-the theory retain good properties (normalization, consistency, etc.) anyway,
-like in System F and CoC; or because we are at a stage at which we do not care.
+well-behavedness. Impredicativity sometimes has its place, either because the
+theory retain good properties (normalization, consistency, etc.) anyway, like in
+System F and CoC; or because we are at a stage at which we do not care.
\subsection{Base Types}
\label{sec:base-types}
projects / bitonic-mengthesis.git / blobdiff