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