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

Hi Chris,

`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

[...]

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

What would the tool do with the proofs of the monad laws?

`If they are just thrown away or stored under some name, then there is
``little value to it. One could also imagine the tool defining derived
``operations like mapM and prove laws about them, but this may be going
``too far.
`

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

`Constructor classes is not something that one can easily mount on top of
``an existing logic, so I am quite sure that this can only happen if one
``finds a way of moving all this into user-space... But this is a
``different story.
`
I think the main advantage of a "monad package" as you describe it is

`that it streamlines the syntax translations. Making a few extra
``definitions and proving some laws is something that a user easily does
``himself, but the translations are always painful and hard to get right.
`

Another question: would this be useful/used for/by users/you? :D

`If it is simple and does it's job well, I am sure that there are as many
``uses for it as there are monads out there.
`

`One further point: The begin-end syntax you have in mind is something
``that can only be implemented by a "target". Targets are the most complex
``part of the local theory infrastructure, and you probably don't want to
``implement one "at home" unless you have a very very good reason.
`
A simpler interface would do just as well, such as
monad option
where return = "Some"
and bind = "option_bind"

`Maybe one should not make new constant definitions here but simply
``assume that they are already constants with the appropriate definition
``(So one can use inductive/primrec/function to define them). Then the
``monad command would basically be equivalent to the translation
``functions, except that it would work out of the box.
`
Alex

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