thesis.lagda

   1 \documentclass[report]{article}
   2
   3 %% Narrow margins
   4 \usepackage{fullpage}
   5
   6 %% Bibtex
   7 \usepackage{natbib}
   8
   9 %% Links
  10 \usepackage{hyperref}
  11
  12 %% -----------------------------------------------------------------------------
  13 %% Commands for Agda
  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}
  19
  20 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
  21
  22 %% -----------------------------------------------------------------------------
  23 %% Commands
  24
  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}
  32
  33 %% -----------------------------------------------------------------------------
  34
  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>}}}
  38 \date{June 2013}
  39
  40 \begin{document}
  41
  42 %if False
  43 \begin{code}
  44 module thesis where
  45 open import Level
  46 \end{code}
  47 %endif
  48
  49 \maketitle
  50
  51 \begin{abstract}
  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.
  55
  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.
  66
  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
  70   principles described.
  71 \end{abstract}
  72
  73 \tableofcontents
  74
  75 \section{Simple and not-so-simple types}
  76 \label{sec:types}
  77
  78 \section{Intuitionistic Type Theory and dependent types}
  79 \label{sec:itt}
  80
  81 \section{The struggle for equality}
  82 \label{sec:equality}
  83
  84 \section{A more useful language}
  85 \label{sec:practical}
  86
  87 \section{Kant}
  88 \label{sec:kant}
  89
  90 \appendix
  91
  92 \section{Notation and syntax}
  93
  94 In the languages presented I will also use different fonts and colors for
  95 different things:
  96
  97 \begin{center}
  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.
 105   \end{tabular}
 106 \end{center}
 107
 108 \section{Agda rendition of a core ITT}
 109 \label{app:agda-code}
 110
 111 \begin{code}
 112 module ITT where
 113   data Empty : Set where
 114
 115   absurd : ∀ {a} {A : Set a} → Empty → A
 116   absurd ()
 117
 118   record Unit : Set where
 119     constructor tt
 120
 121   record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
 122     constructor _,_
 123     field
 124       fst : A
 125       snd : B fst
 126   open _×_ public
 127
 128   data Bool : Set where
 129     true false : Bool
 130
 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
 134
 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
 137
 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))
 147 \end{code}
 148
 149 \nocite{*}
 150 \bibliographystyle{authordate1}
 151 \bibliography{thesis}
 152
 153 \end{document}