# [isabelle] parse and print translations for do-notation (in arbitrary monads)

Hi all,
@makarius:

`1) Sorry for mixing up notions. I do fully agree that it is very
``important to be concise in order to avoid misunderstandings :)
`
2) Syntax.add_term_check sounds interesting and I will give it a try.
@alex:

`1) My interest in the do-notation was actually caused by
``HOL/Library/State_Monad.thy when browsing Isabelle's library. I will
``also have a look at the heap monad.
`

`2) I would very much like to unify all this :D, however, I'm not sure if
``I can manage. Nevertheless, I'll give it a try and consider it as a
``training session in Isabelle ML programming.
`

`In general, my current idea is to have something, where I could do the
``following:
`
monad option: "option" begin
definition "return x == Some x"
definition "bind m f == case m of Some x => f x | e => e"
(* maybe 'fail' for pattern-match errors? *)
definition "fail = None"
monad_laws by (...)
end
monad error: "+" begin
definition "return x == Inr x"
definition "bind m f == case m of Inl x => f x | e => e"
(* maybe 'fail' for pattern-match errors? *)
definition "fail = Inl undefined"
monad_laws by (...)
end

`which then provides the usual >>= and >> combinators as well as
``do-notation for the option type and the sum type (I'm not yet sure if it
``is a good idea / necessary to proof the monad laws for every instance).
`

`This looks very much like type classes. Hence an obvious question would
``be: will there ever be higher-kinded type classes in Isabelle? Is this
``even possible? Of course, it would be futile to make a special "monad"
``version if there is a more general solution.
`
Another question: would this be useful/used for/by users/you? :D
cheers
chris

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