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.
\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 \]}
+ \only<3>{
+ Remember:
+ \[ \myfun{absurd} : \myempty \myarr \myb{A} \]
+ }
\end{frame}
\begin{frame}
Or
\[ \myfun{head} \myappsp \mylistt{3} : \myunit \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:
+ Yes: to typecheck, we reduce terms fully 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 \\
& & & \vdots & & &
\end{array}
\]
-
- This equality, $\mydefeq$, takes the name of \emph{definitional} equality.
- % TODO add break
+ \[
+ \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
+ (\myeq) : \myb{A} \myarr \myb{A} \myarr \mytyp\ \ \ \text{internalises equality \textbf{as a type}}
\]
- We introduce members of $\myeq$ by reflexivity:
+ We introduce members of $\myeq$ by reflexivity, for example
\[
- \myrefl\myappsp\mytmt : \mytmt \myeq \mytmt
+ \myrefl\myappsp5 : 5 \myeq 5
\]
- So that $\myrefl$ will relate definitionally equal terms:
+ But also
\[
- \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\ \text{since}\ (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5
+ \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 we can prove, by induction on $\myb{l}$, that we will always get definitionally equal lists.
+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}$.
-But without the $\myb{l}$, we cannot compute, so we are stuck with
+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})
\]
\frametitle{Observational equality}
Instead of basing its equality on definitional equality, look at the
- structure of the type to decide:
+ structure of the type to decide.
+
+ For functions this will mean that proving
\[
- \begin{array}{@{}l}
- (\myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g} : \mylistt{\myse{A_1}} \myarr \mylistt{\myse{C_1}}) \myeq (\myfun{map}\myappsp (\myse{f} \mycomp \myse{g}) : \mylistt{\myse{A_2}} \myarr \mylistt{\myse{C_2}}) \myred \\
- \myind{2} (\myse{l_1} : \mylistt{\myse{A_1}}) \myarr (\myse{l_2} : \mylistt{\myse{A_2}}) \myarr (\myse{l_1} : \mylistt{\myse{A_1}}) \myeq (\myse{l_2} : \mylistt{\myse{A_2}}) \myarr \\
- \myind{2} ((\myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g}) \myappsp \myse{l} : \mylistt{\myse{C_1}}) \myeq (\myfun{map}\myappsp (\myse{f} \mycomp \myse{g}) \myappsp \myse{l} : \mylistt{\myse{C_2}})
- \end{array}
+ \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.
\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}
\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}
projects / bitonic-mengthesis.git / commitdiff