Re: [isabelle] State of the State Monad
There's yet another one formalised as a state monad transformer stateT in the AFP entry
There are also a bunch of specialised state monads around, e.g., inside Imperative_HOL.
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.
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
On 07/07/17 10:34, Lars Hupel wrote:
for cleaning up my formalization, I need to use a state monad. I did a
brief check on what's currently there in the Isabelle universe. These
are my findings:
- shallow embedding
- a lot of text, but no actual useful setup
- imports Monad_Syntax, but defines its own syntax?!
- mysterious NEWS entry:
"Theory Library/Monad_Syntax provides do-syntax for monad types.
Syntax in Library/State_Monad has been changed to avoid
That actual change is hidden in changeset d00a3f47b607 with the
message "more generous memory settings for scala check"
- only used in "~~/src/HOL/Proofs/Extraction/Higman_Extraction", not
in the AFP
- shallow embedding
- setup for Applicative, but not for Monad_Syntax
* Anything else I'm unaware of?
The disadvantage of shallow embedding is that registering such an
encoding with Monad_Syntax will likely end up generating strange error
I hereby propose the following encoding:
datatype ('a, 's) state = State (run_state: "'s â ('a Ã 's)")
This archive was generated by a fusion of
Pipermail (Mailman edition) and