...

[bitonic-mengthesis.git] / presentation.tex

\documentclass{beamer}
\usepackage[sc,slantedGreek]{mathpazo}


% Comment these out if you don't want a slide with just the
% part/section/subsection/subsubsection title:
\AtBeginPart{\frame{\partpage}}
\AtBeginSection{\frame{\sectionpage}}
\AtBeginSubsection{\frame{\subsectionpage}}
\AtBeginSubsubsection{\frame{\subsubsectionpage}}
\beamertemplatenavigationsymbolsempty

\usepackage{centernot}
\usepackage{cancel}

\setlength{\parindent}{0pt}
\setlength{\parskip}{6pt plus 2pt minus 1pt}
\setlength{\emergencystretch}{3em}  % prevent overfull lines
\setcounter{secnumdepth}{0}

\usepackage[english]{babel}
\usepackage[conor]{agda}
\renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
\renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
\renewcommand{\AgdaField}{\AgdaFunction}
% \definecolor{AgdaBound} {HTML}{000000}
\definecolor{AgdaHole} {HTML} {FFFF33}

\DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}
\DeclareUnicodeCharacter{964}{\ensuremath{\tau}}
\DeclareUnicodeCharacter{963}{\ensuremath{\sigma}}
\DeclareUnicodeCharacter{915}{\ensuremath{\Gamma}}
\DeclareUnicodeCharacter{8799}{\ensuremath{\stackrel{?}{=}}}
\DeclareUnicodeCharacter{9655}{\ensuremath{\rhd}}

