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}, implemented in
234 It is similar in scope to Agda or Coq, but with a more powerful notion
237 We figured out its theory, but do not have a complete
238 implementation---although most of the work is done.
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} First class types: we
284 can return them, have them as arguments, etc.
286 \begin{array}{@{}l@{\ }l@{\ \ \ }l}
287 \mysyn{data}\ \myempty & & \text{No members.} \\
288 \mysyn{data}\ \myunit & = \mytt & \text{One member.} \\
289 \mysyn{data}\ \mynat & = \mydc{zero} \mydcsep \mydc{suc}\myappsp\mynat & \text{Natural numbers.}
292 $\myempty : \mytyp$, $\myunit : \mytyp$, $\mynat : \mytyp$.
294 $\myunit$ is trivially inhabitable: it corresponds to $\top$ in
297 $\myempty$ is \emph{not} inhabitable: it corresponds to $\bot$.
299 \myfun{absurd} : \myempty \myarr \myb{A}
304 \frametitle{Theorem provers, dependent types}
305 % TODO examples first
307 We can express relations:
310 (\myfun{${>}$}) : \mynat \myarr \mynat \myarr \mytyp \\
311 \begin{array}{@{}c@{\,}c@{\,}c@{\ }l}
312 \mydc{zero} & \mathrel{\myfun{$>$}} & \myb{m} & = \myempty \\
313 \myb{n} & \mathrel{\myfun{$>$}} & \mydc{zero} & = \myunit \\
314 (\mydc{suc} \myappsp \myb{n}) & \mathrel{\myfun{$>$}} & (\mydc{suc} \myappsp \myb{m}) & = \myb{n} \mathrel{\myfun{$>$}} \myb{m}
319 A term of type $\myb{m} \mathrel{\myfun{$>$}} \myb{n}$ represents a
320 \emph{proof} that $\myb{m}$ is indeed greater than $\myb{n}$.
323 3 \mathrel{\myfun{$>$}} 1 \myred \myunit \\
324 2 \mathrel{\myfun{$>$}} 2 \myred \myempty \\
325 0 \mathrel{\myfun{$>$}} \myb{m} \myred \myempty
331 \frametitle{Example: safe $\myfun{head}$ function}
335 \mysyn{data}\ \mylist{\myb{A}} = \mynil \mydcsep \myb{A} \mycons \mylist{\myb{A}} \\
337 \myfun{length} : \mylistt{\myb{A}} \myarr \mynat \\
338 \begin{array}{@{}l@{\myappsp}c@{\ }c@{\ }l}
339 \myfun{length} & \mynil & \mapsto & \mydc{zero} \\
340 \myfun{length} & (\myb{x} \mycons \myb{xs}) & \mapsto & \mydc{suc} \myappsp (\myfun{length} \myappsp \myb{xs})
343 \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \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{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \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{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 \myred 0 \mathrel{\myfun{$>$}} 0 \myred \myempty \]}
364 \frametitle{How do we type check this thing?}
366 \myfun{head} \myappsp \mylistt{3} : \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \myarr \mynat
369 \[ \mytt : \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \]
371 \[ \myfun{head} \myappsp \mylistt{3} : \myunit \myarr \mynat \]
373 Will $\mytt : \myunit$ do as an argument? In other words, when type
374 checking, do we have that
376 \begin{array}{@{}c@{\ }c@{\ }c}
377 \myunit & \mydefeq & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\
378 \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \mydefeq & \myempty \\
379 (\myabs{\myb{x}\, \myb{y}}{\myb{y}}) \myappsp \myunit \myappsp \myappsp \mynat & \mydefeq & (\myabs{\myb{x}\, \myb{y}}{\myb{x}}) \myappsp \mynat \myappsp \myunit \\
387 \frametitle{Definitional equality}
389 The type checker needs a notion of equality between types.
391 We reduce terms `as far as possible' (to their \emph{normal form}) and
392 then compare them syntactically:
394 \begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}
395 \myunit & \myredd & \myunit & \mydefeq & \myunit & \myreddd & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\
396 \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \myredd & \myempty & \mydefeq & \myempty & \myreddd & \myempty \\
397 (\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 \\
402 This equality, $\mydefeq$, takes the name of \emph{definitional} equality.
407 \frametitle{Propositional equality} Using definitional equality, we
408 can give the user a type-level notion of term equality.
410 (\myeq) : \myb{A} \myarr \myb{A} \myarr \mytyp
412 We introduce members of $\myeq$ by reflexivity:
414 \myrefl\myappsp\mytmt : \mytmt \myeq \mytmt
416 So that $\myrefl$ will relate definitionally equal terms:
418 \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\ \text{since}\ (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5
420 Then we can use a substitution law to derive other
421 laws---transitivity, congruence, etc.
425 \frametitle{The problem with prop. equality}
426 Going back to $\myfun{map}$, we can prove that
427 \[ \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} \]
428 Because we can prove, by induction on $\myb{l}$, that we will always get definitionally equal lists.
430 But without the $\myb{l}$, we cannot compute, so we are stuck with
432 \myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} \not\mydefeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g})
437 \frametitle{Observational equality}
439 Instead of basing its equality on definitional equality, look at the
440 structure of the type to decide:
443 (\myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g} : \mylistt{\myse{A_1}} \myarr \mylistt{\myse{C_1}}) \myeq (\myfun{map}\myappsp (\myse{f} \mycomp \myse{g}) : \mylistt{\myse{A_2}} \myarr \mylistt{\myse{C_2}}) \myred \\
444 \myind{2} (\myse{l_1} : \mylistt{\myse{A_1}}) \myarr (\myse{l_2} : \mylistt{\myse{A_2}}) \myarr (\myse{l_1} : \mylistt{\myse{A_1}}) \myeq (\myse{l_2} : \mylistt{\myse{A_2}}) \myarr \\
445 \myind{2} ((\myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g}) \myappsp \myse{l} : \mylistt{\myse{C_1}}) \myeq (\myfun{map}\myappsp (\myse{f} \mycomp \myse{g}) \myappsp \myse{l} : \mylistt{\myse{C_2}})
448 This extends to other structures (tuples, inductive types, \dots).
449 Moreover, if we can deem two \emph{types} equal, we can \emph{coerce}
450 values from one to the other.
455 {\huge \mykant' features}
460 \frametitle{Inductive data}
462 \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mynil \mydcsep \myb{A} \mycons \mytyc{List}\myappsp\myb{A}
464 Each with an induction principle:
466 \begin{array}{@{}l@{\ }l}
467 \mytyc{List}.\myfun{elim} : & \AgdaComment{-{}- The property that we want to prove:} \\
468 & (\myb{P} : \mytyc{List}\myappsp\myb{A} \myarr \mytyp) \myarr \\
469 & \AgdaComment{-{}- If it holds for the base case:} \\
470 & \myb{P} \myappsp \mynil \myarr \\
471 & \AgdaComment{-{}- And for the inductive step:} \\
472 & ((\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 \\
473 & \AgdaComment{-{}- Then it holds for every list:} \\
474 & (\myb{l} : \mytyc{List}\myappsp\myb{A}) \myarr \myb{P} \myappsp \myb{l}
477 Induction is also computation, via structural recursion:
479 \begin{array}{@{}l@{\ }l}
480 \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp \mynil & \myred \myse{pn} \\
481 \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 )
490 \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp(\myb{B} : \mytyp) \mapsto \mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} \}
492 Where each field defines a projection from instances of the record:
494 \begin{array}{@{}l@{\ }c@{\ }l}
495 \myfun{fst} & : & \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\
496 \myfun{snd} & : & \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{B}
499 Where the projection's reduction rules are predictably
501 \begin{array}{@{}l@{\ }l}
502 \myfun{fst}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmm \\
503 \myfun{snd}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmn \\
509 \frametitle{Dependent defined types} \emph{Unlike} Haskell, we can
510 have fields of a data constructor to depend on earlier fields:
513 \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp\myhole{$(\myb{B} : \myb{A} \myarr \mytyp)$} \mapsto \\
514 \myind{2}\mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B}\myappsp\myb{fst} \}
518 The \emph{type} of the second element depends on the \emph{value} of
521 \begin{array}{@{}l@{\ }l}
522 \myfun{fst} & : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\
523 \myfun{snd} & : (\myb{x} : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B}) \myarr \myb{B} \myappsp (\myfun{fst} \myappsp \myb{x})
529 \frametitle{Example: the type of even numbers}
530 For example we can define the type of even numbers:
534 \myfun{even} : \mynat \myarr \mytyp \\
535 \begin{array}{@{}l@{\myappsp}c@{\ }l}
536 \myfun{even} & \myzero & \mapsto \myunit \\
537 \myfun{even} & (\mysuc \myappsp \myzero) & \mapsto \myempty \\
538 \myfun{even} & (\mysuc \myappsp (\mysuc \myappsp \myb{n})) & \mapsto \myfun{even} \myappsp \myb{n}
541 \mytyc{Even} : \mytyp \\
542 \mytyc{Even} \mapsto \mytyc{Tuple}\ \mynat\ \myfun{even}
548 \frametitle{Type hierarchy}
549 \[\{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp\]
550 What is the type of $\mytyp$?
552 \cancel{\mytyp : \mytyp}\ \ \ \text{\textbf{inconsistent}}
554 Much like na{\"i}ve set theory is (Girard's paradox).
556 Instead, we have a hierarchy:
558 \{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp_0 : \mytyp_1 : \cdots
560 We talk of types in $\mytyp_0$ as `smaller' than types in $\mytyp_1$.
564 \frametitle{Cumulativity and typical ambiguity}
566 \[ \mytyp_0 : \mytyp_1 \ \ \ \text{but}\ \ \ \mytyp_0 \centernot{:} \mytyp_2\]
567 We have a cumulative hierarchy, so that
568 \[ \mytyp_n : \mytyp_m \ \ \ \text{iff}\ \ \ n < m \]
570 \[ \mynat : \mytyp_0\ \ \ \text{and}\ \ \ \mynat : \mytyp_1\ \ \ \text{and}\ \ \ \mynat : \mytyp_{50} \]
572 But in \mykant, you can forget about levels: the consistency is
573 checked automatically---a mechanised version of what Russell called
574 \emph{typical ambiguity}.
578 \frametitle{OTT + user defined types}
580 For each type, we need to:
582 \item Describe when two types formed by the defined type constructors
584 \item Describe when two values of the defined type are equal;
585 \item Describe how to transport values of the defined type.
590 \frametitle{OTT + hierarchy}
592 Since equalities reduce to functions abstracting over various things,
593 we need to make sure that the hierarchy is respected.
595 For example we have that
598 ((\myb{x_1} {:} \mytya_1) \myarr \mytyb_1 : \mytyp) \myeq ((\myb{x_2} {:} \mytya_2) \myarr \mytyb_2 : \mytyp) \myred \\
599 \myind{2} (\mytya_1 : \mytyp) \myeq (\mytya_2 : \mytyp) \myand \\
600 \myind{2} (\myb{x_1} : \mytya_1) \myarr (\myb{x_2} : \mytya_2) \myarr (\mytyb_1 : \mytyp) \myeq (\mytyb_2 : \mytyp)
604 Subtle point---I discovered a problem in the theory after
605 submitting... but I have a fix.
609 \frametitle{Bidirectional type checking}
611 \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A}\myappsp (\mytyc{List}\myappsp\myb{A})
614 With no type inference, we have explicit types for the constructors:
616 \begin{array}{@{}l@{\ }l}
617 \mydc{nil} & : (\myb{A} : \mytyp) \myarr \mytyc{List}\myappsp\myb{A} \\
618 \mydc{cons} &: (\myb{A} : \mytyp) \myarr \myb{A} \myarr \mytyc{List}\myappsp\myb{A} \myarr \mytyc{List}\myappsp\myb{A}\\
623 \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)))
625 Instead, annotate terms and propagate the type:
627 \mydc{cons}\myappsp 1 \myappsp (\mydc{cons}\myappsp 2 \myappsp (\mydc{cons} \myappsp 3 \myappsp \mydc{nil})) : \mytyc{List}\myappsp\mynat
629 Conversely, when we use eliminators the type can be inferred.
633 \frametitle{Bidirectional type checking}
635 This technique is known as \emph{bidirectional} type checking---some
636 terms get \emph{checked}, some terms \emph{infer} types.
638 Usually used for pre-defined types or core calculi, \mykant\ extends
639 to user-defined types.