--- /dev/null
+module InterimReport where
+
+import Level
+
+module Core where
+ data Exists (A : Set) (B : A -> Set) : Set where
+ _,_ : (x : A) -> B x -> Exists A B
+
+ fst : forall {A B} -> Exists A B -> A
+ fst (x , _) = x
+
+ snd : forall {A B} -> (s : Exists A B) -> B (fst s)
+ snd (_ , x) = x
+
+ data Bot : Set where
+
+ absurd : {A : Set} -> Bot -> A
+ absurd ()
+
+ data Top : Set where
+ <> : Top
+
+ data Bool : Set where
+ true : Bool
+ false : Bool
+
+ if_/_then_else_ : forall {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
+
+ if_then_else_ : forall {a} {P : Bool -> Set a}
+ (x : Bool) -> P true -> P false -> P x
+ if true then x else _ = x
+ if false then _ else y = y
+
+ data W (A : Set) (B : A -> Set) : Set where
+ _<!_ : (a : A) -> (B a -> W A B) -> W A B
+
+ -- Ugh! Comments and definiton stolen from
+ -- <http://www.e-pig.org/epilogue/?p=324>
+ rec : forall {S P}
+ (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))
+
+ _\/_ : (A B : Set) -> Set
+ A \/ B = Exists Bool (\ b -> if b then A else B)
+
+ inl : forall {A B} -> A -> A \/ B
+ inl x = true , x
+
+ inr : forall {A B} -> B -> A \/ B
+ inr x = false , x
+
+ case : {A B C : Set} -> A \/ B -> (A -> C) -> (B -> C) -> C
+ case {A} {B} {C} x f g =
+ (if (fst x) / (\ b -> (if b then A else B) -> C) then f else g)
+ (snd x)
+
+ Tr : Bool -> Set
+ Tr b = if b then Top else Bot
+
+ Nat : Set
+ Nat = W Bool Tr
+
+ zero : Nat
+ zero = false <! absurd
+
+ suc : Nat -> Nat
+ suc n = true <! \ _ -> n
+
+ plus : Nat -> Nat -> Nat
+ plus x y =
+ rec (\ _ -> Nat)
+ (\ b -> if b / (\ b -> (Tr b -> Nat) -> (Tr b -> Nat) -> Nat)
+ then (\ _ f -> suc (f <>)) else (\ _ _ -> y)) x
+
+ data _==_ {A : Set} : A -> A -> Set where
+ refl : {x : A} -> x == x
+
+ subst : forall {A x y} -> (x == y) -> (T : A -> Set) -> T x -> T y
+ subst refl T t = t
+
+ _/==_ : forall {A} -> A -> A -> Set
+ x /== y = x == y -> Bot
+
+module Ext where
+ data List (A : Set) : Set where
+ nil : List A
+ _::_ : A -> List A -> List A
+
+ data Nat : Set where
+ zero : Nat
+ suc : Nat -> Nat
+
+ data Vec (A : Set) : Nat -> Set where
+ nil : Vec A zero
+ _::_ : forall {n} -> A -> Vec A n -> Vec A (suc n)
+
+ head : forall {A n} -> Vec A (suc n) -> A
+ head (x :: _) = x
+
+ data Fin : Nat -> Set where
+ fzero : forall {n} -> Fin (suc n)
+ fsuc : forall {n} -> Fin n -> Fin (suc n)
+
+ _!!_ : forall {A n} -> Vec A n -> Fin n -> A
+ (x :: _) !! fzero = x
+ (x :: xs) !! fsuc i = xs !! i
+
+ open Core using (_==_; refl; subst)
+
+ id : {A : Set} -> A -> A
+ id x = x
+
+ map : forall {A B} -> (A -> B) -> List A -> List B
+ map _ nil = nil
+ map f (x :: xs) = f x :: map f xs
+
+ cong : forall {A B} {x y : A} (f : A -> B) -> x == y -> f x == f y
+ cong f refl = refl
+
+ map-id==id : {A : Set} (xs : List A) -> map id xs == id xs
+ map-id==id nil = refl
+ map-id==id (x :: xs) = cong (_::_ x) (map-id==id xs)
+
+ _#_ : {A B C : Set} -> (B -> C) -> (A -> B) -> (A -> C)
+ f # g = \ x -> f (g x)
+
+ map-#==#-map : forall {A B C} (f : B -> C) (g : A -> B) (xs : List A) ->
+ map (f # g) xs == (map f # map g) xs
+ map-#==#-map f g nil = refl
+ map-#==#-map f g (x :: xs) = cong (_::_ (f (g x))) (map-#==#-map f g xs)
+
+ -- If we could have this...
+ postulate ext : forall {A B} {f g : A -> B} ->
+ ((x : A) -> f x == g x) -> f == g
+
+ map-id==id' : forall {A} -> map {A} id == id
+ map-id==id' = ext map-id==id
+
+ map-#==#-map' : forall {A B C} (f : B -> C) (g : A -> B) ->
+ map (f # g) == (map f # map g)
+ map-#==#-map' f g = ext (map-#==#-map f g)
\ No newline at end of file
--- /dev/null
+
+@inbook{Thompson1991,
+ author = {Thompson, Simon},
+ title = {Type Theory and Functional Programming},
+ publisher = {Addison-Wesley},
+ year = {1991}
+}
+
+@inbook{Pierce2002,
+ author = {Pierce, Benjamin C.},
+ title = {Types and Programming Languages},
+ publisher = {The MIT Press},
+ year = {2002}
+}
+
+@online{Coq,
+ author = {{The Coq Team}},
+ title = {The Coq Proof Assistant},
+ url = {\url{coq.inria.fr}},
+ howpublished = {\url{http://coq.inria.fr}},
+ year = 2013
+}
+
+@online{GHC,
+ author = {{The GHC Team}},
+ title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.1},
+ url = {http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/},
+ howpublished = {\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}},
+ year = 2012
+}
+
+@online{EpigramTut,
+ author = {Conor McBride},
+ title = {Epigram: Practical Programming with Dependent Types},
+ url = {http://strictlypositive.org/epigram-notes.ps.gz},
+ howpublished = {\url{http://strictlypositive.org/epigram-notes.ps.gz}},
+ year = 2004
+}
+
+@online{Haskell2010,
+ author = {Simon Marlow},
+ title = {Haskell 2010, Language Report},
+ url = {http://www.haskell.org/onlinereport/haskell2010/},
+ howpublished = {\url{http://www.haskell.org/onlinereport/haskell2010/}},
+ year = 2010
+}
+
+@online{LYAH,
+ author = {Miran Lipova\v{c}a},
+ title = {Learn You a Haskell for Great Good!},
+ url = {http://learnyouahaskell.com/},
+ howpublished = {\url{http://learnyouahaskell.com/}},
+ year = 2009
+}
+
+@inbook{ProgInHask,
+ author = {Graham Hutton},
+ title = {Programming in Haskell},
+ year = 2007,
+ publisher = {Cambridge University Press}
+}
+
+@inbook{NuPRL,
+ author = {Robert L. Constable and the PRL Group},
+ title = {Implementing Mathematics with The NuPRL Proof Development System},
+ year = 1986,
+ publisher = Prentice-Hall
+}
+
+
+@article{Altenkirch2007,
+address = {New York, New York, USA},
+author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},
+doi = {10.1145/1292597.1292608},
+file = {:home/bitonic/docs/papers/OTT2.pdf:pdf},
+isbn = {9781595936776},
+journal = {Proceedings of the 2007 workshop on Programming languages meets program verification - PLPV '07},
+keywords = {case analysis relies on,datatypes are indexed in,equality,of any language where,ole in the programs,play a crucial internal,rˆ,solving,some way,type theory},
+pages = {57},
+publisher = {ACM Press},
+title = {{Observational equality, now!}},
+url = {http://portal.acm.org/citation.cfm?doid=1292597.1292608},
+year = {2007}
+}
+@article{Bove2009,
+author = {Bove, Ana and Dybjer, Peter and Norell, Ulf},
+file = {:home/bitonic/docs/papers/agda-overview.pdf:pdf},
+journal = {Theorem Proving in Higher Order Logics},
+title = {{A brief overview of Agda - a functional language with dependent types}},
+url = {http://www.springerlink.com/index/h12lq70470983732.pdf},
+year = {2009}
+}
+@article{Pierce2000,
+author = {Pierce, Benjamin C. and Turner, David N.},
+doi = {10.1145/345099.345100},
+file = {:home/bitonic/docs/papers/local-type-inference.pdf:pdf},
+issn = {01640925},
+journal = {ACM Transactions on Programming Languages and Systems},
+month = jan,
+number = {1},
+pages = {1--44},
+title = {{Local type inference}},
+url = {http://portal.acm.org/citation.cfm?doid=345099.345100},
+volume = {22},
+year = {2000}
+}
+@article{Yorgey2012,
+address = {New York, New York, USA},
+author = {Yorgey, Brent a. and Weirich, Stephanie and Cretin, Julien and {Peyton Jones}, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos\'{e} Pedro},
+doi = {10.1145/2103786.2103795},
+file = {:home/bitonic/docs/papers/haskell-promotion.pdf:pdf},
+isbn = {9781450311205},
+journal = {Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation - TLDI '12},
+pages = {53},
+publisher = {ACM Press},
+title = {{Giving Haskell a promotion}},
+url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
+year = {2012}
+}
+@article{Barendregt1991,
+author = {Barendregt, Henk},
+file = {:home/bitonic/docs/papers/lambda-cube.pdf:pdf},
+journal = {Journal of functional programming},
+title = {{Introduction to generalized type systems}},
+url = {http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf},
+year = {1991}
+}
+@article{Hurkens1995,
+author = {Hurkens, Antonius J.C.},
+file = {:home/bitonic/docs/papers/hurkens-paradox.pdf:pdf},
+journal = {Typed Lambda Calculi and Applications},
+title = {{A simplification of Girard's paradox}},
+url = {http://www.springerlink.com/index/W718604JN467672H.pdf},
+year = {1995}
+}
+@book{Martin-Lof1984,
+author = {Martin-L\"{o}f, Per},
+file = {:home/bitonic/docs/papers/martin-lof-tt.pdf:pdf},
+isbn = {8870881059},
+publisher = {Bibliopolis},
+title = {{Intuitionistic type theory}},
+year = {1984}
+}
+@article{Oury2008,
+address = {New York, New York, USA},
+author = {Oury, Nicolas and Swierstra, Wouter},
+doi = {10.1145/1411204.1411213},
+file = {:home/bitonic/docs/papers/powerofpi.pdf:pdf},
+isbn = {9781595939197},
+journal = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08},
+pages = {39},
+publisher = {ACM Press},
+title = {{The power of Pi}},
+url = {http://portal.acm.org/citation.cfm?doid=1411204.1411213},
+year = {2008}
+}
+@article{Chapman2010,
+address = {New York, New York, USA},
+author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
+doi = {10.1145/1863543.1863547},
+file = {:home/bitonic/docs/papers/conor-levitation.pdf:pdf},
+isbn = {9781605587943},
+journal = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming - ICFP '10},
+pages = {3},
+publisher = {ACM Press},
+title = {{The gentle art of levitation}},
+url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547},
+year = {2010}
+}
+@phdthesis{Norell2007,
+author = {Norell, Ulf},
+file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf},
+isbn = {9789172919969},
+school = {Chalmers University of Technology and G\"{o}teborg University},
+title = {{Towards a practical programming language based on dependent type theory}},
+url = {http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
+year = {2007}
+}
+@article{Coquand1986,
+author = {Coquand, Thierry and Huet, Gerard},
+file = {:home/bitonic/docs/papers/coc.pdf:pdf},
+title = {{The calculus of constructions}},
+url = {http://hal.inria.fr/docs/00/07/60/24/PDF/RR-0530.pdf},
+year = {1986}
+}
+@article{Reynolds1994,
+author = {Reynolds, John C.},
+file = {:home/bitonic/docs/papers/reynolds-polymorphic-lc.ps:ps},
+journal = {Logical Foundations of Functional Programming},
+title = {{An introduction to the polymorphic lambda calculus}},
+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.9916\&rep=rep1\&type=pdf},
+year = {1994}
+}
+@article{Brady2012,
+author = {Brady, Edwin},
+file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
+journal = {Unpublished draft},
+number = {November},
+title = {{Implementing General Purpose Dependently Typed Programming Languages}},
+url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf},
+year = {2012}
+}
+@article{Church1936,
+author = {Church, Alonzo},
+file = {:home/bitonic/docs/papers/church-lc.pdf:pdf},
+journal = {American journal of mathematics},
+number = {2},
+pages = {345--363},
+title = {{An unsolvable problem of elementary number theory}},
+url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2371045},
+volume = {58},
+year = {1936}
+}
+@article{Altenkirch2010,
+author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas},
+file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf},
+journal = {Functional and Logic \ldots},
+number = {Sheard 2005},
+title = {{$\Pi$$\Sigma$: dependent types without the sugar}},
+url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
+year = {2010}
+}
+@article{Pollack1990,
+author = {Pollack, Robert},
+file = {:home/bitonic/docs/papers/implicit-syntax.ps:ps},
+journal = {Informal Proceedings of First Workshop on Logical Frameworks},
+title = {{Implicit syntax}},
+url = {http://reference.kfupm.edu.sa/content/i/m/implicit\_syntax\_\_1183660.pdf},
+year = {1992}
+}
+@article{Dybjer1991,
+author = {Dybjer, Peter},
+file = {:home/bitonic/docs/papers/dybjer-inductive.ps:ps},
+journal = {Logical Frameworks},
+title = {{Inductive sets and families in Martin-L\"{o}f's type theory and their set-theoretic semantics}},
+url = {http://books.google.com/books?hl=en\&lr=\&id=X9wfWwslFQIC\&oi=fnd\&pg=PA280\&dq=Inductive+Sets+and+Families+in+Martin-L\%C3\%B6f\%27s+Type+Theory+and+Their+Set-Theoretic+Semantics\&ots=LewzM17GcW\&sig=vF4GgtlEBSf1uwRV1o\_unDtLats},
+year = {1991}
+}
+@article{Sulzmann2007,
+address = {New York, New York, USA},
+author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin},
+doi = {10.1145/1190315.1190324},
+file = {:home/bitonic/docs/papers/systemf-coercions.pdf:pdf},
+isbn = {159593393X},
+journal = {Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation - TLDI '07},
+pages = {53},
+publisher = {ACM Press},
+title = {{System F with type equality coercions}},
+url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
+year = {2007}
+}
+@article{Curry1934,
+author = {Curry, Haskell B.},
+file = {:home/bitonic/docs/papers/curry-stlc.pdf:pdf},
+journal = {Proceedings of the National Academy of Sciences of the United States of America},
+number = {1930},
+pages = {584--590},
+title = {{Functionality in combinatory logic}},
+url = {http://www.ncbi.nlm.nih.gov/pmc/articles/pmc1076489/},
+volume = {511},
+year = {1934}
+}
+@article{Church1940,
+author = {Church, Alonzo},
+file = {:home/bitonic/docs/papers/church-stlc.pdf:pdf},
+journal = {J. Symb. Log.},
+number = {2},
+pages = {56--68},
+title = {{A formulation of the simple theory of types}},
+url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2266170},
+volume = {5},
+year = {1940}
+}
+@article{McBride2004,
+author = {McBride, Conor},
+doi = {10.1017/S0956796803004829},
+file = {:home/bitonic/docs/papers/view-from-the-left.ps.gz:gz},
+journal = {Journal of Functional Programming},
+month = jan,
+number = {1},
+pages = {69--111},
+title = {{The View from The Left}},
+url = {http://strictlypositive.org/view.ps.gz},
+volume = {14},
+year = {2004}
+}
+@article{Vytiniotis2011,
+author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
+file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
+journal = {Journal of Functional Programming},
+number = {4-5},
+pages = {333--412},
+title = {{OutsideIn (X) Modular type inference with local assumptions}},
+url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818},
+volume = {21},
+year = {2011}
+}
+@article{Jacobs1997,
+author = {Jacobs, Bart and Rutten, Jan},
+file = {:home/bitonic/docs/papers/coalgebra-coind.pdf:pdf},
+journal = {EATCS Bulletin},
+number = {1997},
+title = {{A tutorial on (co) algebras and (co) induction}},
+url = {http://synrc.com/publications/cat/Logic/CoinductionCoalgebrasTutorial.pdf},
+volume = {62},
+year = {1997}
+}
--- /dev/null
+\documentclass[article, a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{fixltx2e}
+\usepackage{enumitem}
+\usepackage[normalem]{ulem}
+\usepackage{graphicx}
+\usepackage{subcaption}
+
+% Unicode
+\usepackage{ucs}
+\usepackage[utf8x]{inputenc}
+% \usepackage{autofe}
+
+%% -----------------------------------------------------------------------------
+%% Fonts
+%% \usepackage[osf]{libertine}
+%% \usepackage{helvet}
+%% \usepackage{lmodern}
+%% \IfFileExists{microtype.sty}{\usepackage{microtype}}{}
+
+%% -----------------------------------------------------------------------------
+%% Diagrams
+% \usepackage{tikz}
+% \usetikzlibrary{positioning}
+%% \usetikzlibrary{shapes}
+%% \usetikzlibrary{arrows}
+%% \usepackage{tikz-cd}
+%% \usepackage{pgfplots}
+\usepackage[all]{xy}
+
+%% -----------------------------------------------------------------------------
+%% Symbols
+\usepackage[fleqn]{amsmath}
+\usepackage{amssymb}
+\usepackage{wasysym}
+\usepackage{turnstile}
+\usepackage{centernot}
+\usepackage{stmaryrd}
+
+%% -----------------------------------------------------------------------------
+%% Utils
+\usepackage{bussproofs}
+\usepackage{umoline}
+\usepackage[export]{adjustbox}
+\usepackage{multicol}
+\usepackage{listingsutf8}
+\lstset{
+ basicstyle=\small\ttfamily,
+ extendedchars=\true,
+ inputencoding=utf8x,
+ xleftmargin=1cm
+}
+\usepackage{epigraph}
+
+%% -----------------------------------------------------------------------------
+%% Bibtex
+\usepackage{natbib}
+
+%% Numbering depth
+%% \setcounter{secnumdepth}{0}
+
+%% -----------------------------------------------------------------------------
+% We will generate all images so they have a width \maxwidth. This means
+% that they will get their normal width if they fit onto the page, but
+% are scaled down if they would overflow the margins.
+\makeatletter
+\def\maxwidth{
+ \ifdim\Gin@nat@width>\linewidth\linewidth
+ \else\Gin@nat@width\fi
+}
+\makeatother
+
+%% -----------------------------------------------------------------------------
+%% Links
+\usepackage[
+ setpagesize=false, % page size defined by xetex
+ unicode=false, % unicode breaks when used with xetex
+ xetex
+]{hyperref}
+
+\hypersetup{
+ breaklinks=true,
+ bookmarks=true,
+ pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
+ pdftitle={Observational Equality - Interim Report},
+ colorlinks=false,
+ pdfborder={0 0 0}
+}
+
+% Make links footnotes instead of hotlinks:
+% \renewcommand{\href}[2]{#2\footnote{\url{#1}}}
+
+% avoid problems with \sout in headers with hyperref:
+\pdfstringdefDisableCommands{\renewcommand{\sout}{}}
+
+\title{Observational Equality - Interim Report}
+\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
+\date{December 2012}
+
+\begin{document}
+
+\maketitle
+
+\setlength{\tabcolsep}{12pt}
+
+\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} I 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:practical} will describe additions common in practical programming
+languages based on ITT.
+
+Finally, I will explain why equality has been a tricky business in these
+theories, and talk about the various attempts have been made to make the
+situation better. One interesting development has recently emerged:
+Observational Type theory. I propose to explore the ways to turn these ideas
+into useful practices for programming and theorem proving.
+\end{abstract}
+
+\tableofcontents
+
+\section{Simple and not-so-simple types}
+\label{sec:types}
+
+\subsection{A note on notation}
+
+\newcommand{\appsp}{\hspace{0.07cm}}
+\newcommand{\app}[2]{#1\appsp#2}
+\newcommand{\absspace}{\hspace{0.03cm}}
+\newcommand{\abs}[2]{\lambda #1\absspace.\absspace#2}
+\newcommand{\termt}{t}
+\newcommand{\termm}{m}
+\newcommand{\termn}{n}
+\newcommand{\termp}{p}
+\newcommand{\termf}{f}
+\newcommand{\separ}{\ \ |\ \ }
+\newcommand{\termsyn}{\mathit{term}}
+\newcommand{\axname}[1]{\textbf{#1}}
+\newcommand{\axdesc}[2]{\axname{#1} \fbox{$#2$}}
+\newcommand{\lcsyn}[1]{\mathrm{\underline{#1}}}
+\newcommand{\lccon}[1]{\mathsf{#1}}
+\newcommand{\lcfun}[1]{\mathbf{#1}}
+\newcommand{\tyarr}{\to}
+\newcommand{\tysyn}{\mathit{type}}
+\newcommand{\ctxsyn}{\mathit{context}}
+\newcommand{\emptyctx}{\cdot}
+
+In the following sections I will introduce a lot of syntax, typing, and
+reduction rules, along with examples. To make the exposition clearer, usually
+the rules are preceded by what the rule looks like and what it shows (for
+example \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}).
+
+In the languages presented I will also use different fonts for different things:
+\begin{center}
+ \begin{tabular}{c | l}
+ $\lccon{Sans}$ & Sans serif, capitalised, for type constructors. \\
+ $\lccon{sans}$ & Sans serif, not capitalised, for data constructors. \\
+ $\lcsyn{roman}$ & Roman, underlined, for the syntax of the language. \\
+ $\lcfun{roman}$ & Roman, bold, for defined functions and values. \\
+ $math$ & Math mode font for quantified variables and syntax elements.
+ \end{tabular}
+\end{center}
+
+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
+Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
+
+\subsection{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.
+
+The syntax of $\lambda$-terms consists of just three things: variables,
+abstractions, and applications:
+
+\begin{center}
+\axname{syntax}
+$$
+\begin{array}{rcl}
+ \termsyn & ::= & x \separ (\abs{x}{\termsyn}) \separ (\app{\termsyn}{\termsyn}) \\
+ x & \in & \text{Some enumerable set of symbols, e.g.}\ \{x, y, z, \dots , x_1, x_2, \dots\}
+\end{array}
+$$
+\end{center}
+
+
+% I will omit parethesis in the usual manner. %TODO explain how
+
+I will use $\termt,\termm,\termn,\dots$ to indicate a generic term, and $x,y$
+for variables. I will also assume that all variable names in a term are unique
+to avoid problems with name capturing. Intuitively, abstractions
+($\abs{x}{\termt}$) introduce functions with a named parameter ($x$), and
+applications ($\app{\termt}{\termm}$) apply a function ($\termt$) to an argument
+($\termm$).
+
+The `applying' is more formally explained with a reduction rule:
+
+\newcommand{\bred}{\leadsto}
+\newcommand{\bredc}{\bred^*}
+
+\begin{center}
+\axdesc{reduction}{\termsyn \bred \termsyn}
+$$\app{(\abs{x}{\termt})}{\termm} \bred \termt[\termm / x]$$
+\end{center}
+
+Where $\termt[\termm / x]$ expresses the operation that substitutes all
+occurrences of $x$ with $\termm$ in $\termt$. In the future, I will use
+$[\termt]$ as an abbreviation for $[\termt / x]$. In the systems presented, the
+$\bred$ relation also includes reduction of subterms, for example if $\termt
+\bred \termm$ then $\app{\termt}{\termn} \bred \app{\termm}{\termn}$, and so on.
+
+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):
+\[
+ \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}.
+
+\subsection{The simply typed $\lambda$-calculus}
+\label{sec:stlc}
+
+\newcommand{\tya}{A}
+\newcommand{\tyb}{B}
+\newcommand{\tyc}{C}
+
+One 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}.
+
+We wish to introduce rules of the form $\Gamma \vdash \termt : \tya$, which
+reads `in context $\Gamma$, term $\termt$ has type $\tya$'.
+
+The syntax for types is as follows:
+
+\begin{center}
+ \axname{syntax}
+ $$\tysyn ::= x \separ \tysyn \tyarr \tysyn$$
+\end{center}
+
+I will use $\tya,\tyb,\dots$ to indicate a generic type.
+
+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.}:
+\begin{center}
+ \axname{syntax}
+ $$\termsyn ::= x \separ (\abs{x : \tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$
+\end{center}
+Now we are ready to give the typing judgements:
+
+\begin{center}
+ \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c c}
+ \AxiomC{\phantom{1em}}
+ \UnaryInfC{$\Gamma; x : \tya \vdash x : \tya$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma; x : \tya \vdash \termt : \tyb$}
+ \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \tya \tyarr \tyb$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c}
+ \AxiomC{$\Gamma \vdash \termt : \tya \tyarr \tyb$}
+ \AxiomC{$\Gamma \vdash \termm : \tya$}
+ \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb$}
+ \DisplayProof
+ \end{tabular}
+\end{center}
+
+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 - either it is a \emph{canonical}
+ value or it can take a step according to the evaluation rules. With canonical
+ value we indicate terms formed by canonical constructors, in this case only
+ $\lambda$\footnote{See section \ref{sec:fun-ext} for more information on
+ canonicity.}.
+\item[Preservation] If a well-typed term takes a step of evaluation, then the
+ resulting term is also well typed.
+\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*}
+ \app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})}
+\end{equation*}
+
+\newcommand{\lcfix}[2]{\lcsyn{fix} \appsp #1\absspace.\absspace #2}
+
+This makes the STLC Turing incomplete. We can recover the ability to loop by
+adding a combinator that recurses:
+$$
+ \termsyn ::= \dotsb \separ \lcfix{x : \tysyn}{\termsyn}
+$$
+\begin{center}
+ \begin{prooftree}
+ \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
+ \UnaryInfC{$\Gamma \vdash \lcfix{x : \tya}{\termt} : \tya$}
+ \end{prooftree}
+\end{center}
+$$
+ \lcfix{x : \tya}{\termt} \bred \termt[\lcfix{x : \tya}{\termt}]
+$$
+Which 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}
+\label{sec:curry-howard}
+
+\newcommand{\lcunit}{\lcfun{\langle\rangle}}
+
+It turns out that the STLC can be seen a natural deduction system for
+propositional logic. Terms are proofs, and their types are the propositions
+they prove. This remarkable fact is known as the Curry-Howard correspondence,
+or isomorphism.
+
+The `arrow' ($\to$) type corresponds to implication. If we wish to prove that
+$(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tya \tyarr \tyc)$, all we
+need to do is to devise a $\lambda$-term that has the correct type:
+\begin{equation*}
+ \abs{f : (\tya \tyarr \tyb)}{\abs{g : (\tyb \tyarr \tyc)}{\abs{x : \tya}{\app{g}{(\app{f}{x})}}}}
+\end{equation*}
+That is, function composition. We might want extend our bare lambda calculus
+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$).
+
+\newcommand{\lcinl}{\lccon{inl}\appsp}
+\newcommand{\lcinr}{\lccon{inr}\appsp}
+\newcommand{\lccase}[3]{\lcsyn{case}\appsp#1\appsp\lcsyn{of}\appsp#2\appsp#3}
+\newcommand{\lcfst}{\lcfun{fst}\appsp}
+\newcommand{\lcsnd}{\lcfun{snd}\appsp}
+\newcommand{\orint}{\vee I_{1,2}}
+\newcommand{\orintl}{\vee I_{1}}
+\newcommand{\orintr}{\vee I_{2}}
+\newcommand{\orel}{\vee E}
+\newcommand{\andint}{\wedge I}
+\newcommand{\andel}{\wedge E_{1,2}}
+\newcommand{\botel}{\bot E}
+\newcommand{\lcabsurd}{\lcfun{absurd}\appsp}
+\newcommand{\lcabsurdd}[1]{\lcfun{absurd}_{#1}\appsp}
+
+
+\begin{center}
+ \axname{syntax}
+ $$
+ \begin{array}{rcl}
+ \termsyn & ::= & \dotsb \\
+ & | & \lcinl \termsyn \separ \lcinr \termsyn \separ \lccase{\termsyn}{\termsyn}{\termsyn} \\
+ & | & (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
+ & | & \lcunit \\
+ \tysyn & ::= & \dotsb \separ \tysyn \vee \tysyn \separ \tysyn \wedge \tysyn \separ \bot \separ \top
+ \end{array}
+ $$
+\end{center}
+\begin{center}
+ \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
+ \begin{prooftree}
+ \AxiomC{$\Gamma \vdash \termt : \tya$}
+ \RightLabel{$\orint$}
+ \UnaryInfC{$\Gamma \vdash \lcinl \termt : \tya \vee \tyb$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \lcinr \termt : \tyb \vee \tya$}
+ \end{prooftree}
+ \begin{prooftree}
+ \AxiomC{$\Gamma \vdash \termt : \tya \vee \tyb$}
+ \AxiomC{$\Gamma \vdash \termm : \tya \tyarr \tyc$}
+ \AxiomC{$\Gamma \vdash \termn : \tyb \tyarr \tyc$}
+ \RightLabel{$\orel$}
+ \TrinaryInfC{$\Gamma \vdash \lccase{\termt}{\termm}{\termn} : \tyc$}
+ \end{prooftree}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\Gamma \vdash \termt : \tya$}
+ \AxiomC{$\Gamma \vdash \termm : \tyb$}
+ \RightLabel{$\andint$}
+ \BinaryInfC{$\Gamma \vdash (\tya , \tyb) : \tya \wedge \tyb$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termt : \tya \wedge \tyb$}
+ \RightLabel{$\andel$}
+ \UnaryInfC{$\Gamma \vdash \lcfst \termt : \tya$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\Gamma \vdash \termt : \bot$}
+ \RightLabel{$\botel$}
+ \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$}
+ \DisplayProof
+ &
+ \AxiomC{}
+ \RightLabel{$\top I$}
+ \UnaryInfC{$\Gamma \vdash \lcunit : \top$}
+ \DisplayProof
+ \end{tabular}
+\end{center}
+\begin{center}
+ \axdesc{reduction}{\termsyn \bred \termsyn}
+ \begin{eqnarray*}
+ \lccase{(\lcinl \termt)}{\termm}{\termn} & \bred & \app{\termm}{\termt} \\
+ \lccase{(\lcinr \termt)}{\termm}{\termn} & \bred & \app{\termn}{\termt} \\
+ \lcfst (\termt , \termm) & \bred & \termt \\
+ \lcsnd (\termt , \termm) & \bred & \termm
+ \end{eqnarray*}
+\end{center}
+
+With these rules, our STLC now looks remarkably similar in power and use to the
+natural deduction we already know. $\neg A$ can be expressed as $A \tyarr
+\bot$. However, there is an important omission: there is no term of the type $A
+\vee \neg A$ (excluded middle), or equivalently $\neg \neg A \tyarr A$ (double
+negation), or indeed any term with a type equivalent to those.
+
+This has a considerable effect on our logic and it's no coincidence, since there
+is no obvious computational behaviour for laws like the excluded middle.
+Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
+and all the systems analysed will have this characteristic since they build on
+the foundation of the STLC\footnote{There is research to give computational
+ behaviour to classical logic, but I will not touch those subjects.}.
+
+Finally, going back to our $\lcsyn{fix}$ combinator, it's now easy to see how
+we would want to exclude such a thing if we want to use STLC as a logic, since
+it allows us to prove everything: $(\lcfix{x : \tya}{x}) : \tya$ clearly works
+for any $A$! This is a crucial point: in general we wish to have systems that
+do not let the user devise a term of type $\bot$, otherwise our logic will be
+unsound\footnote{Obviously such a term can be present under a $\lambda$.}.
+
+\subsection{Extending the STLC}
+
+\newcommand{\lctype}{\lccon{Type}}
+\newcommand{\lcite}[3]{\lcsyn{if}\appsp#1\appsp\lcsyn{then}\appsp#2\appsp\lcsyn{else}\appsp#3}
+\newcommand{\lcbool}{\lccon{Bool}}
+\newcommand{\lcforallz}[2]{\forall #1 \absspace.\absspace #2}
+\newcommand{\lcforall}[3]{(#1 : #2) \tyarr #3}
+\newcommand{\lcexists}[3]{(#1 : #2) \times #3}
+
+The STLC can be made more expressive in various ways. Henk Barendregt
+succinctly expressed geometrically how we can expand our type system:
+
+$$
+\xymatrix@!0@=1.5cm{
+ & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
+ & & \lambda C \ar@{-}[dd]
+ \\
+ \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
+ & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
+ \\
+ & \lambda\underline\omega \ar@{-}'[r][rr]
+ & & \lambda P\underline\omega
+ \\
+ \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
+ & & \lambda P \ar@{-}[ur]
+}
+$$
+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}$)] We can quantify over
+ types in our type signatures: $(\abs{A : \lctype}{\abs{x : A}{x}}) :
+ \lcforallz{A}{A \tyarr 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}}$)] We have
+ type operators: $(\abs{A : \lctype}{\abs{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: $(\abs{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. 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'.
+
+\section{Intuitionistic Type Theory and dependent types}
+\label{sec:itt}
+
+\newcommand{\lcset}[1]{\lccon{Type}_{#1}}
+\newcommand{\lcsetz}{\lccon{Type}}
+\newcommand{\defeq}{\cong}
+
+\subsection{A Bit of History}
+
+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}.
+
+A related development is the polymorphic $\lambda$-calculus, and specifically
+the previously mentioned System F, which was developed independently by Girard
+and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
+fact is that while System F is impredicative it is still consistent and strongly
+normalising. \cite{Coquand1986} further extended this line of work with the
+Calculus of Constructions (CoC).
+
+\subsection{A Core Type Theory}
+\label{sec:core-tt}
+
+The calculus I present follows the exposition in \citep{Thompson1991}, and is
+quite close to the original formulation of predicative ITT as found in
+\citep{Martin-Lof1984}.
+
+\begin{center}
+ \axname{syntax}
+ \begin{eqnarray*}
+ \termsyn & ::= & x \\
+ & | & \lcforall{x}{\termsyn}{\termsyn} \separ \abs{x : \termsyn}{\termsyn} \separ \app{\termsyn}{\termsyn} \\
+ & | & \lcexists{x}{\termsyn}{\termsyn} \separ (\termsyn , \termsyn)_{x.\termsyn} \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
+ & | & \bot \separ \lcabsurd_{\termsyn} \termsyn \\
+ & | & \lcset{n} \\
+ n & \in & \mathbb{N}
+ \end{eqnarray*}
+
+ \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c c}
+ \AxiomC{\phantom{1em}}
+ \UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termt : \tya$}
+ \AxiomC{$\tya \defeq \tyb$}
+ \BinaryInfC{$\Gamma \vdash \termt : \tyb$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termt : \bot$}
+ \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
+ \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \lcforall{x}{\tya}{\tyb}$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termt : \lcforall{x}{\tya}{\tyb}$}
+ \AxiomC{$\Gamma \vdash \termm : \tya$}
+ \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb[\termm ]$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\Gamma \vdash \termt : \tya$}
+ \AxiomC{$\Gamma \vdash \termm : \tyb[\termt ]$}
+ \BinaryInfC{$\Gamma \vdash (\termt, \termm)_{x.\tyb} : \lcexists{x}{\tya}{\tyb}$}
+ \noLine
+ \UnaryInfC{$\phantom{1em}$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termt: \lcexists{x}{\tya}{\tyb}$}
+ \UnaryInfC{$\hspace{0.7cm} \Gamma \vdash \lcfst \termt : \tya \hspace{0.7cm}$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb[\lcfst \termt ]$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\phantom{1em}$}
+ \UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$}
+ \noLine
+ \UnaryInfC{$\phantom{1em}$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
+ \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
+ \BinaryInfC{$\Gamma \vdash \lcforall{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \lcexists{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \axdesc{reduction}{\termsyn \bred \termsyn}
+ \begin{eqnarray*}
+ \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm ] \\
+ \lcfst (\termt, \termm) & \bred & \termt \\
+ \lcsnd (\termt, \termm) & \bred & \termm
+ \end{eqnarray*}
+\end{center}
+
+When showing examples types will be omitted when this can be done without loss
+of clarity, for example $\abs{x}{x}$ in place of $\abs{A : \lcsetz}{\abs{x :
+ A}{x}}$. I will also use $\lcsetz$ as $\lcset{0}$.
+
+There are a lot of new factors at play here. The first thing to notice is that
+the separation between types and terms is gone. All we have is terms, that
+include both values (terms of type $\lcset{0}$) and types (terms of type
+$\lcset{n}$, with $n > 0$). This change is reflected in the typing rules.
+While in the STLC values and types are kept well separated (values never go
+`right of the colon'), in ITT types can freely depend on values.
+
+This relation is expressed in the typing rules for $\tyarr$ and $\times$: if a
+function has type $\lcforall{x}{\tya}{\tyb}$, $\tyb$ can depend on $x$.
+Examples will make this clearer once some base types are added in section
+\ref{sec:base-types}.
+
+$\tyarr$ and $\times$ are at the core of the machinery of ITT:
+
+\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$.
+
+\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
+ product'. Like $\wedge$, it is formed by providing a pair of things. In our
+ logic, it represents existential quantification. Similarly to $\tyarr$, it is
+ always written as $\exists x : \tya. \tyb$.
+
+ For added confusion, in the literature that calls forall $\Pi$, $\exists$ 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.
+\end{description}
+
+Another thing to notice is that types are very `first class': we are free to
+create functions that accept and return types. For this reason we define
+$\defeq$ as the smallest equivalence relation extending $\bredc$, where $\bredc$
+is the reflexive transitive closure of $\bred$; and we treat types that are
+relate 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
+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
+$\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 :
+ \lctype}{x})}{\lcbool} \defeq \lcbool$. The theme of equality is central
+and will be analysed better later.
+
+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$
+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.
+
+Note that the Curry-Howard correspondence runs through ITT as it did with the
+STLC with the difference that ITT corresponds to an higher order propositional
+logic.
+
+\subsection{Base Types}
+\label{sec:base-types}
+
+\newcommand{\lctrue}{\lccon{true}}
+\newcommand{\lcfalse}{\lccon{false}}
+\newcommand{\lcw}[3]{\lccon{W} #1 : #2 \absspace.\absspace #3}
+\newcommand{\lcnode}[4]{#1 \lhd_{#2 . #3} #4}
+\newcommand{\lcnodez}[2]{#1 \lhd #2}
+\newcommand{\lcited}[5]{\lcsyn{if}\appsp#1/#2\appsp.\appsp#3\appsp\lcsyn{then}\appsp#4\appsp\lcsyn{else}\appsp#5}
+\newcommand{\lcrec}[4]{\lcsyn{rec}\appsp#1/#2\appsp.\appsp#3\appsp\lcsyn{with}\appsp#4}
+\newcommand{\lcrecz}[2]{\lcsyn{rec}\appsp#1\appsp\lcsyn{with}\appsp#2}
+\newcommand{\AxiomL}[1]{\Axiom$\fCenter #1$}
+\newcommand{\UnaryInfL}[1]{\UnaryInf$\fCenter #1$}
+
+While the ITT presented is a fairly complete logic, it is not that useful for
+programming. If we wish to make it better, we can add some base types to
+represent the data structures we know and love, such as numbers, lists, and
+trees. Apart from some unsurprising data types, we introduce $\lccon{W}$, a
+very general tree-like structure useful to represent inductively defined types
+and that will allow us to express structural recursion in an equally general
+manner.
+
+\begin{center}
+ \axname{syntax}
+ \begin{eqnarray*}
+ \termsyn & ::= & \dots \\
+ & | & \top \separ \lcunit \\
+ & | & \lcbool \separ \lctrue \separ \lcfalse \separ \lcited{\termsyn}{x}{\termsyn}{\termsyn}{\termsyn} \\
+ & | & \lcw{x}{\termsyn}{\termsyn} \separ \lcnode{\termsyn}{x}{\termsyn}{\termsyn} \separ \lcrec{\termsyn}{x}{\termsyn}{\termsyn}
+ \end{eqnarray*}
+
+ \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c c}
+ \AxiomC{}
+ \UnaryInfC{$\hspace{0.2cm}\Gamma \vdash \top : \lcset{0} \hspace{0.2cm}$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \lcbool : \lcset{0}$}
+ \DisplayProof
+ &
+ \AxiomC{}
+ \UnaryInfC{$\Gamma \vdash \lcunit : \top$}
+ \noLine
+ \UnaryInfC{\phantom{1em}}
+ \DisplayProof
+ &
+ \AxiomC{}
+ \UnaryInfC{$\Gamma \vdash \lctrue : \lcbool$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \lcfalse : \lcbool$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c}
+ \AxiomC{$\Gamma \vdash \termt : \lcbool$}
+ \AxiomC{$\Gamma \vdash \termm : \tya[\lctrue]$}
+ \AxiomC{$\Gamma \vdash \termn : \tya[\lcfalse]$}
+ \TrinaryInfC{$\Gamma \vdash \lcited{\termt}{x}{\tya}{\termm}{\termn} : \tya[\termt]$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c}
+ \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
+ \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
+ \BinaryInfC{$\Gamma \vdash \lcw{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c}
+ \AxiomC{$\Gamma \vdash \termt : \tya$}
+ \AxiomC{$\Gamma \vdash \termf : \tyb[\termt ] \tyarr \lcw{x}{\tya}{\tyb}$}
+ \BinaryInfC{$\Gamma \vdash \lcnode{\termt}{x}{\tyb}{\termf} : \lcw{x}{\tya}{\tyb}$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c}
+ \AxiomC{$\Gamma \vdash \termt: \lcw{x}{\tya}{\tyb}$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \lcforall{\termm}{\tya}{\lcforall{\termf}{\tyb[\termm] \tyarr \lcw{x}{\tya}{\tyb}}{(\lcforall{\termn}{\tyb[\termm]}{\tyc[\app{\termf}{\termn}]}) \tyarr \tyc[\lcnodez{\termm}{\termf}]}}$}
+ \UnaryInfC{$\Gamma \vdash \lcrec{\termt}{x}{\tyc}{\termp} : \tyc[\termt]$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \axdesc{reduction}{\termsyn \bred \termsyn}
+ \begin{eqnarray*}
+ \lcited{\lctrue}{x}{\tya}{\termt}{\termm} & \bred & \termt \\
+ \lcited{\lcfalse}{x}{\tya}{\termt}{\termm} & \bred & \termm \\
+ \lcrec{\lcnodez{\termt}{\termf}}{x}{\tya}{\termp} & \bred & \app{\app{\app{\termp}{\termt}}{\termf}}{(\abs{\termm}{\lcrec{\app{f}{\termm}}{x}{\tya}{\termp}})}
+ \end{eqnarray*}
+\end{center}
+
+The introduction and elimination for $\top$ and $\lcbool$ are unsurprising.
+Note that in the $\lcite{\dotsb}{\dotsb}{\dotsb}$ construct the type of the
+branches are dependent on the value of the conditional.
+
+The rules for $\lccon{W}$, on the other hand, are quite an eyesore. The idea
+behind $\lccon{W}$ types is to build up `trees' where the number of `children'
+of each node is dependent on the value (`shape') in the node. This is captured
+by the $\lhd$ constructor, where the argument on the left is the value, and the
+argument on the right is a function that returns a child for each possible value
+of $\tyb[\text{node value}]$, if $\lcw{x}{\tya}{\tyb}$. The recursor
+$\lcrec{\termt}{x}{\tyc}{\termp}$ uses $p$ to inductively prove that
+$\tyc[\termt]$ holds.
+
+\subsection{Some examples}
+
+Now we can finally provide some meaningful examples. Apart from omitting types,
+I will also use some abbreviations:
+\begin{itemize}
+ \item $\_\mathit{operator}\_$ to define infix operators
+ \item $\abs{x\appsp y\appsp z : \tya}{\dotsb}$ to define multiple abstractions at the same
+ time
+\end{itemize}
+
+\subsubsection{Sum types}
+
+We would like to recover our sum type, or disjunction, $\vee$. This is easily
+achieved with $\times$:
+\[
+\begin{array}{rcl}
+ \_\vee\_ & = & \abs{\tya\appsp\tyb : \lcsetz}{\lcexists{x}{\lcbool}{\lcite{x}{\tya}{\tyb}}} \\
+ \lcinl & = & \abs{x}{(\lctrue, x)} \\
+ \lcinr & = & \abs{x}{(\lcfalse, x)} \\
+ \lcfun{case} & = & \abs{x : \tya \vee \tyb}{\abs{f : \tya \tyarr \tyc}{\abs{g : \tyb \tyarr \tyc}{ \\
+ & & \hspace{0.5cm} \app{(\lcited{\lcfst x}{b}{(\lcite{b}{A}{B}) \tyarr C}{f}{g})}{(\lcsnd x)}}}}
+\end{array}
+\]
+What is going on here? We are using $\exists$ with $\lcbool$ as a tag, so that
+we can choose between one of two types in the second element. In
+$\lcfun{case}$ we use $\lcite{\lcfst x}{\dotsb}{\dotsb}$ to discriminate on the
+tag, that is, the first element of $x : \tya \vee \tyb$. If the tag is true,
+then we know that the second element is of type $\tya$, and we will apply $f$.
+The same applies to the other branch, with $\tyb$ and $g$.
+
+\subsubsection{Naturals}
+
+Now it's time to showcase the power of $\lccon{W}$ types.
+\begin{eqnarray*}
+ \lccon{Nat} & = & \lcw{b}{\lcbool}{\lcite{b}{\top}{\bot}} \\
+ \lccon{zero} & = & \lcfalse \lhd \abs{z}{\lcabsurd z} \\
+ \lccon{suc} & = & \abs{n}{(\lctrue \lhd \abs{\_}{n})} \\
+ \lcfun{plus} & = & \abs{x\appsp y}{\lcrecz{x}{(\abs{b}{\lcite{b}{\abs{\_\appsp f}{\app{\lccon{suc}}{(\app{f}{\lcunit})}}}{\abs{\_\appsp\_}{y}}})}}
+\end{eqnarray*}
+Here we encode natural numbers through $\lccon{W}$ types. Each node contains a
+$\lcbool$. If the $\lcbool$ is $\lcfalse$, then there are no children, since we
+have a function $\bot \tyarr \lccon{Nat}$: this is our $0$. If it's $\lctrue$,
+we need one child only: the predecessor. We recurse giving $\lcsyn{rec}$ a
+function that handles the `base case' 0 when the $\lcbool$ is $\lctrue$, and the
+inductive case otherwise.
+
+We postpone more complex examples after the introduction of inductive families
+and pattern matching, since $\lccon{W}$ types get unwieldy very quickly.
+
+\subsection{Propositional Equality}
+\label{sec:propeq}
+
+We can finally introduce one of the central subjects of my project:
+propositional equality.
+
+\newcommand{\lceq}[3]{#2 =_{#1} #3}
+\newcommand{\lceqz}[2]{#1 = #2}
+\newcommand{\lcrefl}[2]{\lccon{refl}_{#1}\appsp #2}
+\newcommand{\lcsubst}[3]{\lcfun{subst}\appsp#1\appsp#2\appsp#3}
+
+\begin{center}
+ \axname{syntax}
+ \begin{eqnarray*}
+ \termsyn & ::= & ... \\
+ & | & \lceq{\termsyn}{\termsyn}{\termsyn} \separ \lcrefl{\termsyn}{\termsyn} \separ \lcsubst{\termsyn}{\termsyn}{\termsyn}
+ \end{eqnarray*}
+
+ \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\Gamma \vdash \termt : \tya$}
+ \UnaryInfC{$\Gamma \vdash \lcrefl{\tya}{\termt} : \lceq{\tya}{\termt}{\termt}$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash \termp : \lceq{\tya}{\termt}{\termm}$}
+ \AxiomC{$\Gamma \vdash \tyb : \tya \tyarr \lcsetz$}
+ \AxiomC{$\Gamma \vdash \termn : \app{\tyb}{\termt}$}
+ \TrinaryInfC{$\Gamma \vdash \lcsubst{\termp}{\tyb}{\termn} : \app{\tyb}{\termm}$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \axdesc{reduction}{\termsyn \bred \termsyn}
+ \begin{eqnarray*}
+ \lcsubst{(\lcrefl{\tya}{\termt})}{\tyb}{\termm} \bred \termm
+ \end{eqnarray*}
+\end{center}
+
+Propositional equality internalises equality as a type. The only way to
+introduce an equality proof is by reflexivity ($\lccon{refl}$). The eliminator
+is in the style of `Leibnitz's law' of equality: `equals can be substituted for
+equals' ($\lcfun{subst}$). The computation rule refers to the fact that every
+proof of equality will be a $\lccon{refl}$. We can use $\neg
+(\lceq{\tya}{x}{y})$ to express inequality.
+
+These elements conclude our presentation of a `core' type theory. For an
+extended example of a similar theory in use see Section 6.2 of
+\citep{Thompson1991}\footnote{Note that while I attempted to formalise the proof
+ in Agda, I found a bug in the book! See the errata for details:
+ \url{http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/errata.html}.}. The above
+language and examples have been codified in Agda\footnote{More on Agda in the
+ next section.}, see appendix \ref{app:agda-code}.
+
+\section{A more useful language}
+\label{sec:practical}
+
+While our core type theory equipped with $\lccon{W}$ types is very usefully
+conceptually as a simple but complete language, things get messy very fast,
+since handling $\lccon{W}$ types directly is incredibly cumbersome. In this
+section I will present the elements that are usually included in theorem provers
+or programming languages to make them usable by mathematicians or programmers.
+
+All the features presented are present in the second version of the Agda system
+\citep{Norell2007, Bove2009}. Agda follows a tradition of theorem provers based
+on ITT with inductive families and pattern matching. The closest relative of
+Agda, apart from previous versions, is Epigram \citep{McBride2004, EpigramTut}.
+Coq is another notable theorem prover based on the same concepts, and the first
+and most popular \citep{Coq}.
+
+The main difference between Coq and Agda/Epigram is that the former focuses on
+theorem proving, while the latter also want to be useful as functional
+programming languages, while still offering good tools to express
+mathematics\footnote{In fact, currently, Agda is used almost exclusively to
+ express mathematics, rather than to program.}. This is reflected in a series
+of differences that I will not discuss here (most notably the absence of tactics
+but better support for pattern matching in Agda/Epigram). Every feature will be
+presented as it is Agda.
+
+As previously, all the examples presented have been codified in Agda, see
+appendix \ref{app:agda-code}.
+
+\subsection{Type inference}
+
+The theory I presented is fully explicit in the sense that the user has to
+specify every type when forming abstractions, products, etc.
+
+For the programmer used to Hindley-Milner as in Haskell and SML (and for any
+human being), this is a great burden. Complete inference is undecidable - which
+is hardly surprising considering the role that types play - but partial
+inference in the style of \cite{Pierce2000}, also called `bidirectional type
+checking' in this context, will have to be deployed in a practical system.
+
+Agda gives users an explicit way to indicate which fields should be implicit, by
+wrapping them in curly braces in type signatures: $\{A : \lcsetz\} \tyarr
+\dotsb$. It also allows to omit types of arguments altimeter, if they can be
+inferred by other arguments: $\{A\} \tyarr (x : A) \tyarr \dotsb$.
+
+\subsection{Inductive families}
+\label{sec:inductive-families}
+
+\newcommand{\lcdata}[1]{\lcsyn{data}\appsp #1}
+\newcommand{\lcdb}{\ |\ }
+\newcommand{\lcind}{\hspace{0.2cm}}
+\newcommand{\lcwhere}{\appsp \lcsyn{where}}
+\newcommand{\lclist}[1]{\app{\lccon{List}}{#1}}
+\newcommand{\lcnat}{\lccon{Nat}}
+\newcommand{\lcvec}[2]{\app{\app{\lccon{Vec}}{#1}}{#2}}
+
+Inductive families were first introduced by \cite{Dybjer1991}. For the reader
+familiar with the recent developments present in the GHC compiler for Haskell,
+inductive families will look similar to GADTs (Generalised Abstract Data Types)
+\citep[Section 7.4.7]{GHC}.
+Haskell-style data types provide \emph{parametric polymorphism}, so that we can
+define types that range over type parameters:
+\begin{lstlisting}
+List a = Nil | Cons a (List a)
+\end{lstlisting}
+In this way we define the \texttt{List} type once while allowing elements to be
+of any type. In Haskell \texttt{List} will be a type constructor of kind
+\texttt{* -> *}, while \texttt{Nil :: List a} and \texttt{Cons :: a -> List a ->
+ List a}\footnote{Note that the \texttt{a}s are implicitly quantified type
+ variables.}.
+
+Inductive families bring this concept one step further by allowing some of the
+parameters to be constrained by constructors. We call these `variable'
+parameters `indices'. For example we might define natural numbers
+\[
+\begin{array}{l}
+\lcdata{\lcnat} : \lcsetz \lcwhere \\
+ \begin{array}{l@{\ }l}
+ \lcind \lccon{zero} &: \lcnat \\
+ \lcind \lccon{suc} &: \lcnat \tyarr \lcnat
+ \end{array}
+\end{array}
+\]
+And then define a type for lists indexed by length:
+\[
+\begin{array}{l}
+\lcdata{\lccon{Vec}}\appsp (A : \lcsetz) : \lcnat \tyarr \lcsetz \lcwhere \\
+ \begin{array}{l@{\ }l}
+ \lcind \lccon{nil} &: \lcvec{A}{\lccon{zero}} \\
+ \lcind \_::\_ &: \{n : \lccon{Nat}\} \tyarr A \tyarr \lcvec{A}{n} \tyarr \lcvec{A}{\app{(\lccon{suc}}{n})}
+ \end{array}
+\end{array}
+\]
+Note that contrary to the Haskell ADT notation, with inductive families we
+explicitly list the types for the type and data constructors. In $\lccon{Vec}$,
+$A$ is a parameter (same across all constructors) while the $\lcnat$ is an
+index. In our syntax, in the $\lcsyn{data}$ declaration, things to the left of
+the colon are parameters, while on the right we can define the type of indices.
+Also note that the parameters' identifiers will be in scope across all
+constructors, while indices' won't.
+
+In this $\lccon{Vec}$ example, when we form a new list the length is
+$\lccon{zero}$. When we append a new element to an existing list of length $n$,
+the new list is of length $\app{\lccon{suc}}{n}$, that is, one more than the
+previous length. Once $\lccon{Vec}$ is defined we can do things much more
+safely than with normal lists. For example, we can define an $\lcfun{head}$
+function that returns the first element of the list:
+\[
+\begin{array}{l}
+\lcfun{head} : \{A\ n\} \tyarr \lcvec{A}{(\app{\lccon{suc}}{n})} \tyarr A
+\end{array}
+\]
+Note that we will not be able to provide this function with a
+$\lcvec{A}{\lccon{zero}}$, since it needs an index which is a successor of some
+number.
+
+\newcommand{\lcfin}[1]{\app{\lccon{Fin}}{#1}}
+
+If we wish to index a $\lccon{Vec}$ safely, we can define an inductive family
+$\lcfin{n}$, which represents the family of numbers smaller than a given number
+$n$:
+\[
+\begin{array}{l}
+ \lcdata{\lccon{Fin}} : \lcnat \tyarr \lcsetz \lcwhere \\
+ \begin{array}{l@{\ }l}
+ \lcind \lccon{fzero} &: \{n\} \tyarr \lcfin{(\app{\lccon{suc}}{n})} \\
+ \lcind \lccon{fsuc} &: \{n\} \tyarr \lcfin{n} \tyarr \lcfin{(\app{\lccon{suc}}{n})}
+ \end{array}
+\end{array}
+\]
+$\lccon{fzero}$ is smaller than any number apart from $\lccon{zero}$. Given
+the family of numbers smaller than $n$, we can produce the family of numbers
+smaller than $\app{\lccon{suc}}{n}$. Now we can define an `indexing' operation
+for our $\lccon{Vec}$:
+\[
+\begin{array}{l}
+\_\lcfun{!!}\_ : \{A\ n\} \tyarr \lcvec{A}{n} \tyarr \lcfin{n} \tyarr A
+\end{array}
+\]
+In this way we will be sure that the number provided as an index will be smaller
+than the length of the $\lccon{Vec}$ provided.
+
+\subsubsection{Computing with inductive families}
+
+I have carefully avoided to define the functions that I mentioned as example,
+since one question still is unanswered: `how do we work with inductive
+families'? The most basic approach is to work with eliminators, that can be
+automatically provided by the programming language for each data type defined.
+For example the induction principle on natural numbers will serve as an
+eliminator for $\lcnat$:
+\[
+\begin{array}{l@{\ } c@{\ } l}
+ \lcfun{NatInd} & : & (A : \lcsetz) \tyarr \\
+ & & A \tyarr (\lcnat \tyarr A \tyarr A) \tyarr \\
+ & & \lcnat \tyarr A
+\end{array}
+\]
+
+That is, if we provide an $A$ (base case), and then given a number and an $A$ we
+give the next $A$ (inductive step), then an $A$ can be computed for every
+number. This can be expressed easily in Haskell:
+\begin{lstlisting}
+data Nat = Zero | Suc Nat
+natInd :: a -> (Nat -> a -> a) -> Nat -> a
+natInd z _ Zero = z
+natInd z f (Suc n) = f n (natInd z f n)
+\end{lstlisting}
+However, in a dependent setting, we can do better:
+\[
+\begin{array}{l@{\ } c@{\ } l}
+ \lcfun{NatInd} & : & (P : \lcnat \tyarr \lcsetz) \tyarr \\
+ & & \app{P}{\lccon{zero}} \tyarr ((n : \lcnat) \tyarr \app{P}{n} \tyarr \app{P}{(\app{\lccon{suc}}{n})}) \tyarr \\
+ & & (n : \lcnat) \tyarr \app{P}{n}
+\end{array}
+\]
+This expresses the fact that the resulting type can be dependent on the number.
+In other words, we are proving that $P$ holds for all $n : \lcnat$.
+
+Naturally a reduction rule will be associated with each eliminator:
+\[
+\begin{array}{l c l}
+\app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{\lccon{zero}} & \bred & z \\
+\app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{(\app{\lccon{suc}}{n})} & \bred & \app{\app{f}{n}}{(\app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{n})}
+\end{array}
+\]
+Which echoes the \texttt{natInd} function defined in Haskell. An extensive
+account on combinators and inductive families can be found in \citep{McBride2004}.
+
+\subsubsection{Pattern matching and guarded recursion}
+
+However, combinators are far more cumbersome to use than the techniques usually
+employed in functional programming: pattern matching and recursion.
+\emph{General} recursion (exemplified by the $\lcsyn{fix}$ combinator in section
+\ref{sec:stlc}) cannot be added if we want to keep our theory free of $\bot$.
+The common solution to this problem is to allow recursive calls only if the
+arguments are structurally smaller than what the function received, what is
+known as \emph{structural} recursion. For example, if we have a $\lccon{Tree}$
+family with a $\lccon{node}\appsp l \appsp r$ (and maybe others) constructor,
+functions that work on $\lccon{Tree}$ will be able to make recursive calls on
+$l$ and $r$.
+
+Pattern matching on the other hand gains considerable power with inductive
+families, since when we match a constructor we are gaining information on the
+indices of the family. Thus matching constructors will enable us to restrict
+patterns of other arguments.
+
+Following this discipline defining $\lcfun{head}$ becomes easy:
+\[
+\begin{array}{l}
+\lcfun{head} : \{A\ n\} \tyarr \lcvec{A}{(\app{\lccon{suc}}{n})} \tyarr A \\
+\lcfun{head}\appsp(x :: \_) = x
+\end{array}
+\]
+We need no case for $\lccon{nil}$, since the type checker knows that the
+equation $n = \lccon{zero} = \app{\lccon{suc}}{n'}$ cannot be satisfied.
+
+More details on the implementations of inductive families can be found in
+\citep{McBride2004, Norell2007}.
+
+\subsection{Friendlier universes}
+
+Universes as presented in section \ref{sec:core-tt} are quite cumbersome to work
+with. Consider the example where we define an inductive family for booleans and
+then we want to define an `if then else' eliminator:
+\[
+\begin{array}{l}
+\lcdata{\lcbool} : \lcsetz \lcwhere \\
+ \begin{array}{l@{\ }l}
+ \lcind \lccon{true} &: \lcbool \\
+ \lcind \lccon{false} &: \lcbool
+ \end{array}\\
+\\
+\lcfun{ite} : \{A : \lcset{0}\} \tyarr \lcbool \tyarr A \tyarr A \tyarr A \\
+\lcfun{ite} \appsp \lccon{true} \appsp x \appsp \_ = x \\
+\lcfun{ite} \appsp \lccon{false} \appsp \_ \appsp x = x
+\end{array}
+\]
+
+What if we want to use $\lcfun{ite}$ with types, for example $\lcfun{ite} \appsp
+b \appsp \lcnat \appsp \lccon{Bool}$? Clearly $\lcnat$ is not of type
+$\lcset{0}$, so we'd have to redefine $\lcfun{ite}$ with exactly the same body,
+but different type signature. The problem is even more evident with type
+families: for example our $\lccon{List}$ can only contain values, and if we want
+to build lists of types we need to define another identical, but differently
+typed, family.
+
+One option is to have a \emph{cumulative} theory, where $\lcset{n} : \lcset{m}$
+iff $n < m$. Then we can have a sufficiently large level in our type signature
+and forget about it. Moreover, levels in this setting can be inferred
+mechanically \citep{Pollack1990}, and thus we can lift the burden of specifying
+universes from the user. This is the approach taken by Epigram.
+
+Another more expressive (but currently more cumbersome) way is to expose
+universes more, giving the user a way to quantify them and to take the least
+upper bound of two levels. This is the approach taken by Agda, where for
+example we can define a level-polymorphic $\times$:
+\[
+\begin{array}{l}
+\lcdata{\_\times\_}\ \{a\ b : \lccon{Level}\}\ (A : \lcset{a})\ (B : A \tyarr \lcset{b}) : \lcset{a \sqcup b} \lcwhere \\
+ \lcind \_ , \_ : (x : A) \tyarr \app{B}{x} \tyarr A \times \app{B}{x}
+\end{array}
+\]
+Levels can be made implicit as shown and can be almost always inferred.
+However, having to decorate each type signature with quantified levels adds
+quite a lot of noise. An inference algorithm that automatically quantifies and
+instantiates levels (much like Hindley-Milner for types) seems feasible, but is
+currently not implemented anywhere. The ideal situation would be polymorphic,
+cumulative levels, with an easy way to omit treatment of levels unless in the
+(possibly few) cases where the inference algorithm breaks down.
+
+\subsection{Coinduction}
+
+One thing that the Haskell programmer will miss in ITT as presented is the
+possibility to work with infinite data. The classic example is the manipulation
+of infinite streams:
+\begin{lstlisting}
+zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
+
+fibs :: [Int]
+fibs = 0 : 1 : zipWith (+) fibs (tail fibs)
+\end{lstlisting}
+While we can clearly write useful programs of this kind, we need to be careful,
+since \texttt{length fibs}, for example, does not make much sense\footnote{Note
+ that if instead of machine \texttt{Int}s we used naturals as defined
+ previously, getting the length of an infinite list would be a productive
+ definition.}.
+
+In less informal terms, we need to distinguish between \emph{productive} and
+non-productive definitions. A productive definition is one for which pattern
+matching on data will never diverge, which is the case for \texttt{fibs} but
+not, for example, for \texttt{let x = x in x :: [Int]}. It is very desirable to
+recover \emph{only} the productive definition so that total programs working
+with infinite data can be written.
+
+This desire has lead to separate the notion of (finite) data and \emph{codata},
+which can be worked on by \emph{coinduction} - an overview is given in
+\citep{Jacobs1997}. Research is very active on this subject since coinduction
+as implemented by Coq and Agda is not satisfactory in different ways.
+
+\section{Many equalities}
+
+\subsection{Revision, and function extensionality}
+\label{sec:fun-ext}
+
+\epigraph{\emph{Half of my time spent doing research involves thinking up clever
+ schemes to avoid needing functional extensionality.}}{@larrytheliquid}
+
+Up to this point, I have introduced two equalities: \emph{definitional} equality
+($\defeq$) and \emph{propositional} equality ($=_{\tya}$).
+
+Definitional equality relates terms that the type checker identifies as equal.
+Our definition in section \ref{sec:core-tt} consisted of `reduce the two terms
+to their normal forms, then check if they are equal (up to $\alpha$-renaming)'.
+We can extend this definition in other ways so that more terms will be
+identified as equal. Common ones include doing $\eta$-expansion, which converts
+partial appications of functions, and congruence laws for $\lambda$:
+\begin{center}
+ \begin{tabular}{c c c}
+ \AxiomC{$\Gamma \vdash \termf : \tya \tyarr \tyb$}
+ \UnaryInfC{$\Gamma \vdash \termf \defeq \abs{x}{\app{\termf}{x}}$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma; x : \tya \vdash \termf \defeq g$}
+ \UnaryInfC{$\Gamma \vdash \abs{x}{\termf} \defeq \abs{x}{g}$}
+ \DisplayProof
+ \end{tabular}
+\end{center}
+Definitional equality is used in the type checking process, and this means that
+in dependently typed languages type checking and evaluation are intertwined,
+since we need to reduce types to normal forms to check if they are equal. It
+also means that we need be able to compute under binders, for example to
+determine that $\abs{x}{\app{(\abs{y}{y})}{\tya}} \defeq \abs{x}{\tya}$. This
+process goes on `under the hood' and is outside the control of the user.
+
+Propositional equality, on the other hand, is available to the user to reason
+about equality, internalising it as a type. As we have seen in section
+\ref{sec:propeq} propositional equality is introduced by reflexivity and
+eliminated with a `Leibnitz's law' style rule ($\lcfun{subst}$). Note that now
+that we have inductive families and dependent pattern matching we do not need
+hard coded rules to express this concepts\footnote{Here I use Agda notation, and
+ thus I cannot redefine $=$ and use subscripts, so I am forced to use $\equiv$
+ with implicit types. After I will carry on using the old notation.}:
+\[
+\begin{array}{l}
+ \lcdata{\lccon{\_\equiv\_}} : \{A : \lcsetz\} : A \tyarr A \tyarr \lcsetz \lcwhere \\
+ \begin{array}{l@{\ }l}
+ \lcind \lccon{refl} &: \{x : A\} \tyarr x \equiv x
+ \end{array} \\
+ \\
+ \lcfun{subst} : \{A : \lcsetz\} \tyarr \{t\ m : A\} \tyarr t \equiv m \tyarr (B : A \tyarr \lcsetz) \tyarr \app{B}{t} \tyarr \app{B}{m} \\
+ \lcfun{subst} \appsp \lccon{refl}\appsp B \appsp n = n
+\end{array}
+\]
+Here matching $\lccon{refl}$ tells the type checker that $t \defeq m$, and thus
+$\app{B}{t} \defeq \app{B}{m}$, so we can just return $n$. This shows the
+connection between type families indices and propositional equality, also
+highlighted in \citep{McBride2004}.
+
+It is worth noting that all $\lcfun{subst}$s, in ITT, are guaranteed to reduce
+at the top level. This is because $\lccon{refl}$ is the only constructor for
+propositional equality, and thus without false assumptions every top level proof
+will have that shape. Extending this idea to other types, in ITT, at the top
+level, expressions have \emph{canonical} values - a property known as
+\emph{canonicity}. We call canonical those values formed by constructors:
+$\lambda$, $(,)$, $\lhd$, etc. In other words a value is canonical if it's not
+something that is supposed to reduced (an eliminator) but is stuck on some
+variable.
+
+While propositional equality is a very useful construct, we can prove less terms
+equal than we would like to. For example, if we have the usual functions
+\[
+\begin{array}{l@{\ } l}
+\lcfun{id} & : \{A : \lcsetz\} \tyarr A \tyarr A \\
+\lcfun{map} & : \{A\ B : \lcsetz\} \tyarr (A \tyarr B) \tyarr \app{\lccon{List}}{A} \tyarr \app{\lccon{List}}{B}
+\end{array}
+\]
+we would certainly like to have a term of type
+\[\{A\ B : \lcsetz\} \tyarr
+\app{\lcfun{map}}{\lcfun{id}} =_{\lclist{A} \tyarr \lclist{B}} \lcfun{id}\]
+We cannot do this in ITT, since the things on the sides of $=$ look too
+different at the term level. What we can have is
+\[
+\{A\ B : \lcsetz\} \tyarr (x : \lclist{A}) \tyarr \app{\app{\lcfun{map}}{\lcfun{id}}}{x}
+=_{\lclist{B}} \app{\lcfun{id}}{x}
+\]
+Since the type checker has something to compute with (even if only a variable)
+and reduce the two lists to equal normal forms. The root of this problem is
+that \emph{function extensionality} does not hold:
+\[
+\begin{array}{l@{\ } l}
+\lcfun{ext} : & \{A\ B : \lcsetz\} \tyarr (f\ g : A \tyarr B) \tyarr \\
+ & ((x : A) \tyarr \app{f}{x} =_{A} \app{g}{x}) \tyarr f =_{A \tyarr B} g
+\end{array}
+\]
+Which is a long standing issue in ITT.
+
+\subsection{Extensional Type Theory and its problems}
+
+One way to `solve' the problem and gain extensionality is to allow the type
+checker to derive definitional equality from propositional equality, introducing
+what is known as the `equality reflection' rule:
+\begin{center}
+ \begin{prooftree}
+ \AxiomC{$\Gamma \vdash t =_A m$}
+ \UnaryInfC{$\Gamma \vdash t \defeq m$}
+ \end{prooftree}
+\end{center}
+This jump from types to a metatheoretic relation has deep consequences.
+Firstly, let's get extensionality out of the way. Given $\Gamma = \Gamma';
+\lcfun{eq} : (x : A) \tyarr \app{f}{x} = \app{g}{x}$, we have:
+\begin{center}
+ \begin{prooftree}
+ \AxiomC{$\Gamma; x : A \vdash \app{\lcfun{eq}}{x} : \app{f}{x} = \app{g}{x}$}
+ \RightLabel{(equality reflection)}
+ \UnaryInfC{$\Gamma; x : A \vdash \app{f}{x} \defeq \app{g}{x}$}
+ \RightLabel{(congruence for $\lambda$)}
+ \UnaryInfC{$\Gamma \vdash \abs{x : A}{\app{f}{x}} \defeq \abs{x : A}{\app{g}{x}}$}
+ \RightLabel{($\eta$-law)}
+ \UnaryInfC{$\Gamma \vdash f \defeq g$}
+ \RightLabel{($\lccon{refl}$)}
+ \UnaryInfC{$\Gamma \vdash f = g$}
+ \end{prooftree}
+\end{center}
+Since the above is possible, theories that include the equality reflection rule
+are often called `Extensional Type Theories', or ETTs. A notable exponent of
+this discipline is the NuPRL system \citep{NuPRL}. Moreover, equality
+reflection simplifies $\lcfun{subst}$-like operations, since if we have $t = m$
+and $\app{A}{t}$, then by equality reflection clearly $\app{A}{t} \defeq
+\app{A}{m}$.
+
+However equality reflection comes at a great price. The first hit is that it is
+now unsafe to compute under binders, since we can send the type checker into a
+loop given that under binders we can have any equality proof we might want
+(think about what happens with $\abs{x : \bot}{\dotsb}$), and thus we can
+convince the type checker that a term has any type we might want. Secondly,
+equality reflection is not syntax directed, thus the type checker would need to
+`invent' proofs of propositional equality to prove two terms definitionally
+equal, rendering the type checking process undecidable. Thus the type checker
+needs to carry complete derivations for each typing judgement, instead of
+relying on terms only.
+
+\subsection{Observational equality}
+
+\newcommand{\lcprop}{\lccon{Prop}}
+\newcommand{\lcdec}[1]{\llbracket #1 \rrbracket}
+\newcommand{\lcpropsyn}{\mathit{prop}}
+\newcommand{\lcpropf}[3]{\forall #1 : #2.\appsp #3}
+\newcommand{\lcparr}{\Rightarrow}
+
+A recent development by \citet{Altenkirch2007} promises to keep the well
+behavedness of ITT while being able to gain many useful equality proofs,
+including function extensionality. The main idea is to give the user the
+possibility to \emph{coerce} (or transport) values from a type $A$ to a type
+$B$, if the type checker can prove structurally that $A$ and $B$ are equal.
+
+This said, starting from a theory similar to the one presented in section
+\ref{sec:itt} but with only $\lcset{0}$ and without propositional equality, a
+propositional subuniverse of $\lcsetz$ is introduced, plus a `decoding' function
+$\lcdec{\_}$:
+
+\begin{center}
+ \axname{syntax}
+ $$
+ \begin{array}{rcl}
+ \termsyn & ::= & \dotsb \separ \lcprop \separ \lcdec{\lcpropsyn} \\
+ \lcpropsyn & ::= & \bot \separ \top \separ \lcpropsyn \wedge \lcpropsyn \separ \lcpropf{x}{\termsyn}{\lcpropsyn}
+ \end{array}
+ $$
+
+ \axname{typing}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c c}
+ \AxiomC{\phantom{1em}}
+ \UnaryInfC{$\Gamma \vdash \lcprop : \lcsetz$}
+ \noLine
+ \UnaryInfC{\phantom{1em}}
+ \DisplayProof
+ &
+ \AxiomC{\phantom{1em}}
+ \UnaryInfC{$\Gamma \vdash \bot : \lcprop$}
+ \noLine
+ \UnaryInfC{$\Gamma \vdash \top : \lcprop$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash P : \lcprop$}
+ \AxiomC{$\Gamma \vdash Q : \lcprop$}
+ \BinaryInfC{$\Gamma \vdash P \wedge Q : \lcprop$}
+ \noLine
+ \UnaryInfC{\phantom{1em}}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\Gamma \vdash S : \lcsetz$}
+ \AxiomC{$\Gamma \vdash Q : \lcprop$}
+ \BinaryInfC{$\Gamma \vdash \lcpropf{x}{S}{Q} : \lcprop$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash P : \lcprop$}
+ \UnaryInfC{$\Gamma \vdash \lcdec{P} : \lcsetz$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \axdesc{reduction}{\termsyn \bred \termsyn}
+ \begin{eqnarray*}
+ \lcdec{\bot} & \bred & \bot \\
+ \lcdec{\top} & \bred & \top \\
+ \lcdec{P \wedge Q} & \bred & \lcdec{P} \times \lcdec{Q} \\
+ \lcdec{\lcpropf{x}{S}{P}} & \bred & (x : S) \tyarr \lcdec{P}
+ \end{eqnarray*}
+\end{center}
+I will use $P \lcparr Q$ as an abbreviation for $\lcpropf{\_}{P}{Q}$. Note that
+$\lcprop$ has no `data', but only proofs. This has the consequence that code
+using proofs, when compiled, will be able to safely erase every $\lcprop$, as
+long as it doesn't compute under binder - and we most likely don't need to
+compute under binders after we type checked and we just need to run the code.
+Moreover, we can extend $\lcprop$ with other axioms while retaining canonicity,
+since
+
+\newcommand{\lccoe}[4]{\lcfun{coe}\appsp#1\appsp#2\appsp#3\appsp#4}
+\newcommand{\lccoh}[4]{\lcfun{coh}\appsp#1\appsp#2\appsp#3\appsp#4}
+
+Once we have $\lcprop$, we can define the operations that will let us form
+equalities and coerce between types and values:
+\begin{center}
+ \axname{typing}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\Gamma \vdash S : \lcsetz$}
+ \AxiomC{$\Gamma \vdash T : \lcsetz$}
+ \BinaryInfC{$\Gamma \vdash S = T : \lcprop$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash Q : \lcdec{S = T}$}
+ \AxiomC{$\Gamma \vdash s : S$}
+ \BinaryInfC{$\Gamma \vdash \lccoe{S}{T}{Q}{s} : T$}
+ \DisplayProof
+ \end{tabular}
+
+ \vspace{0.5cm}
+
+ \begin{tabular}{c c}
+ \AxiomC{$\Gamma \vdash s : S$}
+ \AxiomC{$\Gamma \vdash t : T$}
+ \BinaryInfC{$\Gamma \vdash (s : S) = (t : T) : \lcprop$}
+ \DisplayProof
+ &
+ \AxiomC{$\Gamma \vdash Q : \lcdec{S = T}$}
+ \AxiomC{$\Gamma \vdash s : S$}
+ \BinaryInfC{$\Gamma \vdash \lccoh{S}{T}{Q}{s} : \lcdec{(s : S) = (\lccoe{S}{T}{Q}{s})}$}
+ \DisplayProof
+ \end{tabular}
+\end{center}
+
+In the first row, $=$ forms equality between types, and $\lcfun{coe}$ (`coerce')
+transports values of equal types. On the second row, $=$ forms equality between
+values, and $\lcfun{coh}$ (`coherence') guarantees that all equalities are
+really between equal things. Now the tricky part is to define reduction rules
+to reduce the proofs of equality to something $\lcdec{\_}$ can reduce, so that
+proof of equality will exist only between equal things, and that $\lcfun{coe}$
+will compute only when those proofs are derivable.
+
+Let's start with type-level $=$:
+$$
+\begin{array}{r@{\ } c@{\ } l c l}
+ \bot & = & \bot & \bred & \top \\
+ \top & = & \top & \bred & \top \\
+ \lcbool & = & \lcbool & \bred & \top \\
+ (s : S) \times T & = & (s' : S') \times T' & \bred & S = S' \wedge \lcpropf{s}{S}{\lcpropf{s'}{S'}{(s : S) = (s' : S') \lcparr T[x] = T'[x']}} \\
+ (s : S) \tyarr T & = & (s' : S') \tyarr T' & \bred & S' = S \wedge \lcpropf{s'}{S'}{\lcpropf{s}{S}{(s' : S') = (s : S) \lcparr T[x] = T'[x']}} \\
+ \lcw{s}{S}{T} & = & \lcw{s'}{S'}{T'} & \bred & S = S' \wedge \lcpropf{s}{S}{\lcpropf{s'}{S'}{(s : S) = (s' : S') \lcparr T'[x'] = T[x]}} \\
+ S & = & T & \bred & \bot\ \text{for every other canonical sets $S$ and $T$}
+\end{array}
+$$
+The rule for $\times$ is unsurprising: it requires the left types to be equal,
+and the right types to be equal when the left values are equal. The rules for
+$\tyarr$ and $\lccon{W}$ are similar but with some twists to make the rules for
+$\lcfun{coe}$ simpler:
+$$
+\begin{array}{r@{} l@{} l@{} l c l}
+ \lccoe{&\bot}{&\bot}{&Q}{z} & \bred & z \\
+ \lccoe{&\top}{&\top}{&Q}{u} & \bred & u \\
+ \lccoe{&\lcbool}{&\lcbool}{&Q}{b} & \bred & b \\
+ \lccoe{&((x : S) \times T)}{&((x' : S') \times T')}{&Q}{(s, t)} & \bred & \\
+ \multicolumn{6}{l}{
+ \lcind
+ \begin{array}{l@{\ } l@{\ } c@{\ } l@{\ }}
+ \lcsyn{let} & Q_S & \mapsto & \lcfst Q : \lcdec{S = S'} \\
+ & s' & \mapsto & \lccoe{S}{S'}{Q}{s} : S' \\
+ & Q_T & \mapsto & \lcsnd Q \appsp s \appsp s' \appsp (\lccoh{S}{S'}{Q_S}{s}) : \lcdec{T[s] = T[s']} \\
+ & t' & \mapsto & \lccoe{T[t]}{T'[s']}{Q_T}{t} : T'[s'] \\
+ \multicolumn{4}{l}{\lcsyn{in}\ (s', t')}
+ \end{array}
+ }\\
+ \lccoe{&((x : S) \tyarr T)}{&((x' : S') \tyarr T')}{&Q}{f} & \bred & \dotsb \\
+ \lccoe{&(\lcw{x}{S}{T})}{&(\lcw{x'}{S'}{T'})}{&Q}{(s \lhd f)} & \bred & \dotsb \\
+ \lccoe{&S}{&T}{&Q}{x} & \bred & \lcabsurdd{T}{Q}
+\end{array}
+$$
+The rule for $\times$ is hairy but straightforward: we are given a $(s, t) : (x
+: S) \times T$ and, given the reduction rules specified before, a $$Q : \lcdec{S
+ = S'} \times ((s : S) \tyarr (s' : S') \tyarr \lcdec{(s : S) = (s' : S')}
+\tyarr \lcdec{T[x] = T'[x']})$$ We need to obtain a $(x' : S') \times T'$. We
+can easily get the left part with the left of $Q$ and a coercion, and the right
+with the help of $\lcfun{coh}$ and the right of $Q$. The rules for the other
+binders are similar but not reproduced here for brevity. The reader can refer
+to the paper for more details.
+
+Now we are left
+
+% TODO put the coind paper
+\section{What to do}
+
+My goal is to advance the practice of OTT. Conor McBride and other
+collaborators already implemented OTT and other measures as part of efforts
+towards a new version of Epigram\footnote{Available at
+ \url{http://www.e-pig.org/darcs/Pig09/web/}.}. However the development is
+stale right now and it is not clear when and if Epigram 2 will be released.
+
+The first thing that would be very useful to do is to have a small, core
+language that supports OTT, on which a more expressive language can be built.
+This follows an established tradition in functional programming and theorem
+proving of layering several languages of increasing complexity, so that type
+checking at a lower level is much simpler and those more prone to bugs. For
+example GHC Haskell uses an internal language, System F\textsubscript{C}
+\citep{Sulzmann2007}, which includes only minimal features compared to Haskell.
+
+I have already implemented a type theory as described in section
+\ref{sec:itt}\footnote{Available at \url{https://github.com/bitonic/mfixed}.} to
+make myself comfortable with how such systems work. From that, a good starting
+point to build something more useful could be $\Pi\Sigma$
+\citep{Altenkirch2007}, a core, partial language, thought to be a good target
+for high level languages like Agda, with facilities to implement inductive
+families and corecursion. Starting to think about how OTT would work in such a
+language is my immediate goal.
+
+If these attempts are successful, I can work towards understanding what a higher
+level language would look like and how it would be `elaborated' to the lower
+level core theory. Epigram 2 can certainly be an inspiration, although it
+employs a sophisticated reflection system \citep{Chapman2010} that I do not plan
+to implement. In any case, there are many things to do, with the most salients
+point being how to treat inductive families and pattern matching, corecursion,
+and what a friendly interface for OTT would be from the
+programmer/mathematician's perspective (or maybe whether it's feasible to always
+infer coercions and/or equality proofs automatically).
+
+Interestingly, the mentioned System F\textsubscript{C} was introduced in GHC to
+be able to implement GADTs, which as said in section
+\ref{sec:inductive-families} bear many similarities to inductive families. To
+do that it uses a system of coercions that is not too far away from OTT
+coercions. This is not a coincidence, since indices and propositional equality
+are often connected, and offers a lot of food for thought. For instance, GHC
+Haskell automatically generates and applies equality proofs, and the inference
+engine that serves this purpose is quite complex \citep{Vytiniotis2011} and
+often very confusing to the user; we would like to have a less `magic' but
+clearer system.
+
+\bibliographystyle{authordate1}
+\bibliography{InterimReport}
+
+\appendix
+\section{Agda code}
+\label{app:agda-code}
+
+\lstset{
+ xleftmargin=0pt
+}
+
+\lstinputlisting{InterimReport.agda}
+
+\end{document}
all: $(OBJECTS)
-background.pdf: background.tex background.bib background.agda
+InterimReport.pdf: InterimReport.tex InterimReport.bib InterimReport.agda
xelatex -halt-on-error $< -o $@
- bibtex background
+ bibtex InterimReport
xelatex -halt-on-error $< -o $@
xelatex -halt-on-error $< -o $@
+++ /dev/null
-* TODO [15/24] Papers
- - [X] “Observational Equality, Now!” OTT2.pdf
- - [X] “The Gentle Art of Levitation” conor-levitation.pdf
- Offers a nice metalanguage
- - [ ] “Dependently Typed Functional Programs and their Proofs” conor-thesis.pdf
- His PhD thesis, probably relevant
- - [ ] “Elaborating Inductive Definition” elaborating-inductive.pdf
- Don’t really knof what it’s about yet, probably interesting
- - [X] “Giving Haskell a Promotion” haskell-promotion.pdf
- Could cite it as related developement in the mainstream.
- - [X] “Implementing General Purpose Dependently Typed Programming Languages” idris-implementation.pdf
- - [ ] “Indexed Containers” indexed-containers.pdf
- Don’t really know what this is about yet, but is probably relevant
- - [X] “Local Type Inference” local-type-inference.pdf
- Will cite when talking about bidirectional type checking
- - [ ] “Unification Under a Mixed Prefix” miller-unification.pdf
- I think it’s needed to write Epigram/Agda style dep. pattern matching
- - [X] “OutsideIn(X)” outsidein.pdf
- Cite this as an example of how damn hard inference is...
- - [ ] “A tutorial implementation of dynamic pattern unification” pattern-unification.pdf
- - [X] “ΠΣ: Dependent Types without the Sugar” PiSigma.pdf
- - [X] “The Power of Pi” powerofpi.pdf
- - [ ] “Simply Easy!” simply-easy.pdf
- - [ ] “Dependently Typed Programming with Singletons” singleton-types.pdf
- As haskell-promotion.pdf, could cite it as related developement in the
- mainstream.
- - [X] “System F with Type Equality Coercions” systemf-coercions.pdf
- Same as haskell-promotion.pdf, but even better
- - [X] “Towards a practical programming language based on dependent type theory” ulf-thesis.pdf
- Agda
- - [X] “The View from the Left” view-from-the-left.ps.gz
- - [X] “Introduction to Generalised Type Systems” lambda-cube.pdf
- - [ ] “Computation and Reasoning: A Type Theory for Computer Science”
- I can’t find this one.
- - [X] “Intuitionistic Type Theory” martin-lof-tt.pdf
- - [ ] “Implicit Syntax” implicit-syntax.pdf
- - [X] “The Calculus of Constructions” coc.pdf
- - [X] “An Extended Calculus of Constructions” luo-thesis.ps
-
-* Outline
-** Simple and not-so-simple types
-*** The untyped lambda-calculus
-*** The STLC
-*** The Curry-Howard isomorphism
-** Intuitionistic Type Theory
-*** A Core Type Theory
-*** More than one equality
-*** Data
- A core type theory with 0, 1, 2, W
-*** Inductive families
-**** Dependent pattern matching
-*** Corecursion
-*** Quotient types
-** Observational Type Theory
-*** Extensionality is hard to get
- The “naive” extensionality and the problems with it
-*** A solution
-*** The problems with W
- See blog post
-** Things to do
-*** Usable, Observational TT implementation
- In the style of ΠΣ, Mini-TT
- Possible features:
- - Corecursion
- - Quotient types
- - Total or non-total?
-*** Inference for coercions
- Specifically, what to do when we express inductive families indices as
- equalities
-*** Eliminators based calculus
- In the style of ETT
+++ /dev/null
-module background where
-
-import Level
-
-module Core where
- data Exists (A : Set) (B : A -> Set) : Set where
- _,_ : (x : A) -> B x -> Exists A B
-
- fst : forall {A B} -> Exists A B -> A
- fst (x , _) = x
-
- snd : forall {A B} -> (s : Exists A B) -> B (fst s)
- snd (_ , x) = x
-
- data Bot : Set where
-
- absurd : {A : Set} -> Bot -> A
- absurd ()
-
- data Top : Set where
- <> : Top
-
- data Bool : Set where
- true : Bool
- false : Bool
-
- if_/_then_else_ : forall {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
-
- if_then_else_ : forall {a} {P : Bool -> Set a} ->
- (x : Bool) -> P true -> P false -> P x
- if true then x else _ = x
- if false then _ else y = y
-
- data W (A : Set) (B : A -> Set) : Set where
- _<!_ : (a : A) -> (B a -> W A B) -> W A B
-
- -- Ugh! Comments and definiton stolen from
- -- <http://www.e-pig.org/epilogue/?p=324>
- rec : forall {S P}
- (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))
-
- _\/_ : (A B : Set) -> Set
- A \/ B = Exists Bool (\ b -> if b then A else B)
-
- inl : forall {A B} -> A -> A \/ B
- inl x = true , x
-
- inr : forall {A B} -> B -> A \/ B
- inr x = false , x
-
- case : {A B C : Set} -> A \/ B -> (A -> C) -> (B -> C) -> C
- case {A} {B} {C} x f g =
- (if (fst x) / (\ b -> (if b then A else B) -> C) then f else g)
- (snd x)
-
- Tr : Bool -> Set
- Tr b = if b then Top else Bot
-
- Nat : Set
- Nat = W Bool Tr
-
- zero : Nat
- zero = false <! absurd
-
- suc : Nat -> Nat
- suc n = true <! \ _ -> n
-
- plus : Nat -> Nat -> Nat
- plus x y =
- rec (\ _ -> Nat)
- (\ b -> if b / (\ b -> (Tr b -> Nat) -> (Tr b -> Nat) -> Nat)
- then (\ _ f -> suc (f <>)) else (\ _ _ -> y)) x
-
- data _==_ {A : Set} : A -> A -> Set where
- refl : {x : A} -> x == x
-
- subst : forall {A x y} -> (x == y) -> (T : A -> Set) -> T x -> T y
- subst refl T t = t
-
- _/==_ : forall {A} -> A -> A -> Set
- x /== y = x == y -> Bot
-
-module Ext where
- data List (A : Set) : Set where
- nil : List A
- _::_ : A -> List A -> List A
-
- data Nat : Set where
- zero : Nat
- suc : Nat -> Nat
-
- data Vec (A : Set) : Nat -> Set where
- nil : Vec A zero
- _::_ : forall {n} -> A -> Vec A n -> Vec A (suc n)
-
- head : forall {A n} -> Vec A (suc n) -> A
- head (x :: _) = x
-
- data Fin : Nat -> Set where
- fzero : forall {n} -> Fin (suc n)
- fsuc : forall {n} -> Fin n -> Fin (suc n)
-
- _!!_ : forall {A n} -> Vec A n -> Fin n -> A
- (x :: _) !! fzero = x
- (x :: xs) !! fsuc i = xs !! i
-
- open Core using (_==_; refl; subst)
-
- id : {A : Set} -> A -> A
- id x = x
-
- map : forall {A B} -> (A -> B) -> List A -> List B
- map _ nil = nil
- map f (x :: xs) = f x :: map f xs
-
- cong : forall {A B} {x y : A} -> (f : A -> B) -> x == y -> f x == f y
- cong f refl = refl
-
- map-id==id : {A : Set} (xs : List A) -> map id xs == id xs
- map-id==id nil = refl
- map-id==id (x :: xs) = cong (_::_ x) (map-id==id xs)
-
- _#_ : forall {A B C : Set} -> (B -> C) -> (A -> B) -> (A -> C)
- f # g = \ x -> f (g x)
-
- map-#==#-map : forall {A B C} (f : B -> C) (g : A -> B) (xs : List A) ->
- map (f # g) xs == (map f # map g) xs
- map-#==#-map f g nil = refl
- map-#==#-map f g (x :: xs) = cong (_::_ (f (g x))) (map-#==#-map f g xs)
-
- -- If we could have this...
- postulate ext : forall {A B} {f g : A -> B} ->
- ((x : A) -> f x == g x) -> f == g
-
- map-id==id' : {A : Set} -> map {A} id == id
- map-id==id' = ext map-id==id
-
- map-#==#-map' : forall {A B C} (f : B -> C) (g : A -> B) ->
- map (f # g) == (map f # map g)
- map-#==#-map' f g = ext (map-#==#-map f g)
\ No newline at end of file
+++ /dev/null
-
-@inbook{Thompson1991,
- author = {Thompson, Simon},
- title = {Type Theory and Functional Programming},
- publisher = {Addison-Wesley},
- year = {1991}
-}
-
-@inbook{Pierce2002,
- author = {Pierce, Benjamin C.},
- title = {Types and Programming Languages},
- publisher = {The MIT Press},
- year = {2002}
-}
-
-@online{Coq,
- author = {{The Coq Team}},
- title = {The Coq Proof Assistant},
- url = {\url{coq.inria.fr}},
- howpublished = {\url{http://coq.inria.fr}},
- year = 2013
-}
-
-@online{GHC,
- author = {{The GHC Team}},
- title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.1},
- url = {http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/},
- howpublished = {\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}},
- year = 2012
-}
-
-@online{EpigramTut,
- author = {Conor McBride},
- title = {Epigram: Practical Programming with Dependent Types},
- url = {http://strictlypositive.org/epigram-notes.ps.gz},
- howpublished = {\url{http://strictlypositive.org/epigram-notes.ps.gz}},
- year = 2004
-}
-
-@online{Haskell2010,
- author = {Simon Marlow},
- title = {Haskell 2010, Language Report},
- url = {http://www.haskell.org/onlinereport/haskell2010/},
- howpublished = {\url{http://www.haskell.org/onlinereport/haskell2010/}},
- year = 2010
-}
-
-@online{LYAH,
- author = {Miran Lipova\v{c}a},
- title = {Learn You a Haskell for Great Good!},
- url = {http://learnyouahaskell.com/},
- howpublished = {\url{http://learnyouahaskell.com/}},
- year = 2009
-}
-
-@inbook{ProgInHask,
- author = {Graham Hutton},
- title = {Programming in Haskell},
- year = 2007,
- publisher = {Cambridge University Press}
-}
-
-
-@inbook{Constable86,
-author = {Constable, Robert L. and Stuart F. Allen and H. M. Bromley and W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and Scott F. Smith},
-title = {Implementing Mathematics with the NuPRL Proof Development System},
-year = {1986},
-publisher = {Prentice-Hall},
-address = {NJ}
-}
-
-
-@article{Altenkirch2010,
-author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas},
-file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf},
-journal = {Functional and Logic \ldots},
-number = {Sheard 2005},
-title = {{$\Pi$$\Sigma$: dependent types without the sugar}},
-url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
-year = {2010}
-}
-@article{Altenkirch2007,
-address = {New York, New York, USA},
-author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},
-doi = {10.1145/1292597.1292608},
-file = {:home/bitonic/docs/papers/OTT2.pdf:pdf},
-isbn = {9781595936776},
-journal = {Proceedings of the 2007 workshop on Programming languages meets program verification - PLPV '07},
-keywords = {case analysis relies on,datatypes are indexed in,equality,of any language where,ole in the programs,play a crucial internal,rˆ,solving,some way,type theory},
-pages = {57},
-publisher = {ACM Press},
-title = {{Observational equality, now!}},
-url = {http://portal.acm.org/citation.cfm?doid=1292597.1292608},
-year = {2007}
-}
-@article{Barendregt1991,
-author = {Barendregt, Henk},
-file = {:home/bitonic/docs/papers/lambda-cube.pdf:pdf},
-journal = {Journal of functional programming},
-title = {{Introduction to generalized type systems}},
-url = {http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf},
-year = {1991}
-}
-@article{Bove2009,
-author = {Bove, Ana and Dybjer, Peter and Norell, Ulf},
-file = {:home/bitonic/docs/papers/agda-overview.pdf:pdf},
-journal = {Theorem Proving in Higher Order Logics},
-title = {{A brief overview of Agda - a functional language with dependent types}},
-url = {http://www.springerlink.com/index/h12lq70470983732.pdf},
-year = {2009}
-}
-@article{Brady2012,
-author = {Brady, Edwin},
-file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
-journal = {Unpublished draft},
-number = {November},
-title = {{Implementing General Purpose Dependently Typed Programming Languages}},
-url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf},
-year = {2012}
-}
-@article{Chapman2010,
-address = {New York, New York, USA},
-author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
-doi = {10.1145/1863543.1863547},
-file = {:home/bitonic/docs/papers/conor-levitation.pdf:pdf},
-isbn = {9781605587943},
-journal = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming - ICFP '10},
-pages = {3},
-publisher = {ACM Press},
-title = {{The gentle art of levitation}},
-url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547},
-year = {2010}
-}
-@article{Church1936,
-author = {Church, Alonzo},
-file = {:home/bitonic/docs/papers/church-lc.pdf:pdf},
-journal = {American journal of mathematics},
-number = {2},
-pages = {345--363},
-title = {{An unsolvable problem of elementary number theory}},
-url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2371045},
-volume = {58},
-year = {1936}
-}
-@article{Church1940,
-author = {Church, Alonzo},
-file = {:home/bitonic/docs/papers/church-stlc.pdf:pdf},
-journal = {J. Symb. Log.},
-number = {2},
-pages = {56--68},
-title = {{A formulation of the simple theory of types}},
-url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2266170},
-volume = {5},
-year = {1940}
-}
-@article{Coquand1986,
-author = {Coquand, Thierry and Huet, Gerard},
-file = {:home/bitonic/docs/papers/coc.pdf:pdf},
-title = {{The calculus of constructions}},
-url = {http://hal.inria.fr/docs/00/07/60/24/PDF/RR-0530.pdf},
-year = {1986}
-}
-@article{Curry1934,
-author = {Curry, Haskell B.},
-file = {:home/bitonic/docs/papers/curry-stlc.pdf:pdf},
-journal = {Proceedings of the National Academy of Sciences of the United States of America},
-number = {1930},
-pages = {584--590},
-title = {{Functionality in combinatory logic}},
-url = {http://www.ncbi.nlm.nih.gov/pmc/articles/pmc1076489/},
-volume = {511},
-year = {1934}
-}
-@article{Dybjer1991,
-author = {Dybjer, Peter},
-file = {:home/bitonic/docs/papers/dybjer-inductive.ps:ps},
-journal = {Logical Frameworks},
-title = {{Inductive sets and families in Martin-L\"{o}f's type theory and their set-theoretic semantics}},
-url = {http://books.google.com/books?hl=en\&lr=\&id=X9wfWwslFQIC\&oi=fnd\&pg=PA280\&dq=Inductive+Sets+and+Families+in+Martin-L\%C3\%B6f\%27s+Type+Theory+and+Their+Set-Theoretic+Semantics\&ots=LewzM17GcW\&sig=vF4GgtlEBSf1uwRV1o\_unDtLats},
-year = {1991}
-}
-@article{Hurkens1995,
-author = {Hurkens, Antonius J.C.},
-file = {:home/bitonic/docs/papers/hurkens-paradox.pdf:pdf},
-journal = {Typed Lambda Calculi and Applications},
-title = {{A simplification of Girard's paradox}},
-url = {http://www.springerlink.com/index/W718604JN467672H.pdf},
-year = {1995}
-}
-@book{Martin-Lof1984,
-author = {Martin-L\"{o}f, Per},
-file = {:home/bitonic/docs/papers/martin-lof-tt.pdf:pdf},
-isbn = {8870881059},
-publisher = {Bibliopolis},
-title = {{Intuitionistic type theory}},
-year = {1984}
-}
-@article{McBride2004,
-author = {McBride, Conor},
-doi = {10.1017/S0956796803004829},
-file = {:home/bitonic/docs/papers/view-from-the-left.ps.gz:gz},
-journal = {Journal of Functional Programming},
-month = jan,
-number = {1},
-pages = {69--111},
-title = {{The View from The Left}},
-url = {http://strictlypositive.org/view.ps.gz},
-volume = {14},
-year = {2004}
-}
-@phdthesis{Norell2007,
-author = {Norell, Ulf},
-file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf},
-isbn = {9789172919969},
-school = {Chalmers University of Technology and G\"{o}teborg University},
-title = {{Towards a practical programming language based on dependent type theory}},
-url = {http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
-year = {2007}
-}
-@article{Oury2008,
-address = {New York, New York, USA},
-author = {Oury, Nicolas and Swierstra, Wouter},
-doi = {10.1145/1411204.1411213},
-file = {:home/bitonic/docs/papers/powerofpi.pdf:pdf},
-isbn = {9781595939197},
-journal = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08},
-pages = {39},
-publisher = {ACM Press},
-title = {{The power of Pi}},
-url = {http://portal.acm.org/citation.cfm?doid=1411204.1411213},
-year = {2008}
-}
-@article{Pierce2000,
-author = {Pierce, Benjamin C. and Turner, David N.},
-doi = {10.1145/345099.345100},
-file = {:home/bitonic/docs/papers/local-type-inference.pdf:pdf},
-issn = {01640925},
-journal = {ACM Transactions on Programming Languages and Systems},
-month = jan,
-number = {1},
-pages = {1--44},
-title = {{Local type inference}},
-url = {http://portal.acm.org/citation.cfm?doid=345099.345100},
-volume = {22},
-year = {2000}
-}
-@article{Pollack1990,
-author = {Pollack, Robert},
-file = {:home/bitonic/docs/papers/implicit-syntax.ps:ps},
-journal = {Informal Proceedings of First Workshop on Logical Frameworks},
-title = {{Implicit syntax}},
-url = {http://reference.kfupm.edu.sa/content/i/m/implicit\_syntax\_\_1183660.pdf},
-year = {1992}
-}
-@article{Reynolds1994,
-author = {Reynolds, John C.},
-file = {:home/bitonic/docs/papers/reynolds-polymorphic-lc.ps:ps},
-journal = {Logical Foundations of Functional Programming},
-title = {{An introduction to the polymorphic lambda calculus}},
-url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.9916\&rep=rep1\&type=pdf},
-year = {1994}
-}
-@article{Sulzmann2007,
-address = {New York, New York, USA},
-author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin},
-doi = {10.1145/1190315.1190324},
-file = {:home/bitonic/docs/papers/systemf-coercions.pdf:pdf},
-isbn = {159593393X},
-journal = {Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation - TLDI '07},
-pages = {53},
-publisher = {ACM Press},
-title = {{System F with type equality coercions}},
-url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
-year = {2007}
-}
-@article{Vytiniotis2011,
-author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
-file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
-journal = {Journal of Functional Programming},
-number = {4-5},
-pages = {333--412},
-title = {{OutsideIn (X) Modular type inference with local assumptions}},
-url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818},
-volume = {21},
-year = {2011}
-}
-@article{Yorgey2012,
-address = {New York, New York, USA},
-author = {Yorgey, Brent a. and Weirich, Stephanie and Cretin, Julien and {Peyton Jones}, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos\'{e} Pedro},
-doi = {10.1145/2103786.2103795},
-file = {:home/bitonic/docs/papers/haskell-promotion.pdf:pdf},
-isbn = {9781450311205},
-journal = {Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation - TLDI '12},
-pages = {53},
-publisher = {ACM Press},
-title = {{Giving Haskell a promotion}},
-url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
-year = {2012}
-}
+++ /dev/null
-\documentclass[article, a4paper]{article}
-\usepackage[T1]{fontenc}
-\usepackage{fixltx2e}
-\usepackage{enumitem}
-\usepackage[normalem]{ulem}
-\usepackage{graphicx}
-\usepackage{subcaption}
-
-% Unicode
-\usepackage{ucs}
-\usepackage[utf8x]{inputenc}
-% \usepackage{autofe}
-
-%% -----------------------------------------------------------------------------
-%% Fonts
-%% \usepackage[osf]{libertine}
-%% \usepackage{helvet}
-%% \usepackage{lmodern}
-%% \IfFileExists{microtype.sty}{\usepackage{microtype}}{}
-
-%% -----------------------------------------------------------------------------
-%% Diagrams
-% \usepackage{tikz}
-% \usetikzlibrary{positioning}
-%% \usetikzlibrary{shapes}
-%% \usetikzlibrary{arrows}
-%% \usepackage{tikz-cd}
-%% \usepackage{pgfplots}
-\usepackage[all]{xy}
-
-%% -----------------------------------------------------------------------------
-%% Symbols
-\usepackage[fleqn]{amsmath}
-\usepackage{amssymb}
-\usepackage{wasysym}
-\usepackage{turnstile}
-\usepackage{centernot}
-
-%% -----------------------------------------------------------------------------
-%% Utils
-\usepackage{bussproofs}
-\usepackage{umoline}
-\usepackage[export]{adjustbox}
-\usepackage{multicol}
-\usepackage{listingsutf8}
-\lstset{
- basicstyle=\small\ttfamily,
- extendedchars=\true,
- inputencoding=utf8x,
- xleftmargin=1cm
-}
-\usepackage{epigraph}
-
-%% -----------------------------------------------------------------------------
-%% Bibtex
-\usepackage{natbib}
-
-%% Numbering depth
-%% \setcounter{secnumdepth}{0}
-
-%% -----------------------------------------------------------------------------
-% We will generate all images so they have a width \maxwidth. This means
-% that they will get their normal width if they fit onto the page, but
-% are scaled down if they would overflow the margins.
-\makeatletter
-\def\maxwidth{
- \ifdim\Gin@nat@width>\linewidth\linewidth
- \else\Gin@nat@width\fi
-}
-\makeatother
-
-%% -----------------------------------------------------------------------------
-%% Links
-\usepackage[
- setpagesize=false, % page size defined by xetex
- unicode=false, % unicode breaks when used with xetex
- xetex
-]{hyperref}
-
-\hypersetup{
- breaklinks=true,
- bookmarks=true,
- pdfauthor={Francesco Mazzoli <fm2209@ic.ac.uk>},
- pdftitle={Observational Equality},
- colorlinks=false,
- pdfborder={0 0 0}
-}
-
-% Make links footnotes instead of hotlinks:
-% \renewcommand{\href}[2]{#2\footnote{\url{#1}}}
-
-% avoid problems with \sout in headers with hyperref:
-\pdfstringdefDisableCommands{\renewcommand{\sout}{}}
-
-\title{Observational Equality}
-\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
-\date{December 2012}
-
-\begin{document}
-
-\maketitle
-
-\setlength{\tabcolsep}{12pt}
-
-\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} I 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:practical} will describe additions common in practical programming
-languages based on ITT.
-
-Finally, I will explain why equality has been a tricky business in these
-theories, and talk about the various attempts have been made to make the
-situation better. One interesting development has recently emerged:
-Observational Type theory. I propose to explore the ways to turn these ideas
-into useful practices for programming and theorem proving.
-\end{abstract}
-
-\tableofcontents
-
-\section{Simple and not-so-simple types}
-\label{sec:types}
-
-\subsection{A note on notation}
-
-\newcommand{\appsp}{\hspace{0.07cm}}
-\newcommand{\app}[2]{#1\appsp#2}
-\newcommand{\absspace}{\hspace{0.03cm}}
-\newcommand{\abs}[2]{\lambda #1\absspace.\absspace#2}
-\newcommand{\termt}{t}
-\newcommand{\termm}{m}
-\newcommand{\termn}{n}
-\newcommand{\termp}{p}
-\newcommand{\termf}{f}
-\newcommand{\separ}{\ \ |\ \ }
-\newcommand{\termsyn}{\mathit{term}}
-\newcommand{\axname}[1]{\textbf{#1}}
-\newcommand{\axdesc}[2]{\axname{#1} \fbox{$#2$}}
-\newcommand{\lcsyn}[1]{\mathrm{\underline{#1}}}
-\newcommand{\lccon}[1]{\mathsf{#1}}
-\newcommand{\lcfun}[1]{\mathbf{#1}}
-\newcommand{\tyarr}{\to}
-\newcommand{\tysyn}{\mathit{type}}
-\newcommand{\ctxsyn}{\mathit{context}}
-\newcommand{\emptyctx}{\cdot}
-
-In the following sections I will introduce a lot of syntax, typing, and
-reduction rules, along with examples. To make the exposition clearer, usually
-the rules are preceded by what the rule looks like and what it shows (for
-example \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}).
-
-In the languages presented I will also use different fonts for different things:
-\begin{tabular}{c | l}
- $\lccon{Sans}$ & Sans serif, capitalised, for type constructors. \\
- $\lccon{sans}$ & Sans serif, not capitalised, for data constructors. \\
- $\lcsyn{roman}$ & Roman, underlined, for the syntax of the language. \\
- $\lcfun{roman}$ & Roman, bold, for defined functions and values. \\
- $math$ & Math mode font for quantified variables and syntax elements.
-\end{tabular}
-
-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
-Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
-
-\subsection{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.
-
-The syntax of $\lambda$-terms consists of just three things: variables,
-abstractions, and applications:
-
-\begin{center}
-\axname{syntax}
-$$
-\begin{array}{rcl}
- \termsyn & ::= & x \separ (\abs{x}{\termsyn}) \separ (\app{\termsyn}{\termsyn}) \\
- x & \in & \text{Some enumerable set of symbols, e.g.}\ \{x, y, z, \dots , x_1, x_2, \dots\}
-\end{array}
-$$
-\end{center}
-
-
-% I will omit parethesis in the usual manner. %TODO explain how
-
-I will use $\termt,\termm,\termn,\dots$ to indicate a generic term, and $x,y$
-for variables. I will also assume that all variable names in a term are unique
-to avoid problems with name capturing. Intuitively, abstractions
-($\abs{x}{\termt}$) introduce functions with a named parameter ($x$), and
-applications ($\app{\termt}{\termm}$) apply a function ($\termt$) to an argument
-($\termm$).
-
-The `applying' is more formally explained with a reduction rule:
-
-\newcommand{\bred}{\leadsto}
-\newcommand{\bredc}{\bred^*}
-
-\begin{center}
-\axdesc{reduction}{\termsyn \bred \termsyn}
-$$\app{(\abs{x}{\termt})}{\termm} \bred \termt[\termm / x]$$
-\end{center}
-
-Where $\termt[\termm / x]$ expresses the operation that substitutes all
-occurrences of $x$ with $\termm$ in $\termt$. In the future, I will use
-$[\termt]$ as an abbreviation for $[\termt / x]$. In the systems presented, the
-$\bred$ relation also includes reduction of subterms, for example if $\termt
-\bred \termm$ then $\app{\termt}{\termn} \bred \app{\termm}{\termn}$, and so on.
-
-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):
-\[
- \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}.
-
-\subsection{The simply typed $\lambda$-calculus}
-
-\newcommand{\tya}{A}
-\newcommand{\tyb}{B}
-\newcommand{\tyc}{C}
-
-One 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}.
-
-We wish to introduce rules of the form $\Gamma \vdash \termt : \tya$, which
-reads `in context $\Gamma$, term $\termt$ has type $\tya$'.
-
-The syntax for types is as follows:
-
-\begin{center}
- \axname{syntax}
- $$\tysyn ::= x \separ \tysyn \tyarr \tysyn$$
-\end{center}
-
-I will use $\tya,\tyb,\dots$ to indicate a generic type.
-
-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.}:
-\begin{center}
- \axname{syntax}
- $$\termsyn ::= x \separ (\abs{x : \tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$
-\end{center}
-Now we are ready to give the typing judgements:
-
-\begin{center}
- \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
-
- \vspace{0.5cm}
-
- \begin{tabular}{c c c}
- \AxiomC{\phantom{1em}}
- \UnaryInfC{$\Gamma; x : \tya \vdash x : \tya$}
- \DisplayProof
- &
- \AxiomC{$\Gamma; x : \tya \vdash \termt : \tyb$}
- \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \tya \tyarr \tyb$}
- \DisplayProof
- \end{tabular}
-
- \vspace{0.5cm}
-
- \begin{tabular}{c}
- \AxiomC{$\Gamma \vdash \termt : \tya \tyarr \tyb$}
- \AxiomC{$\Gamma \vdash \termm : \tya$}
- \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb$}
- \DisplayProof
- \end{tabular}
-\end{center}
-
-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 - either it is a value or it can
- take a step according to the evaluation rules. With `value' we mean a term
- whose subterms (including itself) don't appear to the left of the $\bred$
- relation.
-\item[Preservation] If a well-typed term takes a step of evaluation, then the
- resulting term is also well typed.
-\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*}
- \app{(\abs{x : ?}{\app{x}{x}})}{(\abs{x : ?}{\app{x}{x}})}
-\end{equation*}
-
-\newcommand{\lcfix}[2]{\lcsyn{fix} \appsp #1\absspace.\absspace #2}
-
-This makes the STLC Turing incomplete. We can recover the ability to loop by
-adding a combinator that recurses:
-$$
- \termsyn ::= \dotsb \separ \lcfix{x : \tysyn}{\termsyn}
-$$
-\begin{center}
- \begin{prooftree}
- \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
- \UnaryInfC{$\Gamma \vdash \lcfix{x : \tya}{\termt} : \tya$}
- \end{prooftree}
-\end{center}
-$$
- \lcfix{x : \tya}{\termt} \bred \termt[\lcfix{x : \tya}{\termt}]
-$$
-Which will deprive us of normalisation. There is however a price to pay, which
-will be made clear in the next section.
-
-\subsection{The Curry-Howard correspondence}
-\label{sec:curry-howard}
-
-\newcommand{\lcunit}{\lcfun{\langle\rangle}}
-
-It turns out that the STLC can be seen a natural deduction system for
-propositional logic. Terms are proofs, and their types are the propositions
-they prove. This remarkable fact is known as the Curry-Howard correspondence,
-or isomorphism.
-
-The `arrow' ($\to$) type corresponds to implication. If we wish to prove that
-$(\tya \tyarr \tyb) \tyarr (\tyb \tyarr \tyc) \tyarr (\tya \tyarr \tyc)$, all we
-need to do is to devise a $\lambda$-term that has the correct type:
-\begin{equation*}
- \abs{f : (\tya \tyarr \tyb)}{\abs{g : (\tyb \tyarr \tyc)}{\abs{x : \tya}{\app{g}{(\app{f}{x})}}}}
-\end{equation*}
-That is, function composition. We might want extend our bare lambda calculus
-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$).
-
-\newcommand{\lcinl}{\lccon{inl}\appsp}
-\newcommand{\lcinr}{\lccon{inr}\appsp}
-\newcommand{\lccase}[3]{\lcsyn{case}\appsp#1\appsp\lcsyn{of}\appsp#2\appsp#3}
-\newcommand{\lcfst}{\lcfun{fst}\appsp}
-\newcommand{\lcsnd}{\lcfun{snd}\appsp}
-\newcommand{\orint}{\vee I_{1,2}}
-\newcommand{\orintl}{\vee I_{1}}
-\newcommand{\orintr}{\vee I_{2}}
-\newcommand{\orel}{\vee E}
-\newcommand{\andint}{\wedge I}
-\newcommand{\andel}{\wedge E_{1,2}}
-\newcommand{\botel}{\bot E}
-\newcommand{\lcabsurd}{\lcfun{absurd}\appsp}
-\newcommand{\lcabsurdd}[1]{\lcfun{absurd}_{#1}\appsp}
-
-
-\begin{center}
- \axname{syntax}
- $$
- \begin{array}{rcl}
- \termsyn & ::= & \dotsb \\
- & | & \lcinl \termsyn \separ \lcinr \termsyn \separ \lccase{\termsyn}{\termsyn}{\termsyn} \\
- & | & (\termsyn , \termsyn) \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
- & | & \lcunit \\
- \tysyn & ::= & \dotsb \separ \tysyn \vee \tysyn \separ \tysyn \wedge \tysyn \separ \bot \separ \top
- \end{array}
- $$
-\end{center}
-\begin{center}
- \axdesc{typing}{\Gamma \vdash \termsyn : \tysyn}
- \begin{prooftree}
- \AxiomC{$\Gamma \vdash \termt : \tya$}
- \RightLabel{$\orint$}
- \UnaryInfC{$\Gamma \vdash \lcinl \termt : \tya \vee \tyb$}
- \noLine
- \UnaryInfC{$\Gamma \vdash \lcinr \termt : \tyb \vee \tya$}
- \end{prooftree}
- \begin{prooftree}
- \AxiomC{$\Gamma \vdash \termt : \tya \vee \tyb$}
- \AxiomC{$\Gamma \vdash \termm : \tya \tyarr \tyc$}
- \AxiomC{$\Gamma \vdash \termn : \tyb \tyarr \tyc$}
- \RightLabel{$\orel$}
- \TrinaryInfC{$\Gamma \vdash \lccase{\termt}{\termm}{\termn} : \tyc$}
- \end{prooftree}
-
- \begin{tabular}{c c}
- \AxiomC{$\Gamma \vdash \termt : \tya$}
- \AxiomC{$\Gamma \vdash \termm : \tyb$}
- \RightLabel{$\andint$}
- \BinaryInfC{$\Gamma \vdash (\tya , \tyb) : \tya \wedge \tyb$}
- \DisplayProof
- &
- \AxiomC{$\Gamma \vdash \termt : \tya \wedge \tyb$}
- \RightLabel{$\andel$}
- \UnaryInfC{$\Gamma \vdash \lcfst \termt : \tya$}
- \noLine
- \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb$}
- \DisplayProof
- \end{tabular}
-
- \vspace{0.5cm}
-
- \begin{tabular}{c c}
- \AxiomC{$\Gamma \vdash \termt : \bot$}
- \RightLabel{$\botel$}
- \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$}
- \DisplayProof
- &
- \AxiomC{}
- \RightLabel{$\top I$}
- \UnaryInfC{$\Gamma \vdash \lcunit : \top$}
- \DisplayProof
- \end{tabular}
-\end{center}
-\begin{center}
- \axdesc{reduction}{\termsyn \bred \termsyn}
- \begin{eqnarray*}
- \lccase{(\lcinl \termt)}{\termm}{\termn} & \bred & \app{\termm}{\termt} \\
- \lccase{(\lcinr \termt)}{\termm}{\termn} & \bred & \app{\termn}{\termt} \\
- \lcfst (\termt , \termm) & \bred & \termt \\
- \lcsnd (\termt , \termm) & \bred & \termm
- \end{eqnarray*}
-\end{center}
-
-With these rules, our STLC now looks remarkably similar in power and use to the
-natural deduction we already know. $\neg A$ can be expressed as $A \tyarr
-\bot$. However, there is an important omission: there is no term of the type $A
-\vee \neg A$ (excluded middle), or equivalently $\neg \neg A \tyarr A$ (double
-negation), or indeed any term with a type equivalent to those.
-
-This has a considerable effect on our logic and it's no coincidence, since there
-is no obvious computational behaviour for laws like the excluded middle.
-Theories of this kind are called \emph{intuitionistic}, or \emph{constructive},
-and all the systems analysed will have this characteristic since they build on
-the foundation of the STLC\footnote{There is research to give computational
- behaviour to classical logic, but I will not touch those subjects.}.
-
-Finally, going back to our $\lcsyn{fix}$ combinator, it's now easy to see how
-we would want to exclude such a thing if we want to use STLC as a logic, since
-it allows us to prove everything: $(\lcfix{x : \tya}{x}) : \tya$ clearly works
-for any $A$! This is a crucial point: in general we wish to have systems that
-do not let the user devise a term of type $\bot$, otherwise our logic will be
-unsound\footnote{Obviously such a term can be present under a $\lambda$.}.
-
-\subsection{Extending the STLC}
-
-\newcommand{\lctype}{\lccon{Type}}
-\newcommand{\lcite}[3]{\lcsyn{if}\appsp#1\appsp\lcsyn{then}\appsp#2\appsp\lcsyn{else}\appsp#3}
-\newcommand{\lcbool}{\lccon{Bool}}
-\newcommand{\lcforallz}[2]{\forall #1 \absspace.\absspace #2}
-\newcommand{\lcforall}[3]{(#1 : #2) \tyarr #3}
-\newcommand{\lcexists}[3]{(#1 : #2) \times #3}
-
-The STLC can be made more expressive in various ways. Henk Barendregt
-succinctly expressed geometrically how we can expand our type system:
-
-$$
-\xymatrix@!0@=1.5cm{
- & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
- & & \lambda C \ar@{-}[dd]
- \\
- \lambda2 \ar@{-}[ur]\ar@{-}[rr]\ar@{-}[dd]
- & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
- \\
- & \lambda\underline\omega \ar@{-}'[r][rr]
- & & \lambda P\underline\omega
- \\
- \lambda{\to} \ar@{-}[rr]\ar@{-}[ur]
- & & \lambda P \ar@{-}[ur]
-}
-$$
-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}$)] We can quantify over
- types in our type signatures: $(\abs{A : \lctype}{\abs{x : A}{x}}) :
- \lcforallz{A}{A \tyarr 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}}$)] We have
- type operators: $(\abs{A : \lctype}{\abs{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: $(\abs{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. 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'.
-
-\section{Intuitionistic Type Theory and dependent types}
-\label{sec:itt}
-
-\newcommand{\lcset}[1]{\lccon{Type}_{#1}}
-\newcommand{\lcsetz}{\lccon{Type}}
-\newcommand{\defeq}{\cong}
-
-\subsection{A Bit of History}
-
-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}.
-
-A related development is the polymorphic $\lambda$-calculus, and specifically
-the previously mentioned System F, which was developed independently by Girard
-and Reynolds. An overview can be found in \citep{Reynolds1994}. The surprising
-fact is that while System F is impredicative it is still consistent and strongly
-normalising. \cite{Coquand1986} further extended this line of work with the
-Calculus of Constructions (CoC).
-
-\subsection{A Core Type Theory}
-\label{sec:core-tt}
-
-The calculus I present follows the exposition in \citep{Thompson1991}, and is
-quite close to the original formulation of predicative ITT as found in
-\citep{Martin-Lof1984}.
-
-\begin{center}
- \axname{syntax}
- \begin{eqnarray*}
- \termsyn & ::= & x \\
- & | & \lcforall{x}{\termsyn}{\termsyn} \separ \abs{x : \termsyn}{\termsyn} \separ \app{\termsyn}{\termsyn} \\
- & | & \lcexists{x}{\termsyn}{\termsyn} \separ (\termsyn , \termsyn)_{x.\termsyn} \separ \lcfst \termsyn \separ \lcsnd \termsyn \\
- & | & \bot \separ \lcabsurd_{\termsyn} \termsyn \\
- & | & \lcset{n} \\
- n & \in & \mathbb{N}
- \end{eqnarray*}
-
- \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
-
- \vspace{0.5cm}
-
- \begin{tabular}{c c c}
- \AxiomC{\phantom{1em}}
- \UnaryInfC{$\Gamma;x : \tya \vdash x : \tya$}
- \DisplayProof
- &
- \AxiomC{$\Gamma \vdash \termt : \tya$}
- \AxiomC{$\tya \defeq \tyb$}
- \BinaryInfC{$\Gamma \vdash \termt : \tyb$}
- \DisplayProof
- &
- \AxiomC{$\Gamma \vdash \termt : \bot$}
- \UnaryInfC{$\Gamma \vdash \lcabsurdd{\tya} \termt : \tya$}
- \DisplayProof
- \end{tabular}
-
- \vspace{0.5cm}
-
- \begin{tabular}{c c}
- \AxiomC{$\Gamma;x : \tya \vdash \termt : \tya$}
- \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \lcforall{x}{\tya}{\tyb}$}
- \DisplayProof
- &
- \AxiomC{$\Gamma \vdash \termt : \lcforall{x}{\tya}{\tyb}$}
- \AxiomC{$\Gamma \vdash \termm : \tya$}
- \BinaryInfC{$\Gamma \vdash \app{\termt}{\termm} : \tyb[\termm ]$}
- \DisplayProof
- \end{tabular}
-
- \vspace{0.5cm}
-
- \begin{tabular}{c c}
- \AxiomC{$\Gamma \vdash \termt : \tya$}
- \AxiomC{$\Gamma \vdash \termm : \tyb[\termt ]$}
- \BinaryInfC{$\Gamma \vdash (\termt, \termm)_{x.\tyb} : \lcexists{x}{\tya}{\tyb}$}
- \noLine
- \UnaryInfC{$\phantom{1em}$}
- \DisplayProof
- &
- \AxiomC{$\Gamma \vdash \termt: \lcexists{x}{\tya}{\tyb}$}
- \UnaryInfC{$\hspace{0.7cm} \Gamma \vdash \lcfst \termt : \tya \hspace{0.7cm}$}
- \noLine
- \UnaryInfC{$\Gamma \vdash \lcsnd \termt : \tyb[\lcfst \termt ]$}
- \DisplayProof
- \end{tabular}
-
- \vspace{0.5cm}
-
- \begin{tabular}{c c}
- \AxiomC{$\phantom{1em}$}
- \UnaryInfC{$\Gamma \vdash \lcset{n} : \lcset{n + 1}$}
- \noLine
- \UnaryInfC{$\phantom{1em}$}
- \DisplayProof
- &
- \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
- \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
- \BinaryInfC{$\Gamma \vdash \lcforall{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
- \noLine
- \UnaryInfC{$\Gamma \vdash \lcexists{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
- \DisplayProof
- \end{tabular}
-
- \vspace{0.5cm}
-
- \axdesc{reduction}{\termsyn \bred \termsyn}
- \begin{eqnarray*}
- \app{(\abs{x}{\termt})}{\termm} & \bred & \termt[\termm ] \\
- \lcfst (\termt, \termm) & \bred & \termt \\
- \lcsnd (\termt, \termm) & \bred & \termm
- \end{eqnarray*}
-\end{center}
-
-When showing examples types will be omitted when this can be done without loss
-of clarity, for example $\abs{x}{x}$ in place of $\abs{A : \lcsetz}{\abs{x :
- A}{x}}$. I will also use $\lcsetz$ as $\lcset{0}$.
-
-There are a lot of new factors at play here. The first thing to notice is that
-the separation between types and terms is gone. All we have is terms, that
-include both values (terms of type $\lcset{0}$) and types (terms of type
-$\lcset{n}$, with $n > 0$). This change is reflected in the typing rules.
-While in the STLC values and types are kept well separated (values never go
-`right of the colon'), in ITT types can freely depend on values.
-
-This relation is expressed in the typing rules for $\tyarr$ and $\times$: if a
-function has type $\lcforall{x}{\tya}{\tyb}$, $\tyb$ can depend on $x$.
-Examples will make this clearer once some base types are added in section
-\ref{sec:base-types}.
-
-$\tyarr$ and $\times$ are at the core of the machinery of ITT:
-
-\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$.
-
-\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
- product'. Like $\wedge$, it is formed by providing a pair of things. In our
- logic, it represents existential quantification. Similarly to $\tyarr$, it is
- always written as $\exists x : \tya. \tyb$.
-
- For added confusion, in the literature that calls forall $\Pi$, $\exists$ 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.
-\end{description}
-
-Another thing to notice is that types are very `first class': we are free to
-create functions that accept and return types. For this reason we define
-$\defeq$ as the smallest equivalence relation extending $\bredc$, where $\bredc$
-is the reflexive transitive closure of $\bred$; and we treat types that are
-relate 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
-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
-$\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 :
- \lctype}{x})}{\lcbool} \defeq \lcbool$. The theme of equality is central
-and will be analysed better later.
-
-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$
-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 -
-we will see instances in section \ref{foo}
-% TODO put citation here
-
-Note that the Curry-Howard correspondence runs through ITT as it did with the
-STLC with the difference that ITT corresponds to an higher order propositional
-logic.
-
-\subsection{Base Types}
-\label{sec:base-types}
-
-\newcommand{\lctrue}{\lccon{true}}
-\newcommand{\lcfalse}{\lccon{false}}
-\newcommand{\lcw}[3]{\lccon{W} #1 : #2 \absspace.\absspace #3}
-\newcommand{\lcnode}[4]{#1 \lhd_{#2 . #3} #4}
-\newcommand{\lcnodez}[2]{#1 \lhd #2}
-\newcommand{\lcited}[5]{\lcsyn{if}\appsp#1/#2\appsp.\appsp#3\appsp\lcsyn{then}\appsp#4\appsp\lcsyn{else}\appsp#5}
-\newcommand{\lcrec}[4]{\lcsyn{rec}\appsp#1/#2\appsp.\appsp#3\appsp\lcsyn{with}\appsp#4}
-\newcommand{\lcrecz}[2]{\lcsyn{rec}\appsp#1\appsp\lcsyn{with}\appsp#2}
-\newcommand{\AxiomL}[1]{\Axiom$\fCenter #1$}
-\newcommand{\UnaryInfL}[1]{\UnaryInf$\fCenter #1$}
-
-While the ITT presented is a fairly complete logic, it is not that useful for
-programming. If we wish to make it better, we can add some base types to
-represent the data structures we know and love, such as numbers, lists, and
-trees. Apart from some unsurprising data types, we introduce $\lccon{W}$, a
-very general tree-like structure useful to represent inductively defined types
-and that will allow us to express structural recursion in an equally general
-manner.
-
-\begin{center}
- \axname{syntax}
- \begin{eqnarray*}
- \termsyn & ::= & \dots \\
- & | & \top \separ \lcunit \\
- & | & \lcbool \separ \lctrue \separ \lcfalse \separ \lcited{\termsyn}{x}{\termsyn}{\termsyn}{\termsyn} \\
- & | & \lcw{x}{\termsyn}{\termsyn} \separ \lcnode{\termsyn}{x}{\termsyn}{\termsyn} \separ \lcrec{\termsyn}{x}{\termsyn}{\termsyn}
- \end{eqnarray*}
-
- \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
-
- \vspace{0.5cm}
-
- \begin{tabular}{c c c}
- \AxiomC{}
- \UnaryInfC{$\hspace{0.2cm}\Gamma \vdash \top : \lcset{0} \hspace{0.2cm}$}
- \noLine
- \UnaryInfC{$\Gamma \vdash \lcbool : \lcset{0}$}
- \DisplayProof
- &
- \AxiomC{}
- \UnaryInfC{$\Gamma \vdash \lcunit : \top$}
- \noLine
- \UnaryInfC{\phantom{1em}}
- \DisplayProof
- &
- \AxiomC{}
- \UnaryInfC{$\Gamma \vdash \lctrue : \lcbool$}
- \noLine
- \UnaryInfC{$\Gamma \vdash \lcfalse : \lcbool$}
- \DisplayProof
- \end{tabular}
-
- \vspace{0.5cm}
-
- \begin{tabular}{c}
- \AxiomC{$\Gamma \vdash \termt : \lcbool$}
- \AxiomC{$\Gamma \vdash \termm : \tya[\lctrue]$}
- \AxiomC{$\Gamma \vdash \termn : \tya[\lcfalse]$}
- \TrinaryInfC{$\Gamma \vdash \lcited{\termt}{x}{\tya}{\termm}{\termn} : \tya[\termt]$}
- \DisplayProof
- \end{tabular}
-
- \vspace{0.5cm}
-
- \begin{tabular}{c}
- \AxiomC{$\Gamma \vdash \tya : \lcset{n}$}
- \AxiomC{$\Gamma; x : \tya \vdash \tyb : \lcset{m}$}
- \BinaryInfC{$\Gamma \vdash \lcw{x}{\tya}{\tyb} : \lcset{n \sqcup m}$}
- \DisplayProof
- \end{tabular}
-
- \vspace{0.5cm}
-
- \begin{tabular}{c}
- \AxiomC{$\Gamma \vdash \termt : \tya$}
- \AxiomC{$\Gamma \vdash \termf : \tyb[\termt ] \tyarr \lcw{x}{\tya}{\tyb}$}
- \BinaryInfC{$\Gamma \vdash \lcnode{\termt}{x}{\tyb}{\termf} : \lcw{x}{\tya}{\tyb}$}
- \DisplayProof
- \end{tabular}
-
- \vspace{0.5cm}
-
- \begin{tabular}{c}
- \AxiomC{$\Gamma \vdash \termt: \lcw{x}{\tya}{\tyb}$}
- \noLine
- \UnaryInfC{$\Gamma \vdash \lcforall{\termm}{\tya}{\lcforall{\termf}{\tyb[\termm] \tyarr \lcw{x}{\tya}{\tyb}}{(\lcforall{\termn}{\tyb[\termm]}{\tyc[\app{\termf}{\termn}]}) \tyarr \tyc[\lcnodez{\termm}{\termf}]}}$}
- \UnaryInfC{$\Gamma \vdash \lcrec{\termt}{x}{\tyc}{\termp} : \tyc[\termt]$}
- \DisplayProof
- \end{tabular}
-
- \vspace{0.5cm}
-
- \axdesc{reduction}{\termsyn \bred \termsyn}
- \begin{eqnarray*}
- \lcited{\lctrue}{x}{\tya}{\termt}{\termm} & \bred & \termt \\
- \lcited{\lcfalse}{x}{\tya}{\termt}{\termm} & \bred & \termm \\
- \lcrec{\lcnodez{\termt}{\termf}}{x}{\tya}{\termp} & \bred & \app{\app{\app{\termp}{\termt}}{\termf}}{(\abs{\termm}{\lcrec{\app{f}{\termm}}{x}{\tya}{\termp}})}
- \end{eqnarray*}
-\end{center}
-
-The introduction and elimination for $\top$ and $\lcbool$ are unsurprising.
-Note that in the $\lcite{\dotsb}{\dotsb}{\dotsb}$ construct the type of the
-branches are dependent on the value of the conditional.
-
-% TODO: explain better here
-
-The rules for $\lccon{W}$, on the other hand, are quite an eyesore. The idea
-behind $\lccon{W}$ types is to build up `trees' where the number of `children'
-of each node is dependent on the value in the node. This is captured by the
-$\lhd$ constructor, where the argument on the left is the value, and the
-argument on the right is a function that returns a child for each possible value
-of $\tyb[\text{node value}]$, if $\lcw{x}{\tya}{\tyb}$. The recursor
-$\lcrec{\termt}{x}{\tyc}{\termp}$ uses $p$ to inductively prove that
-$\tyc[\termt]$ holds.
-
-\subsection{Some examples}
-
-Now we can finally provide some meaningful examples. Apart from omitting types,
-I will also use some abbreviations:
-\begin{itemize}
- \item $\_\mathit{operator}\_$ to define infix operators
- \item $\abs{x\appsp y\appsp z : \tya}{\dotsb}$ to define multiple abstractions at the same
- time
-\end{itemize}
-
-\subsubsection{Sum types}
-
-We would like to recover our sum type, or disjunction, $\vee$. This is easily
-achieved with $\times$:
-\[
-\begin{array}{rcl}
- \_\vee\_ & = & \abs{\tya\appsp\tyb : \lcsetz}{\lcexists{x}{\lcbool}{\lcite{x}{\tya}{\tyb}}} \\
- \lcinl & = & \abs{x}{(\lctrue, x)} \\
- \lcinr & = & \abs{x}{(\lcfalse, x)} \\
- \lcfun{case} & = & \abs{x : \tya \vee \tyb}{\abs{f : \tya \tyarr \tyc}{\abs{g : \tyb \tyarr \tyc}{ \\
- & & \hspace{0.5cm} \app{(\lcited{\lcfst x}{b}{(\lcite{b}{A}{B}) \tyarr C}{f}{g})}{(\lcsnd x)}}}}
-\end{array}
-\]
-What is going on here? We are using $\exists$ with $\lcbool$ as a tag, so that
-we can choose between one of two types in the second element. In
-$\lcfun{case}$ we use $\lcite{\lcfst x}{\dotsb}{\dotsb}$ to discriminate on the
-tag, that is, the first element of $x : \tya \vee \tyb$. If the tag is true,
-then we know that the second element is of type $\tya$, and we will apply $f$.
-The same applies to the other branch, with $\tyb$ and $g$.
-
-\subsubsection{Naturals}
-
-Now it's time to showcase the power of $\lccon{W}$ types.
-\begin{eqnarray*}
- \lccon{Nat} & = & \lcw{b}{\lcbool}{\lcite{b}{\top}{\bot}} \\
- \lccon{zero} & = & \lcfalse \lhd \abs{z}{\lcabsurd z} \\
- \lccon{suc} & = & \abs{n}{(\lctrue \lhd \abs{\_}{n})} \\
- \lcfun{plus} & = & \abs{x\appsp y}{\lcrecz{x}{(\abs{b}{\lcite{b}{\abs{\_\appsp f}{\app{\lccon{suc}}{(\app{f}{\lcunit})}}}{\abs{\_\appsp\_}{y}}})}}
-\end{eqnarray*}
-Here we encode natural numbers through $\lccon{W}$ types. Each node contains a
-$\lcbool$. If the $\lcbool$ is $\lcfalse$, then there are no children, since we
-have a function $\bot \tyarr \lccon{Nat}$: this is our $0$. If it's $\lctrue$,
-we need one child only: the predecessor. We recurse giving $\lcsyn{rec}$ a
-function that handles the `base case' 0 when the $\lcbool$ is $\lctrue$, and the
-inductive case otherwise.
-
-We postpone more complex examples after the introduction of inductive families
-and pattern matching, since $\lccon{W}$ types get unwieldy very quickly.
-
-\subsection{Propositional Equality}
-\label{sec:propeq}
-
-We can finally introduce one of the central subjects of my project:
-propositional equality.
-
-\newcommand{\lceq}[3]{#2 =_{#1} #3}
-\newcommand{\lceqz}[2]{#1 = #2}
-\newcommand{\lcrefl}[2]{\lccon{refl}_{#1}\appsp #2}
-\newcommand{\lcsubst}[3]{\lcfun{subst}\appsp#1\appsp#2\appsp#3}
-
-\begin{center}
- \axname{syntax}
- \begin{eqnarray*}
- \termsyn & ::= & ... \\
- & | & \lceq{\termsyn}{\termsyn}{\termsyn} \separ \lcrefl{\termsyn}{\termsyn} \separ \lcsubst{\termsyn}{\termsyn}{\termsyn}
- \end{eqnarray*}
-
- \axdesc{typing}{\Gamma \vdash \termsyn : \termsyn}
-
- \vspace{0.5cm}
-
- \begin{tabular}{c c}
- \AxiomC{$\Gamma \vdash \termt : \tya$}
- \UnaryInfC{$\Gamma \vdash \lcrefl{\tya}{\termt} : \lceq{\tya}{\termt}{\termt}$}
- \DisplayProof
- &
- \AxiomC{$\Gamma \vdash \termp : \lceq{\tya}{\termt}{\termm}$}
- \AxiomC{$\Gamma \vdash \tyb : \tya \tyarr \lcsetz$}
- \AxiomC{$\Gamma \vdash \termn : \app{\tyb}{\termt}$}
- \TrinaryInfC{$\Gamma \vdash \lcsubst{\termp}{\tyb}{\termn} : \app{\tyb}{\termm}$}
- \DisplayProof
- \end{tabular}
-
- \vspace{0.5cm}
-
- \axdesc{reduction}{\termsyn \bred \termsyn}
- \begin{eqnarray*}
- \lcsubst{(\lcrefl{\tya}{\termt})}{\tyb}{\termm} \bred \termm
- \end{eqnarray*}
-\end{center}
-
-Propositional equality internalises equality as a type. The only way to
-introduce an equality proof is by reflexivity ($\lccon{refl}$). The eliminator
-is in the style of `Leibnitz's law' of equality: `equals can be substituted for
-equals' ($\lcfun{subst}$). The computation rule refers to the fact that every
-proof of equality will be a $\lccon{refl}$. We can use $\neg
-(\lceq{\tya}{x}{y})$ to express inequality.
-
-These elements conclude our presentation of a `core' type theory. For an
-extended example of a similar theory in use see Section 6.2 of
-\cite{Thompson1991}\footnote{Note that while I attempted to formalise the proof
- in Agda, I found a bug in the book! See the errata for details:
- \url{http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/errata.html}.}. The above
-language and examples have been codified in Agda\footnote{More on Agda in the
- next section.}, see appendix \ref{app:agda-code}.
-
-\section{A more useful language}
-\label{sec:practical}
-
-While our core type theory equipped with $\lccon{W}$ types is very usefully
-conceptually as a simple but complete language, things get messy very fast. In
-this section I will present the elements that are usually included in theorem
-provers or programming languages to make them usable by mathematicians or
-programmers.
-
-All the features presented are present in the second version of the Agda system
-\citep{Norell2007, Bove2009}. Agda follows a tradition of theorem provers based
-on ITT with inductive families and pattern matching. The closest relative of
-Agda, apart from previous versions, is Epigram \citep{McBride2004, EpigramTut}.
-Coq is another notable theorem prover based on the same concepts, and the first
-and most popular \citep{Coq}.
-
-The main difference between Coq and Agda/Epigram is that the former focuses on
-theorem proving, while the latter also want to be useful as functional
-programming languages, while still offering good tools to express
-mathematics\footnote{In fact, currently, Agda is used almost exclusively to
- express mathematics, rather than to program.}. This is reflected in a series
-of differences that I will not discuss here (most notably the absence of tactics
-but better support for pattern matching in Agda/Epigram). I will take the same
-approach as Agda/Epigram and will give a perspective focused on functional
-programming rather than theorem proving. Every feature will be presented as it
-is Agda.
-
-\subsection{Bidirectional type checking}
-
-Lastly, the theory I present is fully explicit in the sense that the user has to
-specify every type when forming abstractions, products, etc. This can be a
-great burden if one wants to use the theory directly. Complete inference is
-undecidable (which is hardly surprising considering the role that types play)
-but partial inference (also called `bidirectional type checking' in this
-context) in the style of \cite{Pierce2000} will have to be deployed in a
-practical system.
-
-\subsection{Inductive families}
-
-\newcommand{\lcdata}[1]{\lcsyn{data}\appsp #1}
-\newcommand{\lcdb}{\ |\ }
-\newcommand{\lcind}{\hspace{0.2cm}}
-\newcommand{\lcwhere}{\appsp \lcsyn{where}}
-\newcommand{\lclist}[1]{\app{\lccon{List}}{#1}}
-\newcommand{\lcnat}{\lccon{Nat}}
-\newcommand{\lcvec}[2]{\app{\app{\lccon{Vec}}{#1}}{#2}}
-
-Inductive families were first introduced by \cite{Dybjer1991}. For the reader
-familiar with the recent developments present in the GHC compiler for Haskell,
-inductive families will look similar to GADTs (Generalised Abstract Data Types)
-\citep[Section 7.4.7]{GHC}.
-Haskell style data types provide \emph{parametric polymorphism}, so that we can
-define types that range over type parameters:
-\begin{lstlisting}
-List a = Nil | Cons a (List a)
-\end{lstlisting}
-In this way we define the \texttt{List} type once while allowing elements to be
-of any type. In Haskell \texttt{List} will be a type constructor of kind
-\texttt{* -> *}, while \texttt{Nil :: List a} and \texttt{Cons :: a -> List a -> List a}\footnote{Note that the \texttt{a}s are implicitly quantified type variables}.
-
-Inductive families bring this concept one step further by allowing some of the
-parameters to be constrained by constructors. We call these `variable'
-parameters `indices'. For example we might define natural numbers
-\[
-\begin{array}{l}
-\lcdata{\lcnat} : \lcsetz \lcwhere \\
- \begin{array}{l@{\ }l}
- \lcind \lccon{zero} &: \lcnat \\
- \lcind \lccon{suc} &: \lcnat \tyarr \lcnat
- \end{array}
-\end{array}
-\]
-And then define a type for lists indexed by length:
-\[
-\begin{array}{l}
-\lcdata{\lccon{Vec}}\appsp (A : \lcsetz) : \lcnat \tyarr \lcsetz \lcwhere \\
- \begin{array}{l@{\ }l}
- \lcind \lccon{nil} &: \lcvec{A}{\lccon{zero}} \\
- \lcind \_::\_ &: \{n : \lccon{Nat}\} \tyarr A \tyarr \lcvec{A}{n} \tyarr \lcvec{A}{\app{(\lccon{suc}}{n})}
- \end{array}
-\end{array}
-\]
-Note that contrary to the Haskell ADT notation, with inductive families we
-explicitly list the types for the type and data constructors. In $\lccon{Vec}$,
-$A$ is a parameter (same across all constructors) while the $\lcnat$ is an
-index. In our syntax, in the $\lcsyn{data}$ declaration, things to the left of
-the colon are parameters, while on the right we can define the type of indices.
-Also note that the parameters' identifiers will be in scope across all
-constructors, while indices' won't.
-
-In this $\lccon{Vec}$ example, when we form a new list the length is
-$\lccon{zero}$. When we append a new element to an existing list of length $n$,
-the new list is of length $\app{\lccon{suc}}{n}$, that is, one more than the
-previous length. Also note that we are using the $\{n : \lcnat\} \tyarr \dotsb$
-syntax to indicate an argument that we will omit when using $\_::\_$. In the
-future I shall also omit the type of these implicit parameters, in line with how
-Agda works.
-
-Once we have $\lccon{Vec}$ we can do things much more safely than with normal
-lists. For example, we can define an $\lcfun{head}$ function that returns the
-first element of the list:
-\[
-\begin{array}{l}
-\lcfun{head} : \{A\ n\} \tyarr \lcvec{A}{(\app{\lccon{suc}}{n})} \tyarr A
-\end{array}
-\]
-Note that we will not be able to provide this function with a
-$\lcvec{A}{\lccon{zero}}$, since it needs an index which is a successor of some
-number.
-
-\newcommand{\lcfin}[1]{\app{\lccon{Fin}}{#1}}
-
-If we wish to index a $\lccon{Vec}$ safely, we can define an inductive family
-$\lcfin{n}$, which represents the family of numbers smaller than a given number
-$n$:
-\[
-\begin{array}{l}
- \lcdata{\lccon{Fin}} : \lcnat \tyarr \lcsetz \lcwhere \\
- \begin{array}{l@{\ }l}
- \lcind \lccon{fzero} &: \{n\} \tyarr \lcfin{(\app{\lccon{suc}}{n})} \\
- \lcind \lccon{fsuc} &: \{n\} \tyarr \lcfin{n} \tyarr \lcfin{(\app{\lccon{suc}}{n})}
- \end{array}
-\end{array}
-\]
-$\lccon{fzero}$ is smaller than any number apart from $\lccon{zero}$. Given
-the family of numbers smaller than $n$, we can produce the family of numbers
-smaller than $\app{\lccon{suc}}{n}$. Now we can define an `indexing' operation
-for our $\lccon{Vec}$:
-\[
-\begin{array}{l}
-\_\lcfun{!!}\_ : \{A\ n\} \tyarr \lcvec{A}{n} \tyarr \lcfin{n} \tyarr A
-\end{array}
-\]
-In this way we will be sure that the number provided as an index will be smaller
-than the length of the $\lccon{Vec}$ provided.
-
-\subsubsection{Computing with inductive families}
-
-I have carefully avoided to define the functions that I mentioned as example,
-since one question still is unanswered: `how do we work with inductive
-families'? The most basic approach is to work with eliminators, that can be
-automatically provided by the programming language for each data type defined.
-For example the induction principle on natural numbers will serve as an
-eliminator for $\lcnat$:
-\[
-\begin{array}{l@{\ } c@{\ } l}
- \lcfun{NatInd} & : & (A : \lcsetz) \tyarr \\
- & & A \tyarr (\lcnat \tyarr A \tyarr A) \tyarr \\
- & & \lcnat \tyarr A
-\end{array}
-\]
-
-That is, if we provide an $A$ (base case), and then given a number and an $A$ we
-give the next $A$ (inductive step), then an $A$ can be computed for every
-number. This can be expressed easily in Haskell:
-\begin{lstlisting}
-data Nat = Zero | Suc Nat
-natInd :: a -> (Nat -> a -> a) -> Nat -> a
-natInd z _ Zero = z
-natInd z f (Suc n) = f n (natInd z f n)
-\end{lstlisting}
-However, in a dependent setting, we can do better:
-\[
-\begin{array}{l@{\ } c@{\ } l}
- \lcfun{NatInd} & : & (P : \lcnat \tyarr \lcsetz) \tyarr \\
- & & \app{P}{\lccon{zero}} \tyarr ((n : \lcnat) \tyarr \app{P}{n} \tyarr \app{P}{(\app{\lccon{suc}}{n})}) \tyarr \\
- & & (n : \lcnat) \tyarr \app{P}{n}
-\end{array}
-\]
-This expresses the fact that the resulting type can be dependent on the number.
-In other words, we are proving that $P$ holds for all $n : \lcnat$.
-
-Naturally a reduction rule will be associated with each eliminator:
-$$
-\begin{array}{l c l}
-\app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{\lccon{zero}} & \bred & z \\
-\app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{(\app{\lccon{suc}}{n})} & \bred & \app{\app{f}{n}}{(\app{\app{\app{\app{\lcfun{NatInd}}{P}}{z}}{f}}{n})}
-\end{array}
-$$
-Which echoes the \texttt{natInd} function defined in Haskell. An extensive
-account on combinators and inductive families can be found in \cite{McBride2004}.
-
-\subsubsection{Pattern matching and guarded recursion}
-
-However, combinators are far more cumbersome to use than the techniques usually
-employed in functional programming: pattern matching and recursion.
-\emph{General} recursion cannot be added if we want to keep our theory free of
-$\bot$. The common solution to this problem is to allow recursive calls only if
-the arguments are structurally smaller than what the function received. Pattern
-matching on the other hand gains considerable power with inductive families,
-since when we match a constructor we are gaining information on the indices of
-the family. Thus matching constructors will enable us to restrict patterns of
-other arguments.
-
-Following this discipline defining $\lcfun{head}$ becomes easy:
-\[
-\begin{array}{l}
-\lcfun{head} : \{A\ n\} \tyarr \lcvec{A}{(\app{\lccon{suc}}{n})} \tyarr A \\
-\lcfun{head}\appsp(x :: \_) = x
-\end{array}
-\]
-We need no case for $\lccon{nil}$, since the type checker knows that the
-equation $n = \lccon{zero} = \app{\lccon{suc}}{n'}$ cannot be satisfied.
-
-More details on the implementations of inductive families can be found in
-\citep{McBride2004, Norell2007}.
-
-\subsection{Friendlier universes}
-
-Universes as presented in section \ref{sec:core-tt} are quite cumbersome to work
-with. Consider the example where we define an inductive family for booleans and
-then we want to define an `if then else' eliminator:
-\[
-\begin{array}{l}
-\lcdata{\lcbool} : \lcsetz \lcwhere \\
- \begin{array}{l@{\ }l}
- \lcind \lccon{true} &: \lcbool \\
- \lcind \lccon{false} &: \lcbool
- \end{array}\\
-\\
-\lcfun{ite} : \{A : \lcset{0}\} \tyarr \lcbool \tyarr A \tyarr A \tyarr A \\
-\lcfun{ite} \appsp \lccon{true} \appsp x \appsp \_ = x \\
-\lcfun{ite} \appsp \lccon{false} \appsp \_ \appsp x = x
-\end{array}
-\]
-
-What if we want to use $\lcfun{ite}$ with types, for example $\lcfun{ite} \appsp
-b \appsp \lcnat \appsp \lccon{Bool}$? Clearly $\lcnat$ is not of type
-$\lcset{0}$, so we'd have to redefine $\lcfun{ite}$ with exactly the same body,
-but different type signature. The problem is even more evident with type
-families: for example our $\lccon{List}$ can only contain values, and if we want
-to build lists of types we need to define another identical, but differently
-typed, family.
-
-One option is to have a \emph{cumulative} theory, where $\lcset{n} : \lcset{m}$
-iff $n < m$. Then we can have a sufficiently large level in our type signature
-and forget about it. Moreover, levels in this setting can be inferred
-mechanically \citep{Pollack1990}, and thus we might lift the burden of universes
-from the user. This is the approach taken by Epigram.
-
-Another more expressive (but currently more cumbersome) way is to expose
-universes more, giving the user a way to quantify them and to take the least
-upper bound of two levels. This is the approach taken by Agda, where for
-example we can define a level-polymorphic $\times$:
-\[
-\begin{array}{l}
-\lcdata{\_\times\_}\ \{a\ b : \lccon{Level}\}\ (A : \lcset{a})\ (B : A \tyarr \lcset{b}) : \lcset{a \sqcup b} \lcwhere \\
- \lcind \_ , \_ : (x : A) \tyarr \app{B}{x} \tyarr A \times \app{B}{x}
-\end{array}
-\]
-Levels can be made implicit as shown and can be almost always inferred.
-However, having to decorate each type signature with quantified levels adds
-quite a lot of noise. An inference algorithm that automatically quantifies and
-instantiates levels (much like Hindley-Milner for types) seems feasible, but
-currently not implemented anywhere.
-
-\subsection{Coinduction}
-
-One thing that the Haskell programmer will miss in ITT as presented is the
-possibility to work with infinite data. The classic example is the manipulation
-of infinite streams:
-\begin{lstlisting}
-zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
-
-fibs :: [Int]
-fibs = 0 : 1 : zipWith (+) fibs (tail fibs)
-\end{lstlisting}
-While we can clearly write useful programs of this kind, we need to be careful,
-since \texttt{length fibs}, for example, does not make much sense\footnote{Note
- that if instead of machine \texttt{Int}s we used naturals as defined
- previously, getting the length of an infinite list would a productive
- definition.}.
-
-In less informal terms, we need to distinguish between \emph{productive} and
-non-productive definitions. A productive definition is one for which pattern
-matching on data will never diverge, which is the case for \texttt{fibs} but
-not, for example, for \texttt{let x = x in x :: [Int]}. It is very desirable to
-recover \emph{only} the productive definition so that total programs working
-with infinite data can be written.
-
-This desire has lead to work on coindunction
-% TODO finish
-
-\section{Many equalities}
-
-\subsection{Revision, and function extensionality}
-
-\epigraph{\emph{Half of my time spent doing research involves thinking up clever
- schemes to avoid needing functional extensionality.}}{@larrytheliquid}
-
-Up to this point, I have introduced two equalities: \emph{definitional} equality
-($\defeq$) and \emph{propositional} equality ($=_{\tya}$).
-
-Definitional equality relates terms that the type checker identifies as equal.
-Our definition in section \ref{sec:core-tt} consisted of `reduce the two terms
-to their normal forms, then check if they are equal (up to $\alpha$-renaming)'.
-We can extend this definition in other ways so that more terms will be
-identified as equal. Common ones include doing $\eta$-expansion, which converts
-partial appications of functions, and congruence laws for $\lambda$:
-\begin{center}
- \begin{tabular}{c c c}
- \AxiomC{$\Gamma \vdash \termf : \tya \tyarr \tyb$}
- \UnaryInfC{$\Gamma \vdash \termf \defeq \abs{x}{\app{\termf}{x}}$}
- \DisplayProof
- &
- \AxiomC{$\Gamma; x : \tya \vdash \termf \defeq g$}
- \UnaryInfC{$\Gamma \vdash \abs{x}{\termf} \defeq \abs{x}{g}$}
- \DisplayProof
- \end{tabular}
-\end{center}
-Definitional equality is used in the type checking process, and this means that
-in dependently typed languages type checking and evaluation are intertwined,
-since we need to reduce types to normal forms to check if they are equal. It
-also means that we need be able to compute under binders, for example to
-determine that $\abs{x}{\app{(\abs{y}{y})}{\tya}} \defeq \abs{x}{\tya}$. This
-process goes on `under the hood' and is outside the control of the user.
-
-Propositional equality, on the other hand, is available to the user to reason
-about equality, internalising it as a type. As we have seen in section
-\ref{sec:propeq} propositional equality is introduced by reflexivity and
-eliminated with a `Leibnitz's law' style rule ($\lcfun{subst}$). Now that we
-have inductive families and dependent pattern matching we do not need hard coded
-rules to express this concepts\footnote{Here I use Agda notation, and thus I
- cannot redefine $=$ and use subscripts, so I am forced to use $\equiv$ with
- implicit types. After I will carry on using the old notation.}:
-\[
-\begin{array}{l}
- \lcdata{\lccon{\_\equiv\_}} : \{A : \lcsetz\} : A \tyarr A \tyarr \lcsetz \lcwhere \\
- \begin{array}{l@{\ }l}
- \lcind \lccon{refl} &: \{x : A\} \tyarr x \equiv x
- \end{array} \\
- \\
- \lcfun{subst} : \{A : \lcsetz\} \tyarr \{t\ m : A\} \tyarr t \equiv m \tyarr (B : A \tyarr \lcsetz) \tyarr \app{B}{t} \tyarr \app{B}{m} \\
- \lcfun{subst} \appsp \lccon{refl}\appsp B \appsp n = n
-\end{array}
-\]
-Here matching $\lccon{refl}$ tells the type checker that $t \defeq m$, and thus
-$\app{B}{t} \defeq \app{B}{m}$, so we can just return $n$.
-
-While propositional equality is a very useful construct, we can prove less terms
-equal than we would like to. For example, if we have the usual functions
-\[
-\begin{array}{l@{\ } l}
-\lcfun{id} & : \{A : \lcsetz\} \tyarr A \tyarr A \\
-\lcfun{map} & : \{A\ B : \lcsetz\} \tyarr (A \tyarr B) \tyarr \app{\lccon{List}}{A} \tyarr \app{\lccon{List}}{B}
-\end{array}
-\]
-we would certainly like to have a term of type
-\[\{A\ B : \lcsetz\} \tyarr
-\app{\lcfun{map}}{\lcfun{id}} =_{\lclist{A} \tyarr \lclist{B}} \lcfun{id}\]
-We cannot do this in ITT, since the things on the sides of $=$ look too
-different at the term level. What we can have is
-\[
-\{A\ B : \lcsetz\} \tyarr (x : \lclist{A}) \tyarr \app{\app{\lcfun{map}}{\lcfun{id}}}{x}
-=_{\lclist{B}} \app{\lcfun{id}}{x}
-\]
-Since the type checker has something to compute with (even if only a variable)
-and reduce the two lists to equal normal forms. The root of this problem is
-that \emph{function extensionality} does not hold:
-\[
-\begin{array}{l@{\ } l}
-\lcfun{ext} : & \{A\ B : \lcsetz\} \tyarr (f\ g : A \tyarr B) \tyarr \\
- & ((x : A) \tyarr \app{f}{x} =_{A} \app{g}{x}) \tyarr f =_{A \tyarr B} g
-\end{array}
-\]
-Which is a long standing issue in ITT.
-
-\subsection{Extensional Type Theory and its problems}
-
-One way to `solve' the problem and gain extensionality is to allow the type
-checker to derive definitional equality from propositional equality, introducing
-what is known as the `equality reflection' rule:
-\begin{center}
- \begin{prooftree}
- \AxiomC{$\Gamma \vdash t =_A m$}
- \UnaryInfC{$\Gamma \vdash t \defeq m$}
- \end{prooftree}
-\end{center}
-This jump from types to a metatheoretic relation has deep consequences. But
-firstly, let's get extensionality out of the way. Given $\Gamma = \lcfun{eq} :
-(x : A) \tyarr \app{f}{x} = \app{g}{x}$, we have:
-\begin{center}
- \begin{prooftree}
- \AxiomC{$\Gamma; x : A \vdash \app{\lcfun{eq}}{x} : \app{f}{x} = \app{g}{x}$}
- \RightLabel{(equality reflection)}
- \UnaryInfC{$\Gamma; x : A \vdash \app{f}{x} \defeq \app{g}{x}$}
- \RightLabel{(congruence for $\lambda$)}
- \UnaryInfC{$\Gamma \vdash \abs{x : A}{\app{f}{x}} \defeq \abs{x : A}{\app{g}{x}}$}
- \RightLabel{($\eta$-law)}
- \UnaryInfC{$\Gamma \vdash f \defeq g$}
- \RightLabel{($\lccon{refl}$)}
- \UnaryInfC{$\Gamma \vdash f = g$}
- \end{prooftree}
-\end{center}
-Since the above is possible, theories that include the equality reflection rule
-are often called `Extensional Type Theories', or ETTs. A notable exponent of
-this discipline is the NuPRL system \citep{Constable86}. Moreover, equality
-reflection simplifies $\lcfun{subst}$-like operations, since if we have $t = m$
-and $\app{A}{t}$, then by equality reflection clearly $\app{A}{t} \defeq
-\app{A}{m}$.
-
-However equality reflection comes at a great price. The first hit is that it is
-now unsafe to compute under binders, since we can send the type checker into a
-loop given that under binders we can have any equality proof we might want
-(think about what happens with $\abs{x : \bot}{\dotsb}$), and thus we can
-convince the type checker that a term has any type we might want. Secondly,
-equality reflection is not syntax directed, thus the type checker would need to
-`invent' proofs of propositional equality to prove two terms definitionally
-equal, rendering the type checking process undecidable. Thus the type checker
-needs to carry complete derivations for each typing judgement, instead of
-relying on terms only.
-
-\subsection{Observational equality}
-
-A recent development by \cite{Altenkirch2007} promises to keep the well
-behavedness of ITT while being able to gain many useful equality proofs,
-including function extensionality. Starting from a theory similar to the one
-presented in section \ref{sec:itt} but with only $\lcset{0}$, a propositional
-subuniverse of $\lcsetz$ is introduced, plus a `decoding' function:
-
-\newcommand{\lcprop}{\lccon{Prop}}
-
-\begin{center}
- \begin{tabular}{c c c}
- \AxiomC{\phantom{1em}}
- \UnaryInfC{$\Gamma \vdash \lcprop : \lcsetz$}
- \noLine
- \UnaryInfC{\phantom{1em}}
- \DisplayProof
- &
- \AxiomC{\phantom{1em}}
- \UnaryInfC{$\Gamma \vdash \bot : \lcprop$}
- \noLine
- \UnaryInfC{$\Gamma \vdash \top : \lcprop$}
- \DisplayProof
- &
- \AxiomC{$\Gamma \vdash P : \lcprop$}
- \AxiomC{$\Gamma \vdash Q : \lcprop$}
- \BinaryInfC{$\Gamma \vdash P \wedge Q : \lcprop$}
- \noLine
- \UnaryInfC{\phantom{1em}}
- \DisplayProof
- \end{tabular}
-
- \vspace{0.5cm}
-
- \begin{tabular}{c}
- \AxiomC{$\Gamma \vdash S : \lcsetz$}
- \AxiomC{$\Gamma \vdash q : \lcprop$}
- \BinaryInfC{$\Gamma \vdash p \wedge q : \lcprop$}
- \noLine
- \UnaryInfC{\phantom{1em}}
- \DisplayProof
- \end{tabular}
-\end{center}
-
-\section{What to do}
-
-
-\bibliographystyle{authordate1}
-\bibliography{background}
-
-\appendix
-\section{Agda code}
-\label{app:agda-code}
-
-\lstset{
- xleftmargin=0pt
-}
-
-\lstinputlisting{background.agda}
-
-\end{document}
projects / bitonic-mengthesis.git / commitdiff