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.