Re: [Caml-list] Transforming side-effects to a monad

[Yaron Minsky <yminsky@janestreet.com>]

I like monadic encodings of concurrency because they make the places
at which interleavings can occur explicit in the types and the code.
What I've seen from more direct encodings does not have this killer
feature. I don't want to go back to the world of mutexes and
semaphores...

Maybe some version of algebraic effects plus appropriate tracking in
the type system will solve all the problems. But for now, I like my
monads.

y

On Tue, May 9, 2017 at 9:40 AM, Oleg <oleg@okmij.org> wrote:
>
> Back on Mar 24, Christoph Höger wrote:
>
>> Assume a simple OCaml program with two primitives that can cause
>> side-effects:
>
>> let counter = ref 0
>> let incr x = counter := !counter + x ; !counter
>> let put n = counter := n; !counter
>> put (5 + let f x = incr x in f 3)
>
>> This example can be transformed into a pure program using a counter
>> monad (using ppx_monadic syntax):
>
>> do_;
>>   i <-- let f x = incr x in f 3 ;
>>   p <-- put (5 + i)
>>   return p
>
>> For a suitable definition of bind and return, both programs behave
>> equivalently. My question is: How can one automatically translate a
>> program of the former kind to the latter?
>
> More recently (Apr 29), Yaron Minsky, contrasting his view with the
> moderate position by Anil Madhavapeddy, spoke very highly about
> monads.
>
> One really wonders why this obsession with monads. Why to use monadic
> encoding if effects can be expressed directly? Is really
>
>> do_;
>>   i <-- let f x = incr x in f 3 ;
>>   p <-- put (5 + i)
>>   return p
>
> so much better than
>         let res = put (int 5 + let f x = incr x in f 3)
>
> ?
>
> One can say that the do-notation lets us use the other ways to
> implement counters. Well, so does the direct notation:
>         let res = put (int 5 + let f x = incr x in f 3)
> This is truly OCaml code, with no PPX or other pre-processors.
>
> It all depends on how the `primitives' int, put, incr are
> defined. They can use a reference cell or pass the state or talk to a
> remote computer via some RPC. If we abstract over the primitives, the
> same expression can be evaluated with different models of
> `counters'. Incidentally, we did not have to abstract over `let' in
> this example. And we did not have to abstract over functions. Very
> often our DSL can be kept to first order. Embedding into expressive
> OCaml compensates. Incidentally, types really help to tell which
> expression belongs to which `level' -- effectful DSL or OCaml (which
> acts as a higher-order, typed `macro' language).
>
> The recent article
>         http://okmij.org/ftp/tagless-final/nondet-effect.html
>
> presents quite a bit more challenging example, of
> non-determinism. Once can write literally Curry (*) code in OCaml --
> with no PPX or other preprocessors, using multiple interpretations of
> non-determinism.  All works in vanilla OCaml 4.04. We don't have to
> put up with functors: first-class modules really help. The modular
> implicits will help even more, by putting the `implementation'
> argument out of sight.
>
> (*) Curry is a functional-logic programming language, with built-in
> non-determinism