X-Git-Url: https://git.enpas.org/?a=blobdiff_plain;f=presentation.tex;fp=presentation.tex;h=f3381bc273d653487bdebbfccb6fd9ca20852406;hb=ebdf439a201d6fda0780284fc7f49b1f8deb88ab;hp=0000000000000000000000000000000000000000;hpb=7e1d2c79545c573617ccedf458ba11bda1cc3eb8;p=bitonic-mengthesis.git diff --git a/presentation.tex b/presentation.tex new file mode 100644 index 0000000..f3381bc --- /dev/null +++ b/presentation.tex @@ -0,0 +1,568 @@ +\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{}} +\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}