Re: [isabelle] Monadic do notation for Isabelle

Hi Chris,

I am not a syntax wizard, so I cannot help much with the actual task, but note that there are two monads in the library already, each with its own syntax setup for do notation:

You might want to look at them if you haven't already. In the AFP there is also MiniML/Maybe.thy, but with a rather basic syntax.

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 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.