RE: [MetaOCaml] Monads, monadic notation and OCaml

RE: [MetaOCaml] Monads, monadic notation and OCaml

[Harrison, William L.]

Hi Jacques and Walid-
 
<PLUG>
     I've been reading your recent posts, and given the interest in stream (a.k.a. resumption) monads, I thought you might be interested in a draft I've submitted about the use of just such monads:
                                 http://www.cs.missouri.edu/~harrison/drafts/CheapThreads.pdf
This article describes the construction of a multitasking operating system kernel in Haskell 98 using resumption monads; the kernel has all the "usual" OS behaviors (e.g., process forking, preemption, message passing, synchronization, etc.) captured succintly.
</PLUG>
 
Bill

________________________________

From: metaocaml-users-l-bounces@mailman.rice.edu on behalf of Walid Taha
Sent: Mon 3/28/2005 12:17 PM
To: Jacques Carette
Cc: metaocaml-users@cs.rice.edu; caml-list@inria.fr
Subject: Re: [MetaOCaml] Monads, monadic notation and OCaml




This is pretty cool!

Are you using the same monad we used in the FFT work?

Also, can you either get rid of the ";" after the "in" or the "in" before
the ";"?  :)

Walid.

On Sun, 27 Mar 2005, Jacques Carette wrote:

