[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 {*
monad_bind = @{term "%xs f. concat (map f xs)"},
}
*}

(Here "monad_then = NONE" means that "bind m (%_. n)" is used instead of "then m n".)

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 {*
monad_bind = @{term "%m f. Option.map f m"},
}
*}

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.