[isabelle] State of the State Monad



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.