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