diff options
| -rw-r--r-- | presentation.tex | 156 |
1 files changed, 73 insertions, 83 deletions
diff --git a/presentation.tex b/presentation.tex index 22e619a..a1b2419 100644 --- a/presentation.tex +++ b/presentation.tex @@ -233,9 +233,6 @@ It is similar in scope to Agda or Coq, but with a more powerful notion of \emph{equality}. - - We figured out its theory, but do not have a complete - implementation---although most of the work is done. \end{frame} \begin{frame} @@ -293,16 +290,18 @@ \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 & \mapsto \mytt & \text{One member.} + \begin{array}{@{}l@{\ \ \ }l} + \mysyn{data}\ \myempty & \text{No members.} \\ + \mysyn{data}\ \myunit \mapsto \mytt & \text{One member.} \end{array} \] - $\myempty : \mytyp$, $\myunit : \mytyp$, $\mynat : \mytyp$. + $\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} @@ -314,49 +313,31 @@ \[ \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@{\myappsp}c@{\ }l} - \myfun{non-empty} : \mylist{\myb{A}} \myarr \mytyp \\ - \myfun{non-empty} & \mynil & = \myempty \\ - \myfun{non-empty} & (\myb{x} \mycons \myb{l}) & = \myunit - \end{array} - \] - - \[ \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} + \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 $\myb{m} \mathrel{\myfun{$>$}} \myb{n}$ represents a - \emph{proof} that $\myb{m}$ is indeed greater than $\myb{n}$. + A term of type $\myfun{non-empty} \myappsp \myb{l}$ represents a + \emph{proof} that $\myb{l}$ is indeed not empty. \[ - \begin{array}{@{}l} - 3 \mathrel{\myfun{$>$}} 1 \myred \myunit \\ - 2 \mathrel{\myfun{$>$}} 2 \myred \myempty \\ - 0 \mathrel{\myfun{$>$}} \myb{m} \myred \myempty + \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} - \mysyn{data}\ \mylist{\myb{A}} = \mynil \mydcsep \myb{A} \mycons \mylist{\myb{A}} \\ - \ \\ - \myfun{length} : \mylistt{\myb{A}} \myarr \mynat \\ - \begin{array}{@{}l@{\myappsp}c@{\ }c@{\ }l} - \myfun{length} & \mynil & \mapsto & \mydc{zero} \\ - \myfun{length} & (\myb{x} \mycons \myb{xs}) & \mapsto & \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}} \\ + \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} @@ -367,13 +348,13 @@ \only<1>{ The logic equivalent would be \[ - \forall \myb{l} {:} \mylist{\myb{A}}.\ \myfun{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \myarr \myb{A} + \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{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 \myred 0 \mathrel{\myfun{$>$}} 0 \myred \myempty \]} + \[\myfun{non-empty}\myappsp\mynil \myred \myempty \]} \only<3>{ Remember: \[ \myfun{absurd} : \myempty \myarr \myb{A} \] @@ -383,18 +364,18 @@ \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 + \myfun{head} \myappsp (3 \mycons \mynil) : \myfun{non-empty}\myappsp(3 \mycons \mynil) \myarr \mynat \] Is it the case that - \[ \mytt : \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \] + \[ \mytt : \myfun{non-empty}\myappsp(3 \mycons \mynil) \] Or - \[ \myfun{head} \myappsp \mylistt{3} : \myunit \myarr \mynat \] + \[ \myfun{head} \myappsp (3 \mycons \mynil) : \myunit \myarr \mynat \] - Yes: to typecheck, we reduce terms fully before comparing: + 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{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\ - \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \myredd & \myempty & \mydefeq & \myempty & \myreddd & \myempty \\ + \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} @@ -542,8 +523,6 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with \mytyc{Even} \mapsto \mytyc{Tuple}\ \mynat\ \myfun{even} \end{array} \] - In logic this would be - \[ \exists x \in \mathbb{N}.\ even(x) \] \end{frame} \begin{frame} @@ -577,6 +556,40 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with \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: @@ -604,9 +617,9 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with For example we have that \[ \begin{array}{@{}l} - ((\myb{x_1} {:} \mytya_1) \myarr \mytyb_1 : \mytyp) \myeq ((\myb{x_2} {:} \mytya_2) \myarr \mytyb_2 : \mytyp) \myred \\ - \myind{2} (\mytya_1 : \mytyp) \myeq (\mytya_2 : \mytyp) \myand \\ - \myind{2} (\myb{x_1} : \mytya_1) \myarr (\myb{x_2} : \mytya_2) \myarr (\mytyb_1 : \mytyp) \myeq (\mytyb_2 : \mytyp) + (\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} \] @@ -615,43 +628,20 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with \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. +\begin{center} +{\Huge Demo} +\end{center} \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. + \frametitle{Further work} - Usually used for pre-defined types or core calculi, \mykant\ extends - to user-defined types. -\end{frame} - -\begin{frame} -\begin{center} -{\Huge Demo} -\end{center} + \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} |