Email Gateway (Aug 18 2022 at 15:19): Email Gateway (Aug 18 2022 at 15:19):From: Alexander Krauss <krauss@in.tum.de>
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
Email Gateway (Aug 18 2022 at 15:19):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
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
Last updated: Apr 16 2024 at 20:15 UTC