\newcommand{\mysmall}{}
\newcommand{\mysyn}{\AgdaKeyword}
\newcommand{\mytyc}[1]{\textup{\AgdaDatatype{#1}}}
\newcommand{\mydc}[1]{\textup{\AgdaInductiveConstructor{#1}}}
\newcommand{\myfld}[1]{\textup{\AgdaField{#1}}}
\newcommand{\myfun}[1]{\textup{\AgdaFunction{#1}}}
\newcommand{\myb}[1]{\AgdaBound{$#1$}}
\newcommand{\myfield}{\AgdaField}
\newcommand{\myind}{\AgdaIndent}
\newcommand{\mykant}{{\rmfamily\scshape Bertus}}
\newcommand{\mysynel}[1]{#1}
\newcommand{\myse}{\mysynel}
\newcommand{\mytmsyn}{\langle t \rangle}
\newcommand{\mysp}{\ }
\newcommand{\myabs}[2]{\mydc{$\lambda$} #1 \mathrel{\mydc{$\mapsto$}} #2}
\newcommand{\myappsp}{\hspace{0.07cm}}
\newcommand{\myapp}[2]{#1 \myappsp #2}
\newcommand{\mysynsep}{\ \ |\ \ }
\newcommand{\myITE}[3]{\myfun{If}\, #1\, \myfun{Then}\, #2\, \myfun{Else}\, #3}
\newcommand{\mycumul}{\preceq}

\newcommand{\mydesc}[3]{
  \noindent
  \mbox{
    \parbox{\textwidth}{
      {\mysmall
        \vspace{0.2cm}
        \hfill \textup{\phantom{ygp}\textbf{#1}} $#2$
        \framebox[\textwidth]{
          \parbox{\textwidth}{
            \vspace{0.1cm}
            \centering{
              #3
            }
            \vspace{0.2cm}
          }
        }
        \vspace{0.2cm}
      }
    }
  }
}

\newcommand{\mytmt}{\mysynel{t}}
\newcommand{\mytmm}{\mysynel{m}}
\newcommand{\mytmn}{\mysynel{n}}
\newcommand{\myred}{\leadsto}
\newcommand{\myredd}{\stackrel{*}{\leadsto}}
\newcommand{\myreddd}{\stackrel{*}{\reflectbox{$\leadsto$}}}
\newcommand{\mysub}[3]{#1[#3 / #2]}
\newcommand{\mytysyn}{\langle ty \rangle}
\newcommand{\mybasetys}{K}
\newcommand{\mybasety}[1]{B_{#1}}
\newcommand{\mytya}{\myse{A}}
\newcommand{\mytyb}{\myse{B}}
\newcommand{\mytycc}{\myse{C}}
\newcommand{\myarr}{\mathrel{\textcolor{AgdaDatatype}{\to}}}
\newcommand{\myprod}{\mathrel{\textcolor{AgdaDatatype}{\times}}}
\newcommand{\myctx}{\Gamma}
\newcommand{\myvalid}[1]{#1 \vdash \underline{\mathrm{valid}}}
\newcommand{\myjudd}[3]{#1 \vdash #2 : #3}
\newcommand{\myjud}[2]{\myjudd{\myctx}{#1}{#2}}
\newcommand{\myabss}[3]{\mydc{$\lambda$} #1 {:} #2 \mathrel{\mydc{$\mapsto$}} #3}
\newcommand{\mytt}{\mydc{$\langle\rangle$}}
\newcommand{\myunit}{\mytyc{Unit}}
\newcommand{\mypair}[2]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #2\mathclose{\mydc{$\rangle$}}}
\newcommand{\myfst}{\myfld{fst}}
\newcommand{\mysnd}{\myfld{snd}}
\newcommand{\myconst}{\myse{c}}
\newcommand{\myemptyctx}{\varepsilon}
\newcommand{\myhole}{\AgdaHole}
\newcommand{\myfix}[3]{\mysyn{fix} \myappsp #1 {:} #2 \mapsto #3}
\newcommand{\mysum}{\mathbin{\textcolor{AgdaDatatype}{+}}}
\newcommand{\myleft}[1]{\mydc{left}_{#1}}
\newcommand{\myright}[1]{\mydc{right}_{#1}}
\newcommand{\myempty}{\mytyc{Empty}}
\newcommand{\mycase}[2]{\mathopen{\myfun{[}}#1\mathpunct{\myfun{,}} #2 \mathclose{\myfun{]}}}
\newcommand{\myabsurd}[1]{\myfun{absurd}_{#1}}
\newcommand{\myarg}{\_}
\newcommand{\myderivsp}{}
\newcommand{\myderivspp}{\vspace{0.3cm}}
\newcommand{\mytyp}{\mytyc{Type}}
\newcommand{\myneg}{\myfun{$\neg$}}
\newcommand{\myar}{\,}
\newcommand{\mybool}{\mytyc{Bool}}
\newcommand{\mytrue}{\mydc{true}}
\newcommand{\myfalse}{\mydc{false}}
\newcommand{\myitee}[5]{\myfun{if}\,#1 / {#2.#3}\,\myfun{then}\,#4\,\myfun{else}\,#5}
\newcommand{\mynat}{\mytyc{$\mathbb{N}$}}
\newcommand{\myrat}{\mytyc{$\mathbb{R}$}}
\newcommand{\myite}[3]{\myfun{if}\,#1\,\myfun{then}\,#2\,\myfun{else}\,#3}
\newcommand{\myfora}[3]{(#1 {:} #2) \myarr #3}
\newcommand{\myexi}[3]{(#1 {:} #2) \myprod #3}
\newcommand{\mypairr}[4]{\mathopen{\mydc{$\langle$}}#1\mathpunct{\mydc{,}} #4\mathclose{\mydc{$\rangle$}}_{#2{.}#3}}
\newcommand{\mynil}{\mydc{[]}}
\newcommand{\mycons}{\mathbin{\mydc{∷}}}
\newcommand{\myfoldr}{\myfun{foldr}}
\newcommand{\myw}[3]{\myapp{\myapp{\mytyc{W}}{(#1 {:} #2)}}{#3}}
\newcommand{\mynodee}{\mathbin{\mydc{$\lhd$}}}
\newcommand{\mynode}[2]{\mynodee_{#1.#2}}
\newcommand{\myrec}[4]{\myfun{rec}\,#1 / {#2.#3}\,\myfun{with}\,#4}
\newcommand{\mylub}{\sqcup}
\newcommand{\mydefeq}{\cong}
\newcommand{\myrefl}{\mydc{refl}}
\newcommand{\mypeq}{\mytyc{=}}
\newcommand{\myjeqq}{\myfun{$=$-elim}}
\newcommand{\myjeq}[3]{\myapp{\myapp{\myapp{\myjeqq}{#1}}{#2}}{#3}}
\newcommand{\mysubst}{\myfun{subst}}
\newcommand{\myprsyn}{\myse{prop}}
\newcommand{\myprdec}[1]{\mathopen{\mytyc{$\llbracket$}} #1 \mathclose{\mytyc{$\rrbracket$}}}
\newcommand{\myand}{\mathrel{\mytyc{$\wedge$}}}
\newcommand{\mybigand}{\mathrel{\mytyc{$\bigwedge$}}}
\newcommand{\myprfora}[3]{\forall #1 {:} #2.\, #3}
\newcommand{\myimpl}{\mathrel{\mytyc{$\Rightarrow$}}}
\newcommand{\mybot}{\mytyc{$\bot$}}
\newcommand{\mytop}{\mytyc{$\top$}}
\newcommand{\mycoe}{\myfun{coe}}
\newcommand{\mycoee}[4]{\myapp{\myapp{\myapp{\myapp{\mycoe}{#1}}{#2}}{#3}}{#4}}
\newcommand{\mycoh}{\myfun{coh}}
\newcommand{\mycohh}[4]{\myapp{\myapp{\myapp{\myapp{\mycoh}{#1}}{#2}}{#3}}{#4}}
\newcommand{\myjm}[4]{(#1 {:} #2) \mathrel{\mytyc{=}} (#3 {:} #4)}
\newcommand{\myeq}{\mathrel{\mytyc{=}}}
\newcommand{\myprop}{\mytyc{Prop}}
\newcommand{\mytmup}{\mytmsyn\uparrow}
\newcommand{\mydefs}{\Delta}
\newcommand{\mynf}{\Downarrow}
\newcommand{\myinff}[3]{#1 \vdash #2 \Uparrow #3}
\newcommand{\myinf}[2]{\myinff{\myctx}{#1}{#2}}
\newcommand{\mychkk}[3]{#1 \vdash #2 \Downarrow #3}
\newcommand{\mychk}[2]{\mychkk{\myctx}{#1}{#2}}
\newcommand{\myann}[2]{#1 : #2}
\newcommand{\mydeclsyn}{\myse{decl}}
\newcommand{\myval}[3]{#1 : #2 \mapsto #3}
\newcommand{\mypost}[2]{\mysyn{abstract}\ #1 : #2}
\newcommand{\myadt}[4]{\mysyn{data}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
\newcommand{\myreco}[4]{\mysyn{record}\ #1 #2\ \mysyn{where}\ #3\{ #4 \}}
\newcommand{\myelabt}{\vdash}
\newcommand{\myelabf}{\rhd}
\newcommand{\myelab}[2]{\myctx \myelabt #1 \myelabf #2}
\newcommand{\mytele}{\Delta}
\newcommand{\mytelee}{\delta}
\newcommand{\mydcctx}{\Gamma}
\newcommand{\mynamesyn}{\myse{name}}
\newcommand{\myvec}{\overrightarrow}
\newcommand{\mymeta}{\textsc}
\newcommand{\myhyps}{\mymeta{hyps}}
\newcommand{\mycc}{;}
\newcommand{\myemptytele}{\varepsilon}
\newcommand{\mymetagoes}{\Longrightarrow}
% \newcommand{\mytesctx}{\
\newcommand{\mytelesyn}{\myse{telescope}}
\newcommand{\myrecs}{\mymeta{recs}}
\newcommand{\myle}{\mathrel{\lcfun{$\le$}}}
\newcommand{\mylet}{\mysyn{let}}
\newcommand{\myhead}{\mymeta{head}}
\newcommand{\mytake}{\mymeta{take}}
\newcommand{\myix}{\mymeta{ix}}
\newcommand{\myapply}{\mymeta{apply}}
\newcommand{\mydataty}{\mymeta{datatype}}
\newcommand{\myisreco}{\mymeta{record}}
\newcommand{\mydcsep}{\ |\ }
\newcommand{\mytree}{\mytyc{Tree}}
\newcommand{\myproj}[1]{\myfun{$\pi_{#1}$}}
\newcommand{\mysigma}{\mytyc{$\Sigma$}}
\newcommand{\mynegder}{\vspace{-0.3cm}}
\newcommand{\myquot}{\Uparrow}
\newcommand{\mynquot}{\, \Downarrow}
\newcommand{\mycanquot}{\ensuremath{\textsc{quote}{\Downarrow}}}
\newcommand{\myneuquot}{\ensuremath{\textsc{quote}{\Uparrow}}}
\newcommand{\mymetaguard}{\ |\ }
\newcommand{\mybox}{\Box}
\newcommand{\mytermi}[1]{\text{\texttt{#1}}}
\newcommand{\mysee}[1]{\langle\myse{#1}\rangle}
\newcommand{\mycomp}{\mathbin{\myfun{$\circ$}}}
\newcommand{\mylist}[1]{\mytyc{List}\myappsp #1}
\newcommand{\mylistt}[1]{\mathopen{\mydc{$[$}} #1 \mathclose{\mydc{$]$}}}
\newcommand{\myplus}{\mathbin{\myfun{$+$}}}
\newcommand{\mytimes}{\mathbin{\myfun{$*$}}}
\newcommand{\mysuc}{\mydc{suc}}
\newcommand{\myzero}{\mydc{zero}}

\renewcommand{\[}{\begin{equation*}}
\renewcommand{\]}{\end{equation*}}
\newcommand{\mymacol}[2]{\text{\textcolor{#1}{$#2$}}}

\title{\mykant: Implementing Observational Equality}
\author{Francesco Mazzoli \texttt{<fm2209@ic.ac.uk>}}
\date{June 2013}

\begin{document}
\frame{\titlepage}

\begin{frame}
  \frametitle{\mykant?}

  \mykant\ is an \emph{interactive theorem prover}/\emph{functional
    programming language}, implemented in Haskell.

  It is in the tradition of Agda and Epigram (and to a lesser extent
  Coq), but with a more powerful notion of \emph{equality}.

  We have figured out theory of \mykant, and have a near-complete
  implementation.
\end{frame}

\begin{frame}
  \frametitle{Theorem provers are short-sighted}

  Two functions dear to the Haskell practitioner:
  \[
  \begin{array}{@{}l}
    \myfun{map} : (\myb{a} \myarr \myb{b}) \myarr \mylist{\myb{a}} \myarr \mylist{\myb{b}} \\
      \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l}
        \myfun{map} & \myb{f} & \mynil & = & \mynil \\
        \myfun{map} & \myb{f} & (\myb{x} \mycons \myb{xs}) & = & \myapp{\myb{f}}{\myb{x}} \mycons \myfun{map} \myappsp \myb{f} \myappsp \myb{xs} \\
      \end{array}
      \\
      \ \\
    (\myfun{${\circ}$}) : (\myb{b} \myarr \myb{c}) \myarr (\myb{a} \myarr \myb{b}) \myarr (\myb{a} \myarr \myb{c}) \\
    (\myb{f} \mathbin{\myfun{$\circ$}} \myb{g}) \myappsp \myb{x} = \myapp{\myb{g}}{(\myapp{\myb{f}}{\myb{x}})}
  \end{array}
  \]
\end{frame}

\begin{frame}
  \frametitle{Theorem provers are short-sighted}
  $\myfun{map}$'s composition law states that:
  \[
    \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})
  \]
  We can convince Coq or Agda that
  \[
    \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}    
  \]
  But we cannot get rid of the $\myb{l}$.  Why?
\end{frame}

\begin{frame}
  \frametitle{\mykant\ and observational equality}

  \emph{Observational} equality solves this and other annoyances.

  \mykant\ is a system aiming at making observational equality more
  usable.
\end{frame}

\begin{frame}
  \frametitle{Theorem provers, dependent types}
  \begin{center}
    \Huge
    types $\leftrightarrow$ propositions

    programs $\leftrightarrow$ proofs
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{Theorem provers, dependent types} First class types: we
  can return them, have them as arguments, etc.
  \[
  \begin{array}{@{}l@{\ \ \ }l}
    \mysyn{data}\ \myempty & \text{No members.} \\
    \mysyn{data}\ \myunit \mapsto \mytt & \text{One member.}
  \end{array}
  \]
  $\myempty : \mytyp$, $\myunit : \mytyp$.

  $\myunit$ is trivially inhabitable: it corresponds to $\top$ in
  logic.
  \[
  \mytt : \myunit
  \]
  $\myempty$ is \emph{not} inhabitable: it corresponds to $\bot$.
  \[
  \myfun{absurd} : \myempty \myarr \myb{A}
  \]
\end{frame}

\begin{frame}
  \frametitle{Theorem provers, dependent types}
  \[ \mysyn{data}\ \mylist{\myb{A}} \mapsto \mynil \mydcsep \myb{A} \mycons \mylist{\myb{A}} \]
  We want to express a `non-emptiness' property for lists:
  \[
  \begin{array}{@{}l}
    \myfun{non-empty} : \mylist{\myb{A}} \myarr \mytyp \\
    \begin{array}{@{}l@{\myappsp}c@{\ }l}    
    \myfun{non-empty} & \mynil & \mapsto \myempty \\
    \myfun{non-empty} & (\myb{x} \mycons \myb{l}) & \mapsto \myunit
    \end{array}
  \end{array}
  \]

  A term of type $\myfun{non-empty} \myappsp \myb{l}$ represents a
  \emph{proof} that $\myb{l}$ is indeed not empty.
  \[
  \begin{array}{@{}l@{\ \ \ }l}
    \text{Can't prove} & \myfun{non-empty}\myappsp \mynil \myred \myempty \\
    \text{Trivial to prove}  & \myfun{non-empty}\myappsp(2 \mycons \mynil) \myred \myunit
  \end{array}
  \]
\end{frame}

\begin{frame}
  \frametitle{Example: safe $\myfun{head}$ function}
  \only<3>{We can eliminate the `empty list' case:}
  \[
  \begin{array}{@{}l}
    \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{non-empty}\myappsp\myb{l} \myarr \myb{A}} \\
    \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l}
      \myfun{head} & \mynil & \myb{p} & \mapsto & \only<1,2>{\myhole{?}}\only<3>{\myabsurd\myappsp\myb{p}} \\
      \myfun{head} & (\myb{x} \mycons \myb{xs}) & \myb{p} & \mapsto & \myb{x}
    \end{array}
  \end{array}
  \]

  \only<1>{
    The logic equivalent would be
    \[
    \forall \myb{l} {:} \mylist{\myb{A}}.\ \myfun{non-empty}\myappsp\myb{l} \myarr \myb{A}
    \]
    `For all non-empty lists of type $\myb{A}$, we can get an element of $\myb{A}$.'
  }
  \only<2>{
  The type of $\myb{p}$ in the $\myhole{?}$ is $\myempty$, since
  \[\myfun{non-empty}\myappsp\mynil \myred \myempty \]}
  \only<3>{
    Remember:
    \[ \myfun{absurd} : \myempty \myarr \myb{A} \]
  }
\end{frame}

\begin{frame}
  \frametitle{How do we type check this thing?}
  \[\text{Is\ } \myfun{non-empty}\myappsp(3 \mycons \mynil) \text{\ the same as\ } \myunit\text{?}\]
  Or in other words, is
  \[ \mytt : \myunit \]
  A valid argument to
  \[
  \myfun{head} \myappsp (3 \mycons \mynil) : \myfun{non-empty}\myappsp(3 \mycons \mynil) \myarr \mynat
  \]

  Yes: to typecheck, we reduce terms fully (to their \emph{normal form})
  before comparing:
  \[
  \begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}
    \myunit & \myredd & \myunit & \mydefeq & \myunit & \myreddd & \myfun{non-empty}\myappsp(3 \mycons \mynil) \\
    (\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 \\
    & & & \vdots & & & 
  \end{array}
  \]
  \[
  \mydefeq\ \text{takes the name of \textbf{definitional equality}.}
  \]
\end{frame}

\begin{frame}
  \frametitle{Propositional equality} Using definitional equality, we
  can give the user a type-level notion of term equality.
  \[
  (\myeq) : \myb{A} \myarr \myb{A} \myarr \mytyp\ \ \ \text{internalises equality \textbf{as a type}}
  \]
  We introduce members of $\myeq$ by reflexivity, for example
  \[
  \myrefl\myappsp5 : 5 \myeq 5
  \]
  But also
  \[
  \begin{array}{@{}l}
  \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\text{, since}\\
  (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5
  \end{array}
  \]
  Then we can use a substitution law to derive other
  laws---transitivity, congruence, etc.
  \[ \myeq\ \text{takes the name of \textbf{propositional equality}} \]
\end{frame}

\begin{frame}
\frametitle{The problem with prop. equality}
Going back to $\myfun{map}$, we can prove that
\[    \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}    \]
Because
\[
(\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}
\]
By induction on $\myb{l}$.

Without the $\myb{l}$ we cannot compute, so we are stuck with
\[
\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} \not\mydefeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g})
\]
\end{frame}

\begin{frame}
  \frametitle{Observational equality}

  Instead of basing its equality on definitional equality, look at the
  structure of the type to decide.

  For functions this will mean that proving
  \[
    \myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g} \myeq \myfun{map}\myappsp (\myse{f} \mycomp \myse{g})
  \]
  Will reduce to proving that
  \[
  (\myb{l} : \mylist{\myb{A}}) \myarr 
    (\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}
  \]
  Which is what we want.  The interesting part is how to make the system
  compute nicely.
\end{frame}

\begin{frame}
  \begin{center}
    {\huge \mykant' features}
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{Inductive data}
  \[
  \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mynil \mydcsep \myb{A} \mycons \mytyc{List}\myappsp\myb{A}
  \]
  Each with an induction principle:
  \[
  \begin{array}{@{}l@{\ }l}
    \mytyc{List}.\myfun{elim} : & \AgdaComment{-{}- The property that we want to prove:} \\
     & (\myb{P} : \mytyc{List}\myappsp\myb{A} \myarr \mytyp) \myarr \\
     & \AgdaComment{-{}- If it holds for the base case:} \\
    & \myb{P} \myappsp \mynil \myarr \\
    & \AgdaComment{-{}- And for the inductive step:} \\
    & ((\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 \\
    & \AgdaComment{-{}- Then it holds for every list:} \\
    & (\myb{l} : \mytyc{List}\myappsp\myb{A}) \myarr \myb{P} \myappsp \myb{l}
  \end{array}
  \]
  Induction is also computation, via structural recursion:
  \[
  \begin{array}{@{}l@{\ }l}
    \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp \mynil & \myred \myse{pn} \\
    \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 )
  \end{array}
  \]
\end{frame}

\begin{frame}
  \frametitle{Dependent defined types} \emph{Unlike} Haskell, we can
  have fields of a data constructor to depend on earlier fields:
  \[
  \begin{array}{@{}l}
    \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp\myhole{$(\myb{B} : \myb{A} \myarr \mytyp)$} \mapsto \\
    \myind{2}\mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B}\myappsp\myb{fst} \}
  \end{array}
  \]

  The \emph{type} of the second element depends on the \emph{value} of
  the first:
  \[
  \begin{array}{@{}l@{\ }l}
    \myfun{fst} & : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\
    \myfun{snd} & : (\myb{x} : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B}) \myarr \myb{B} \myappsp (\myfun{fst} \myappsp \myb{x})
  \end{array}
  \]
  Where the projection's reduction rules are predictably
  \[
  \begin{array}{@{}l@{\ }l}
    \myfun{fst}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmm \\
    \myfun{snd}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmn \\
  \end{array}
  \]
\end{frame}

\begin{frame}
  \frametitle{Example: the type of even numbers}
  For example we can define the type of even numbers:
  % TODO fix
  \[
  \begin{array}{@{}l}
    \mysyn{data}\ \mynat \mapsto \mydc{zero} \mydcsep \mydc{suc}\myappsp\mynat \\
    \ \\
    \myfun{even} : \mynat \myarr \mytyp \\
    \begin{array}{@{}l@{\myappsp}c@{\ }l}
      \myfun{even} & \myzero & \mapsto \myunit \\
      \myfun{even} & (\mysuc \myappsp \myzero) & \mapsto \myempty \\
      \myfun{even} & (\mysuc \myappsp (\mysuc \myappsp \myb{n})) & \mapsto \myfun{even} \myappsp \myb{n}
    \end{array} \\
    \ \\
    \mytyc{Even} : \mytyp \\
    \mytyc{Even} \mapsto \mytyc{Tuple}\ \mynat\ \myfun{even}
  \end{array}
  \]
\end{frame}

\begin{frame}
  \frametitle{Type hierarchy}
  \[\{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp\]
  What is the type of $\mytyp$?
  \[
  \cancel{\mytyp : \mytyp}\ \ \ \text{\textbf{inconsistent}}
  \]
  Similar to Russel's paradox in na{\"i}ve set theory.

  Instead, we have a hierarchy:
  \[
  \{\mynat, \mybool, \mytyc{List}\myappsp\mynat, \cdots\} : \mytyp_0 : \mytyp_1 : \cdots
  \]
  We talk of types in $\mytyp_0$ as `smaller' than types in $\mytyp_1$.
\end{frame}

\begin{frame}
  \frametitle{Cumulativity and typical ambiguity}
  Instead of:
  \[ \mytyp_0 : \mytyp_1 \ \ \ \text{but}\ \ \ \mytyp_0 \centernot{:} \mytyp_2\]
  We have a cumulative hierarchy, so that
  \[ \mytyp_n : \mytyp_m \ \ \ \text{iff}\ \ \ n < m \]
  For example
  \[ \mynat : \mytyp_0\ \ \ \text{and}\ \ \ \mynat : \mytyp_1\ \ \ \text{and}\ \ \ \mynat : \mytyp_{50} \]

  But in \mykant, you can forget about levels: the consistency is
  checked automatically---a mechanised version of what Russell called
  \emph{typical ambiguity}.
\end{frame}

\begin{frame}
  \frametitle{Bidirectional type checking}
  \[
  \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A}\myappsp (\mytyc{List}\myappsp\myb{A})
  \]

  With no type inference, we have explicit types for the constructors:
  \[
  \begin{array}{@{}l@{\ }l}
    \mydc{nil} & : (\myb{A} : \mytyp) \myarr \mytyc{List}\myappsp\myb{A} \\
    \mydc{cons} &: (\myb{A} : \mytyp) \myarr \myb{A} \myarr \mytyc{List}\myappsp\myb{A} \myarr \mytyc{List}\myappsp\myb{A}\\
  \end{array}
  \]
  ...ugh:
  \[
  \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)))
  \]
  Instead, annotate terms and propagate the type:
  \[
  \mydc{cons}\myappsp 1 \myappsp (\mydc{cons}\myappsp 2 \myappsp (\mydc{cons} \myappsp 3 \myappsp \mydc{nil})) : \mytyc{List}\myappsp\mynat
  \]
  Conversely, when we use eliminators the type can be inferred.
\end{frame}

\begin{frame}
  \frametitle{OTT + user defined types}

  For each type, we need to:
  \begin{itemize}
  \item Describe when two types formed by the defined type constructors
    are equal;
    \[ \mylist{\mytya_1} \myeq \mylist{\mytya_2} \]
  \item Describe when two values of the defined type are equal;
    \[
    \begin{array}{@{}c@{\ \ \ \ \ \ }c}
      \mynil \myeq \mynil & \mynil \myeq \mytmm \mycons \mytmn \\
      \mytmm \mycons \mytmn \myeq \mynil & \mytmm_1 \mycons \mytmn_1 \myeq \mytmm_2 \mycons \mytmn_2
    \end{array}
    \]
  \item Describe how to transport values of the defined type.
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{OTT + hierarchy}

  Since equalities reduce to functions abstracting over various things,
  we need to make sure that the hierarchy is respected.

  For example we have that
  \[
  \begin{array}{@{}l}
    \myjm{(\myb{x_1} {:} \mytya_1) \myarr \mytyb_1}{\mytyp}{(\myb{x_2} {:} \mytya_2) \myarr \mytyb_2}{\mytyp} \myred \\ 
    \myind{2} \myjm{\mytya_1}{\mytyp}{\mytya_2}{\mytyp} \myand  \\
    \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}])
  \end{array}
  \]

  Subtle point---I discovered a problem in the theory after
  submitting... but I have a fix.
\end{frame}

\begin{frame}
  \frametitle{Bonus!  WebSocket prompt}
  \url{http://bertus.mazzo.li}, go DDOS it!

  \includegraphics[width=\textwidth]{web-prompt.png}
\end{frame}

\begin{frame}
\begin{center}
{\Huge Demo}
\end{center}
\end{frame}

\begin{frame}
  \frametitle{What have we done?}

  \begin{itemize}
    \item A small theorem prover for intuitionistic logic, featuring:
    \item Inductive data and record types;
    \item A cumulative, implicit type hierarchy;
    \item Partial type inference---bidirectional type checking;
    \item Observational equality---coming soon to the implementation.
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Further work}

  \begin{itemize}
    \item Pattern matching and explicit recursion
    \item More expressive data types
    \item Inference via unification
    \item Codata
  \end{itemize}
\end{frame}

\begin{frame}
\begin{center}
{\Huge Questions?}
\end{center}
\end{frame}

\end{document}