1 \documentclass[report]{article}
4 % \usepackage{fullpage}
16 \usepackage[fleqn]{amsmath}
19 \usepackage{bussproofs}
21 %% -----------------------------------------------------------------------------
23 \usepackage[english]{babel}
24 \usepackage[conor]{agda}
25 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
26 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
27 \renewcommand{\AgdaField}{\AgdaFunction}
28 \definecolor{AgdaBound} {HTML}{000000}
30 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
32 %% -----------------------------------------------------------------------------
35 \newcommand{\mysyn}{\AgdaKeyword}
36 \newcommand{\mytyc}{\AgdaDatatype}
37 \newcommand{\mydc}{\AgdaInductiveConstructor}
38 \newcommand{\myfld}{\AgdaField}
39 \newcommand{\myfun}{\AgdaFunction}
40 % TODO make this use AgdaBount
41 \newcommand{\myb}[1]{\ensuremath{#1}}
42 \newcommand{\myfield}{\AgdaField}
43 \newcommand{\myind}{\AgdaIndent}
44 \newcommand{\mykant}{\textsc{Kant}}
45 \newcommand{\mysynel}[1]{\langle #1 \rangle}
46 \newcommand{\mytmsyn}{\mysynel{term}}
47 \newcommand{\mysp}{\ }
48 \newcommand{\myabs}[2]{\lambda #1 \mapsto #2}
49 \newcommand{\myappsp}{\hspace{0.07cm}}
50 \newcommand{\myapp}[2]{#1 \myappsp #2}
51 \newcommand{\mysynsep}{\ \ |\ \ }
54 \newcommand{\mydesc}[3]{
55 \hfill \textbf{#1} $#2$
62 % TODO is \mathbin the correct thing for arrow and times?
64 \newcommand{\mytmt}{\myb{T}}
65 \newcommand{\mytmm}{\myb{M}}
66 \newcommand{\mytmn}{\myb{N}}
67 \newcommand{\myred}{\leadsto}
68 \newcommand{\mysub}[3]{#1[#2 \mapsto #3]}
69 \newcommand{\mytysyn}{\mysynel{type}}
70 \newcommand{\mybasetys}{K}
71 % TODO change this name
72 \newcommand{\mybasety}[1]{B_{#1}}
73 \newcommand{\mytya}{\myb{A}}
74 \newcommand{\mytyb}{\myb{B}}
75 \newcommand{\myarr}{\mathbin{\textcolor{AgdaDatatype}{\to}}}
76 \newcommand{\myprod}{\mathbin{\textcolor{AgdaDatatype}{\times}}}
77 \newcommand{\myctx}{\Gamma}
78 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
79 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
80 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
81 \newcommand{\myabss}[3]{\lambda #1 {:} #2 \mapsto #3}
82 \newcommand{\mytt}{\mydc{tt}}
83 \newcommand{\myunit}{\mytyc{$\top$}}
84 \newcommand{\mypair}[2]{(#1\mathpunct{\textcolor{AgdaInductiveConstructor}{,}} #2)}
85 \newcommand{\myfst}[1]{\myapp{\myfld{fst}}{#1}}
86 \newcommand{\mysnd}[1]{\myapp{\myfld{snd}}{#1}}
87 \newcommand{\myconst}{\myb{c}}
88 \newcommand{\myemptyctx}{\cdot}
89 \newcommand{\myhole}{\AgdaUnsolvedMeta}
90 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
92 %% -----------------------------------------------------------------------------
94 \title{\mykant: Implementing Observational Equality}
95 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
110 The marriage between programming and logic has been a very fertile one. In
111 particular, since the simply typed lambda calculus (STLC), a number of type
112 systems have been devised with increasing expressive power.
114 Section \ref{sec:types} will give a very brief overview of STLC, and then
115 illustrate how it can be interpreted as a natural deduction system. Section
116 \ref{sec:itt} will introduce Inutitionistic Type Theory (ITT), which expands
117 on this concept, employing a more expressive logic. The exposition is quite
118 dense since there is a lot of material to cover; for a more complete treatment
119 of the material the reader can refer to \citep{Thompson1991, Pierce2002}.
120 Section \ref{sec:equality} will explain why equality has always been a tricky
121 business in these theories, and talk about the various attempts that have been
122 made to make the situation better. One interesting development has recently
123 emerged: Observational Type theory.
125 Section \ref{sec:practical} will describe common extensions found in the
126 systems currently in use. Finally, section \ref{sec:kant} will describe a
127 system developed by the author that implements a core calculus based on the
128 principles described.
133 \section{Simple and not-so-simple types}
136 \subsection{The untyped $\lambda$-calculus}
138 Along with Turing's machines, the earliest attempts to formalise computation
139 lead to the $\lambda$-calculus \citep{Church1936}. This early programming
140 language encodes computation with a minimal syntax and no `data' in the
141 traditional sense, but just functions. Here we give a brief overview of the
142 language, which will give the chance to introduce concepts central to the
143 analysis of all the following calculi. The exposition follows the one found in
144 chapter 5 of \cite{Queinnec2003}.
146 The syntax of $\lambda$-terms consists of three things: variables, abstractions,
151 \begin{array}{r@{\ }c@{\ }l}
152 \mytmsyn & ::= & \myb{x} \mysynsep \myabs{\myb{x}}{\mytmsyn} \mysynsep (\myapp{\mytmsyn}{\mytmsyn}) \\
153 x & \in & \text{Some enumerable set of symbols}
158 Through this text, I will use $\mytmt$, $\mytmm$, $\mytmn$ to indicate a generic
159 term, and $x$, $y$ to refer to variables. Parenthesis will be omitted in the
160 usual way: $\myapp{\myapp{\mytmt}{\mytmm}}{\mytmn} =
161 \myapp{(\myapp{\mytmt}{\mytmm})}{\mytmn}$.
163 Abstractions roughly corresponds to functions, and their semantics is more
164 formally explained by the $\beta$-reduction rule:
166 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
169 \myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{x}{\mytmn}\text{, where} \\
171 \begin{array}{l@{\ }c@{\ }l}
172 \mysub{x}{x}{\mytmn} & = & \mytmn \\
173 \mysub{y}{x}{\mytmn} & = & y\text{, with } x \neq y \\
174 \mysub{\myapp{\mytmt}{\mytmm}}{x}{\mytmn} & = & (\myapp{\mysub{\mytmt}{x}{\mytmn}}{\mysub{\mytmm}{x}{\mytmn}}) \\
175 \mysub{(\myabs{x}{\mytmm})}{x}{\mytmn} & = & \myabs{x}{\mytmm} \\
176 \mysub{(\myabs{y}{\mytmm})}{x}{\mytmn} & = & \myabs{z}{\mysub{\mysub{\mytmm}{y}{z}}{x}{\mytmn}}, \\
177 \multicolumn{3}{l}{\myind{1} \text{with $x \neq y$ and $z$ not free in $\myapp{\mytmm}{\mytmn}$}}
183 The care required during substituting variables for terms is required to avoid
186 These few elements are of remarkable expressiveness, and in fact Turing
187 complete. As a corollary, we must be able to devise a term that reduces forever
188 (`loops' in imperative terms):
190 (\myapp{\omega}{\omega}) \myred (\myapp{\omega}{\omega}) \myred \dots\text{, with $\omega = \myabs{x}{\myapp{x}{x}}$}
193 A \emph{redex} is a term that can be reduced. In the untyped $\lambda$-calculus
194 this will be the case for an application in which the first term is an
195 abstraction, but in general a term is reducible if it appears to the left of a
196 reduction rule. When a term contains no redex it's said to be in \emph{normal
197 form}. Given the observation above, not all terms reduce to a normal forms:
198 we call the ones that do \emph{normalising}, and the ones that don't
199 \emph{non-normalising}.
201 The reduction rule presented is not syntax directed, but \emph{evaluation
202 strategies} can be employed to reduce term systematically. Common evaluation
203 strategies include \emph{call by value} (or \emph{strict}), where arguments of
204 abstractions are reduced before being applied to the abstraction; and conversely
205 \emph{call by name} (or \emph{lazy}), where we reduce only when we need to do so
206 to proceed---in other words when we have an application where the function is
207 still not a $\lambda$. In both these reduction strategies we never reduce under
208 an abstraction: for this reason a weaker form of normalisation is used, where
209 both abstractions and normal forms are said to be in \emph{weak head normal
212 \subsection{The simply typed $\lambda$-calculus}
214 A convenient way to `discipline' $\lambda$-terms is to assign \emph{types} to
215 them, and then check that the terms that we are forming make sense given our
216 typing rules \citep{Curry1934}. The first most basic instance of this idea
217 takes the name of \emph{simply typed $\lambda$ calculus}.
219 Our types contain a set of \emph{type variables} $\Phi$, which might correspond
220 to some `primitive' types; and $\myarr$, the type former for `arrow' types, the
221 types of functions. The language is explicitly typed: when we bring a variable
222 into scope with an abstraction, we explicitly declare its type. $\mytya$,
223 $\mytyb$ will be used to refer to a generic type. Reduction is unchanged from
224 the untyped $\lambda$-calculus.
228 \begin{array}{r@{\ }c@{\ }l}
229 \mytmsyn & ::= & \myb{x} \mysynsep \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
230 (\myapp{\mytmsyn}{\mytmsyn}) \\
231 \mytysyn & ::= & \myb{\phi} \mysynsep \mytysyn \myarr \mytysyn \mysynsep \\
232 \myb{x} & \in & \text{Some enumerable set of symbols} \\
233 \myb{\phi} & \in & \Phi
238 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
241 \AxiomC{$\myctx(x) = A$}
242 \UnaryInfC{$\myjud{\myb{x}}{A}$}
245 \AxiomC{$\myjudd{\myctx;\myb{x} : A}{\mytmt}{\mytyb}$}
246 \UnaryInfC{$\myjud{\myabss{x}{A}{\mytmt}}{\mytyb}$}
249 \AxiomC{$\myjud{\mytmm}{\mytya \myarr \mytyb}$}
250 \AxiomC{$\myjud{\mytmn}{\mytya}$}
251 \BinaryInfC{$\myjud{\myapp{\mytmm}{\mytmn}}{\mytyb}$}
257 In the typing rules, a context $\myctx$ is used to store the types of bound
258 variables: $\myctx; \myb{x} : \mytya$ adds a variable to the context and
259 $\myctx(x)$ returns the type of the rightmost occurrence of $x$.
261 This typing system takes the name of `simply typed lambda calculus' (STLC), and
262 enjoys a number of properties. Two of them are expected in most type systems
265 \item[Progress] A well-typed term is not stuck---it is either a variable, or its
266 constructor does not appear on the left of the $\myred$ relation (currently
267 only $\lambda$), or it can take a step according to the evaluation rules.
268 \item[Preservation] If a well-typed term takes a step of evaluation, then the
269 resulting term is also well-typed, and preserves the previous type.
272 However, STLC buys us much more: every well-typed term is normalising. It is
273 easy to see that we can't fill the blanks if we want to give types to the
274 non-normalising term shown before:
276 \myapp{(\myabss{x}{\myhole{?}}{\myapp{x}{x}})}{(\myabss{x}{\myhole{?}}{\myapp{x}{x}})}
279 This makes the STLC Turing incomplete. We can recover the ability to loop by
280 adding a combinator that recurses:
282 % TODO make this more compact
285 $ \mytmsyn ::= \dotsb \mysynsep \myfix{x}{\mytysyn}{\mytmsyn} $
288 \mydesc{typing:}{ } {
289 \AxiomC{$\myjudd{\myctx; x : \mytya}{\mytmt}{\mytya}$}
290 \UnaryInfC{$\myjud{\myfix{x}{\mytya}{\mytmt}}{\mytya}$}
294 \mydesc{reduction:}{ }{
295 $ \myfix{x}{\mytya}{\mytmt} \myred \mysub{\mytmt}{x}{(\myfix{x}{\mytya}{\mytmt})}$
298 This will deprive us of normalisation, which is a particularly bad thing if we
299 want to use the STLC as described in the next section.
301 \subsection{The Curry-Howard correspondence}
304 we have a product (or pair, or tuple) type $\mytya \myprod \mytyb$ for each pair
305 of types $\mytya$ and $\mytyb$, and a function (or arrow) type $\mytya \myarr
306 \mytyb$ for each pair of types $\mytya$ and $\mytyb$. $\beta$-reduction is
307 unchanged, but we have added reduction rules for products. Products are not
308 essential, but they serve as a good example of a type former apart from the
313 \begin{array}{r@{\ }c@{\ }l}
314 \mytmsyn & ::= & \myb{x} \mysynsep \myconst \mysynsep
315 \myabss{\myb{x}}{\mytysyn}{\mytmsyn} \mysynsep
316 (\myapp{\mytmsyn}{\mytmsyn}) \\
317 & | & \mytt \mysynsep \mypair{\mytmsyn}{\mytmsyn} \mysynsep
318 \myfst{\mytmsyn} \mysynsep \mysnd{\mytmsyn} \\
319 \mytysyn & ::= & \mytysyn \myprod \mytysyn \mysynsep
320 \mytysyn \myarr \mytysyn \mysynsep
321 \mybasety{\myconst} \\
322 \myb{x} & \in & \text{Some enumerable set of symbols} \\
323 \myconst & \in & \text{Some set $C$ of constants} \\
328 \mydesc{reduction:}{\mytmsyn \myred \mytmsyn}{
331 $\myapp{(\myabs{\myb{x}}{\mytmm})}{\mytmn} \myred \mysub{\mytmm}{x}{\mytmn}$ &
333 \begin{array}{r@{\ }c@{\ }l}
334 \myapp{\myfst}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmm \\
335 \myapp{\mysnd}{\mypair{\mytmm}{\mytmn}} & \myred & \mytmn
342 % TODO write context rules
343 % \mydesc{validity:}{\myvalid{\myctx}}{
345 % \begin{tabular}{ccc}
347 % \UnaryInfC{$\myvalid{\myemptyctx}$}
350 % \AxiomC{$\mytmt : \mytya$}
351 % \UnaryInfC{$\myvalid{\myctx; x : \mytya
358 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
361 \AxiomC{$x : A \in \myctx$}
362 \UnaryInfC{$\myjud{x}{A}$}
370 \section{Intuitionistic Type Theory}
373 \section{The struggle for equality}
376 \section{Extending ITT}
377 \label{sec:practical}
384 \section{Notation and syntax}
386 Syntax, derivation rules, and reduction rules, are enclosed in frames describing
387 the type of relation being established and the syntactic elements appearing,
390 \mydesc{typing:}{\myjud{\mytmsyn}{\mytysyn}}{
391 Typing derivations here.
394 In the languages presented I will also use different fonts and colors for
398 \begin{tabular}{c | l}
399 $\mytyc{Sans}$ & Type constructors. \\
400 $\mydc{sans}$ & Data constructors. \\
401 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
402 $\mysyn{roman}$ & Syntax of the language. \\
403 $\myfun{roman}$ & Defined values. \\
404 $\myb{math}$ & Bound variables.
408 \section{Agda rendition of a core ITT}
409 \label{app:agda-code}
413 data Empty : Set where
415 absurd : ∀ {a} {A : Set a} → Empty → A
418 record Unit : Set where
421 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
427 data Bool : Set where
430 if_/_then_else_ : ∀ {a}
431 (x : Bool) → (P : Bool → Set a) → P true → P false → P x
432 if true / _ then x else _ = x
433 if false / _ then _ else x = x
435 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
436 _◁_ : (s : S) → (P s → W S P) → W S P
438 rec : ∀ {a b} {S : Set a} {P : S → Set b}
439 (C : W S P → Set) → -- some conclusion we hope holds
440 ((s : S) → -- given a shape...
441 (f : P s → W S P) → -- ...and a bunch of kids...
442 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
443 C (s ◁ f)) → -- ...does C hold for the node?
444 (x : W S P) → -- If so, ...
445 C x -- ...C always holds.
446 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
450 \bibliographystyle{authordate1}
451 \bibliography{thesis}