Hi all,

I would like to play a little bit with the implementation of Monads in coq-ext-lib. In particular, I am curious of how one could extend this example

https://github.com/coq-community/coq-ext-lib/blob/master/examples/StateGame.v to use also an either monad as in

https://github.com/coq-community/coq-ext-lib/blob/master/examples/EvalWithExc.v

Extending StateMonad to return an error if "d" is encountered would serve my need.

By analysing https://github.com/coq-community/coq-ext-lib/blob/master/theories/Data/Monads/StateMonad.v, one could get the feeling that some aspects of the Either monad are also present in the StateMonad. But the code lacks documentation or hints at how to use it.

Thanks!

It might be a case where you'd like to use a monad transformer. There's a MonadTrans file in ext-lib but it's rather short :)

Yes, monad transformer seems the way to go. There are a couple of very nice papers that explain the concept. Now my problem is to either implement mine (and I apply cool stuff I learnt) or try to apply (and learn) from existing code. It seems many projects developed their own monad.

MonadTrans that you mention is just an interface. StateMonad.v provides some realization of this interface, including lift. If only the authors could provide an example ;) But fair point, I can spend some time on this as well.

That's the thing with monads - you can't compose them generically, and have to implement a transformer for each one separately. Regarding the state transformer, you might find some inspiration in Haskell documentation, e.g. https://wiki.haskell.org/Simple_StateT_use

Yes, this is part of what I read separately. I found some lecture notes by Xavier Leroy that explained that nicely (unfortunately I lost the link, probably in one of his lecture for MPRI). Also this paper is an interesting source: https://arxiv.org/abs/1805.08059 for learners.

But my question was in the context of ExtLib. The lack of documentation for non-experts means that I would have to implement my own monad, which is unfortunate. I was hoping one of the maintainer of ExtLib could provide some hints before I start working on my own solution.

Both `stateT`

and `eitherT`

are in extlib already, what else do you need? Monad transformers is a rather well-covered FP/Haskell topic, so there's less incentive to redo it in Coq for a much smaller audience (who are most likely polyglots anyway).

