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 \renewcommand{\AgdaField}{\AgdaFunction}
  19 \definecolor{AgdaBound} {HTML}{000000}
  20
  21 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
  22
  23 %% -----------------------------------------------------------------------------
  24 %% Commands
  25
  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}
  33
  34 %% -----------------------------------------------------------------------------
  35
  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>}}}
  39 \date{June 2013}
  40
  41 \begin{document}
  42
  43 \iffalse
  44 \begin{code}
  45 module thesis where
  46 open import Level
  47 \end{code}
  48 \fi
  49
  50 \maketitle
  51
  52 \begin{abstract}
  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.
  56
  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.
  67
  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
  71   principles described.
  72 \end{abstract}
  73
  74 \tableofcontents
  75
  76 \section{Simple and not-so-simple types}
  77 \label{sec:types}
  78
  79 \section{Intuitionistic Type Theory and dependent types}
  80 \label{sec:itt}
  81
  82 \section{The struggle for equality}
  83 \label{sec:equality}
  84
  85 \section{A more useful language}
  86 \label{sec:practical}
  87
  88 \section{Kant}
  89 \label{sec:kant}
  90
  91 \appendix
  92
  93 \section{Notation and syntax}
  94
  95 In the languages presented I will also use different fonts and colors for
  96 different things:
  97
  98 \begin{center}
  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.
 106   \end{tabular}
 107 \end{center}
 108
 109 \section{Agda rendition of a core ITT}
 110 \label{app:agda-code}
 111
 112 \begin{code}
 113 module ITT where
 114   data Empty : Set where
 115
 116   absurd : ∀ {a} {A : Set a} → Empty → A
 117   absurd ()
 118
 119   record Unit : Set where
 120     constructor tt
 121
 122   record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
 123     constructor _,_
 124     field
 125       fst : A
 126       snd : B fst
 127
 128   data Bool : Set where
 129     true false : Bool
 130
 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
 135
 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
 138
 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))
 148 \end{code}
 149
 150 \nocite{*}
 151 \bibliographystyle{authordate1}
 152 \bibliography{thesis}
 153
 154 \end{document}