diff options
| -rw-r--r-- | final.lagda | 4 | ||||
| -rw-r--r-- | presentation.tex | 47 |
2 files changed, 28 insertions, 23 deletions
diff --git a/final.lagda b/final.lagda index 8928ec7..4b7484a 100644 --- a/final.lagda +++ b/final.lagda @@ -4357,11 +4357,11 @@ Tokenisation is performed by a simple hand written lexer. \multicolumn{3}{@{}l}{\text{Abstracted variables.}} \\ \mysee{abstract} & ::= & \mytermi{postulate}\ \mysee{typed} \\ \multicolumn{3}{@{}l}{\text{Data types, and their constructors.}} \\ - \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\ + \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mytermi{:}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\ \mysee{constrs} & ::= & \mysee{typed} \\ & | & \mysee{typed}\ \mytermi{|}\ \mysee{constrs} \\ \multicolumn{3}{@{}l}{\text{Records, and their projections. The $\mysee{name}$ before the projections is the constructor name.}} \\ - \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\ + \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mytermi{:}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\ \mysee{projs} & ::= & \mysee{typed} \\ & | & \mysee{typed}\ \mytermi{,}\ \mysee{projs} \end{array} diff --git a/presentation.tex b/presentation.tex index 3728511..1089ae6 100644 --- a/presentation.tex +++ b/presentation.tex @@ -366,13 +366,13 @@ \begin{frame} \frametitle{How do we type check this thing?} + \[\text{Is\ } \myfun{non-empty}\myappsp(3 \mycons \mynil) \text{\ the same as\ } \myunit\text{?}\] + Or in other words, is + \[ \mytt : \myunit \] + A valid argument to \[ \myfun{head} \myappsp (3 \mycons \mynil) : \myfun{non-empty}\myappsp(3 \mycons \mynil) \myarr \mynat \] - Is it the case that - \[ \mytt : \myfun{non-empty}\myappsp(3 \mycons \mynil) \] - Or - \[ \myfun{head} \myappsp (3 \mycons \mynil) : \myunit \myarr \mynat \] Yes: to typecheck, we reduce terms fully (to their \emph{normal form}) before comparing: @@ -443,10 +443,6 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with \] 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. \end{frame} \begin{frame} @@ -585,16 +581,6 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with \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: @@ -622,9 +608,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 \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}]) + \myjm{(\myb{x_1} {:} \mytya_1) \myarr \mytyb_1}{\mytyp}{(\myb{x_2} {:} \mytya_2) \myarr \mytyb_2}{\mytyp} \myred \\ + \myind{2} \myjm{\mytya_1}{\mytyp}{\mytya_2}{\mytyp} \myand \\ + \myind{2} ((\myb{x_1} : \mytya_1) \myarr (\myb{x_2} : \mytya_2) \myarr \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myarr \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}]) \end{array} \] @@ -633,12 +619,31 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with \end{frame} \begin{frame} + \frametitle{Bonus! WebSocket prompt} + \url{http://bertus.mazzo.li}, go DDOS it! + + \includegraphics[width=\textwidth]{web-prompt.png} +\end{frame} + +\begin{frame} \begin{center} {\Huge Demo} \end{center} \end{frame} \begin{frame} + \frametitle{What have we done?} + + \begin{itemize} + \item A small theorem prover for intuitionistic logic, featuring: + \item Inductive data and record types; + \item A cumulative, implicit type hierarchy; + \item Partial type inference---bidirectional type checking; + \item Observational equality---coming soon to the implementation. + \end{itemize} +\end{frame} + +\begin{frame} \frametitle{Further work} \begin{itemize} |