projects
/
bitonic-mengthesis.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
e319c3d
)
...
author
Francesco Mazzoli
<f@mazzo.li>
Wed, 26 Jun 2013 23:02:00 +0000
(
00:02
+0100)
committer
Francesco Mazzoli
<f@mazzo.li>
Wed, 26 Jun 2013 23:02:00 +0000
(
00:02
+0100)
final.lagda
patch
|
blob
|
history
presentation.tex
patch
|
blob
|
history
diff --git
a/final.lagda
b/final.lagda
index 8928ec700b5efc0e3c6e20310dbac15d0baed95c..4b7484a9dfb84b161ec3dad25ad9175d05293b69 100644
(file)
--- 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.}} \\
\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}\ \my
termi{:}\ \my
see{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{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}\ \my
termi{:}\ \my
see{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
\mysee{projs} & ::= & \mysee{typed} \\
& | & \mysee{typed}\ \mytermi{,}\ \mysee{projs}
\end{array}
\mysee{projs} & ::= & \mysee{typed} \\
& | & \mysee{typed}\ \mytermi{,}\ \mysee{projs}
\end{array}
diff --git
a/presentation.tex
b/presentation.tex
index 3728511aebdea18f9e34abaaf7fb702f3637f80d..1089ae6d3370fd8806f05c118936f10b0ccda34e 100644
(file)
--- a/
presentation.tex
+++ b/
presentation.tex
@@
-366,13
+366,13
@@
\begin{frame}
\frametitle{How do we type check this thing?}
\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
\]
\[
\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:
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.
\]
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}
\end{frame}
\begin{frame}
@@
-584,16
+580,6
@@
Without the $\myb{l}$ we cannot compute, so we are stuck with
Conversely, when we use eliminators the type can be inferred.
\end{frame}
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}
\begin{frame}
\frametitle{OTT + user defined types}
@@
-622,9
+608,9
@@
Without the $\myb{l}$ we cannot compute, so we are stuck with
For example we have that
\[
\begin{array}{@{}l}
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} \my
tya_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} \my
jm{\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}
\]
\end{array}
\]
@@
-632,12
+618,31
@@
Without the $\myb{l}$ we cannot compute, so we are stuck with
submitting... but I have a fix.
\end{frame}
submitting... but I have a fix.
\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}
\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{frame}
\frametitle{Further work}