\documentclass[report]{article}

%% Narrow margins
% \usepackage{fullpage}

%% Bibtex
\usepackage{natbib}

%% Links
\usepackage{hyperref}

%% Frames
\usepackage{framed}

%% Symbols
\usepackage[fleqn]{amsmath}

%% Proof trees
\usepackage{bussproofs}

%% -----------------------------------------------------------------------------
%% Commands for Agda
\usepackage[english]{babel}
\usepackage[conor]{agda}
\renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
\renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
\renewcommand{\AgdaField}{\AgdaFunction}
\definecolor{AgdaBound} {HTML}{000000}

\DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}

%% -----------------------------------------------------------------------------
%% Commands

\newcommand{\mysyn}{\AgdaKeyword}
\newcommand{\mytyc}{\AgdaDatatype}
\newcommand{\mydc}{\AgdaInductiveConstructor}
\newcommand{\myfld}{\AgdaField}
\newcommand{\myfun}{\AgdaFunction}
% TODO make this use AgdaBount
\newcommand{\myb}[1]{\ensuremath{#1}}
\newcommand{\myfield}{\AgdaField}
\newcommand{\myind}{\AgdaIndent}
\newcommand{\mykant}{\textsc{Kant}}
\newcommand{\mysynel}[1]{\langle #1 \rangle}
\newcommand{\mytmsyn}{\mysynel{term}}
\newcommand{\mysp}{\ }
\newcommand{\myabs}[2]{\lambda #1 \mapsto #2}
\newcommand{\myappsp}{\hspace{0.07cm}}
\newcommand{\myapp}[2]{#1 \myappsp #2}
\newcommand{\mysynsep}{\ \ |\ \ }

\FrameSep0.3cm
\newcommand{\mydesc}[3]{
  \hfill \textbf{#1} $#2$
  \vspace{-0.2cm}
  \begin{framed}
    #3
  \end{framed}
}

% TODO is \mathbin the correct thing for arrow and times?

\newcommand{\mytmt}{\myb{T}}
\newcommand{\mytmm}{\myb{M}}
\newcommand{\mytmn}{\myb{N}}
\newcommand{\myred}{\leadsto}
\newcommand{\mysub}[3]{#1[#2 \mapsto #3]}
\newcommand{\mytysyn}{\mysynel{type}}
\newcommand{\mybasetys}{K}
% TODO change this name
\newcommand{\mybasety}[1]{B_{#1}}
\newcommand{\mytya}{\myb{A}}
\newcommand{\mytyb}{\myb{B}}
\newcommand{\myarr}{\mathbin{\textcolor{AgdaDatatype}{\to}}}
\newcommand{\myprod}{\mathbin{\textcolor{AgdaDatatype}{\times}}}
\newcommand{\myctx}{\Gamma}
\newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
\newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
\newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
\newcommand{\myabss}[3]{\lambda #1 {:} #2 \mapsto #3}
\newcommand{\mytt}{\mydc{tt}}
\newcommand{\myunit}{\mytyc{$\top$}}
\newcommand{\mypair}[2]{(#1\mathpunct{\textcolor{AgdaInductiveConstructor}{,}} #2)}
\newcommand{\myfst}[1]{\myapp{\myfld{fst}}{#1}}
\newcommand{\mysnd}[1]{\myapp{\myfld{snd}}{#1}}
\newcommand{\myconst}{\myb{c}}
\newcommand{\myemptyctx}{\cdot}
\newcommand{\myhole}{\AgdaUnsolvedMeta}
\newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}

%% -----------------------------------------------------------------------------

\title{\mykant: Implementing Observational Equality}
\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
\date{June 2013}

\begin{document}

\iffalse
\begin{code}
module thesis where
open import Level
\end{code}
\fi

\maketitle

\begin{abstract}
  The marriage between programming and logic has been a very fertile one.  In
  particular, since the simply typed lambda calculus (STLC), a number of type
  systems have been devised with increasing expressive power.

  Section \ref{sec:types} will give a very brief overview of STLC, and then
  illustrate how it can be interpreted as a natural deduction system.  Section
  \ref{sec:itt} will introduce Inutitionistic Type Theory (ITT), which expands
  on this concept, employing a more expressive logic.  The exposition is quite
  dense since there is a lot of material to cover; for a more complete treatment
  of the material the reader can refer to \citep{Thompson1991, Pierce2002}.
  Section \ref{sec:equality} will explain why equality has always been a tricky
  business in these theories, and talk about the various attempts that have been
  made to make the situation better.  One interesting development has recently
  emerged: Observational Type theory.

  Section \ref{sec:practical} will describe common extensions found in the
  systems currently in use.  Finally, section \ref{sec:kant} will describe a
  system developed by the author that implements a core calculus based on the
  principles described.
\end{abstract}

\tableofcontents

\section{Simple and not-so-simple types}
\label{sec:types}

\subsection{The untyped $\lambda$-calculus}

Along with Turing's machines, the earliest attempts to formalise computation
lead to the $\lambda$-calculus \citep{Church1936}.  This early programming
language encodes computation with a minimal syntax and no `data' in the
traditional sense, but just functions.  Here we give a brief overview of the
language, which will give the chance to introduce concepts central to the
analysis of all the following calculi.  The exposition follows the one found in
chapter 5 of \cite{Queinnec2003}.

The syntax of $\lambda$-terms consists of three things: variables, abstractions,
and applications:

\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
    x          & \in & \text{Some enumerable set of symbols}
  \end{array}
  $
}

Through this text, I will use $\mytmt$, $\mytmm$, $\mytmn$ to indicate a generic
term, and $x$, $y$ to refer to variables.  Parenthesis will be omitted in the
usual way: $\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} =
\myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$.

Abstractions roughly corresponds to functions, and their semantics is more
formally explained by the $\beta$-reduction rule:

\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
  $
  \begin{array}{l}
    \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{x}{\mytmn}\text{, where} \\
    \myind{1}
    \begin{array}{l@{\ }c@{\ }l}
      \mysub{x}{x}{\mytmn} & = & \mytmn \\
      \mysub{y}{x}{\mytmn} & = & y\text{, with } x \neq y \\
      \mysub{\myapp{\mytmt}{\mytmm}}{x}{\mytmn} & = & (\myapp{\mysub{\mytmt}{x}{\mytmn}}{\mysub{\mytmm}{x}{\mytmn}}) \\
      \mysub{(\myabs{x}{\mytmm})}{x}{\mytmn} & = & \myabs{x}{\mytmm} \\
      \mysub{(\myabs{y}{\mytmm})}{x}{\mytmn} & = & \myabs{z}{\mysub{\mysub{\mytmm}{y}{z}}{x}{\mytmn}}, \\
      \multicolumn{3}{l}{\myind{1} \text{with $x \neq y$ and $z$ not free in $\myapp{\mytmm}{\mytmn}$}}
    \end{array}
  \end{array}
  $
}

The care required during substituting variables for terms is required to avoid
name capturing.

These few elements are of remarkable expressiveness, and in fact Turing
complete.  As a corollary, we must be able to devise a term that reduces forever
(`loops' in imperative terms):
\[
  (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \dots\text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
\]

A \emph{redex} is a term that can be reduced.  In the untyped $\lambda$-calculus
this will be the case for an application in which the first term is an
abstraction, but in general a term is reducible if it appears to the left of a
reduction rule.  When a term contains no redex it's said to be in \emph{normal
  form}.  Given the observation above, not all terms reduce to a normal forms:
we call the ones that do \emph{normalising}, and the ones that don't
\emph{non-normalising}.

The reduction rule presented is not syntax directed, but \emph{evaluation
  strategies} can be employed to reduce term systematically. Common evaluation
strategies include \emph{call by value} (or \emph{strict}), where arguments of
abstractions are reduced before being applied to the abstraction; and conversely
\emph{call by name} (or \emph{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: for this reason a weaker form of normalisation is used, where
both abstractions and normal forms are said to be in \emph{weak head normal
  form}.

\subsection{The simply typed $\lambda$-calculus}

A convenient way to `discipline' $\lambda$-terms is to assign \emph{types} to
them, and then check that the terms that we are forming make sense given our
typing rules \citep{Curry1934}.  The first most basic instance of this idea
takes the name of \emph{simply typed $\lambda$ calculus}.

Our types contain a set of \emph{type variables} $\Phi$, which might correspond
to some `primitive' types; and $\myarr$, the type former for `arrow' types, the
types of functions.  The language is explicitly typed: when we bring a variable
into scope with an abstraction, we explicitly declare its type. $\mytya$,
$\mytyb$ will be used to refer to a generic type.  Reduction is unchanged from
the untyped $\lambda$-calculus.

\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn   & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
                       (\myapp{\mytmsyn}{\mytmsyn}) \\
    \mytysyn   & ::= & \myb{\phi} \mysynsep \mytysyn \myarr \mytysyn  \mysynsep \\
    \myb{x}    & \in & \text{Some enumerable set of symbols} \\
    \myb{\phi} & \in & \Phi
  \end{array}
  $
}

\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
  \centering{
    \begin{tabular}{ccc}
      \AxiomC{$\myctx(x) = A$}
      \UnaryInfC{$\myjud{\myb{x}}{A}$}
      \DisplayProof
      &
      \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
      \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
      \DisplayProof
      &
      \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
      \AxiomC{$\myjud{\mytmn}{\mytya}$}
      \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
      \DisplayProof
    \end{tabular}
  }
}

In the typing rules, a context $\myctx$ is used to store the types of bound
variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
$\myctx(x)$ returns the type of the rightmost occurrence of $x$.

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
\citep{Pierce2002}:
\begin{description}
\item[Progress] A well-typed term is not stuck---it is either a variable, or its
  constructor does not appear on the left of the $\myred$ relation (currently
  only $\lambda$), or it can take a step according to the evaluation rules.
\item[Preservation] If a well-typed term takes a step of evaluation, then the
  resulting term is also well-typed, and preserves the previous type.
\end{description}

However, STLC buys us much more: every well-typed term is normalising.  It is
easy to see that we can't fill the blanks if we want to give types to the
non-normalising term shown before:
\begin{equation*}
  \myapp{(\myabss{x}{\myhole{?}}{\myapp{x}{x}})}{(\myabss{x}{\myhole{?}}{\myapp{x}{x}})}
\end{equation*}

This makes the STLC Turing incomplete.  We can recover the ability to loop by
adding a combinator that recurses:

% TODO make this more compact

\mydesc{syntax}{ } {
  $ \mytmsyn ::= \dotsb \mysynsep \myfix{x}{\mytysyn}{\mytmsyn} $
}

\mydesc{typing:}{ } {
  \AxiomC{$\myjudd{\myctx; x : \mytya}{\mytmt}{\mytya}$}
  \UnaryInfC{$\myjud{\myfix{x}{\mytya}{\mytmt}}{\mytya}$}
  \DisplayProof
}

\mydesc{reduction:}{ }{
  $ \myfix{x}{\mytya}{\mytmt} \myred \mysub{\mytmt}{x}{(\myfix{x}{\mytya}{\mytmt})}$
}

This will deprive us of normalisation, which is a particularly bad thing if we
want to use the STLC as described in the next section.

\subsection{The Curry-Howard correspondence}

Moreover,
we have a product (or pair, or tuple) type $\mytya \myprod \mytyb$ for each pair
of types $\mytya$ and $\mytyb$, and a function (or arrow) type $\mytya \myarr
\mytyb$ for each pair of types $\mytya$ and $\mytyb$.  $\beta$-reduction is
unchanged, but we have added reduction rules for products.  Products are not
essential, but they serve as a good example of a type former apart from the
arrow type.

\mydesc{syntax}{ }{
  $
  \begin{array}{r@{\ }c@{\ }l}
    \mytmsyn & ::= & \myb{x} \mysynsep \myconst \mysynsep
                     \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
                     (\myapp{\mytmsyn}{\mytmsyn}) \\
             & |   & \mytt \mysynsep \mypair{\mytmsyn}{\mytmsyn} \mysynsep
                     \myfst{\mytmsyn} \mysynsep \mysnd{\mytmsyn} \\
    \mytysyn & ::= & \mytysyn \myprod \mytysyn \mysynsep
                     \mytysyn \myarr \mytysyn  \mysynsep
                     \mybasety{\myconst} \\
    \myb{x}  & \in & \text{Some enumerable set of symbols} \\
    \myconst & \in & \text{Some set $C$ of constants} \\
  \end{array}
  $
}

\mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
  \centering{
    \begin{tabular}{cc}
      $\myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{x}{\mytmn}$ &
      $
      \begin{array}{r@{\ }c@{\ }l}
        \myapp{\myfst}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
        \myapp{\mysnd}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
      \end{array}
      $
    \end{tabular}
  }
}

% TODO write context rules
% \mydesc{validity:}{\myvalid{\myctx}}{
%   \centering{
%     \begin{tabular}{ccc}
%       \AxiomC{}
%       \UnaryInfC{$\myvalid{\myemptyctx}$}
%       \DisplayProof
%       &
%       \AxiomC{$\mytmt : \mytya$}
%       \UnaryInfC{$\myvalid{\myctx; x : \mytya
%       bar &
%       baz
%     \end{tabular}
%   }
% }

\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
  \centering{
    \begin{tabular}{cc}
      \AxiomC{$x : A \in \myctx$}
      \UnaryInfC{$\myjud{x}{A}$}
      \DisplayProof
      &
      foo
    \end{tabular}
  }
}

\section{Intuitionistic Type Theory}
\label{sec:itt}

\section{The struggle for equality}
\label{sec:equality}

\section{Extending ITT}
\label{sec:practical}

\section{\mykant}
\label{sec:kant}

\appendix

\section{Notation and syntax}

Syntax, derivation rules, and reduction rules, are enclosed in frames describing
the type of relation being established and the syntactic elements appearing,
for example

\mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
  Typing derivations here.
}

In the languages presented I will also use different fonts and colors for
different things:

\begin{center}
  \begin{tabular}{c | l}
    $\mytyc{Sans}$  & Type constructors. \\
    $\mydc{sans}$  & Data constructors. \\
    % $\myfld{sans}$  & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
    $\mysyn{roman}$ & Syntax of the language. \\
    $\myfun{roman}$ & Defined values. \\
    $\myb{math}$    & Bound variables.
  \end{tabular}
\end{center}

\section{Agda rendition of a core ITT}
\label{app:agda-code}

\begin{code}
module ITT where
  data Empty : Set where

  absurd : ∀ {a} {A : Set a} → Empty → A
  absurd ()

  record Unit : Set where
    constructor tt

  record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
    constructor _,_
    field
      fst : A
      snd : B fst

  data Bool : Set where
    true false : Bool

  if_/_then_else_ : ∀ {a}
    (x : Bool) → (P : Bool → Set a) → P true → P false → P x
  if true / _ then x else _ = x
  if false / _ then _ else x = x

  data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
    _◁_ : (s : S) → (P s → W S P) → W S P

  rec : ∀ {a b} {S : Set a} {P : S → Set b}
    (C : W S P → Set) →      -- some conclusion we hope holds
    ((s : S) →               -- given a shape...
     (f : P s → W S P) →     -- ...and a bunch of kids...
     ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
     C (s ◁ f)) →            -- ...does C hold for the node?
    (x : W S P) →            -- If so, ...
    C x                      -- ...C always holds.
  rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
\end{code}

\nocite{*}
\bibliographystyle{authordate1}
\bibliography{thesis}

\end{document}