|Attached is a camlp4 syntax extension for a 'monadic do notation' for OCaml, much like Haskell's.  The syntax
|extension is joint work with Oleg Kiselyov, and is loosely based on previous work of Lydia van Dijk on a similar
|syntax extension.
|
|Naturally, in OCaml certain monads (like State and IO) are unnecessary.  But other monads (List, option, etc) can be
|quite convenient.
|
|But monads can be much more than convenient.  Below is some code written in a non-deterministic monad of streams.
|This example is particularly interesting in that it cannot be (naively) done in either Prolog or in Haskell's
|MonadPlus monad, both of which would go into an infinite loop on this example.
|
|(* test non-determinism monad, the simplest possible implementation *)
|type 'a stream = Nil | Cons of 'a * (unit -> 'a stream)
|                      | InC of (unit -> 'a stream)
|let test_nondet () =
|   let mfail = fun () -> Nil in
|   let ret a = fun () -> Cons (a,mfail) in
|   (* actually, interleave: a fair disjunction with breadth-first search*)
|   let rec mplus a b = fun () -> match a () with
|                   | Nil -> InC b
|                 | InC a -> (match b () with
|                   | Nil -> InC a
|                   | InC b -> InC (mplus a b)
|                   | Cons (b1,b2) -> Cons (b1, (mplus a b2)))
|                   | Cons (a1,a2) -> Cons (a1,(mplus b a2)) in
|   (* a fair conjunction *)
|   let rec bind m f = fun () -> match m () with
|                   | Nil -> mfail ()
|                 | InC a -> InC (bind a f)
|                   | Cons (a,b) -> mplus (f a) (bind b f) () in
|   let guard be = if be then ret () else mfail in
|   let rec run n m = if n = 0 then [] else
|                 match m () with
|               | Nil -> []
|               | InC a -> run n a
|               | Cons (a,b) -> (a::run (n-1) b)
|   in
|   let rec numb () = InC (mplus (ret 0) (mdo { n <-- numb; ret (n+1) })) in
|   (* Don't try this in Prolog or in Haskell's MonadPlus! *)
|   let tst = mdo {
|                   i <-- numb;
|                   guard (i>0);
|                   j <-- numb;
|                   guard (j>0);
|                   k <-- numb;
|                   guard (k>0);
|                   (* Just to illustrate the `let' form within mdo *)
|                   let test x = x*x = j*j + k*k in;
|                   guard (test i);
|                 ret (i,j,k)
|                 }
|   in run 7 tst
|;;
|
|We ourselves have been experimenting with a combined state-passing, continuation-passing monad, where the values
|returned and manipulated are code fragments (in MetaOCaml).  This allows for considerably simpler, typed code
|combinators.  Details of this work will be reported elsewhere.
|
|Jacques
|
|
|!DSPAM:42476c8f13209207723021!
|
_______________________________________________
metaocaml-users-L mailing list
metaocaml-users-L@mailman.rice.edu
https://mailman.rice.edu/mailman/listinfo/metaocaml-users-l

RE: [MetaOCaml] Monads, monadic notation and OCaml

[Jacques Carette]

> This is pretty cool!

Thanks.

> Are you using the same monad we used in the FFT work?

Yes.  For those on caml-list, the paper Walid refers to is
@inproceedings{KiselyovSwadiTaha2004,
	author = {Oleg Kiselyov and Kedar N.~Swadi and Walid Taha},
	title = {A methodology for generating verified combinatorial
circuits},
	booktitle = {ACM International conference on Embedded Software
(EMSOFT)},
	year = {2004}
}

> Also, can you either get rid of the ";" after the "in" or the "in" before
the ";"?  :)

See the comments in pa_monad.ml.  Unfortunately we cannot easily do that; in
fact the required amount of work to achieve this might be quite large!  It
would be by far easier to integrate this right into the grammar rather than
to post-facto extend the grammar via camlp4.  At least, as far as my current
understanding of camlp4 goes -- maybe if a lot more of the tricks of the
camlp4 Masters were documented, it would not look so hard anymore!

Jacques

Re: [MetaOCaml] Monads, monadic notation and OCaml

[Walid Taha]

This is pretty cool!

Are you using the same monad we used in the FFT work?

Also, can you either get rid of the ";" after the "in" or the "in" before
the ";"?  :)

Walid.

On Sun, 27 Mar 2005, Jacques Carette wrote:

|Attached is a camlp4 syntax extension for a 'monadic do notation' for OCaml, much like Haskell's.  The syntax
|extension is joint work with Oleg Kiselyov, and is loosely based on previous work of Lydia van Dijk on a similar
|syntax extension.
|
|Naturally, in OCaml certain monads (like State and IO) are unnecessary.  But other monads (List, option, etc) can be
|quite convenient.
|
|But monads can be much more than convenient.  Below is some code written in a non-deterministic monad of streams.
|This example is particularly interesting in that it cannot be (naively) done in either Prolog or in Haskell's
|MonadPlus monad, both of which would go into an infinite loop on this example.
|
|(* test non-determinism monad, the simplest possible implementation *)
|type 'a stream = Nil | Cons of 'a * (unit -> 'a stream)
|                      | InC of (unit -> 'a stream)
|let test_nondet () =
|   let mfail = fun () -> Nil in
|   let ret a = fun () -> Cons (a,mfail) in
|   (* actually, interleave: a fair disjunction with breadth-first search*)
|   let rec mplus a b = fun () -> match a () with
|                   | Nil -> InC b
|		  | InC a -> (match b () with
|		    | Nil -> InC a
|		    | InC b -> InC (mplus a b)
|		    | Cons (b1,b2) -> Cons (b1, (mplus a b2)))
|                   | Cons (a1,a2) -> Cons (a1,(mplus b a2)) in
|   (* a fair conjunction *)
|   let rec bind m f = fun () -> match m () with
|                   | Nil -> mfail ()
|		  | InC a -> InC (bind a f)
|                   | Cons (a,b) -> mplus (f a) (bind b f) () in
|   let guard be = if be then ret () else mfail in
|   let rec run n m = if n = 0 then [] else
|                 match m () with
|		| Nil -> []
|		| InC a -> run n a
|		| Cons (a,b) -> (a::run (n-1) b)
|   in
|   let rec numb () = InC (mplus (ret 0) (mdo { n <-- numb; ret (n+1) })) in
|   (* Don't try this in Prolog or in Haskell's MonadPlus! *)
|   let tst = mdo {
|                   i <-- numb;
|                   guard (i>0);
|                   j <-- numb;
|                   guard (j>0);
|                   k <-- numb;
|                   guard (k>0);
|                   (* Just to illustrate the `let' form within mdo *)
|                   let test x = x*x = j*j + k*k in;
|                   guard (test i);
|		  ret (i,j,k)
|                 }
|   in run 7 tst
|;;
|
|We ourselves have been experimenting with a combined state-passing, continuation-passing monad, where the values
|returned and manipulated are code fragments (in MetaOCaml).  This allows for considerably simpler, typed code
|combinators.  Details of this work will be reported elsewhere.
|
|Jacques
|
|
|!DSPAM:42476c8f13209207723021!
|