[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 similar in scope to Agda or 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?}
  \[
  \myfun{head} \myappsp (3 \mycons \mynil) : \myfun{non-empty}\myappsp(3 \mycons \mynil) \myarr \mynat
  \]
  Is it the case that
  \[ \mytt : \myfun{non-empty}\myappsp(3 \mycons \mynil) \]
  Or
  \[ \myfun{head} \myappsp (3 \mycons \mynil) : \myunit \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.
  
  This extends to other structures (tuples, inductive types, \dots).
  Moreover, if we can deem two \emph{types} equal, we can \emph{coerce}
  values from one to the other.
\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 \mytmt )
  \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}
    \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{Bidirectional type checking}

  This technique is known as \emph{bidirectional} type checking---some
  terms get \emph{checked}, some terms \emph{infer} types.

  Usually used for pre-defined types or core calculi, \mykant\ extends
  to user-defined types.
\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}
    (\myb{x_1} {:} \mytya_1) \myarr \mytyb_1 \myeq (\myb{x_2} {:} \mytya_2) \myarr \mytyb_2 \myred \\
    \myind{2} \mytya_1 \myeq \mytya_2 \myand 
    ((\myb{x_1} : \mytya_1) \myarr (\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}
\begin{center}
{\Huge Demo}
\end{center}
\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}