--- /dev/null
+\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
+
+\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}{\textmd{\textsc{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]{\mathopen{\mytyc{$[$}} #1 \mathclose{\mytyc{$]$}}}
+\newcommand{\mylistt}[1]{\mathopen{\mydc{$[$}} #1 \mathclose{\mydc{$]$}}}
+\newcommand{\myplus}{\mathbin{\myfun{$+$}}}
+\newcommand{\mytimes}{\mathbin{\myfun{$*$}}}
+
+\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{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{Observational equality and \mykant}
+
+ \emph{Observational equality} is a solution to this and other equality
+ annoyances.
+
+ \mykant\ is a system making observational equality more usable.
+
+ The theory of \mykant\ is complete, the practice, not quite.
+\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@{\ \ \ }l}
+ \mysyn{data}\ \myempty & & \text{No members.} \\
+ \mysyn{data}\ \myunit & = \mytt & \text{One member.} \\
+ \mysyn{data}\ \mynat & = \mydc{zero} \mydcsep \mydc{suc}\myappsp\mynat & \text{Natural numbers.}
+ \end{array}
+ \]
+ $\myempty : \mytyp$, $\myunit : \mytyp$, $\mynat : \mytyp$.
+
+ $\myunit$ is trivially inhabitable: it corresponds to $\top$ in
+ logic.
+
+ $\myempty$ is \emph{not} inhabitable: it corresponds to $\bot$.
+
+\end{frame}
+
+\begin{frame}
+ \frametitle{Theorem provers, dependent types}
+
+ We can express relations:
+ \[
+ \begin{array}{@{}l}
+ (\myfun{${>}$}) : \mynat \myarr \mynat \myarr \mytyp \\
+ \begin{array}{@{}c@{\,}c@{\,}c@{\ }l}
+ \mydc{zero} & \mathrel{\myfun{$>$}} & \myb{m} & = \myempty \\
+ \myb{n} & \mathrel{\myfun{$>$}} & \mydc{zero} & = \myunit \\
+ (\mydc{suc} \myappsp \myb{n}) & \mathrel{\myfun{$>$}} & (\mydc{suc} \myappsp \myb{m}) & = \myb{n} \mathrel{\myfun{$>$}} \myb{m}
+ \end{array}
+ \end{array}
+ \]
+
+ A term of type $\myb{m} \mathrel{\myfun{$>$}} \myb{n}$ represents a
+ \emph{proof} that $\myb{n}$ is indeed greater than $\myb{n}$.
+ \[
+ \begin{array}{@{}l}
+ 3 \mathrel{\myfun{$>$}} 1 \myred \myunit \\
+ 2 \mathrel{\myfun{$>$}} 2 \myred \myempty \\
+ 0 \mathrel{\myfun{$>$}} \myb{m} \myred \myempty
+ \end{array}
+ \]
+
+ Thus, proving that $2 \mathrel{\myfun{$>$}} 2$ corresponds to proving
+ falsity, while $3 \mathrel{\myfun{$>$}} 1$ is fine.
+\end{frame}
+
+\begin{frame}
+ \frametitle{Example: safe $\myfun{head}$ function}
+
+ \[
+ \begin{array}{@{}l}
+ \mysyn{data}\ \mylistt{\myb{A}} = \mynil \mydcsep \myb{A} \mycons \mylistt{\myb{A}} \\
+ \ \\
+ \myfun{length} : \mylistt{\myb{A}} \myarr \mynat \\
+ \begin{array}{@{}l@{\myappsp}c@{\ }c@{\ }l}
+ \myfun{length} & \mynil & = & \mydc{zero} \\
+ \myfun{length} & (\myb{x} \mycons \myb{xs}) & = & \mydc{suc} \myappsp (\myfun{length} \myappsp \myb{xs})
+ \end{array} \\
+ \ \\
+ \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \myarr \myb{A}} \\
+ \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l}
+ \myfun{head} & \mynil & \myb{p} & = & \myhole{?} \\
+ \myfun{head} & (\myb{x} \mycons \myb{xs}) & \myb{p} & = & \myb{x}
+ \end{array}
+ \end{array}
+ \]
+
+ The type of $\myb{p}$ in the $\myhole{?}$ is $\myempty$, since
+ \[\myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 \myred 0 \mathrel{\myfun{$>$}} 0 \myred \myempty \]
+\end{frame}
+
+
+\begin{frame}
+ \frametitle{Example: safe $\myfun{head}$ function}
+
+ \[
+ \begin{array}{@{}l}
+ \mysyn{data}\ \mylistt{\myb{A}} = \mynil \mydcsep \myb{A} \mycons \mylistt{\myb{A}} \\
+ \ \\
+ \myfun{length} : \mytyc{List}\myappsp\myb{A} \myarr \mynat \\
+ \begin{array}{@{}l@{\myappsp}c@{\ }c@{\ }l}
+ \myfun{length} & \mynil & = & \mydc{zero} \\
+ \myfun{length} & (\myb{x} \mycons \myb{xs}) & = & \mydc{suc} \myappsp (\myfun{length} \myappsp \myb{xs})
+ \end{array} \\
+ \ \\
+ \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \myarr \myb{A}} \\
+ \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l}
+ \myfun{head} & \mynil & \myb{p} & = & \myabsurd \myappsp \myb{p} \\
+ \myfun{head} & (\myb{x} \mycons \myb{xs}) & \myb{p} & = & \myb{x}
+ \end{array}
+ \end{array}
+ \]
+
+ Where $\myfun{absurd}$ corresponds to the logical \emph{ex falso
+ quodlibet}---given $\myempty$, we can get anything:
+ \[
+ \myfun{absurd} : \myempty \myarr \myb{A}
+ \]
+\end{frame}
+
+\begin{frame}
+ \frametitle{How do we type check this thing?}
+ \[
+ \myfun{head} \myappsp \mylistt{3} : \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \myarr \mynat
+ \]
+
+ Will $\mytt : \myunit$ do as an argument? In other words, when type
+ checking, do we have that
+ \[
+ \begin{array}{@{}c@{\ }c@{\ }c}
+ \myunit & \mydefeq & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\
+ \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \mydefeq & \myempty \\
+ (\myabs{\myb{x}\, \myb{y}}{\myb{y}}) \myappsp \myunit \myappsp \myappsp \mynat & \mydefeq & (\myabs{\myb{x}\, \myb{y}}{\myb{x}}) \myappsp \mynat \myappsp \myunit \\
+ & \vdots &
+ \end{array}
+ \]
+ ?
+\end{frame}
+
+\begin{frame}
+ \frametitle{Definitional equality}
+
+ The type checker needs a notion of equality between types.
+
+ We reduce terms `as far as possible' (to their \emph{normal form}) and
+ then compare them syntactically:
+ \[
+ \begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}
+ \myunit & \myredd & \myunit & \mydefeq & \myunit & \myreddd & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\
+ \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \myredd & \myempty & \mydefeq & \myempty & \myreddd & \myempty \\
+ (\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}
+ \]
+
+ This equality, $\mydefeq$, takes the name of \emph{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
+ \]
+ We introduce members of $\myeq$ by reflexivity:
+ \[
+ \myrefl\myappsp\mytmt : \mytmt \myeq \mytmt
+ \]
+ So that $\myrefl$ will relate definitionally equal terms:
+ \[
+ \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\ \text{since}\ (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5
+ \]
+ Then we can use a substitution law to derive other
+ laws---transitivity, congruence, etc.
+\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 we can prove, by induction on $\myb{l}$, that we will always get definitionally equal lists.
+
+But 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{The solution}
+
+ \emph{Observational} equality, instead of basing its equality on
+ definitional equality, looks at the structure of the type to decide:
+ \[
+ \begin{array}{@{}l}
+ (\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} : \mylistt{\myb{A_1}} \myarr \mylistt{\myb{C_1}}) \myeq (\myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) : \mylistt{\myb{A_2}} \myarr \mylistt{\myb{C_2}}) \myred \\
+ \myind{2} (\myb{l_1} : \myb{A_1}) \myarr (\myb{l_2} : \myb{A_2}) \myarr (\myb{l_1} : \myb{A_1}) \myeq (\myb{l_2} : \myb{A_2}) \myarr \\
+ \myind{2} ((\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g}) \myappsp \myb{l} : \mylistt{\myb{C_1}}) \myeq (\myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l} : \mylistt{\myb{C_2}})
+ \end{array}
+ \]
+ 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}
+ \frametitle{\mykant}
+
+ Observational equality was described in a very restricted theory.
+
+ \mykant\ aims to incorporate it in a more `practical' environment,
+ where we have:
+ \begin{itemize}
+ \item User defined data types (inductive data and records).
+ \item A type hierarchy.
+ \item Partial type inference (bidirectional type checking).
+ \item Type holes.
+ \end{itemize}
+\end{frame}
+
+\begin{frame}
+ \frametitle{Inductive data}
+ Good old Haskell data types:
+ \[
+ \mysyn{data}\ \mytyc{List}\myappsp \myb{A} = \mynil \mydcsep \myb{A} \mycons \mytyc{List}\myappsp\myb{A}
+ \]
+ But instead of general recursion and pattern matching, we have
+ structural induction:
+ \[
+ \begin{array}{@{}l@{\ }l}
+ \mytyc{List}.\myfun{elim} : & (\myb{P} : \mytyc{List}\myappsp\myb{A} \myarr \mytyp) \myarr \\
+ & \myb{P} \myappsp \mynil \myarr \\
+ & ((\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 \\
+ & (\myb{l} : \mytyc{List}\myappsp\myb{A}) \myarr \myb{P} \myappsp \myb{l}
+ \end{array}
+ \]
+ Reduction:
+ \[
+ \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{Records}
+ But also records:
+ \[
+ \mysyn{record}\ \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} = \mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} \}
+ \]
+ Where each field defines a projection from instances of the record:
+ \[
+ \begin{array}{@{}l@{\ }c@{\ }l}
+ \myfun{fst} & : & \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\
+ \myfun{snd} & : & \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{B}
+ \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{Dependend 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(\myb{B} : \myb{A} \myarr \mytyp) = \\
+ \myind{2}\mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B}\myappsp\myb{fst} \}
+ \end{array}
+ \]
+ $\mytyc{Tuple}$ takes a $\mytyp$, $\myb{A}$, and a predicate from
+ elements of $\myb{A}$ to types, $\myb{B}$.
+
+ This way, 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}
+ \]
+\end{frame}
+
+\begin{frame}
+ \frametitle{Type hierarchy}
+ Up to now, we have thrown $\mytyp$ around, as `the type of types'.
+
+ But what is the type of $\mytyp$ itself? The simple way out is
+ \[
+ \mytyp : \mytyp
+ \]
+ This solution is not only simple, but inconsistent, for the same
+ reason that the notion of a `powerset' in na{\"i}ve set theory is.
+
+ Instead, following Russell, we shall have
+ \[
+ \{\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}
+ Is it OK to take
+ \[ \mytyp_0 : \mytyp_2 \]
+ ?
+\end{frame}
+
+\begin{frame}
+\begin{center}
+{\Huge Questions?}
+\end{center}
+\end{frame}
+
+\end{document}
projects / bitonic-mengthesis.git / blobdiff