1 \documentclass[report]{article}
12 %% -----------------------------------------------------------------------------
14 \usepackage[english]{babel}
15 \usepackage[conor]{agda}
16 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
17 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
18 \renewcommand{\AgdaField}{\AgdaFunction}
19 \definecolor{AgdaBound} {HTML}{000000}
21 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
23 %% -----------------------------------------------------------------------------
26 \newcommand{\mysyn}{\AgdaKeyword}
27 \newcommand{\mytyc}{\AgdaDatatype}
28 \newcommand{\myind}{\AgdaInductiveConstructor}
29 \newcommand{\myfld}{\AgdaField}
30 \newcommand{\myfun}{\AgdaFunction}
31 \newcommand{\myb}{\AgdaBound}
32 \newcommand{\myfield}{\AgdaField}
34 %% -----------------------------------------------------------------------------
36 \title{\textsc{Kant}: Implementing Observational Equality}
37 % TODO remove double @ if we get rid of lhs2TeX
38 \author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
53 The marriage between programming and logic has been a very fertile one. In
54 particular, since the simply typed lambda calculus (STLC), a number of type
55 systems have been devised with increasing expressive power.
57 Section \ref{sec:types} will give a very brief overview of STLC, and then
58 illustrate how it can be interpreted as a natural deduction system. Section
59 \ref{sec:itt} will introduce Inutitionistic Type Theory (ITT), which expands
60 on this concept, employing a more expressive logic. The exposition is quite
61 dense since there is a lot of material to cover; for a more complete treatment
62 of the material the reader can refer to \citep{Thompson1991, Pierce2002}.
63 Section \ref{sec:equality} will explain why equality has always been a tricky
64 business in these theories, and talk about the various attempts that have been
65 made to make the situation better. One interesting development has recently
66 emerged: Observational Type theory.
68 Section \ref{sec:practical} will describe common extensions found in the
69 systems currently in use. Finally, section \ref{sec:kant} will describe a
70 system developed by the author that implements a core calculus based on the
76 \section{Simple and not-so-simple types}
79 \section{Intuitionistic Type Theory and dependent types}
82 \section{The struggle for equality}
85 \section{A more useful language}
93 \section{Notation and syntax}
95 In the languages presented I will also use different fonts and colors for
99 \begin{tabular}{c | l}
100 $\mytyc{Sans}$ & Type constructors. \\
101 $\myind{sans}$ & Data constructors. \\
102 % $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
103 $\mysyn{roman}$ & Syntax of the language. \\
104 $\myfun{roman}$ & Defined values. \\
105 $\myb{math}$ & Bound variables.
109 \section{Agda rendition of a core ITT}
110 \label{app:agda-code}
114 data Empty : Set where
116 absurd : ∀ {a} {A : Set a} → Empty → A
119 record Unit : Set where
122 record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
128 data Bool : Set where
131 if_/_then_else_ : ∀ {a}
132 (x : Bool) → (P : Bool → Set a) → P true → P false → P x
133 if true / _ then x else _ = x
134 if false / _ then _ else x = x
136 data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
137 _◁_ : (s : S) → (P s → W S P) → W S P
139 rec : ∀ {a b} {S : Set a} {P : S → Set b}
140 (C : W S P → Set) → -- some conclusion we hope holds
141 ((s : S) → -- given a shape...
142 (f : P s → W S P) → -- ...and a bunch of kids...
143 ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
144 C (s ◁ f)) → -- ...does C hold for the node?
145 (x : W S P) → -- If so, ...
146 C x -- ...C always holds.
147 rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
151 \bibliographystyle{authordate1}
152 \bibliography{thesis}