Re: [isabelle] State of the State Monad

Hi Lars,

> * ~~/src/HOL/Library/State_Monad

this is indeed a quite different tradition and maybe nothing more than a
historic point of reference.

Such an Âopen state monad is indeed just syntactic sugar for the
combinators Âscomp and ÂfcompÂ, corresponding to #-> and #> in
Isabelle/ML.  These combinators themselves are indeed used for
quickcheck generators.

If you want to reuse that theory name for a Haskell-style state monad,
feel free to rename it to Open_State_Monad or similar.

A considerable practical impact would be to implement the same syntactic
sugar transformations for Isabelle/ML, which would provide an
alternative to all those fancy |-> ||> ||>> #-> ##> ##>> combinators ;-).



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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