Update the slides
This commit is contained in:
parent
2d5b7a8047
commit
295969e0aa
40
slides.tex
40
slides.tex
|
@ -118,11 +118,23 @@ If \lstinline{'a co} was a monad we could write
|
|||
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Example with another applicative}
|
||||
\begin{frame}[fragile]{Example with another applicative}
|
||||
|
||||
\only<1>{
|
||||
\begin{itemize}
|
||||
\item An applicative \lstinline{'a cloud} for ``computations in the cloud''
|
||||
\item Operating on a resource (here a remote file) comes with a ``cost''
|
||||
\end{itemize}}
|
||||
\only<2>{
|
||||
\lstinline[basicstyle=\footnotesize\ttfamily]{val with_input : path -> (in_channel -> 'r cloud) -> (cost * 'r) cloud}
|
||||
\lstinline[basicstyle=\footnotesize\ttfamily]{val with_inputs : path list -> (in_channel list -> 'r cloud)}
|
||||
\lstinline[basicstyle=\footnotesize\ttfamily]{ -> (cost * 'r) cloud}
|
||||
}
|
||||
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}[fragile]{CPS solution}
|
||||
\begin{lstlisting}
|
||||
\begin{lstlisting}[basicstyle=\footnotesize\ttfamily]
|
||||
| ML.Tuple us ->
|
||||
let rec traverse us (k : variable list -> 'r co)
|
||||
: ((F.term * F.ty) list * 'r) co
|
||||
|
@ -184,7 +196,7 @@ val exist : (Infer.variable *\ \alert<4>{F.ty co} -> 'r co) -> 'r co
|
|||
|
||||
\begin{frame}[fragile]{New API}
|
||||
|
||||
\begin{lstlisting}[columns=flexible]
|
||||
\begin{lstlisting}[basicstyle=\footnotesize\ttfamily]
|
||||
type ('a, 'r) binder = ('a -> 'r co) -> 'r co
|
||||
val exist : (Infer.variable * F.ty co, 'r) binder
|
||||
|
||||
|
@ -195,7 +207,27 @@ val (and+) : 'a co -> 'b co -> ('a * 'b) co (* pair *)
|
|||
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{New code example}
|
||||
\begin{frame}[fragile]{New code example}
|
||||
\begin{lstlisting}[basicstyle=\footnotesize\ttfamily]
|
||||
| ML.Tuple us ->
|
||||
let rec traverse (us : ML.term list)
|
||||
: (variable list * (F.term * F.ty) list co, 'r) binder
|
||||
= fun k -> match us with
|
||||
| [] -> k ([], pure [])
|
||||
| u::us ->
|
||||
let@ v, ty = exist in
|
||||
let@ (vs, us') = traverse us in
|
||||
k (v :: vs,
|
||||
let+ u' = hastype u v
|
||||
and+ ty = ty
|
||||
and+ us' = us'
|
||||
in (u', ty) :: us')
|
||||
in
|
||||
let@ (vs, utys) = traverse us in
|
||||
let+ () = w --- Infer.product vs
|
||||
and+ utys = utys
|
||||
in F.Tuple utys
|
||||
\end{lstlisting}
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Conclusion}
|
||||
|
|
Loading…
Reference in New Issue