[ just some context: my interest is in applying Coq to revisit some existing tools, and my background is in architecture of safety-critical systems, so quite different from the core Coq community. That being said, the Coq learning curve has been quite a fun ride until I hit Monad (so far I played with building a parser using Menhir, inductive types for a large AST, a few type checking and some modeling of behaviors using state machines-like formalisms, all thanks to public books available. Combining state and either monad would help building some scenarios I want to represent. ]

As I said, I kind of miss a minimal working example. I am still in the process of learning Coq, with a different CS background than most of you. Perhaps this request is trivial .. but ..

I tried to adapt the example from https://github.com/coq-community/coq-ext-lib/blob/master/examples/StateGame.v

Obviously the following is wrong: `Context {MonadExc_m : MonadExc string (state GameState)}.`

does not bring the right element in context. Therefore the call to evalState is wrong. And I agree, https://github.com/coq-community/coq-ext-lib/blob/master/theories/Data/Monads/StateMonad.v certainly has all the data structures I need, except for a user guide.

So here is where I am, not far from the original example I confess. Any hint to go further would be greatly appreciated.

```
Require Import Coq.ZArith.ZArith_base Coq.Strings.String Coq.Strings.Ascii.
Require Import ExtLib.Data.Monads.StateMonad ExtLib.Structures.Monads.
Section StateGame.
Import MonadNotation.
Local Open Scope Z_scope.
Local Open Scope char_scope.
Local Open Scope monad_scope.
Definition GameValue : Type := Z.
Definition GameState : Type := (prod bool Z).
Variable m : Type -> Type.
Context {Monad_m: Monad m}.
Context {State_m: MonadState GameState m}.
Context {MonadExc_m : MonadExc string (state GameState)}.
Fixpoint playGame (s: string) {struct s} :=
match s with
| EmptyString =>
v <- get ;;
let '(on, score) := v in ret score
| String x xs =>
v <- get ;;
let '(on, score) := v in
match x, on with
| "a", true => put (on, score + 1)
| "b", true => put (on, score - 1)
| "c", _ => put (negb on, score)
| "d", _ => raise ("unexpected cmd")%string
| _, _ => put (on, score)
end ;; playGame xs
end.
Definition startState: GameState := (false, 0).
End StateGame.
Check playGame.
Definition main :=
(@evalState GameState GameValue (playGame (state GameState) "abcaaacbbcabbab") startState).
```

Thanks for reading so far.

I'd not be surprised if in fact a large proportion of people learning Coq are not familiar with the FP side of the knowledge base. And since you're learning this, it might even be a necessary step to roll your own implementation to understand things. Anyway, here's a working version:

```
Require Import Coq.ZArith.ZArith_base Coq.Strings.String Coq.Strings.Ascii.
From ExtLib Require Import
Data.Monads.EitherMonad
Data.Monads.StateMonad Structures.Monads.
Section StateGame.
Import MonadNotation.
Local Open Scope Z_scope.
Local Open Scope char_scope.
Local Open Scope monad_scope.
Definition GameValue : Type := Z.
Definition GameState : Type := (prod bool Z).
Variable m : Type -> Type.
Context {Monad_m: Monad m}.
Context {State_m: MonadState GameState m}.
Context {MonadExc_m : MonadExc string m}.
Fixpoint playGame (s: string) {struct s} : m Z :=
match s with
| EmptyString =>
v <- get ;;
let '(on, score) := v in ret score
| String x xs =>
v <- get ;;
let '(on, score) := v in
match x, on with
| "a", true => put (on, score + 1)
| "b", true => put (on, score - 1)
| "c", _ => put (negb on, score)
| "d", _ => raise ("unexpected cmd")%string
| _, _ => put (on, score)
end ;; playGame xs
end.
Definition startState: GameState := (false, 0).
End StateGame.
Check playGame.
Definition main : string + GameValue :=
(evalStateT (playGame (stateT GameState (sum string)) "abcaaacbbcabbab") startState).
```

Some thoughts:

- the monad in the end is
`stateT GameState (sum string)`

(where`sum _`

, aka the "`Either`

monad", provides exceptions; note an extra`Require`

to get its monad instance). It could also be`eitherT string (state GameState)`

. (the difference is`GS -> string + (GS * Value)`

vs`GS -> GS * (string + Value)`

) - in the "implementation" part, the constraints
`Monad`

,`MonadState`

and`MonadExc`

are all to be applied to the parameter`m`

. Or you could set`m`

to be the concrete monad`stateT GameState (sum string)`

upfront and rely on its instances directly and implicitly (not adding the constraints); less general, but more concrete.

Thanks Li-yao for your detailed answer.

I guess there is a gap between FP a-la LISP (that is definitely something I am familiar with at an entry level) and the more advanced concepts promoted by Coq like typeclasses, use of implicit parameters, to name a few things that obfuscate my learning experience. The learning gap is complex to cover because of the diversity of resources that you must process when you are not immersed in a research team or a teaching environment. But this is another debate we can have separately if you are interested in feedback on Coq learning journey.

Thanks for the solution, this definitely clarifies a few thing, especially the concrete monad type.

Note there is an issue with your solution with recent Coq version (8.13.2) and coq-ext-lib (I have dev installed), see https://github.com/coq-community/coq-ext-lib/blob/master/examples/StateTMonad.v and the corresponding issue/patch.

Adding `Existing Instance Monad_stateT.`

before the definition of main addresses the following error

```
The following term contains unresolved implicit arguments:
(evalStateT (playGame (stateT GameState (sum string)) "abcaaacbbcabbab")
startState)
More precisely:
- ?Monad_m: Cannot infer the implicit parameter Monad_m of playGame whose
type is "Monad (stateT GameState (sum string))" (no type class instance
found).
```

@Jerome Hugues indeed there's a large gap already between Lisp FP and Haskell-like FP. In this whole thread, "FP" is best understood as the latter.

The learning curve is real, and I wouldn't be surprised if the quickest road were to jump to Haskell learning materials — some of those are good.

Jerome Hugues has marked this topic as resolved.

Last updated: Feb 06 2023 at 11:03 UTC