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

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

[Christoph Höger]

[-- Attachment #1.1: Type: text/plain, Size: 974 bytes --]

Dear all,

this is not entirely OCaml related, but somewhat more general. However,
I hope that someone on that list can give me a pointer on how to proceed.

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? I assume, one needs a normal
form that makes the order of evaluation explicit, but which normal form
would that be? Is there a textbook algorithm for that kind of analysis?

any pointers are appreciated,

Christoph


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 181 bytes --]

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

[Jeremy Yallop]

Dear Christoph,

On 23 March 2017 at 19:56, Christoph Höger <choeger@umpa-net.de> wrote:
> 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?

You might be interested in the following paper, which describes
exactly such a translation:

   Lightweight Monadic Programming in ML
   Nikhil Swamy, Nataliya Guts, Daan Leijen, and Michael Hicks
   ICFP 2011
   https://www.cs.umd.edu/~mwh/papers/swamy11monad.html

Kind regards,

Jeremy

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

[Oleg]

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

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

[Yaron Minsky]

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