Jerome Hugues (Jul 02 2021 at 00:01): Jerome Hugues (Jul 02 2021 at 00:01):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!
Matthieu Sozeau (Jul 12 2021 at 09:08):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 :)
Jerome Hugues (Jul 13 2021 at 13:46):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.
Alexander Gryzlov (Jul 13 2021 at 14:38):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
Jerome Hugues (Jul 13 2021 at 14:48):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.
Li-yao (Jul 13 2021 at 20:01):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).
Jerome Hugues (Jul 13 2021 at 23:08):[ 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.
Li-yao (Jul 14 2021 at 00:35):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:
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))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. Jerome Hugues (Jul 14 2021 at 04:03):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.
Paolo Giarrusso (Jul 17 2021 at 19:05):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.
Notification Bot (Aug 06 2021 at 18:09):Jerome Hugues has marked this topic as resolved.
Last updated: Oct 01 2023 at 17:01 UTC