Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] State of the State Monad

view this post on Zulip Email Gateway (Aug 22 2022 at 15:40):

From: Lars Hupel <hupel@in.tum.de>
Hi Andreas,

thanks for that.

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.

Yeah, that's also what Peter said.

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?

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

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 15:40):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 15:40):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars,

this is indeed a quite different tradition and maybe nothing more than a
historic point of reference.

Such an »open« state monad is indeed just syntactic sugar for the
combinators »scomp« and »fcomp«, corresponding to #-> and #> in
Isabelle/ML. These combinators themselves are indeed used for
quickcheck generators.

If you want to reuse that theory name for a Haskell-style state monad,
feel free to rename it to Open_State_Monad or similar.

A considerable practical impact would be to implement the same syntactic
sugar transformations for Isabelle/ML, which would provide an
alternative to all those fancy |-> ||> ||>> #-> ##> ##>> combinators ;-).

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 15:44):

From: Lars Hupel <hupel@in.tum.de>
I've spent a few hours polishing my representation. See attachment.

Given the integration with the "Optics" and "Applicative" entries I'd
consider this worthy of inclusion in the AFP.

The existing "State_Monad" can be folded into its only use site
("~~/src/HOL/Proofs/Extraction/Higman_Extraction").

Andreas: Would you be also interested in consolidating Tree_Relabeling
with the fresh monad I've implemented on top of state?

Cheers
Lars
State_Lens.thy
State_Monad.thy

view this post on Zulip Email Gateway (Aug 22 2022 at 15:45):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,

Replacing the existing state monad in Applicative_Lifting with yours shouldn't be hard.
Except that if your theories become an AFP entry of their own, then we have a circular
dependency between the entries.

So it might be easier to put your theory without the AFP entry integration into
HOL/Library and do the integration in the respective AFP entries. What do you think?

Best,
Andreas

view this post on Zulip Email Gateway (Aug 22 2022 at 15:45):

From: Lars Hupel <hupel@in.tum.de>
Good point. If nobody objects I'll do that later this week. I was
planning to clean up some stuff in the vicinity ("Finite_Map") anyway.

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 15:45):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

The existing "State_Monad" can be folded into its only use site
("~~/src/HOL/Proofs/Extraction/Higman_Extraction").

I would welcome to have it as a separate theory (though under a
different name maybe) since it can also be used for pretty printing
quickcheck random generator expressions.

Florian
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 15:45):

From: Lars Hupel <hupel@in.tum.de>
If you say "can be used", does that mean it already works or that it can
be implemented?

In any case, since it's purely syntactic, I propose calling it
"State_Syntax".

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 15:45):

From: Lars Hupel <hupel@in.tum.de>

Good point. If nobody objects I'll do that later this week. I was
planning to clean up some stuff in the vicinity ("Finite_Map") anyway.

See now Isabelle/d157195a468a and AFP/9f41cb6d9cfa.

I'll leave the porting of the tree relabeling to you, Andreas :-)

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 15:46):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,

I've ported the tree relabelling (AFP/6a4641399c0a). I had to prove a bunch of lemmas
about how the state monad operations interact. They are at the top of
Tree_Relabelling.thy, but you might want to move them to State_Monad in HOL/Library.

Cheers,
Andreas

view this post on Zulip Email Gateway (Aug 22 2022 at 15:46):

From: Lars Hupel <hupel@in.tum.de>
Excellent, thanks!

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 15:47):

From: Lars Hupel <hupel@in.tum.de>
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:

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

view this post on Zulip Email Gateway (Aug 22 2022 at 15:48):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Last updated: Apr 19 2024 at 08:19 UTC