# [isabelle] Monadic do notation for Isabelle

*To*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>
*Subject*: [isabelle] Monadic do notation for Isabelle
*From*: Christian Sternagel <christian.sternagel at uibk.ac.at>
*Date*: Mon, 17 May 2010 12:27:20 +0200
*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.9) Gecko/20100330 Fedora/3.0.4-1.fc12 Lightning/1.0b2pre Thunderbird/3.0.4

Hi there,

`I wrote a theory (plus accompanying ML file) that allows to use
``do-notation (as in Haskell and where braces and semicolons are
``mandatory) for arbitrary monads (in this case, arbitrary bind- and
``then-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 different
``monads. 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 in
`
do List { ... do Option { ... } ... }
This brings me to my actual question ;)

`If I would use Theory_Data to store the "current monad", my
``parse_translations would have to modify the current theory. I assume,
``this is bad (furthermore, I have no clue how to do this :)). Would it be
``okay to use a reference for this? What about potential problems?
`
cheers
chris

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*