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}
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@{\ \ \ }l}
297 \mysyn{data}\ \myempty & & \text{No members.} \\
298 \mysyn{data}\ \myunit & \mapsto \mytt & \text{One member.}
301 $\myempty : \mytyp$, $\myunit : \mytyp$, $\mynat : \mytyp$.
303 $\myunit$ is trivially inhabitable: it corresponds to $\top$ in
306 $\myempty$ is \emph{not} inhabitable: it corresponds to $\bot$.
308 \myfun{absurd} : \myempty \myarr \myb{A}
313 \frametitle{Theorem provers, dependent types}
314 \[ \mysyn{data}\ \mylist{\myb{A}} \mapsto \mynil \mydcsep \myb{A} \mycons \mylist{\myb{A}} \]
315 We want to express a `non-emptiness' property for lists:
317 \begin{array}{@{}l@{\myappsp}c@{\ }l}
318 \myfun{non-empty} : \mylist{\myb{A}} \myarr \mytyp \\
319 \myfun{non-empty} & \mynil & = \myempty \\
320 \myfun{non-empty} & (\myb{x} \mycons \myb{l}) & = \myunit
326 (\myfun{${>}$}) : \mynat \myarr \mynat \myarr \mytyp \\
327 \begin{array}{@{}c@{\,}c@{\,}c@{\ }l}
328 \mydc{zero} & \mathrel{\myfun{$>$}} & \myb{m} & = \myempty \\
329 \myb{n} & \mathrel{\myfun{$>$}} & \mydc{zero} & = \myunit \\
330 (\mydc{suc} \myappsp \myb{n}) & \mathrel{\myfun{$>$}} & (\mydc{suc} \myappsp \myb{m}) & = \myb{n} \mathrel{\myfun{$>$}} \myb{m}
335 A term of type $\myb{m} \mathrel{\myfun{$>$}} \myb{n}$ represents a
336 \emph{proof} that $\myb{m}$ is indeed greater than $\myb{n}$.
339 3 \mathrel{\myfun{$>$}} 1 \myred \myunit \\
340 2 \mathrel{\myfun{$>$}} 2 \myred \myempty \\
341 0 \mathrel{\myfun{$>$}} \myb{m} \myred \myempty
347 \frametitle{Example: safe $\myfun{head}$ function}
351 \mysyn{data}\ \mylist{\myb{A}} = \mynil \mydcsep \myb{A} \mycons \mylist{\myb{A}} \\
353 \myfun{length} : \mylistt{\myb{A}} \myarr \mynat \\
354 \begin{array}{@{}l@{\myappsp}c@{\ }c@{\ }l}
355 \myfun{length} & \mynil & \mapsto & \mydc{zero} \\
356 \myfun{length} & (\myb{x} \mycons \myb{xs}) & \mapsto & \mydc{suc} \myappsp (\myfun{length} \myappsp \myb{xs})
359 \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \myarr \myb{A}} \\
360 \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l}
361 \myfun{head} & \mynil & \myb{p} & \mapsto & \only<1,2>{\myhole{?}}\only<3>{\myabsurd\myappsp\myb{p}} \\
362 \myfun{head} & (\myb{x} \mycons \myb{xs}) & \myb{p} & \mapsto & \myb{x}
368 The logic equivalent would be
370 \forall \myb{l} {:} \mylist{\myb{A}}.\ \myfun{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \myarr \myb{A}
372 `For all non-empty lists of type $\myb{A}$, we can get an element of $\myb{A}$.'
375 The type of $\myb{p}$ in the $\myhole{?}$ is $\myempty$, since
376 \[\myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 \myred 0 \mathrel{\myfun{$>$}} 0 \myred \myempty \]}
379 \[ \myfun{absurd} : \myempty \myarr \myb{A} \]
384 \frametitle{How do we type check this thing?}
386 \myfun{head} \myappsp \mylistt{3} : \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \myarr \mynat
389 \[ \mytt : \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \]
391 \[ \myfun{head} \myappsp \mylistt{3} : \myunit \myarr \mynat \]
393 Yes: to typecheck, we reduce terms fully before comparing:
395 \begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}
396 \myunit & \myredd & \myunit & \mydefeq & \myunit & \myreddd & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\
397 \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \myredd & \myempty & \mydefeq & \myempty & \myreddd & \myempty \\
398 (\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 \\
403 \mydefeq\ \text{takes the name of \textbf{definitional equality}.}
408 \frametitle{Propositional equality} Using definitional equality, we
409 can give the user a type-level notion of term equality.
411 (\myeq) : \myb{A} \myarr \myb{A} \myarr \mytyp\ \ \ \text{internalises equality \textbf{as a type}}
413 We introduce members of $\myeq$ by reflexivity, for example
415 \myrefl\myappsp5 : 5 \myeq 5
420 \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\text{, since}\\
421 (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5
424 Then we can use a substitution law to derive other
425 laws---transitivity, congruence, etc.
426 \[ \myeq\ \text{takes the name of \textbf{propositional equality}} \]
430 \frametitle{The problem with prop. equality}
431 Going back to $\myfun{map}$, we can prove that
432 \[ \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} \]
435 (\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}
437 By induction on $\myb{l}$.
439 Without the $\myb{l}$ we cannot compute, so we are stuck with
441 \myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} \not\mydefeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g})
446 \frametitle{Observational equality}
448 Instead of basing its equality on definitional equality, look at the
449 structure of the type to decide.
451 For functions this will mean that proving
453 \myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g} \myeq \myfun{map}\myappsp (\myse{f} \mycomp \myse{g})
455 Will reduce to proving that
457 (\myb{l} : \mylist{\myb{A}}) \myarr
458 (\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}
460 Which is what we want. The interesting part is how to make the system
463 This extends to other structures (tuples, inductive types, \dots).
464 Moreover, if we can deem two \emph{types} equal, we can \emph{coerce}
465 values from one to the other.
470 {\huge \mykant' features}
475 \frametitle{Inductive data}
477 \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mynil \mydcsep \myb{A} \mycons \mytyc{List}\myappsp\myb{A}
479 Each with an induction principle:
481 \begin{array}{@{}l@{\ }l}
482 \mytyc{List}.\myfun{elim} : & \AgdaComment{-{}- The property that we want to prove:} \\
483 & (\myb{P} : \mytyc{List}\myappsp\myb{A} \myarr \mytyp) \myarr \\
484 & \AgdaComment{-{}- If it holds for the base case:} \\
485 & \myb{P} \myappsp \mynil \myarr \\
486 & \AgdaComment{-{}- And for the inductive step:} \\
487 & ((\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 \\
488 & \AgdaComment{-{}- Then it holds for every list:} \\
489 & (\myb{l} : \mytyc{List}\myappsp\myb{A}) \myarr \myb{P} \myappsp \myb{l}
492 Induction is also computation, via structural recursion:
494 \begin{array}{@{}l@{\ }l}
495 \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp \mynil & \myred \myse{pn} \\
496 \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 )
502 \frametitle{Dependent defined types} \emph{Unlike} Haskell, we can
503 have fields of a data constructor to depend on earlier fields:
506 \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp\myhole{$(\myb{B} : \myb{A} \myarr \mytyp)$} \mapsto \\
507 \myind{2}\mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B}\myappsp\myb{fst} \}
511 The \emph{type} of the second element depends on the \emph{value} of
514 \begin{array}{@{}l@{\ }l}
515 \myfun{fst} & : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\
516 \myfun{snd} & : (\myb{x} : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B}) \myarr \myb{B} \myappsp (\myfun{fst} \myappsp \myb{x})
519 Where the projection's reduction rules are predictably
521 \begin{array}{@{}l@{\ }l}
522 \myfun{fst}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmm \\
523 \myfun{snd}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmn \\
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}
545 In logic this would be
546 \[ \exists x \in \mathbb{N}.\ even(x) \]
550 \frametitle{Type hierarchy}
551 \[\{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp\]
552 What is the type of $\mytyp$?
554 \cancel{\mytyp : \mytyp}\ \ \ \text{\textbf{inconsistent}}
556 Much like na{\"i}ve set theory is (Girard's paradox).
558 Instead, we have a hierarchy:
560 \{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp_0 : \mytyp_1 : \cdots
562 We talk of types in $\mytyp_0$ as `smaller' than types in $\mytyp_1$.
566 \frametitle{Cumulativity and typical ambiguity}
568 \[ \mytyp_0 : \mytyp_1 \ \ \ \text{but}\ \ \ \mytyp_0 \centernot{:} \mytyp_2\]
569 We have a cumulative hierarchy, so that
570 \[ \mytyp_n : \mytyp_m \ \ \ \text{iff}\ \ \ n < m \]
572 \[ \mynat : \mytyp_0\ \ \ \text{and}\ \ \ \mynat : \mytyp_1\ \ \ \text{and}\ \ \ \mynat : \mytyp_{50} \]
574 But in \mykant, you can forget about levels: the consistency is
575 checked automatically---a mechanised version of what Russell called
576 \emph{typical ambiguity}.
580 \frametitle{OTT + user defined types}
582 For each type, we need to:
584 \item Describe when two types formed by the defined type constructors
586 \[ \mylist{\mytya_1} \myeq \mylist{\mytya_2} \]
587 \item Describe when two values of the defined type are equal;
589 \begin{array}{@{}c@{\ \ \ \ \ \ }c}
590 \mynil \myeq \mynil & \mynil \myeq \mytmm \mycons \mytmn \\
591 \mytmm \mycons \mytmn \myeq \mynil & \mytmm_1 \mycons \mytmn_1 \myeq \mytmm_2 \mycons \mytmn_2
594 \item Describe how to transport values of the defined type.
599 \frametitle{OTT + hierarchy}
601 Since equalities reduce to functions abstracting over various things,
602 we need to make sure that the hierarchy is respected.
604 For example we have that
607 ((\myb{x_1} {:} \mytya_1) \myarr \mytyb_1 : \mytyp) \myeq ((\myb{x_2} {:} \mytya_2) \myarr \mytyb_2 : \mytyp) \myred \\
608 \myind{2} (\mytya_1 : \mytyp) \myeq (\mytya_2 : \mytyp) \myand \\
609 \myind{2} (\myb{x_1} : \mytya_1) \myarr (\myb{x_2} : \mytya_2) \myarr (\mytyb_1 : \mytyp) \myeq (\mytyb_2 : \mytyp)
613 Subtle point---I discovered a problem in the theory after
614 submitting... but I have a fix.
618 \frametitle{Bidirectional type checking}
620 \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A}\myappsp (\mytyc{List}\myappsp\myb{A})
623 With no type inference, we have explicit types for the constructors:
625 \begin{array}{@{}l@{\ }l}
626 \mydc{nil} & : (\myb{A} : \mytyp) \myarr \mytyc{List}\myappsp\myb{A} \\
627 \mydc{cons} &: (\myb{A} : \mytyp) \myarr \myb{A} \myarr \mytyc{List}\myappsp\myb{A} \myarr \mytyc{List}\myappsp\myb{A}\\
632 \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)))
634 Instead, annotate terms and propagate the type:
636 \mydc{cons}\myappsp 1 \myappsp (\mydc{cons}\myappsp 2 \myappsp (\mydc{cons} \myappsp 3 \myappsp \mydc{nil})) : \mytyc{List}\myappsp\mynat
638 Conversely, when we use eliminators the type can be inferred.
642 \frametitle{Bidirectional type checking}
644 This technique is known as \emph{bidirectional} type checking---some
645 terms get \emph{checked}, some terms \emph{infer} types.
647 Usually used for pre-defined types or core calculi, \mykant\ extends
648 to user-defined types.