2 \usepackage[sc,slantedGreek]{mathpazo}
5 % Comment these out if you don't want a slide with just the
6 % part/section/subsection/subsubsection title:
7 \AtBeginPart{\frame{\partpage}}
8 \AtBeginSection{\frame{\sectionpage}}
9 \AtBeginSubsection{\frame{\subsectionpage}}
10 \AtBeginSubsubsection{\frame{\subsubsectionpage}}
11 \beamertemplatenavigationsymbolsempty
13 \usepackage{centernot}
16 \setlength{\parindent}{0pt}
17 \setlength{\parskip}{6pt plus 2pt minus 1pt}
18 \setlength{\emergencystretch}{3em} % prevent overfull lines
19 \setcounter{secnumdepth}{0}
21 \usepackage[english]{babel}
22 \usepackage[conor]{agda}
23 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
24 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
25 \renewcommand{\AgdaField}{\AgdaFunction}
26 % \definecolor{AgdaBound} {HTML}{000000}
27 \definecolor{AgdaHole} {HTML} {FFFF33}
29 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
30 \DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
31 \DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
32 \DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
33 \DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
34 \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
36 \newcommand{\mysmall}{}
37 \newcommand{\mysyn}{\AgdaKeyword}
38 \newcommand{\mytyc}[1]{\textup{\AgdaDatatype{#1}}}
39 \newcommand{\mydc}[1]{\textup{\AgdaInductiveConstructor{#1}}}
40 \newcommand{\myfld}[1]{\textup{\AgdaField{#1}}}
41 \newcommand{\myfun}[1]{\textup{\AgdaFunction{#1}}}
42 \newcommand{\myb}[1]{\AgdaBound{$#1$}}
43 \newcommand{\myfield}{\AgdaField}
44 \newcommand{\myind}{\AgdaIndent}
45 \newcommand{\mykant}{{\rmfamily\scshape Bertus}}
46 \newcommand{\mysynel}[1]{#1}
47 \newcommand{\myse}{\mysynel}
48 \newcommand{\mytmsyn}{\langle t \rangle}
49 \newcommand{\mysp}{\ }
50 \newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
51 \newcommand{\myappsp}{\hspace{0.07cm}}
52 \newcommand{\myapp}[2]{#1 \myappsp #2}
53 \newcommand{\mysynsep}{\ \ |\ \ }
54 \newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
55 \newcommand{\mycumul}{\preceq}
57 \newcommand{\mydesc}[3]{
63 \hfill \textup{\phantom{ygp}\textbf{#1}} $#2$
64 \framebox[\textwidth]{
79 \newcommand{\mytmt}{\mysynel{t}}
80 \newcommand{\mytmm}{\mysynel{m}}
81 \newcommand{\mytmn}{\mysynel{n}}
82 \newcommand{\myred}{\leadsto}
83 \newcommand{\myredd}{\stackrel{*}{\leadsto}}
84 \newcommand{\myreddd}{\stackrel{*}{\reflectbox{$\leadsto$}}}
85 \newcommand{\mysub}[3]{#1[#3 / #2]}
86 \newcommand{\mytysyn}{\langle ty \rangle}
87 \newcommand{\mybasetys}{K}
88 \newcommand{\mybasety}[1]{B_{#1}}
89 \newcommand{\mytya}{\myse{A}}
90 \newcommand{\mytyb}{\myse{B}}
91 \newcommand{\mytycc}{\myse{C}}
92 \newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
93 \newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
94 \newcommand{\myctx}{\Gamma}
95 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
96 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
97 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
98 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
99 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
100 \newcommand{\myunit}{\mytyc{Unit}}
101 \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
102 \newcommand{\myfst}{\myfld{fst}}
103 \newcommand{\mysnd}{\myfld{snd}}
104 \newcommand{\myconst}{\myse{c}}
105 \newcommand{\myemptyctx}{\varepsilon}
106 \newcommand{\myhole}{\AgdaHole}
107 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
108 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
109 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
110 \newcommand{\myright}[1]{\mydc{right}_{#1}}
111 \newcommand{\myempty}{\mytyc{Empty}}
112 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
113 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
114 \newcommand{\myarg}{\_}
115 \newcommand{\myderivsp}{}
116 \newcommand{\myderivspp}{\vspace{0.3cm}}
117 \newcommand{\mytyp}{\mytyc{Type}}
118 \newcommand{\myneg}{\myfun{$\neg$}}
119 \newcommand{\myar}{\,}
120 \newcommand{\mybool}{\mytyc{Bool}}
121 \newcommand{\mytrue}{\mydc{true}}
122 \newcommand{\myfalse}{\mydc{false}}
123 \newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
124 \newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
125 \newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
126 \newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
127 \newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
128 \newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
129 \newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
130 \newcommand{\mynil}{\mydc{[]}}
131 \newcommand{\mycons}{\mathbin{\mydc{∷}}}
132 \newcommand{\myfoldr}{\myfun{foldr}}
133 \newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
134 \newcommand{\mynodee}{\mathbin{\mydc{$\lhd$}}}
135 \newcommand{\mynode}[2]{\mynodee_{#1.#2}}
136 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
137 \newcommand{\mylub}{\sqcup}
138 \newcommand{\mydefeq}{\cong}
139 \newcommand{\myrefl}{\mydc{refl}}
140 \newcommand{\mypeq}{\mytyc{=}}
141 \newcommand{\myjeqq}{\myfun{$=$-elim}}
142 \newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
143 \newcommand{\mysubst}{\myfun{subst}}
144 \newcommand{\myprsyn}{\myse{prop}}
145 \newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathclose{\mytyc{$\rrbracket$}}}
146 \newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
147 \newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
148 \newcommand{\myprfora}[3]{\forall #1 {:} #2.\, #3}
149 \newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
150 \newcommand{\mybot}{\mytyc{$\bot$}}
151 \newcommand{\mytop}{\mytyc{$\top$}}
152 \newcommand{\mycoe}{\myfun{coe}}
153 \newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
154 \newcommand{\mycoh}{\myfun{coh}}
155 \newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
156 \newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
157 \newcommand{\myeq}{\mathrel{\mytyc{=}}}
158 \newcommand{\myprop}{\mytyc{Prop}}
159 \newcommand{\mytmup}{\mytmsyn\uparrow}
160 \newcommand{\mydefs}{\Delta}
161 \newcommand{\mynf}{\Downarrow}
162 \newcommand{\myinff}[3]{#1 \vdash #2 \Uparrow #3}
163 \newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
164 \newcommand{\mychkk}[3]{#1 \vdash #2 \Downarrow #3}
165 \newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
166 \newcommand{\myann}[2]{#1 : #2}
167 \newcommand{\mydeclsyn}{\myse{decl}}
168 \newcommand{\myval}[3]{#1 : #2 \mapsto #3}
169 \newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2}
170 \newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
171 \newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
172 \newcommand{\myelabt}{\vdash}
173 \newcommand{\myelabf}{\rhd}
174 \newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
175 \newcommand{\mytele}{\Delta}
176 \newcommand{\mytelee}{\delta}
177 \newcommand{\mydcctx}{\Gamma}
178 \newcommand{\mynamesyn}{\myse{name}}
179 \newcommand{\myvec}{\overrightarrow}
180 \newcommand{\mymeta}{\textsc}
181 \newcommand{\myhyps}{\mymeta{hyps}}
182 \newcommand{\mycc}{;}
183 \newcommand{\myemptytele}{\varepsilon}
184 \newcommand{\mymetagoes}{\Longrightarrow}
185 % \newcommand{\mytesctx}{\
186 \newcommand{\mytelesyn}{\myse{telescope}}
187 \newcommand{\myrecs}{\mymeta{recs}}
188 \newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
189 \newcommand{\mylet}{\mysyn{let}}
190 \newcommand{\myhead}{\mymeta{head}}
191 \newcommand{\mytake}{\mymeta{take}}
192 \newcommand{\myix}{\mymeta{ix}}
193 \newcommand{\myapply}{\mymeta{apply}}
194 \newcommand{\mydataty}{\mymeta{datatype}}
195 \newcommand{\myisreco}{\mymeta{record}}
196 \newcommand{\mydcsep}{\ |\ }
197 \newcommand{\mytree}{\mytyc{Tree}}
198 \newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
199 \newcommand{\mysigma}{\mytyc{$\Sigma$}}
200 \newcommand{\mynegder}{\vspace{-0.3cm}}
201 \newcommand{\myquot}{\Uparrow}
202 \newcommand{\mynquot}{\, \Downarrow}
203 \newcommand{\mycanquot}{\ensuremath{\textsc{quote}{\Downarrow}}}
204 \newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Uparrow}}}
205 \newcommand{\mymetaguard}{\ |\ }
206 \newcommand{\mybox}{\Box}
207 \newcommand{\mytermi}[1]{\text{\texttt{#1}}}
208 \newcommand{\mysee}[1]{\langle\myse{#1}\rangle}
209 \newcommand{\mycomp}{\mathbin{\myfun{$\circ$}}}
210 \newcommand{\mylist}[1]{\mytyc{List}\myappsp #1}
211 \newcommand{\mylistt}[1]{\mathopen{\mydc{$[$}} #1 \mathclose{\mydc{$]$}}}
212 \newcommand{\myplus}{\mathbin{\myfun{$+$}}}
213 \newcommand{\mytimes}{\mathbin{\myfun{$*$}}}
214 \newcommand{\mysuc}{\mydc{suc}}
215 \newcommand{\myzero}{\mydc{zero}}
217 \renewcommand{\[}{\begin{equation*}}
218 \renewcommand{\]}{\end{equation*}}
219 \newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}}
221 \title{\mykant: Implementing Observational Equality}
222 \author{Francesco Mazzoli \texttt{<fm2209@ic.ac.uk>}}
229 \frametitle{\mykant?}
231 \mykant\ is an \emph{interactive theorem prover}/\emph{functional
232 programming language}, implemented in Haskell.
234 It is in the tradition of Agda and Epigram (and to a lesser extent
235 Coq), but with a more powerful notion of \emph{equality}.
237 We have figured out theory of \mykant, and have a near-complete
242 \frametitle{Theorem provers are short-sighted}
244 Two functions dear to the Haskell practitioner:
247 \myfun{map} : (\myb{a} \myarr \myb{b}) \myarr \mylist{\myb{a}} \myarr \mylist{\myb{b}} \\
248 \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l}
249 \myfun{map} & \myb{f} & \mynil & = & \mynil \\
250 \myfun{map} & \myb{f} & (\myb{x} \mycons \myb{xs}) & = & \myapp{\myb{f}}{\myb{x}} \mycons \myfun{map} \myappsp \myb{f} \myappsp \myb{xs} \\
254 (\myfun{${\circ}$}) : (\myb{b} \myarr \myb{c}) \myarr (\myb{a} \myarr \myb{b}) \myarr (\myb{a} \myarr \myb{c}) \\
255 (\myb{f} \mathbin{\myfun{$\circ$}} \myb{g}) \myappsp \myb{x} = \myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}
261 \frametitle{Theorem provers are short-sighted}
262 $\myfun{map}$'s composition law states that:
264 \forall \myb{f} {:} (\myb{b} \myarr \myb{c}), \myb{g} {:} (\myb{a} \myarr \myb{b}). \myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} \myeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g})
266 We can convince Coq or Agda that
268 \forall \myb{f} {:} (\myb{b} \myarr \myb{c}), \myb{g} {:} (\myb{a} \myarr \myb{b}), \myb{l} {:} \mylist{\myb{a}}. (\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g}) \myappsp \myb{l} \myeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l}
270 But we cannot get rid of the $\myb{l}$. Why?
274 \frametitle{\mykant\ and observational equality}
276 \emph{Observational} equality solves this and other annoyances.
278 \mykant\ is a system aiming at making observational equality more
283 \frametitle{Theorem provers, dependent types}
286 types $\leftrightarrow$ propositions
288 programs $\leftrightarrow$ proofs
293 \frametitle{Theorem provers, dependent types} First class types: we
294 can return them, have them as arguments, etc.
296 \begin{array}{@{}l@{\ \ \ }l}
297 \mysyn{data}\ \myempty & \text{No members.} \\
298 \mysyn{data}\ \myunit \mapsto \mytt & \text{One member.}
301 $\myempty : \mytyp$, $\myunit : \mytyp$.
303 $\myunit$ is trivially inhabitable: it corresponds to $\top$ in
308 $\myempty$ is \emph{not} inhabitable: it corresponds to $\bot$.
310 \myfun{absurd} : \myempty \myarr \myb{A}
315 \frametitle{Theorem provers, dependent types}
316 \[ \mysyn{data}\ \mylist{\myb{A}} \mapsto \mynil \mydcsep \myb{A} \mycons \mylist{\myb{A}} \]
317 We want to express a `non-emptiness' property for lists:
320 \myfun{non-empty} : \mylist{\myb{A}} \myarr \mytyp \\
321 \begin{array}{@{}l@{\myappsp}c@{\ }l}
322 \myfun{non-empty} & \mynil & \mapsto \myempty \\
323 \myfun{non-empty} & (\myb{x} \mycons \myb{l}) & \mapsto \myunit
328 A term of type $\myfun{non-empty} \myappsp \myb{l}$ represents a
329 \emph{proof} that $\myb{l}$ is indeed not empty.
331 \begin{array}{@{}l@{\ \ \ }l}
332 \text{Can't prove} & \myfun{non-empty}\myappsp \mynil \myred \myempty \\
333 \text{Trivial to prove} & \myfun{non-empty}\myappsp(2 \mycons \mynil) \myred \myunit
339 \frametitle{Example: safe $\myfun{head}$ function}
340 \only<3>{We can eliminate the `empty list' case:}
343 \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{non-empty}\myappsp\myb{l} \myarr \myb{A}} \\
344 \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l}
345 \myfun{head} & \mynil & \myb{p} & \mapsto & \only<1,2>{\myhole{?}}\only<3>{\myabsurd\myappsp\myb{p}} \\
346 \myfun{head} & (\myb{x} \mycons \myb{xs}) & \myb{p} & \mapsto & \myb{x}
352 The logic equivalent would be
354 \forall \myb{l} {:} \mylist{\myb{A}}.\ \myfun{non-empty}\myappsp\myb{l} \myarr \myb{A}
356 `For all non-empty lists of type $\myb{A}$, we can get an element of $\myb{A}$.'
359 The type of $\myb{p}$ in the $\myhole{?}$ is $\myempty$, since
360 \[\myfun{non-empty}\myappsp\mynil \myred \myempty \]}
363 \[ \myfun{absurd} : \myempty \myarr \myb{A} \]
368 \frametitle{How do we type check this thing?}
370 \myfun{head} \myappsp (3 \mycons \mynil) : \myfun{non-empty}\myappsp(3 \mycons \mynil) \myarr \mynat
373 \[ \mytt : \myfun{non-empty}\myappsp(3 \mycons \mynil) \]
375 \[ \myfun{head} \myappsp (3 \mycons \mynil) : \myunit \myarr \mynat \]
377 Yes: to typecheck, we reduce terms fully (to their \emph{normal form})
380 \begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}
381 \myunit & \myredd & \myunit & \mydefeq & \myunit & \myreddd & \myfun{non-empty}\myappsp(3 \mycons \mynil) \\
382 (\myabs{\myb{x}\, \myb{y}}{\myb{y}}) \myappsp \myunit \myappsp \myappsp \mynat & \myredd & \mynat & \mydefeq & \mynat & \myreddd & (\myabs{\myb{x}\, \myb{y}}{\myb{x}}) \myappsp \mynat \myappsp \myunit \\
387 \mydefeq\ \text{takes the name of \textbf{definitional equality}.}
392 \frametitle{Propositional equality} Using definitional equality, we
393 can give the user a type-level notion of term equality.
395 (\myeq) : \myb{A} \myarr \myb{A} \myarr \mytyp\ \ \ \text{internalises equality \textbf{as a type}}
397 We introduce members of $\myeq$ by reflexivity, for example
399 \myrefl\myappsp5 : 5 \myeq 5
404 \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\text{, since}\\
405 (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5
408 Then we can use a substitution law to derive other
409 laws---transitivity, congruence, etc.
410 \[ \myeq\ \text{takes the name of \textbf{propositional equality}} \]
414 \frametitle{The problem with prop. equality}
415 Going back to $\myfun{map}$, we can prove that
416 \[ \forall \myb{f} {:} (\myb{b} \myarr \myb{c}), \myb{g} {:} (\myb{a} \myarr \myb{b}), \myb{l} {:} \mylist{\myb{a}}.\ (\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g}) \myappsp \myb{l} \myeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l} \]
419 (\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g})\myappsp \myb{l} \mydefeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l}
421 By induction on $\myb{l}$.
423 Without the $\myb{l}$ we cannot compute, so we are stuck with
425 \myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} \not\mydefeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g})
430 \frametitle{Observational equality}
432 Instead of basing its equality on definitional equality, look at the
433 structure of the type to decide.
435 For functions this will mean that proving
437 \myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g} \myeq \myfun{map}\myappsp (\myse{f} \mycomp \myse{g})
439 Will reduce to proving that
441 (\myb{l} : \mylist{\myb{A}}) \myarr
442 (\myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g})\myappsp\myb{l} \myeq \myfun{map}\myappsp (\myse{f} \mycomp \myse{g})\myappsp \myb{l}
444 Which is what we want. The interesting part is how to make the system
447 This extends to other structures (tuples, inductive types, \dots).
448 Moreover, if we can deem two \emph{types} equal, we can \emph{coerce}
449 values from one to the other.
454 {\huge \mykant' features}
459 \frametitle{Inductive data}
461 \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mynil \mydcsep \myb{A} \mycons \mytyc{List}\myappsp\myb{A}
463 Each with an induction principle:
465 \begin{array}{@{}l@{\ }l}
466 \mytyc{List}.\myfun{elim} : & \AgdaComment{-{}- The property that we want to prove:} \\
467 & (\myb{P} : \mytyc{List}\myappsp\myb{A} \myarr \mytyp) \myarr \\
468 & \AgdaComment{-{}- If it holds for the base case:} \\
469 & \myb{P} \myappsp \mynil \myarr \\
470 & \AgdaComment{-{}- And for the inductive step:} \\
471 & ((\myb{x} : \myb{A}) \myarr (\myb{l} : \mytyc{List}\myappsp \myb{A}) \myarr \myb{P} \myappsp \myb{l} \myarr \myb{P} \myappsp (\myb{x} \mycons \myb{l})) \myarr \\
472 & \AgdaComment{-{}- Then it holds for every list:} \\
473 & (\myb{l} : \mytyc{List}\myappsp\myb{A}) \myarr \myb{P} \myappsp \myb{l}
476 Induction is also computation, via structural recursion:
478 \begin{array}{@{}l@{\ }l}
479 \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp \mynil & \myred \myse{pn} \\
480 \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp (\mytmm \mycons \mytmn) & \myred \myse{pc} \myappsp \mytmm \myappsp \mytmn \myappsp (\mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{ps} \myappsp \mytmn )
486 \frametitle{Dependent defined types} \emph{Unlike} Haskell, we can
487 have fields of a data constructor to depend on earlier fields:
490 \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp\myhole{$(\myb{B} : \myb{A} \myarr \mytyp)$} \mapsto \\
491 \myind{2}\mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B}\myappsp\myb{fst} \}
495 The \emph{type} of the second element depends on the \emph{value} of
498 \begin{array}{@{}l@{\ }l}
499 \myfun{fst} & : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\
500 \myfun{snd} & : (\myb{x} : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B}) \myarr \myb{B} \myappsp (\myfun{fst} \myappsp \myb{x})
503 Where the projection's reduction rules are predictably
505 \begin{array}{@{}l@{\ }l}
506 \myfun{fst}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmm \\
507 \myfun{snd}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmn \\
513 \frametitle{Example: the type of even numbers}
514 For example we can define the type of even numbers:
518 \mysyn{data}\ \mynat \mapsto \mydc{zero} \mydcsep \mydc{suc}\myappsp\mynat \\
520 \myfun{even} : \mynat \myarr \mytyp \\
521 \begin{array}{@{}l@{\myappsp}c@{\ }l}
522 \myfun{even} & \myzero & \mapsto \myunit \\
523 \myfun{even} & (\mysuc \myappsp \myzero) & \mapsto \myempty \\
524 \myfun{even} & (\mysuc \myappsp (\mysuc \myappsp \myb{n})) & \mapsto \myfun{even} \myappsp \myb{n}
527 \mytyc{Even} : \mytyp \\
528 \mytyc{Even} \mapsto \mytyc{Tuple}\ \mynat\ \myfun{even}
534 \frametitle{Type hierarchy}
535 \[\{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp\]
536 What is the type of $\mytyp$?
538 \cancel{\mytyp : \mytyp}\ \ \ \text{\textbf{inconsistent}}
540 Similar to Russel's paradox in na{\"i}ve set theory.
542 Instead, we have a hierarchy:
544 \{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp_0 : \mytyp_1 : \cdots
546 We talk of types in $\mytyp_0$ as `smaller' than types in $\mytyp_1$.
550 \frametitle{Cumulativity and typical ambiguity}
552 \[ \mytyp_0 : \mytyp_1 \ \ \ \text{but}\ \ \ \mytyp_0 \centernot{:} \mytyp_2\]
553 We have a cumulative hierarchy, so that
554 \[ \mytyp_n : \mytyp_m \ \ \ \text{iff}\ \ \ n < m \]
556 \[ \mynat : \mytyp_0\ \ \ \text{and}\ \ \ \mynat : \mytyp_1\ \ \ \text{and}\ \ \ \mynat : \mytyp_{50} \]
558 But in \mykant, you can forget about levels: the consistency is
559 checked automatically---a mechanised version of what Russell called
560 \emph{typical ambiguity}.
564 \frametitle{Bidirectional type checking}
566 \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A}\myappsp (\mytyc{List}\myappsp\myb{A})
569 With no type inference, we have explicit types for the constructors:
571 \begin{array}{@{}l@{\ }l}
572 \mydc{nil} & : (\myb{A} : \mytyp) \myarr \mytyc{List}\myappsp\myb{A} \\
573 \mydc{cons} &: (\myb{A} : \mytyp) \myarr \myb{A} \myarr \mytyc{List}\myappsp\myb{A} \myarr \mytyc{List}\myappsp\myb{A}\\
578 \mydc{cons}\myappsp \mynat\myappsp 1 \myappsp (\mydc{cons}\myappsp \mynat \myappsp 2 \myappsp (\mydc{cons}\myappsp \mynat \myappsp 3 \myappsp (\mydc{nil}\myappsp \mynat)))
580 Instead, annotate terms and propagate the type:
582 \mydc{cons}\myappsp 1 \myappsp (\mydc{cons}\myappsp 2 \myappsp (\mydc{cons} \myappsp 3 \myappsp \mydc{nil})) : \mytyc{List}\myappsp\mynat
584 Conversely, when we use eliminators the type can be inferred.
588 \frametitle{Bidirectional type checking}
590 This technique is known as \emph{bidirectional} type checking---some
591 terms get \emph{checked}, some terms \emph{infer} types.
593 Usually used for pre-defined types or core calculi, \mykant\ extends
594 to user-defined types.
598 \frametitle{OTT + user defined types}
600 For each type, we need to:
602 \item Describe when two types formed by the defined type constructors
604 \[ \mylist{\mytya_1} \myeq \mylist{\mytya_2} \]
605 \item Describe when two values of the defined type are equal;
607 \begin{array}{@{}c@{\ \ \ \ \ \ }c}
608 \mynil \myeq \mynil & \mynil \myeq \mytmm \mycons \mytmn \\
609 \mytmm \mycons \mytmn \myeq \mynil & \mytmm_1 \mycons \mytmn_1 \myeq \mytmm_2 \mycons \mytmn_2
612 \item Describe how to transport values of the defined type.
617 \frametitle{OTT + hierarchy}
619 Since equalities reduce to functions abstracting over various things,
620 we need to make sure that the hierarchy is respected.
622 For example we have that
625 (\myb{x_1} {:} \mytya_1) \myarr \mytyb_1 \myeq (\myb{x_2} {:} \mytya_2) \myarr \mytyb_2 \myred \\
626 \myind{2} \mytya_1 \myeq \mytya_2 \myand
627 ((\myb{x_1} : \mytya_1) \myarr (\myb{x_2} : \mytya_2) \myarr \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}])
631 Subtle point---I discovered a problem in the theory after
632 submitting... but I have a fix.
642 \frametitle{Further work}
645 \item Pattern matching and explicit recursion
646 \item More expressive data types
647 \item Inference via unification