Re: [isabelle] parse and print translations for do-notation (in arbitrary monads)
In general, my current idea is to have something, where I could do the
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 (...)
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
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and