[isabelle] Monadic do notation for Isabelle



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.