Re: [isabelle] State of the State Monad
On 07/07/17 11:10, Lars Hupel wrote:
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.
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
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
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and