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 similar in scope to Agda or Coq, but with a more powerful notion
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 \mytmt )
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 \myfun{even} : \mynat \myarr \mytyp \\
519 \begin{array}{@{}l@{\myappsp}c@{\ }l}
520 \myfun{even} & \myzero & \mapsto \myunit \\
521 \myfun{even} & (\mysuc \myappsp \myzero) & \mapsto \myempty \\
522 \myfun{even} & (\mysuc \myappsp (\mysuc \myappsp \myb{n})) & \mapsto \myfun{even} \myappsp \myb{n}
525 \mytyc{Even} : \mytyp \\
526 \mytyc{Even} \mapsto \mytyc{Tuple}\ \mynat\ \myfun{even}
532 \frametitle{Type hierarchy}
533 \[\{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp\]
534 What is the type of $\mytyp$?
536 \cancel{\mytyp : \mytyp}\ \ \ \text{\textbf{inconsistent}}
538 Similar to Russel's paradox in na{\"i}ve set theory.
540 Instead, we have a hierarchy:
542 \{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp_0 : \mytyp_1 : \cdots
544 We talk of types in $\mytyp_0$ as `smaller' than types in $\mytyp_1$.
548 \frametitle{Cumulativity and typical ambiguity}
550 \[ \mytyp_0 : \mytyp_1 \ \ \ \text{but}\ \ \ \mytyp_0 \centernot{:} \mytyp_2\]
551 We have a cumulative hierarchy, so that
552 \[ \mytyp_n : \mytyp_m \ \ \ \text{iff}\ \ \ n < m \]
554 \[ \mynat : \mytyp_0\ \ \ \text{and}\ \ \ \mynat : \mytyp_1\ \ \ \text{and}\ \ \ \mynat : \mytyp_{50} \]
556 But in \mykant, you can forget about levels: the consistency is
557 checked automatically---a mechanised version of what Russell called
558 \emph{typical ambiguity}.
562 \frametitle{Bidirectional type checking}
564 \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A}\myappsp (\mytyc{List}\myappsp\myb{A})
567 With no type inference, we have explicit types for the constructors:
569 \begin{array}{@{}l@{\ }l}
570 \mydc{nil} & : (\myb{A} : \mytyp) \myarr \mytyc{List}\myappsp\myb{A} \\
571 \mydc{cons} &: (\myb{A} : \mytyp) \myarr \myb{A} \myarr \mytyc{List}\myappsp\myb{A} \myarr \mytyc{List}\myappsp\myb{A}\\
576 \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)))
578 Instead, annotate terms and propagate the type:
580 \mydc{cons}\myappsp 1 \myappsp (\mydc{cons}\myappsp 2 \myappsp (\mydc{cons} \myappsp 3 \myappsp \mydc{nil})) : \mytyc{List}\myappsp\mynat
582 Conversely, when we use eliminators the type can be inferred.
586 \frametitle{Bidirectional type checking}
588 This technique is known as \emph{bidirectional} type checking---some
589 terms get \emph{checked}, some terms \emph{infer} types.
591 Usually used for pre-defined types or core calculi, \mykant\ extends
592 to user-defined types.
596 \frametitle{OTT + user defined types}
598 For each type, we need to:
600 \item Describe when two types formed by the defined type constructors
602 \[ \mylist{\mytya_1} \myeq \mylist{\mytya_2} \]
603 \item Describe when two values of the defined type are equal;
605 \begin{array}{@{}c@{\ \ \ \ \ \ }c}
606 \mynil \myeq \mynil & \mynil \myeq \mytmm \mycons \mytmn \\
607 \mytmm \mycons \mytmn \myeq \mynil & \mytmm_1 \mycons \mytmn_1 \myeq \mytmm_2 \mycons \mytmn_2
610 \item Describe how to transport values of the defined type.
615 \frametitle{OTT + hierarchy}
617 Since equalities reduce to functions abstracting over various things,
618 we need to make sure that the hierarchy is respected.
620 For example we have that
623 (\myb{x_1} {:} \mytya_1) \myarr \mytyb_1 \myeq (\myb{x_2} {:} \mytya_2) \myarr \mytyb_2 \myred \\
624 \myind{2} \mytya_1 \myeq \mytya_2 \myand
625 ((\myb{x_1} : \mytya_1) \myarr (\myb{x_2} : \mytya_2) \myarr \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}])
629 Subtle point---I discovered a problem in the theory after
630 submitting... but I have a fix.
640 \frametitle{Further work}
643 \item Pattern matching and explicit recursion
644 \item More expressive data types
645 \item Inference via unification