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}
\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}
\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@{\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}
\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} \]
\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}
\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}
\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 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}
\]
\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}
projects / bitonic-mengthesis.git / commitdiff