presentation.tex

   1 \documentclass{beamer}
   2 \usepackage[sc,slantedGreek]{mathpazo}
   3
   4
   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
  12
  13 \usepackage{centernot}
  14 \usepackage{cancel}
  15 \usepackage{tikz}
  16 \usetikzlibrary{shapes,arrows,positioning}
  17 \usetikzlibrary{intersections}
  18 \pgfdeclarelayer{background}
  19 \pgfdeclarelayer{foreground}
  20 \pgfsetlayers{background,main,foreground}
  21
  22
  23 \setlength{\parindent}{0pt}
  24 \setlength{\parskip}{6pt plus 2pt minus 1pt}
  25 \setlength{\emergencystretch}{3em}  % prevent overfull lines
  26 \setcounter{secnumdepth}{0}
  27
  28 \usepackage[english]{babel}
  29 \usepackage[conor]{agda}
  30 \renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
  31 \renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
  32 \renewcommand{\AgdaField}{\AgdaFunction}
  33 % \definecolor{AgdaBound} {HTML}{000000}
  34 \definecolor{AgdaHole} {HTML} {FFFF33}
  35
  36 \DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
  37 \DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
  38 \DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
  39 \DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
  40 \DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
  41 \DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}
  42
  43 \newcommand{\mysmall}{}
  44 \newcommand{\mysyn}{\AgdaKeyword}
  45 \newcommand{\mytyc}[1]{\textup{\AgdaDatatype{#1}}}
  46 \newcommand{\mydc}[1]{\textup{\AgdaInductiveConstructor{#1}}}
  47 \newcommand{\myfld}[1]{\textup{\AgdaField{#1}}}
  48 \newcommand{\myfun}[1]{\textup{\AgdaFunction{#1}}}
  49 \newcommand{\myb}[1]{\AgdaBound{$#1$}}
  50 \newcommand{\myfield}{\AgdaField}
  51 \newcommand{\myind}{\AgdaIndent}
  52 \newcommand{\mykant}{{\rmfamily\scshape Bertus}}
  53 \newcommand{\mysynel}[1]{#1}
  54 \newcommand{\myse}{\mysynel}
  55 \newcommand{\mytmsyn}{\langle t \rangle}
  56 \newcommand{\mysp}{\ }
  57 \newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
  58 \newcommand{\myappsp}{\hspace{0.07cm}}
  59 \newcommand{\myapp}[2]{#1 \myappsp #2}
  60 \newcommand{\mysynsep}{\ \ |\ \ }
  61 \newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
  62 \newcommand{\mycumul}{\preceq}
  63
  64 \newcommand{\mydesc}[3]{
  65   \noindent
  66   \mbox{
  67     \parbox{\textwidth}{
  68       {\mysmall
  69         \vspace{0.2cm}
  70         \hfill \textup{\phantom{ygp}\textbf{#1}} $#2$
  71         \framebox[\textwidth]{
  72           \parbox{\textwidth}{
  73             \vspace{0.1cm}
  74             \centering{
  75               #3
  76             }
  77             \vspace{0.2cm}
  78           }
  79         }
  80         \vspace{0.2cm}
  81       }
  82     }
  83   }
  84 }
  85
  86 \newcommand{\mytmt}{\mysynel{t}}
  87 \newcommand{\mytmm}{\mysynel{m}}
  88 \newcommand{\mytmn}{\mysynel{n}}
  89 \newcommand{\myred}{\leadsto}
  90 \newcommand{\myredd}{\stackrel{*}{\leadsto}}
  91 \newcommand{\myreddd}{\stackrel{*}{\reflectbox{$\leadsto$}}}
  92 \newcommand{\mysub}[3]{#1[#3 / #2]}
  93 \newcommand{\mytysyn}{\langle ty \rangle}
  94 \newcommand{\mybasetys}{K}
  95 \newcommand{\mybasety}[1]{B_{#1}}
  96 \newcommand{\mytya}{\myse{A}}
  97 \newcommand{\mytyb}{\myse{B}}
  98 \newcommand{\mytycc}{\myse{C}}
  99 \newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
 100 \newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
 101 \newcommand{\myctx}{\Gamma}
 102 \newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
 103 \newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
 104 \newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
 105 \newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
 106 \newcommand{\mytt}{\mydc{$\langle\rangle$}}
 107 \newcommand{\myunit}{\mytyc{Unit}}
 108 \newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
 109 \newcommand{\myfst}{\myfld{fst}}
 110 \newcommand{\mysnd}{\myfld{snd}}
 111 \newcommand{\myconst}{\myse{c}}
 112 \newcommand{\myemptyctx}{\varepsilon}
 113 \newcommand{\myhole}{\AgdaHole}
 114 \newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
 115 \newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
 116 \newcommand{\myleft}[1]{\mydc{left}_{#1}}
 117 \newcommand{\myright}[1]{\mydc{right}_{#1}}
 118 \newcommand{\myempty}{\mytyc{Empty}}
 119 \newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
 120 \newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
 121 \newcommand{\myarg}{\_}
 122 \newcommand{\myderivsp}{}
 123 \newcommand{\myderivspp}{\vspace{0.3cm}}
 124 \newcommand{\mytyp}{\mytyc{Type}}
 125 \newcommand{\myneg}{\myfun{$\neg$}}
 126 \newcommand{\myar}{\,}
 127 \newcommand{\mybool}{\mytyc{Bool}}
 128 \newcommand{\mytrue}{\mydc{true}}
 129 \newcommand{\myfalse}{\mydc{false}}
 130 \newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
 131 \newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
 132 \newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
 133 \newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
 134 \newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
 135 \newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
 136 \newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
 137 \newcommand{\mynil}{\mydc{[]}}
 138 \newcommand{\mycons}{\mathbin{\mydc{∷}}}
 139 \newcommand{\myfoldr}{\myfun{foldr}}
 140 \newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
 141 \newcommand{\mynodee}{\mathbin{\mydc{$\lhd$}}}
 142 \newcommand{\mynode}[2]{\mynodee_{#1.#2}}
 143 \newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
 144 \newcommand{\mylub}{\sqcup}
 145 \newcommand{\mydefeq}{\cong}
 146 \newcommand{\myrefl}{\mydc{refl}}
 147 \newcommand{\mypeq}{\mytyc{=}}
 148 \newcommand{\myjeqq}{\myfun{$=$-elim}}
 149 \newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
 150 \newcommand{\mysubst}{\myfun{subst}}
 151 \newcommand{\myprsyn}{\myse{prop}}
 152 \newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathclose{\mytyc{$\rrbracket$}}}
 153 \newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
 154 \newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
 155 \newcommand{\myprfora}[3]{\forall #1 {:} #2.\, #3}
 156 \newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
 157 \newcommand{\mybot}{\mytyc{$\bot$}}
 158 \newcommand{\mytop}{\mytyc{$\top$}}
 159 \newcommand{\mycoe}{\myfun{coe}}
 160 \newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
 161 \newcommand{\mycoh}{\myfun{coh}}
 162 \newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
 163 \newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
 164 \newcommand{\myeq}{\mathrel{\mytyc{=}}}
 165 \newcommand{\myprop}{\mytyc{Prop}}
 166 \newcommand{\mytmup}{\mytmsyn\uparrow}
 167 \newcommand{\mydefs}{\Delta}
 168 \newcommand{\mynf}{\Downarrow}
 169 \newcommand{\myinff}[3]{#1 \vdash #2 \Uparrow #3}
 170 \newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
 171 \newcommand{\mychkk}[3]{#1 \vdash #2 \Downarrow #3}
 172 \newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
 173 \newcommand{\myann}[2]{#1 : #2}
 174 \newcommand{\mydeclsyn}{\myse{decl}}
 175 \newcommand{\myval}[3]{#1 : #2 \mapsto #3}
 176 \newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2}
 177 \newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
 178 \newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
 179 \newcommand{\myelabt}{\vdash}
 180 \newcommand{\myelabf}{\rhd}
 181 \newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
 182 \newcommand{\mytele}{\Delta}
 183 \newcommand{\mytelee}{\delta}
 184 \newcommand{\mydcctx}{\Gamma}
 185 \newcommand{\mynamesyn}{\myse{name}}
 186 \newcommand{\myvec}{\overrightarrow}
 187 \newcommand{\mymeta}{\textsc}
 188 \newcommand{\myhyps}{\mymeta{hyps}}
 189 \newcommand{\mycc}{;}
 190 \newcommand{\myemptytele}{\varepsilon}
 191 \newcommand{\mymetagoes}{\Longrightarrow}
 192 % \newcommand{\mytesctx}{\
 193 \newcommand{\mytelesyn}{\myse{telescope}}
 194 \newcommand{\myrecs}{\mymeta{recs}}
 195 \newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
 196 \newcommand{\mylet}{\mysyn{let}}
 197 \newcommand{\myhead}{\mymeta{head}}
 198 \newcommand{\mytake}{\mymeta{take}}
 199 \newcommand{\myix}{\mymeta{ix}}
 200 \newcommand{\myapply}{\mymeta{apply}}
 201 \newcommand{\mydataty}{\mymeta{datatype}}
 202 \newcommand{\myisreco}{\mymeta{record}}
 203 \newcommand{\mydcsep}{\ |\ }
 204 \newcommand{\mytree}{\mytyc{Tree}}
 205 \newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
 206 \newcommand{\mysigma}{\mytyc{$\Sigma$}}
 207 \newcommand{\mynegder}{\vspace{-0.3cm}}
 208 \newcommand{\myquot}{\Uparrow}
 209 \newcommand{\mynquot}{\, \Downarrow}
 210 \newcommand{\mycanquot}{\ensuremath{\textsc{quote}{\Downarrow}}}
 211 \newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Uparrow}}}
 212 \newcommand{\mymetaguard}{\ |\ }
 213 \newcommand{\mybox}{\Box}
 214 \newcommand{\mytermi}[1]{\text{\texttt{#1}}}
 215 \newcommand{\mysee}[1]{\langle\myse{#1}\rangle}
 216 \newcommand{\mycomp}{\mathbin{\myfun{$\circ$}}}
 217 \newcommand{\mylist}[1]{\mytyc{List}\myappsp #1}
 218 \newcommand{\mylistt}[1]{\mathopen{\mydc{$[$}} #1 \mathclose{\mydc{$]$}}}
 219 \newcommand{\myplus}{\mathbin{\myfun{$+$}}}
 220 \newcommand{\mytimes}{\mathbin{\myfun{$*$}}}
 221 \newcommand{\mysuc}{\mydc{suc}}
 222 \newcommand{\myzero}{\mydc{zero}}
 223
 224 \renewcommand{\[}{\begin{equation*}}
 225 \renewcommand{\]}{\end{equation*}}
 226 \newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}}
 227
 228 \title{\mykant: Implementing Observational Equality}
 229 \author{Francesco Mazzoli \texttt{<fm2209@ic.ac.uk>}}
 230 \date{June 2013}
 231
 232 \begin{document}
 233 \frame{\titlepage}
 234
 235 \begin{frame}
 236   \frametitle{\mykant?}
 237
 238   \mykant\ is an \emph{interactive theorem prover}/\emph{functional
 239     programming language}, implemented in Haskell.
 240
 241   It is in the tradition of Agda and Epigram (and to a lesser extent
 242   Coq), but with a more powerful notion of \emph{equality}.
 243
 244   We have figured out theory of \mykant, and have a near-complete
 245   implementation.
 246 \end{frame}
 247
 248 \begin{frame}
 249   \frametitle{Theorem provers are short-sighted}
 250
 251   Two functions dear to the Haskell practitioner:
 252   \[
 253   \begin{array}{@{}l}
 254     \myfun{map} : (\myb{a} \myarr \myb{b}) \myarr \mylist{\myb{a}} \myarr \mylist{\myb{b}} \\
 255       \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l}
 256         \myfun{map} & \myb{f} & \mynil & = & \mynil \\
 257         \myfun{map} & \myb{f} & (\myb{x} \mycons \myb{xs}) & = & \myapp{\myb{f}}{\myb{x}} \mycons \myfun{map} \myappsp \myb{f} \myappsp \myb{xs} \\
 258       \end{array}
 259       \\
 260       \ \\
 261     (\myfun{${\circ}$}) : (\myb{b} \myarr \myb{c}) \myarr (\myb{a} \myarr \myb{b}) \myarr (\myb{a} \myarr \myb{c}) \\
 262     (\myb{f} \mathbin{\myfun{$\circ$}} \myb{g}) \myappsp \myb{x} = \myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}
 263   \end{array}
 264   \]
 265 \end{frame}
 266
 267 \begin{frame}
 268   \frametitle{Theorem provers are short-sighted}
 269   $\myfun{map}$'s composition law states that:
 270   \[
 271     \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})
 272   \]
 273   We can convince Coq or Agda that
 274   \[
 275     \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}
 276   \]
 277   But we cannot get rid of the $\myb{l}$.  Why?
 278 \end{frame}
 279
 280 \begin{frame}
 281   \frametitle{\mykant\ and observational equality}
 282
 283   \emph{Observational} equality solves this and other annoyances.
 284
 285   \mykant\ is a system aiming at making observational equality more
 286   usable.
 287 \end{frame}
 288
 289 \begin{frame}
 290   \frametitle{Theorem provers, dependent types}
 291   \begin{center}
 292     \Huge
 293     types $\leftrightarrow$ propositions
 294
 295     programs $\leftrightarrow$ proofs
 296   \end{center}
 297 \end{frame}
 298
 299 \begin{frame}
 300   \frametitle{Theorem provers, dependent types}
 301   \[
 302   \begin{array}{@{}l@{\ \ \ }l}
 303     \mysyn{data}\ \myempty & \text{No members.} \\
 304     \mysyn{data}\ \myunit \mapsto \mytt & \text{One member.}
 305   \end{array}
 306   \]
 307
 308   $\myunit$ is trivially inhabitable: it corresponds to $\top$ in
 309   logic.
 310   \[
 311   \mytt : \myunit
 312   \]
 313   $\myempty$ is \emph{not} inhabitable: it corresponds to $\bot$.
 314   \[
 315   \myfun{absurd} : \myempty \myarr \myb{A}
 316   \]
 317
 318   First class types: we can return them, have them as arguments, etc:
 319   $\myempty : \mytyp$, $\myunit : \mytyp$.
 320 \end{frame}
 321
 322 \begin{frame}
 323   \frametitle{Theorem provers, dependent types}
 324   \[ \mysyn{data}\ \mylist{\myb{A}} \mapsto \mynil \mydcsep \myb{A} \mycons \mylist{\myb{A}} \]
 325   We want to express a `non-emptiness' property for lists:
 326   \[
 327   \begin{array}{@{}l}
 328     \myfun{non-empty} : \mylist{\myb{A}} \myarr \mytyp \\
 329     \begin{array}{@{}l@{\myappsp}c@{\ }l}
 330     \myfun{non-empty} & \mynil & \mapsto \myempty \\
 331     \myfun{non-empty} & (\myb{x} \mycons \myb{l}) & \mapsto \myunit
 332     \end{array}
 333   \end{array}
 334   \]
 335
 336   A term of type $\myfun{non-empty} \myappsp \myb{l}$ represents a
 337   \emph{proof} that $\myb{l}$ is indeed not empty.
 338   \[
 339   \begin{array}{@{}l@{\ \ \ }l}
 340     \text{Can't prove} & \myfun{non-empty}\myappsp \mynil \myred \myempty \\
 341     \text{Trivial to prove}  & \myfun{non-empty}\myappsp(2 \mycons \mynil) \myred \myunit
 342   \end{array}
 343   \]
 344 \end{frame}
 345
 346 \begin{frame}
 347   \frametitle{Example: safe $\myfun{head}$ function}
 348   \only<3>{We can eliminate the `empty list' case:}
 349   \[
 350   \begin{array}{@{}l}
 351     \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{non-empty}\myappsp\myb{l} \myarr \myb{A}} \\
 352     \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l}
 353       \myfun{head} & \mynil & \myb{p} & \mapsto & \only<1,2>{\myhole{?}}\only<3>{\myabsurd\myappsp\myb{p}} \\
 354       \myfun{head} & (\myb{x} \mycons \myb{xs}) & \myb{p} & \mapsto & \myb{x}
 355     \end{array}
 356   \end{array}
 357   \]
 358
 359   \only<1>{
 360     The logic equivalent would be
 361     \[
 362     \forall \myb{l} {:} \mylist{\myb{A}}.\ \myfun{non-empty}\myappsp\myb{l} \myarr \myb{A}
 363     \]
 364     `For all non-empty lists of type $\myb{A}$, we can get an element of $\myb{A}$.'
 365   }
 366   \only<2>{
 367   The type of $\myb{p}$ in the $\myhole{?}$ is $\myempty$, since
 368   \[\myfun{non-empty}\myappsp\mynil \myred \myempty \]}
 369   \only<3>{
 370     Remember:
 371     \[ \myfun{absurd} : \myempty \myarr \myb{A} \]
 372   }
 373 \end{frame}
 374
 375 \begin{frame}
 376   \frametitle{How do we type check this thing?}
 377   \[\text{Is\ } \myfun{non-empty}\myappsp(3 \mycons \mynil) \text{\ the same as\ } \myunit\text{?}\]
 378   Or in other words, is
 379   \[ \mytt : \myunit \]
 380   A valid argument to
 381   \[
 382   \myfun{head} \myappsp (3 \mycons \mynil) : \myfun{non-empty}\myappsp(3 \mycons \mynil) \myarr \mynat
 383   \]
 384
 385   Yes: to typecheck, we reduce terms fully (to their \emph{normal form})
 386   before comparing:
 387   \[
 388   \begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}
 389     \myunit & \myredd & \myunit & \mydefeq & \myunit & \myreddd & \myfun{non-empty}\myappsp(3 \mycons \mynil) \\
 390     (\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 \\
 391     & & & \vdots & & &
 392   \end{array}
 393   \]
 394   \[
 395   \mydefeq\ \text{takes the name of \textbf{definitional equality}.}
 396   \]
 397 \end{frame}
 398
 399 \begin{frame}
 400   \frametitle{Propositional equality} Using definitional equality, we
 401   can give the user a type-level notion of term equality.
 402   \[
 403   (\myeq) : \myb{A} \myarr \myb{A} \myarr \mytyp\ \ \ \text{internalises equality \textbf{as a type}}
 404   \]
 405   We introduce members of $\myeq$ by reflexivity, for example
 406   \[
 407   \myrefl\myappsp5 : 5 \myeq 5
 408   \]
 409   But also
 410   \[
 411   \begin{array}{@{}l}
 412   \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\text{, since}\\
 413   (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5
 414   \end{array}
 415   \]
 416   Then we can use a substitution law to derive other
 417   laws---transitivity, congruence, etc.
 418   \[ \myeq\ \text{takes the name of \textbf{propositional equality}} \]
 419 \end{frame}
 420
 421 \begin{frame}
 422 \frametitle{The problem with prop. equality}
 423 Going back to $\myfun{map}$, we can prove that
 424 \[    \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}    \]
 425 Because
 426 \[
 427 (\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}
 428 \]
 429 By induction on $\myb{l}$.
 430
 431 Without the $\myb{l}$ we cannot compute, so we are stuck with
 432 \[
 433 \myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} \not\mydefeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g})
 434 \]
 435 \end{frame}
 436
 437 \begin{frame}
 438   \frametitle{Observational equality}
 439
 440   Instead of basing its equality on definitional equality, look at the
 441   structure of the type to decide.
 442
 443   For functions this will mean that proving
 444   \[
 445     \myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g} \myeq \myfun{map}\myappsp (\myse{f} \mycomp \myse{g})
 446   \]
 447   Will reduce to proving that
 448   \[
 449   (\myb{l} : \mylist{\myb{A}}) \myarr
 450     (\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}
 451   \]
 452   Which is what we want.  The interesting part is how to make the system
 453   compute nicely.
 454 \end{frame}
 455
 456 \begin{frame}
 457   \begin{center}
 458     {\huge \mykant' features}
 459   \end{center}
 460 \end{frame}
 461
 462 \begin{frame}
 463   \frametitle{Inductive data}
 464   \[
 465   \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mynil \mydcsep \myb{A} \mycons \mytyc{List}\myappsp\myb{A}
 466   \]
 467   Each with an induction principle:
 468   \[
 469   \begin{array}{@{}l@{\ }l}
 470     \mytyc{List}.\myfun{elim} : & \AgdaComment{-{}- The property that we want to prove:} \\
 471      & (\myb{P} : \mytyc{List}\myappsp\myb{A} \myarr \mytyp) \myarr \\
 472      & \AgdaComment{-{}- If it holds for the base case:} \\
 473     & \myb{P} \myappsp \mynil \myarr \\
 474     & \AgdaComment{-{}- And for the inductive step:} \\
 475     & ((\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 \\
 476     & \AgdaComment{-{}- Then it holds for every list:} \\
 477     & (\myb{l} : \mytyc{List}\myappsp\myb{A}) \myarr \myb{P} \myappsp \myb{l}
 478   \end{array}
 479   \]
 480   Induction is also computation, via structural recursion:
 481   \[
 482   \begin{array}{@{}l@{\ }l}
 483     \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp \mynil & \myred \myse{pn} \\
 484     \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp (\mytmm \mycons \mytmn) & \myred \myse{pc} \myappsp \mytmm \myappsp \mytmn \myappsp (\mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{ps} \myappsp \mytmn )
 485   \end{array}
 486   \]
 487 \end{frame}
 488
 489 \begin{frame}
 490   \frametitle{Dependent defined types} \emph{Unlike} Haskell, we can
 491   have fields of a data constructor to depend on earlier fields:
 492   \[
 493   \begin{array}{@{}l}
 494     \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp\myhole{$(\myb{B} : \myb{A} \myarr \mytyp)$} \mapsto \\
 495     \myind{2}\mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B}\myappsp\myb{fst} \}
 496   \end{array}
 497   \]
 498
 499   The \emph{type} of the second element depends on the \emph{value} of
 500   the first:
 501   \[
 502   \begin{array}{@{}l@{\ }l}
 503     \myfun{fst} & : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\
 504     \myfun{snd} & : (\myb{x} : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B}) \myarr \myb{B} \myappsp (\myfun{fst} \myappsp \myb{x})
 505   \end{array}
 506   \]
 507   Where the projection's reduction rules are predictably
 508   \[
 509   \begin{array}{@{}l@{\ }l}
 510     \myfun{fst}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmm \\
 511     \myfun{snd}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmn \\
 512   \end{array}
 513   \]
 514 \end{frame}
 515
 516 \begin{frame}
 517   \frametitle{Example: the type of even numbers}
 518   For example we can define the type of even numbers:
 519   % TODO fix
 520   \[
 521   \begin{array}{@{}l}
 522     \mysyn{data}\ \mynat \mapsto \mydc{zero} \mydcsep \mydc{suc}\myappsp\mynat \\
 523     \ \\
 524     \myfun{even} : \mynat \myarr \mytyp \\
 525     \begin{array}{@{}l@{\myappsp}c@{\ }l}
 526       \myfun{even} & \myzero & \mapsto \myunit \\
 527       \myfun{even} & (\mysuc \myappsp \myzero) & \mapsto \myempty \\
 528       \myfun{even} & (\mysuc \myappsp (\mysuc \myappsp \myb{n})) & \mapsto \myfun{even} \myappsp \myb{n}
 529     \end{array} \\
 530     \ \\
 531     \mytyc{Even} : \mytyp \\
 532     \mytyc{Even} \mapsto \mytyc{Tuple}\ \mynat\ \myfun{even}
 533   \end{array}
 534   \]
 535 \end{frame}
 536
 537 \begin{frame}
 538   \frametitle{Type hierarchy}
 539   \[\{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp\]
 540   What is the type of $\mytyp$?
 541   \[
 542   \cancel{\mytyp : \mytyp}\ \ \ \text{\textbf{inconsistent}}
 543   \]
 544   Similar to Russel's paradox in na{\"i}ve set theory.
 545
 546   Instead, we have a hierarchy:
 547   \[
 548   \{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp_0 : \mytyp_1 : \cdots
 549   \]
 550   We talk of types in $\mytyp_0$ as `smaller' than types in $\mytyp_1$.
 551 \end{frame}
 552
 553 \begin{frame}
 554   \frametitle{Cumulativity and typical ambiguity}
 555   Instead of:
 556   \[ \mytyp_0 : \mytyp_1 \ \ \ \text{but}\ \ \ \mytyp_0 \centernot{:} \mytyp_2\]
 557   We have a cumulative hierarchy, so that
 558   \[ \mytyp_n : \mytyp_m \ \ \ \text{iff}\ \ \ n < m \]
 559   For example
 560   \[ \mynat : \mytyp_0\ \ \ \text{and}\ \ \ \mynat : \mytyp_1\ \ \ \text{and}\ \ \ \mynat : \mytyp_{50} \]
 561
 562   But in \mykant, you can forget about levels: the consistency is
 563   checked automatically---a mechanised version of what Russell called
 564   \emph{typical ambiguity}.
 565
 566   \begin{center}
 567     \begin{tikzpicture}[remember picture, node distance=1.5cm]
 568       \begin{pgfonlayer}{foreground}
 569       % Place nodes
 570       \node (x) {$x$};
 571       \node [right of=x] (y) {$y$};
 572       \node [right of=y] (z) {$z$};
 573       \node [below of=z] (k) {$k$};
 574       \node [left  of=k] (j) {$j$};
 575       %% Lines
 576       \path[->]
 577       (x) edge node [above] {$<$}   (y)
 578       (y) edge node [above] {$\le$} (z)
 579       (z) edge node [right] {$<$}   (k)
 580       (k) edge node [below] {$\le$} (j)
 581       (j) edge node [left ] {$\le$} (y);
 582     \end{pgfonlayer}{foreground}
 583     \end{tikzpicture}
 584     \begin{tikzpicture}[remember picture, overlay]
 585       \begin{pgfonlayer}{background}
 586       \fill [red, opacity=0.3, rounded corners]
 587       (-2.7,2.6) rectangle (-0.2,0.05)
 588       (-4.1,2.4) rectangle (-3.3,1.6);
 589     \end{pgfonlayer}{background}
 590     \end{tikzpicture}
 591   \end{center}
 592 \end{frame}
 593
 594 \begin{frame}
 595   \frametitle{Bidirectional type checking}
 596   \[
 597   \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A}\myappsp (\mytyc{List}\myappsp\myb{A})
 598   \]
 599
 600   With no type inference, we have explicit types for the constructors:
 601   \[
 602   \begin{array}{@{}l@{\ }l}
 603     \mydc{nil} & : (\myb{A} : \mytyp) \myarr \mytyc{List}\myappsp\myb{A} \\
 604     \mydc{cons} &: (\myb{A} : \mytyp) \myarr \myb{A} \myarr \mytyc{List}\myappsp\myb{A} \myarr \mytyc{List}\myappsp\myb{A}\\
 605   \end{array}
 606   \]
 607   ...ugh:
 608   \[
 609   \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)))
 610   \]
 611   Instead, annotate terms and propagate the type:
 612   \[
 613   \mydc{cons}\myappsp 1 \myappsp (\mydc{cons}\myappsp 2 \myappsp (\mydc{cons} \myappsp 3 \myappsp \mydc{nil})) : \mytyc{List}\myappsp\mynat
 614   \]
 615   Conversely, when we use eliminators the type can be inferred.
 616 \end{frame}
 617
 618 \begin{frame}
 619   \frametitle{OTT + user defined types}
 620
 621   For each type, we need to:
 622   \begin{itemize}
 623   \item Describe when two types formed by the defined type constructors
 624     are equal;
 625     \[ \mylist{\mytya_1} \myeq \mylist{\mytya_2} \]
 626   \item Describe when two values of the defined type are equal;
 627     \[
 628     \begin{array}{@{}c@{\ \ \ \ \ \ }c}
 629       \mynil \myeq \mynil & \mynil \myeq \mytmm \mycons \mytmn \\
 630       \mytmm \mycons \mytmn \myeq \mynil & \mytmm_1 \mycons \mytmn_1 \myeq \mytmm_2 \mycons \mytmn_2
 631     \end{array}
 632     \]
 633   \item Describe how to transport values of the defined type.
 634   \end{itemize}
 635 \end{frame}
 636
 637 \begin{frame}
 638   \frametitle{OTT + hierarchy}
 639
 640   Since equalities reduce to functions abstracting over various things,
 641   we need to make sure that the hierarchy is respected.
 642
 643   For example we have that
 644   \[
 645   \begin{array}{@{}l}
 646     \myjm{(\myb{x_1} {:} \mytya_1) \myarr \mytyb_1}{\mytyp}{(\myb{x_2} {:} \mytya_2) \myarr \mytyb_2}{\mytyp} \myred \\
 647     \myind{2} \myjm{\mytya_1}{\mytyp}{\mytya_2}{\mytyp} \myand  \\
 648     \myind{2} ((\myb{x_1} : \mytya_1) \myarr (\myb{x_2} : \mytya_2) \myarr \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myarr \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}])
 649   \end{array}
 650   \]
 651
 652   Subtle point---I discovered a problem in the theory after
 653   submitting... but I have a fix.
 654 \end{frame}
 655
 656 \begin{frame}
 657   \frametitle{Bonus!  WebSocket prompt}
 658   \url{http://bertus.mazzo.li}, go DDOS it!
 659
 660   \includegraphics[width=\textwidth]{web-prompt.png}
 661 \end{frame}
 662
 663 \begin{frame}
 664 \begin{center}
 665 {\Huge Demo}
 666 \end{center}
 667 \end{frame}
 668
 669 \begin{frame}
 670   \frametitle{What have we done?}
 671
 672   \begin{itemize}
 673     \item A small theorem prover for intuitionistic logic, featuring:
 674     \item Inductive data and record types;
 675     \item A cumulative, implicit type hierarchy;
 676     \item Partial type inference---bidirectional type checking;
 677     \item Type holes;
 678     \item Observational equality---coming soon to the implementation.
 679   \end{itemize}
 680 \end{frame}
 681
 682 \begin{frame}
 683   \frametitle{Further work}
 684
 685   \begin{itemize}
 686     \item Pattern matching and explicit recursion
 687     \item More expressive data types
 688     \item Inference via unification
 689     \item Codata
 690   \end{itemize}
 691 \end{frame}
 692
 693 \begin{frame}
 694 \begin{center}
 695 {\Huge Questions?}
 696 \end{center}
 697 \end{frame}
 698
 699 \end{document}