Re: [isabelle] State of the State Monad



Hi Andreas,

thanks for that.

> Your formalisation as a datatype seems canonical to me and from my
> experience, I can just recommend to use a proper type constructor rather
> than a type_synonym. The datatype version needs a bit more reasoning
> setup, but also provides an abstraction boundary that is not broken just
> by typing a space (for function application). Moreover, I'd expect
> adhoc_overloading and type classes to work better with type constructors
> than type synonyms.

Yeah, that's also what Peter said.

> The main problem with your proposed formalisation is that the state type
> shows up explicitly in the type. This may lead to problems if you want
> to combine functions that operate on disjoint parts of the state: you
> need a lot of formal plumbing for that. In Imperative_HOL, there's a
> formalisation of a state monad where you can only store values of
> countable types and which avoids this problem.
> 
> Simon Foster and Zeyda Frank has formalised lenses using locales in
> Isabelle (http://eprints.whiterose.ac.uk/117267/).

I didn't quite get this part. How is countability related to accessing
disjoint parts of the state?

Furthermore, I would expect that I can integrate this with the "Optics"
AFP entry you mentioned. This should give rise to a combinator like:

  in_lens :: ('a, 'b) lens => ('c, 'a) state => ('c, 'b) state

Cheers
Lars




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