Can phantom types be used to restrict the possible transitions in a state machine?

Learn
1

Hi, there was some discussion about state machines in Elm on Slack and it was suggested that it might be possible to use phantom types to control possible state transitions in a state machine. I have no idea how.

Suppose you have some set of states defined as a tagged union:

type Game =
    Loading
  | Ready
  | InPlay GameState -- GameState models score, position, enemies still alive etc.
  | GameOver Int -- Final score

These states form a loop, once you reach GameOver you can go back to Ready and have a new game. So the possible transistions are “Loading -> Ready”, “Ready -> InPlay”, “InPlay -> GameOver”, and “GameOver -> Ready”, and no other transitions are allowed.

I would tend to model this with transition functions like:

toReady : Game -> Maybe Game
toReady game =
   case game of
      Loading -> Just Ready
      GameOver _ -> Just Ready
      _ -> Nothing

The idea of using phantom types to eliminate the Maybe and enforce possible state transition checking at compile time intrigues me. Can it be done?

5 Likes
2

I’m not sure if it can be done, but I also don’t think it’s a good idea! Phantom types have the worst name… they sound like they’d be way more useful than they usually are (but you for sure do need them sometimes!)

Basically the problem I see is that you have:

type Game a = GameState

type Loading = Loading

type Ready = Ready

type InPlay = InPlay

type GameOver = GameOver

But then what do you use as your model type? Can’t be Game a; you need to specify a concrete type at some level. But then your transition Game Loading -> Game Ready needs to change the type as specified in program. The reward is not worth the work, in my opinion.

A easier solution is to use a regular update function, but with tuples:

type Msg
    = LoadedAssets
    | InGameMsg Game.Msg

update : Msg -> Game -> (Game, Cmd Msg)
update msg game =
    case (game, msg) of
        (Loading, LoadedAssets) -> ...

        (InPlay state, InGameMsg msg) -> InPlay <| Game.update state msg

        -- you've specified all valid combinations, so everything else
        -- is invalid and should just be discarded.
        _ -> (model, Cmd.none)

Of course, this gives up a little type safety: the compiler can’t do exhaustiveness checking any more! (unless you also specify the invalid combinations but that’s annoying and noisy.) So if someone else has a better way to do this, I’m all ears!

1 Like
3

I think to do it with phantom types, there would need to be one type variable per state that can be transitioned into.

type Allowed = Allowed
-- will use the type Never, for transitions that are not allowed.

Cannot transition into Loading, so 3 type vars needed for Ready, InPlay and GameOver

type Game a b c =
    Loading
  | Ready
  | InPlay GameState
  | GameOver Int

these constructors will not be exposed, so will provide constructor functions that instantiate the type vars correctly:

loading : Game Allowed Never Never
loading = Loading 

ready : Game Never Allowed Never
ready = Ready

inPlay : Game Never Never Allowed
inPlay = InPlay

gameOver : Game Allowed Never Never
gameOver = GameOver

then define state transition functions like

toReady : Game Allowed b c -> Game Never Allowed Never

That would let the type checker enforce the state transitions, but as you say Brian, it seems a bit unwieldy with all those type parameters, so doesn’t look like a pattern that is worth using. Yes, I’ve seen phantom types suggested as a solution far too soon a few times now.

4

An alternative that doesn’t scale so badly in the number of states
is to use records with the valid transitions as fields.

type alias Loading = Game { ready : Allowed } 
type alias Ready a = Game { inPlay : Allowed } 

loading : Loading
loading = Loading

ready : Ready
ready = Ready

toReady : Game { a | ready : Allowed } -> Ready 
toReady _ = ready
1 Like
5

Interesting. I would say that is a lot better than my attempt because as new states are added it doesn’t require changing lots of places in the code to add the extra type variables. I will give this pattern a go on real world example and see how it comes out.

7

So here is a Gist where I took the suggestion of folkertdev and worked out the example more fully based on that idea:

For comparison, my previous way of modelling state machines can be found in this one:

