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