Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

state monad using record as a state #48

Open
vzaliva opened this issue Nov 13, 2018 · 4 comments
Open

state monad using record as a state #48

vzaliva opened this issue Nov 13, 2018 · 4 comments
Labels

Comments

@vzaliva
Copy link
Contributor

vzaliva commented Nov 13, 2018

I am observing a strange error when using ExtLib. I am unsure if it is a bug or some sort of limitation, related to universes. In short, I've modified examples/StateGame.v ExtLib example, changing state type from Definition GameState: Type := (prod bool Z) with Record GameState : Type := mkGameState {on:bool; score:Z}.. This lead to the following error message:

Error:
Unable to satisfy the following constraints:

?State_m : "MonadState GameState (state GameState)"

At first glance MonadState_state instance should satisfy this constraint, but there is universe mismatch.
The full example is enclosed below:

Require Import Coq.ZArith.ZArith_base Coq.Strings.String.
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.
  Record GameState : Type := mkGameState {on:bool; score: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 ;; ret (score v)
    |  String x xs =>
       v <- get ;;
         match x, (on v) with
         | "a", true =>  put {| on := on v ; score := (score v) + 1 |}
         | "b", true => put {| on := on v ; score := (score v) - 1 |}
         | "c", _ =>   put {| on := negb (on v) ; score := score v |}
         |  _, _  =>   put v
         end ;; playGame xs
    end.

  Definition startState: GameState := {| on:=false; score:=0 |}.

End StateGame.

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

(* The following should return '2%Z' *)
Compute main.

@gmalecha
Copy link
Collaborator

Interesting. Coq shouldn't care about the record vs the pair, so a universe problem is possible, though I would highly doubt it, you aren't doing anything interesting with universes. Can you print the relevant universes?

@vzaliva
Copy link
Contributor Author

vzaliva commented Nov 13, 2018

Changing definition of main as follows:

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

Gives the following error:

Error:
The term "MonadState_state GameState" has type
 "MonadState@{ExtLib.Data.Monads.StateMonad.1 ExtLib.Data.Monads.StateMonad.2
    ExtLib.Data.Monads.StateMonad.2} GameState (state GameState)"
while it is expected to have type
 "MonadState@{Set Top.20455 Top.20456} GameState (state GameState)".

vzaliva added a commit to vzaliva/helix that referenced this issue Nov 13, 2018
vzaliva added a commit to vzaliva/helix that referenced this issue Nov 13, 2018
@gmalecha
Copy link
Collaborator

This seems to be fixed by making state universe polymorphic.

@gmalecha
Copy link
Collaborator

gmalecha commented Jul 1, 2019

Is this still an issue?

@github-actions github-actions bot added the Stale label Sep 25, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants