Re: [isabelle] State of the State Monad



Hi Lars,

There's yet another one formalised as a state monad transformer stateT in the AFP entry Monomorphic_Monad.

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 (http://eprints.whiterose.ac.uk/117267/).

Andreas

On 07/07/17 10:34, Lars Hupel wrote:
Dear list,

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:

* ~~/src/HOL/Library/State_Monad

   - 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
     ambiguities."
     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

* $AFP/thys/Applicative_Lifting/Applicative_State

   - 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
messages.

I hereby propose the following encoding:

   datatype ('a, 's) state = State (run_state: "'s â ('a à 's)")

Any comments?

Cheers
Lars





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