One of the main differences is that I was able to make the state transition functions, and the map and update functions return values without Maybes. This will make composing these functions together easier, as there is no longer any need to deal with the cases where they fail to match the state or the data that they need.

The actual state is held in the game model in a field called ‘state’, so pattern matching on this in the update function is still possible:

update : Msg -> Game pre { m | state : State } -> (Game pre { m | state : State }, Cmd Msg)
update msg (Game model) =
    case (model.state, msg) of
        (Loading, LoadedAssets) -> ...

The problem though is that the type of Game in the above update function is not known completely enough to match it against the state transition functions, or map/update functions.

8

So I updated the Gist with some fresh ideas.

An important aspect of working with phantom types would seem to be that the phantom type cannot be exposed at the top-level in your model, otherwise you run into the chicken and egg situation of needing to know exactly what type you are currently modelling at the same time as using it as a type that has been deliberately designed to be varied in different situations; you can’t have it both ways.

So I had to make sure the phantom type was buried within the state machine:

type Allowed
    = Allowed

type State trans model
    = State model

type Game
    = Loading Loading
    | Ready Ready
    | InPlay InPlay
    | GameOver GameOver

type alias Loading =
    State { ready : Allowed } {}


type alias Ready =
    State { inPlay : Allowed } { definition : GameDefinition }


type alias InPlay =
    State { gameOver : Allowed } { definition : GameDefinition, play : PlayState }


type alias GameOver =
    State { ready : Allowed } { definition : GameDefinition, finalScore : Int }

For each state in the state machine, I can extract as a ‘State’ something that tells me what state transitions are possible, and what the shape of the model in that state looks like.

The example in the Gist runs through the state machine for the game, and prints out the states. As you read down the output you can see how the shape of the model varies as the game progresses, and that only fields that are relevant to each state exist when that state is active (make invalid states unreachable):

Loading (State {})

Ready (State { definition = { boardSize = 100 } })

InPlay (State { definition = { boardSize = 100 }, play = { score = 0, position = [] } })

GameOver (State { definition = { boardSize = 100 }, finalScore = 123 })

Ready (State { definition = { boardSize = 100 } })

The current state is pattern matched along with the Msg in the update function (as per Brian’s suggestion). From there on the type variables on the State type keep the map, update and state transition functions total, eliminating the need to deal with Maybes that I am already sure about.

It adds a degree of complexity, but also some parts of the code are more concise than what I was doing before. On the whole I think its an improvement.

2 Likes
9

A nice but subtle separation of concerns. update makes sure that messages match the current state — pretty much essential since asynchronous messages could arrive after a state transition — but it’s the type system that enforces that the actual state transitions are allowed.

What do the error messages look like when you try to violate the constraints?

Mark

P.S. I was thrown for a bit by mapGameDefinition since map functions tend to be container to container. I don’t have a better name to suggest, however.

10 
The argument to function `toGameOver` is causing a mismatch.

71|                                        toGameOver gameOver 
                                                  ^^^^^^^^
Function `toGameOver` is expecting the argument to be:

    State
        { a | gameOver : Allowed }
        { m | definition : GameDefinition, play : PlayState }

But it is:

    GameOver

Hint: The record fields do not match up. One has gameOver. The other has ready.
11

Perhaps its better to just have:

toGameDefinition : State p { m | definition : GameDefinition } -> GameDefinition
toGameDefinition (State model) =
    model.definition
12

I also note that my State type is identical to Tagged in joneshf/elm-tagged:

type Tagged tag value = Tagged value

joneshf/elm-tagged already provides ‘untag’ which can be used to extract the value. It also provides a ‘map’ function which I could use to implement my 'update’s.

I considered just using joneshf/elm-tagged, but it also provides the ‘tag’ and ‘retag’ operations, which could be used to tag/retag a state to a different one, and cheat the type checking on state transitions.

So for these reasons I think I will just include the ‘map’ and ‘untag’ operations with the state machine, drop my badly named map functions, and re-write my update functions in terms of map.

13

I was looking at Elm tagged recently as well to replace our very repetitive code for handling different ID types. I liked the simplification. I was less happy with the number of backdoors.

Mark