Stream: Coq users

Topic: Map monad state

Proof By Sledgehammer (Oct 29 2021 at 15:36):

I use the monads from coq-ext-lib and I am stuck at a probably pretty easy problem.
I have two types, Foo and Bar, where Bar is a record with a field foo : Foo.

I have a "stateful" operation useFoo : state Foo nat and want to write an operation useBar : state Bar nat that does nothing but call useFoo. However, I can't seem to figure out how to transform useFoo so that it can be used in useBar. I assume I would like some function that just maps these two states like mapState {A B C} : (A -> B) -> state A C -> state B C, but couldn't find one. But probably there is an even easier solution?

Li-yao (Oct 29 2021 at 16:13):

There is no function of that type. Best to write what you need specifically for Foo and Bar. In the general case you need a lens between A and B ((B -> A) * (B -> A -> B)).

Last updated: Sep 28 2023 at 10:01 UTC