introduce the 'other example' in the workshop abstract
This commit is contained in:
parent
909ec2a556
commit
2efc9b87f4
|
@ -72,7 +72,7 @@ let rec with_inputs paths (k : in_channel list -> 'r cloud) : (cost * 'r) cloud
|
||||||
(* we assume that this combinator has been implemented *)
|
(* we assume that this combinator has been implemented *)
|
||||||
val mapM : ('a -> 'b cloud) -> 'a list -> 'b list cloud
|
val mapM : ('a -> 'b cloud) -> 'a list -> 'b list cloud
|
||||||
|
|
||||||
let cat_all paths : report cloud =
|
let cat_all paths =
|
||||||
let@ chans = with_inputs paths in
|
let@ chans = with_inputs paths in
|
||||||
let+ inputs = mapM read_all chans in
|
let+ inputs = mapM read_all chans in
|
||||||
String.concat "" inputs
|
String.concat "" inputs
|
||||||
|
@ -86,7 +86,7 @@ val with_input : (channel * cost cloud -> 'r cloud) -> 'r cloud
|
||||||
|
|
||||||
(* or, introducing a concept of "binder" *)
|
(* or, introducing a concept of "binder" *)
|
||||||
type ('a, 'r) binder = ('a -> 'r cloud) -> 'r cloud
|
type ('a, 'r) binder = ('a -> 'r cloud) -> 'r cloud
|
||||||
val with_input : (channel * cost cloud, 'r) binder
|
val with_input : (in_channel * cost cloud, 'r) binder
|
||||||
|
|
||||||
let rec with_inputs paths : (in_channel list * cost cloud, 'r) binder =
|
let rec with_inputs paths : (in_channel list * cost cloud, 'r) binder =
|
||||||
fun k -> match paths with
|
fun k -> match paths with
|
||||||
|
@ -94,8 +94,12 @@ let rec with_inputs paths : (in_channel list * cost cloud, 'r) binder =
|
||||||
| p :: ps ->
|
| p :: ps ->
|
||||||
let@ chan, cost_p = with_input p in
|
let@ chan, cost_p = with_input p in
|
||||||
let@ chans, cost_ps = with_input ps in
|
let@ chans, cost_ps = with_input ps in
|
||||||
let+ res = k (p :: ps) in
|
let+ res = k (p :: ps)
|
||||||
(cost_p + cost_ps, res)
|
and+ cost_p = cost_p
|
||||||
|
and+ cost_ps = cost_ps
|
||||||
|
in (cost_p + cost_ps, res)
|
||||||
|
(* notice how 'cost' variables are now declared more locally ,
|
||||||
|
making code easier to read.*)
|
||||||
|
|
||||||
(* Note: this approach also increases readability in the non-generic approach *)
|
(* Note: this approach also increases readability in the non-generic approach *)
|
||||||
let cat_all paths cloud =
|
let cat_all paths cloud =
|
||||||
|
|
79
workshop.tex
79
workshop.tex
|
@ -468,7 +468,84 @@ unpacking place corresponds to the place, in the previous style, where
|
||||||
the variable would have been first named. Unpacking is a fair price to
|
the variable would have been first named. Unpacking is a fair price to
|
||||||
pay to recover readable code.
|
pay to recover readable code.
|
||||||
|
|
||||||
% Acknolwedgements: François Pottier.
|
\subsection{Another example} To conclude, we would like to demonstrate
|
||||||
|
the generality of this approach to a wider family of applicative
|
||||||
|
functions with ``quantifier''-like combinators, by briefly showcasing
|
||||||
|
the same refactoring in a different applicative functor -- an
|
||||||
|
artificial example.
|
||||||
|
|
||||||
|
Consider an applicative \lstinline{'a cloud} for ``computations in the
|
||||||
|
cloud'', where operating on a resources (here a remote file) comes
|
||||||
|
with a ``cost'' (API usage, time, money, or something else) that is
|
||||||
|
returned to the programmer when they conclude using the resource. In
|
||||||
|
this model, opening a (remote) file for reading could be exposed by
|
||||||
|
the following quantifier-like operation:
|
||||||
|
|
||||||
|
\begin{lstlisting}
|
||||||
|
val with_input : path -> (in_channel -> 'r cloud) -> (cost * 'r) cloud
|
||||||
|
\end{lstlisting}
|
||||||
|
|
||||||
|
and now the user desires to generalize this into a function that opens
|
||||||
|
a list of paths, operates on the correspond list of input channels,
|
||||||
|
and returns the sum of all costs (we will assume that
|
||||||
|
\lstinline{type cost = int} for simplicity). They want to implement:
|
||||||
|
|
||||||
|
\begin{lstlisting}
|
||||||
|
val with_inputs : path list -> (in_channel list -> 'r cloud) -> (cost * 'r) cloud
|
||||||
|
\end{lstlisting}
|
||||||
|
|
||||||
|
and this is tricky. Our proposal, ``turning direct outputs into modal
|
||||||
|
inputs'', suggests the following change to the primitive operation,
|
||||||
|
introducing a \lstinline{binder} type that marks the place where
|
||||||
|
continuation-passing-style should be used:
|
||||||
|
|
||||||
|
\begin{lstlisting}
|
||||||
|
type ('a, 'r) binder = ('a -> 'r cloud) -> 'r cloud
|
||||||
|
val with_input : (in_channel * cost cloud, 'r) binder
|
||||||
|
\end{lstlisting}
|
||||||
|
|
||||||
|
An implementation of \lstinline{with_inputs} using the original API is on the left,
|
||||||
|
and our proposed approach is on the right.
|
||||||
|
|
||||||
|
\hspace{-3em}
|
||||||
|
\begin{minipage}{0.45\linewidth}
|
||||||
|
\begin{lstlisting}
|
||||||
|
let rec with_inputs paths k =
|
||||||
|
match paths with
|
||||||
|
| [] ->
|
||||||
|
let+ r = k [] in (0, r)
|
||||||
|
| p :: ps ->
|
||||||
|
let+ (cost_p, (cost_ps, r)) =
|
||||||
|
let@ chan = with_input p in
|
||||||
|
let@ chans = with_inputs pts in
|
||||||
|
k (chan :: chans)
|
||||||
|
in (cost_p + cost_ps, r)
|
||||||
|
\end{lstlisting}
|
||||||
|
\end{minipage}
|
||||||
|
\hfill
|
||||||
|
\begin{minipage}{0.55\linewidth}
|
||||||
|
\begin{lstlisting}
|
||||||
|
let rec with_inputs paths =
|
||||||
|
fun k -> match paths with
|
||||||
|
| [] -> k ([], pure 0)
|
||||||
|
| p :: ps ->
|
||||||
|
let@ chan, cost_p = with_input p in
|
||||||
|
let@ chans, cost_ps = with_input ps in
|
||||||
|
let+ res = k (p :: ps)
|
||||||
|
and+ cost_p = cost_p
|
||||||
|
and+ cost_ps = cost_ps
|
||||||
|
in (cost_p + cost_ps, res)
|
||||||
|
\end{lstlisting}
|
||||||
|
\end{minipage}
|
||||||
|
|
||||||
|
Notice, again, that the original API pushes the cost ``on the stack'',
|
||||||
|
and that the variables \lstinline{cost_p}, \lstinline{cost_ps} are
|
||||||
|
bound far from the place that logically introduces them in the left
|
||||||
|
solution. The issue is solved on the right, at the cost of explicit
|
||||||
|
unpacking of the modal inputs.
|
||||||
|
|
||||||
|
\subsection*{Acknowledgments}
|
||||||
|
We wish to thank François Pottier and our anonymous reviewers for their feedback.
|
||||||
|
|
||||||
\bibliography{biblio}
|
\bibliography{biblio}
|
||||||
\end{document}
|
\end{document}
|
||||||
|
|
Loading…
Reference in New Issue