*To*: Christian Sternagel <christian.sternagel at uibk.ac.at>*Subject*: Re: [isabelle] Monadic do notation for Isabelle*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Wed, 19 May 2010 11:58:19 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4BF11A08.3030604@uibk.ac.at>*References*: <4BF11A08.3030604@uibk.ac.at>*User-agent*: Mozilla-Thunderbird 2.0.0.22 (X11/20091109)

Hi Chris,

HOL/Library/State_Monad.thy HOL/Imperative_HOL/Heap_Monad.thy

If you manage to unify all this somehow, this would be a really cool thing. Alex Christian Sternagel wrote:

Hi there,I wrote a theory (plus accompanying ML file) that allows to usedo-notation (as in Haskell and where braces and semicolons aremandatory) for arbitrary monads (in this case, arbitrary bind- andthen-functions), after a setup via:setup {* add_monad "List" { monad_bind = @{term "%xs f. concat (map f xs)"}, monad_then = NONE } *}(Here "monad_then = NONE" means that "bind m (%_. n)" is used instead of"then m n".)setup {* use_monad "List" *} Now, we can write, e.g., do { let xs = [0..2]; x <- xs; y <- xs; [(x, y)] } to obtain the list [(0, 0), (0, 1), (0, 2), ..., (2, 2)].So far so good :). In this setup it is not possible to combine differentmonads. Consider for example the following option monad:setup {* add_monad "Option" { monad_bind = @{term "%m f. Option.map f m"}, monad_then = NONE } *} I would like to be able to write, e.g., do { let xs = [Some 0, Some 1, None]; x <- xs; y <- xs; let r = do { m <- x; n <- y; Some (x + y) }; return [r] }which is an admittedly contrived example. My first thought, was to give"do" an optional argument (the name of the monad that should be used),as indo List { ... do Option { ... } ... } This brings me to my actual question ;)If I would use Theory_Data to store the "current monad", myparse_translations would have to modify the current theory. I assume,this is bad (furthermore, I have no clue how to do this :)). Would it beokay to use a reference for this? What about potential problems?cheers chris

**References**:**[isabelle] Monadic do notation for Isabelle***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] parse and print translations
- Next by Date: [isabelle] parse and print translations for do-notation (in arbitrary monads)
- Previous by Thread: Re: [isabelle] Monadic do notation for Isabelle
- Next by Thread: [isabelle] Automatheo 2010 at FLoC: Call for Participation and Registration
- Cl-isabelle-users May 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list