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 ;-).

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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