How to use indexed monad as FSM?

Question

I am trying to create a simple state machine that changes color state when input is valid: Red -> Green -> Blue -> Red ...

I want to be able to explicitly define the state transitions. After reading What is indexed monad? and Stephen Diehl's What I Wish I Knew, the indexed monad seems to be what I need. So far I have the following code:

import Prelude hiding ( return )

newtype IState i o a = IState { runIState :: i -> (a, o) }

execIState :: IState i o a -> i -> o
execIState st i = snd $ runIState st i

return :: a -> IState s s a
return a = IState $ \s -> (a,s)

put :: o -> IState i o ()
put o = IState $ const ((), o)

data Red   = Red
data Green = Green
data Blue  = Blue

blueToRed :: IState Blue Red ()
blueToRed = put Red

redToGreen :: IState Red Green ()
redToGreen = put Green

greenToBlue :: IState Green Blue ()
greenToBlue = put Blue

newtype Color a = Color a

colorChange
  :: Color a
  -> Bool
  -> Color a
colorChange s@(Color c) valid = Color $ flip execIState c $ case s of
  (Color Red)   | valid -> redToGreen
  (Color Green) | valid -> greenToBlue
  (Color Blue)  | valid -> blueToRed
  _ -> return ()

This code gives the error:

Couldn't match type `Blue' with `Green'
      Expected type: IState a Green ()
        Actual type: IState Green Blue ()
    * In the expression: greenToBlue
      In a case alternative: (Color Green) | valid -> greenToBlue
      In the second argument of `($)', namely
        `case s of
           (Color Red) | valid -> redToGreen
           (Color Green) | valid -> greenToBlue
           (Color Blue) | valid -> blueToRed
           _ -> return ()'
   |
39 |   (Color Green) | valid -> greenToBlue


Couldn't match type `Red' with `Green'
      Expected type: IState a Green ()
        Actual type: IState Blue Red ()
    * In the expression: blueToRed
      In a case alternative: (Color Blue) | valid -> blueToRed
      In the second argument of `($)', namely
        `case s of
           (Color Red) | valid -> redToGreen
           (Color Green) | valid -> greenToBlue
           (Color Blue) | valid -> blueToRed
           _ -> return ()'
   |
40 |   (Color Blue)  | valid -> blueToRed

I understand that the types Red, Green, and Blue are different. But the errors do not make sense to me, why would the compiler expect IState a Green () when greenToBlue :: IState Green Blue ()? It seems to me it is expecting all types to "match" the first case pattern redToGreen. How do I work around this to create my state transfer function? The "What is indexed monad?" post used GADTs, so I thought maybe that would help, but I could not get the example in that post working and I have not used GADTs before, just read about them.

Note this is very simple for debugging and learning purposes, I plan to use this when complexity of my FSMs increase.

Clarification: I want the compiler to give an error if the state transfer function does not preserve the state machine structure. Say I define the state machine structure as: Red -> Green -> Blue -> Red ... but if I accidentally change my colorChange function so Red -> Blue, the compiler should issue an error as this violates the state machine structure where Green must follow Red.

Continuing the "indexed monad" intuition, I suppose you might consider including something like `bind :: IState a b v -> (v -> IState b c v') -> IState a c v'`, no? But then `bind redToGreen (\_ -> greenToBlue)` is well-typed and changes from `Red` to `Blue`. Should the compiler reject that, too? — Daniel Wagner, Apr 23 '19 at 15:03
@DanielWagner To address your comment below, the main interaction would be `step :: s -> i -> s'`, (moore version). My goal is to separate the definition of the state machine (its structure, which states are adjacent to each-other) from the implementation of the state transitions (`step`s). If `f :: Red -> Green`, `g :: Green -> Blue`, `h :: Blue -> Red` are all my transition functions, then `step` should be defined in such a way that it NEVER goes `Red -> Blue`, if it does warn me. So `bind redToGreen (\_ -> greenToBlue)` should be rejected. Perhaps the indexed monad is not what I want. — dopamane, Apr 25 '19 at 19:15
I should have posted the working code (basically what you answered, though not as concise), then asked how can I make the compiler warn me if `colorChange Red _ = Green` accidentally gets changed to `colorChange Red _ = Blue`. Or any change that would break the structure `Red -> Green -> Blue -> Red` and so on. Instead I muddied the water with an indexed monad. — dopamane, Apr 25 '19 at 19:35
But your code already breaks that structure: `colorChange _ False` does e.g. a transition `Red -> Red`... — Daniel Wagner, Apr 25 '19 at 19:45
Sorry, my example was poor. In this case I would also have identity transitions for each state, `idRed :: Red -> Red`, `idGreen :: Green -> Green`, `idBlue :: Blue -> Blue`. Along with `f :: Red -> Green`, `g :: Green -> Blue`, `h :: Blue -> Red`. — dopamane, Apr 25 '19 at 19:53
furthermore, invalid transitions are: `Red -> Blue`, `Green -> Red`, `Blue -> Green`. — dopamane, Apr 25 '19 at 20:01

score 1 · Answer 1 · answered Apr 23 '19 at 01:10

1

I recommend keeping it simple.

data Color = Red | Green | Blue

colorChange :: Color -> Bool -> Color
colorChange s     False = s
colorChange Red   _     = Green
colorChange Green _     = Blue
colorChange Blue  _     = Red

answered Apr 23 '19 at 01:10

Daniel Wagner

145,880
9
220
380

This is what I am currently using in my project and it works great for this specific example. However, if I change `colorChange Red _ = Green` to `colorChange Red _ = Blue` the compiler doesn't warn me that the structure of the state machine has changed, because `Green` and `Blue` are the same type. Thats the issue I have started to encounter as machine complexity increases and was hoping Indexed monads could help solve. Kind of like an added sanity check that the overall state machine structure is still preserved as I add more changes. – dopamane Apr 23 '19 at 01:23
@dopamane Okay. Then I don't understand the question. The types you've proposed in the question don't enforce anything like that (even after fixing up your `colorChange` type errors). Perhaps it would help if you talked a little bit about what interactions with the state machine you want to make available. Running it, I suppose? What else? What things are illegal in what states, or what interactions do you want to rule out, or... just generally what is it exactly you're trying to do? – Daniel Wagner Apr 23 '19 at 14:29

How to use indexed monad as FSM?

1 Answers1