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 & = \mytt & \text{One member.} \\
299 \mysyn{data}\ \mynat & = \mydc{zero} \mydcsep \mydc{suc}\myappsp\mynat & \text{Natural numbers.}
302 $\myempty : \mytyp$, $\myunit : \mytyp$, $\mynat : \mytyp$.
304 $\myunit$ is trivially inhabitable: it corresponds to $\top$ in
307 $\myempty$ is \emph{not} inhabitable: it corresponds to $\bot$.
309 \myfun{absurd} : \myempty \myarr \myb{A}
314 \frametitle{Theorem provers, dependent types}
315 % TODO examples first
317 We can express relations:
320 (\myfun{${>}$}) : \mynat \myarr \mynat \myarr \mytyp \\
321 \begin{array}{@{}c@{\,}c@{\,}c@{\ }l}
322 \mydc{zero} & \mathrel{\myfun{$>$}} & \myb{m} & = \myempty \\
323 \myb{n} & \mathrel{\myfun{$>$}} & \mydc{zero} & = \myunit \\
324 (\mydc{suc} \myappsp \myb{n}) & \mathrel{\myfun{$>$}} & (\mydc{suc} \myappsp \myb{m}) & = \myb{n} \mathrel{\myfun{$>$}} \myb{m}
329 A term of type $\myb{m} \mathrel{\myfun{$>$}} \myb{n}$ represents a
330 \emph{proof} that $\myb{m}$ is indeed greater than $\myb{n}$.
333 3 \mathrel{\myfun{$>$}} 1 \myred \myunit \\
334 2 \mathrel{\myfun{$>$}} 2 \myred \myempty \\
335 0 \mathrel{\myfun{$>$}} \myb{m} \myred \myempty
341 \frametitle{Example: safe $\myfun{head}$ function}
345 \mysyn{data}\ \mylist{\myb{A}} = \mynil \mydcsep \myb{A} \mycons \mylist{\myb{A}} \\
347 \myfun{length} : \mylistt{\myb{A}} \myarr \mynat \\
348 \begin{array}{@{}l@{\myappsp}c@{\ }c@{\ }l}
349 \myfun{length} & \mynil & \mapsto & \mydc{zero} \\
350 \myfun{length} & (\myb{x} \mycons \myb{xs}) & \mapsto & \mydc{suc} \myappsp (\myfun{length} \myappsp \myb{xs})
353 \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \myarr \myb{A}} \\
354 \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l}
355 \myfun{head} & \mynil & \myb{p} & \mapsto & \only<1,2>{\myhole{?}}\only<3>{\myabsurd\myappsp\myb{p}} \\
356 \myfun{head} & (\myb{x} \mycons \myb{xs}) & \myb{p} & \mapsto & \myb{x}
362 The logic equivalent would be
364 \forall \myb{l} {:} \mylist{\myb{A}}.\ \myfun{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \myarr \myb{A}
366 `For all non-empty lists of type $\myb{A}$, we can get an element of $\myb{A}$.'
369 The type of $\myb{p}$ in the $\myhole{?}$ is $\myempty$, since
370 \[\myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 \myred 0 \mathrel{\myfun{$>$}} 0 \myred \myempty \]}
373 \[ \myfun{absurd} : \myempty \myarr \myb{A} \]
378 \frametitle{How do we type check this thing?}
380 \myfun{head} \myappsp \mylistt{3} : \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \myarr \mynat
383 \[ \mytt : \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \]
385 \[ \myfun{head} \myappsp \mylistt{3} : \myunit \myarr \mynat \]
387 Yes: to typecheck, we reduce terms fully before comparing:
389 \begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}
390 \myunit & \myredd & \myunit & \mydefeq & \myunit & \myreddd & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\
391 \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \myredd & \myempty & \mydefeq & \myempty & \myreddd & \myempty \\
392 (\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 \\
397 \mydefeq\ \text{takes the name of \textbf{definitional equality}.}
402 \frametitle{Propositional equality} Using definitional equality, we
403 can give the user a type-level notion of term equality.
405 (\myeq) : \myb{A} \myarr \myb{A} \myarr \mytyp\ \ \ \text{internalises equality \textbf{as a type}}
407 We introduce members of $\myeq$ by reflexivity, for example
409 \myrefl\myappsp5 : 5 \myeq 5
414 \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\text{, since}\\
415 (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5
418 Then we can use a substitution law to derive other
419 laws---transitivity, congruence, etc.
420 \[ \myeq\ \text{takes the name of \textbf{propositional equality}} \]
424 \frametitle{The problem with prop. equality}
425 Going back to $\myfun{map}$, we can prove that
426 \[ \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} \]
429 (\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}
431 By induction on $\myb{l}$.
433 Without the $\myb{l}$ we cannot compute, so we are stuck with
435 \myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} \not\mydefeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g})
440 \frametitle{Observational equality}
442 Instead of basing its equality on definitional equality, look at the
443 structure of the type to decide.
445 For functions this will mean that proving
447 \myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g} \myeq \myfun{map}\myappsp (\myse{f} \mycomp \myse{g})
449 Will reduce to proving that
451 (\myb{l} : \mylist{\myb{A}}) \myarr
452 (\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}
454 Which is what we want. The interesting part is how to make the system
457 This extends to other structures (tuples, inductive types, \dots).
458 Moreover, if we can deem two \emph{types} equal, we can \emph{coerce}
459 values from one to the other.
464 {\huge \mykant' features}
469 \frametitle{Inductive data}
471 \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mynil \mydcsep \myb{A} \mycons \mytyc{List}\myappsp\myb{A}
473 Each with an induction principle:
475 \begin{array}{@{}l@{\ }l}
476 \mytyc{List}.\myfun{elim} : & \AgdaComment{-{}- The property that we want to prove:} \\
477 & (\myb{P} : \mytyc{List}\myappsp\myb{A} \myarr \mytyp) \myarr \\
478 & \AgdaComment{-{}- If it holds for the base case:} \\
479 & \myb{P} \myappsp \mynil \myarr \\
480 & \AgdaComment{-{}- And for the inductive step:} \\
481 & ((\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 \\
482 & \AgdaComment{-{}- Then it holds for every list:} \\
483 & (\myb{l} : \mytyc{List}\myappsp\myb{A}) \myarr \myb{P} \myappsp \myb{l}
486 Induction is also computation, via structural recursion:
488 \begin{array}{@{}l@{\ }l}
489 \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp \mynil & \myred \myse{pn} \\
490 \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 )
499 \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp(\myb{B} : \mytyp) \mapsto \mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} \}
501 Where each field defines a projection from instances of the record:
503 \begin{array}{@{}l@{\ }c@{\ }l}
504 \myfun{fst} & : & \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\
505 \myfun{snd} & : & \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{B}
508 Where the projection's reduction rules are predictably
510 \begin{array}{@{}l@{\ }l}
511 \myfun{fst}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmm \\
512 \myfun{snd}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmn \\
518 \frametitle{Dependent defined types} \emph{Unlike} Haskell, we can
519 have fields of a data constructor to depend on earlier fields:
522 \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp\myhole{$(\myb{B} : \myb{A} \myarr \mytyp)$} \mapsto \\
523 \myind{2}\mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B}\myappsp\myb{fst} \}
527 The \emph{type} of the second element depends on the \emph{value} of
530 \begin{array}{@{}l@{\ }l}
531 \myfun{fst} & : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\
532 \myfun{snd} & : (\myb{x} : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B}) \myarr \myb{B} \myappsp (\myfun{fst} \myappsp \myb{x})
538 \frametitle{Example: the type of even numbers}
539 For example we can define the type of even numbers:
543 \myfun{even} : \mynat \myarr \mytyp \\
544 \begin{array}{@{}l@{\myappsp}c@{\ }l}
545 \myfun{even} & \myzero & \mapsto \myunit \\
546 \myfun{even} & (\mysuc \myappsp \myzero) & \mapsto \myempty \\
547 \myfun{even} & (\mysuc \myappsp (\mysuc \myappsp \myb{n})) & \mapsto \myfun{even} \myappsp \myb{n}
550 \mytyc{Even} : \mytyp \\
551 \mytyc{Even} \mapsto \mytyc{Tuple}\ \mynat\ \myfun{even}
554 In logic this would be
555 \[ \exists x \in \mathbb{N}.\ even(x) \]
559 \frametitle{Type hierarchy}
560 \[\{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp\]
561 What is the type of $\mytyp$?
563 \cancel{\mytyp : \mytyp}\ \ \ \text{\textbf{inconsistent}}
565 Much like na{\"i}ve set theory is (Girard's paradox).
567 Instead, we have a hierarchy:
569 \{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp_0 : \mytyp_1 : \cdots
571 We talk of types in $\mytyp_0$ as `smaller' than types in $\mytyp_1$.
575 \frametitle{Cumulativity and typical ambiguity}
577 \[ \mytyp_0 : \mytyp_1 \ \ \ \text{but}\ \ \ \mytyp_0 \centernot{:} \mytyp_2\]
578 We have a cumulative hierarchy, so that
579 \[ \mytyp_n : \mytyp_m \ \ \ \text{iff}\ \ \ n < m \]
581 \[ \mynat : \mytyp_0\ \ \ \text{and}\ \ \ \mynat : \mytyp_1\ \ \ \text{and}\ \ \ \mynat : \mytyp_{50} \]
583 But in \mykant, you can forget about levels: the consistency is
584 checked automatically---a mechanised version of what Russell called
585 \emph{typical ambiguity}.
589 \frametitle{OTT + user defined types}
591 For each type, we need to:
593 \item Describe when two types formed by the defined type constructors
595 \[ \mylist{\mytya_1} \myeq \mylist{\mytya_2} \]
596 \item Describe when two values of the defined type are equal;
598 \begin{array}{@{}c@{\ \ \ \ \ \ }c}
599 \mynil \myeq \mynil & \mynil \myeq \mytmm \mycons \mytmn \\
600 \mytmm \mycons \mytmn \myeq \mynil & \mytmm_1 \mycons \mytmn_1 \myeq \mytmm_2 \mycons \mytmn_2
603 \item Describe how to transport values of the defined type.
608 \frametitle{OTT + hierarchy}
610 Since equalities reduce to functions abstracting over various things,
611 we need to make sure that the hierarchy is respected.
613 For example we have that
616 ((\myb{x_1} {:} \mytya_1) \myarr \mytyb_1 : \mytyp) \myeq ((\myb{x_2} {:} \mytya_2) \myarr \mytyb_2 : \mytyp) \myred \\
617 \myind{2} (\mytya_1 : \mytyp) \myeq (\mytya_2 : \mytyp) \myand \\
618 \myind{2} (\myb{x_1} : \mytya_1) \myarr (\myb{x_2} : \mytya_2) \myarr (\mytyb_1 : \mytyp) \myeq (\mytyb_2 : \mytyp)
622 Subtle point---I discovered a problem in the theory after
623 submitting... but I have a fix.
627 \frametitle{Bidirectional type checking}
629 \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A}\myappsp (\mytyc{List}\myappsp\myb{A})
632 With no type inference, we have explicit types for the constructors:
634 \begin{array}{@{}l@{\ }l}
635 \mydc{nil} & : (\myb{A} : \mytyp) \myarr \mytyc{List}\myappsp\myb{A} \\
636 \mydc{cons} &: (\myb{A} : \mytyp) \myarr \myb{A} \myarr \mytyc{List}\myappsp\myb{A} \myarr \mytyc{List}\myappsp\myb{A}\\
641 \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)))
643 Instead, annotate terms and propagate the type:
645 \mydc{cons}\myappsp 1 \myappsp (\mydc{cons}\myappsp 2 \myappsp (\mydc{cons} \myappsp 3 \myappsp \mydc{nil})) : \mytyc{List}\myappsp\mynat
647 Conversely, when we use eliminators the type can be inferred.
651 \frametitle{Bidirectional type checking}
653 This technique is known as \emph{bidirectional} type checking---some
654 terms get \emph{checked}, some terms \emph{infer} types.
656 Usually used for pre-defined types or core calculi, \mykant\ extends
657 to user-defined types.