Simple example of using StateMonad.

[vzaliva]

I was learning how to use ExtLib Monads and adopted this trivial example from Haskell tutorial.
It might useful to other users learning how to use ExtLib.

[gmalecha]

Thanks, this is great.

Just a note, you can decide if you want to update the example or not. In the past, we have found directly using monads can be a bit difficult to debug when you make small mistakes because type class inference can be pretty bad when things go wrong. A way to solve this problem is to parameterize the function by the monad and then apply it. Something like:

Section with_monad.
  Variable m : Type -> Type.
  Context {Monad_m : Monad m} {MonadState_m : MonadState nat m}.

  Definition get_times_2' : m nat :=
     x <- get ;; ret (2 * x).
End with_monad.
Definition get_times_2 := get_times_2 := @get_times_2' (state nate) _ _.

In addition to getting more sensible error messages, another benefit is that when you use monad transformers you can leave the order of the transformers unspecified until later (and possibly even use the same function with monads composed in different orders). This is similar to the way the Haskell MTL library works.

[vzaliva]

Thanks for the suggestion. Let me rework the example tomorrow.

[vzaliva]

I tried to rework my example to use your approach, but could not make it work. I will appreciate if you can show me how to do this based on the example. I want to learn this technique.

[gmalecha]

I'm not certain how to edit your file, but it is almost there. The main thing is that when you are in the section, you can not run the computation (because the monad is opaque). So you end up with something like this:

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}.

  Fixpoint playGame (s: string) {struct s}: m GameValue :=
    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)
         |  _, _  =>    put (on, score)
         end ;; playGame xs
    end.

  Definition startState: GameState := (false, 0).

End StateGame.

Definition main : GameValue :=
  (@evalState GameState GameValue (playGame (state GameState) "abcaaacbbcabbab") startState).

Compute main.

[vzaliva]

Thanks! I've updated the example in the pull request.
Perhaps this example could be a good starting point for #5 ...