blob: 4407487576d51c940dfba9fd9af1020d814001b2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
\documentclass[report]{article}
%% Narrow margins
\usepackage{fullpage}
%% Bibtex
\usepackage{natbib}
%% Links
\usepackage{hyperref}
%% -----------------------------------------------------------------------------
%% Commands for Agda
\usepackage[english]{babel}
\usepackage[conor]{agda}
\renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
\renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
\renewcommand{\AgdaField}{\AgdaFunction}
\definecolor{AgdaBound} {HTML}{000000}
\DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
%% -----------------------------------------------------------------------------
%% Commands
\newcommand{\mysyn}{\AgdaKeyword}
\newcommand{\mytyc}{\AgdaDatatype}
\newcommand{\myind}{\AgdaInductiveConstructor}
\newcommand{\myfld}{\AgdaField}
\newcommand{\myfun}{\AgdaFunction}
\newcommand{\myb}{\AgdaBound}
\newcommand{\myfield}{\AgdaField}
%% -----------------------------------------------------------------------------
\title{\textsc{Kant}: Implementing Observational Equality}
% TODO remove double @ if we get rid of lhs2TeX
\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
\date{June 2013}
\begin{document}
\iffalse
\begin{code}
module thesis where
open import Level
\end{code}
\fi
\maketitle
\begin{abstract}
The marriage between programming and logic has been a very fertile one. In
particular, since the simply typed lambda calculus (STLC), a number of type
systems have been devised with increasing expressive power.
Section \ref{sec:types} will give a very brief overview of STLC, and then
illustrate how it can be interpreted as a natural deduction system. Section
\ref{sec:itt} will introduce Inutitionistic Type Theory (ITT), which expands
on this concept, employing a more expressive logic. The exposition is quite
dense since there is a lot of material to cover; for a more complete treatment
of the material the reader can refer to \citep{Thompson1991, Pierce2002}.
Section \ref{sec:equality} will explain why equality has always been a tricky
business in these theories, and talk about the various attempts that have been
made to make the situation better. One interesting development has recently
emerged: Observational Type theory.
Section \ref{sec:practical} will describe common extensions found in the
systems currently in use. Finally, section \ref{sec:kant} will describe a
system developed by the author that implements a core calculus based on the
principles described.
\end{abstract}
\tableofcontents
\section{Simple and not-so-simple types}
\label{sec:types}
\section{Intuitionistic Type Theory and dependent types}
\label{sec:itt}
\section{The struggle for equality}
\label{sec:equality}
\section{A more useful language}
\label{sec:practical}
\section{Kant}
\label{sec:kant}
\appendix
\section{Notation and syntax}
In the languages presented I will also use different fonts and colors for
different things:
\begin{center}
\begin{tabular}{c | l}
$\mytyc{Sans}$ & Type constructors. \\
$\myind{sans}$ & Data constructors. \\
% $\myfld{sans}$ & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
$\mysyn{roman}$ & Syntax of the language. \\
$\myfun{roman}$ & Defined values. \\
$\myb{math}$ & Bound variables.
\end{tabular}
\end{center}
\section{Agda rendition of a core ITT}
\label{app:agda-code}
\begin{code}
module ITT where
data Empty : Set where
absurd : ∀ {a} {A : Set a} → Empty → A
absurd ()
record Unit : Set where
constructor tt
record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
constructor _,_
field
fst : A
snd : B fst
data Bool : Set where
true false : Bool
if_/_then_else_ : ∀ {a}
(x : Bool) → (P : Bool → Set a) → P true → P false → P x
if true / _ then x else _ = x
if false / _ then _ else x = x
data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
_◁_ : (s : S) → (P s → W S P) → W S P
rec : ∀ {a b} {S : Set a} {P : S → Set b}
(C : W S P → Set) → -- some conclusion we hope holds
((s : S) → -- given a shape...
(f : P s → W S P) → -- ...and a bunch of kids...
((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
C (s ◁ f)) → -- ...does C hold for the node?
(x : W S P) → -- If so, ...
C x -- ...C always holds.
rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
\end{code}
\nocite{*}
\bibliographystyle{authordate1}
\bibliography{thesis}
\end{document}
|
