Re: [isabelle] Monadic do notation for Isabelle

On Mon, May 17, 2010 at 3:27 AM, Christian Sternagel
<christian.sternagel at> wrote:
> 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?

Hi Christian,

I can see that your parse_translation might need to read information
from the current theory, but I don't see why it would have to *modify*
the current theory. The parse_translation for case syntax (function
case_tr in HOL/Tools/Datatype/datatype_case.ML) probably uses all the
relevant techniques that you would need to implement your generic
monadic syntax: it reads information about constructors from theory
data, and translates the case branches (built with the "_case1" and
"_case2" syntactic constructors) into the appropriate case
combinators. It does not modify any theory data during parsing.

I'm not sure how your current parse_translation is implemented, but
here's the approach I would take: First, define some syntactic
constructors for the do-syntax, similar to how the case syntax is
defined in HOL.thy:

nonterminals dobinds

  "_do1" :: "'a => dobinds" ("_")
  "_do2" :: "[pttrn, 'a, dobinds] => dobinds" ("_ <- _;/ _")
  "_do_syntax" :: "[string, dobinds] => 'a" ("do _ {_}")

Then define a parse_translation for "_do_syntax" that would parse the
list of "_do2" and "_do1" constructors, then choose an appropriate
monad instance based on the value of the string argument (obtaining
the table of monad instances from the theory data).

Alternatively you could omit the "string" argument to "_do_syntax" and
look up the monad instance based on the type of the last statement of
the do-block (except I'm not sure whether the type information would
be available yet). Or you could do a lookup based on what the
top-level constant of the last statement is, e.g. a term of the form
[_] indicates the list monad, and Some _ indicates the option monad.

- Brian

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