Re: [isabelle] State of the State Monad



Hi Lars,


On 07/07/17 11:10, Lars Hupel wrote:
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?
Well, if you impose some cardinality constraint on the type of values you store, then you can embed them in a universal domain. For Imperative_HOL, countability was chosen as the cardinality constraint, but any other would do. So you can model the state explicitly as a finite map from locations to values and start building a kind of separation logic to deal with locations and their allocation.

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

Yes, this can work out nicely if you make sure that you always stay in an abstract setting. Makarius once also had a paper that went into that direction (Schirmer/Wenzel, SSV 2009).

Cheers,
Andreas




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