Model state machines with types | Blog: Mr. Mathiesen

Background

This seems a topic that keeps showing up again and again. After every MF#K Meetup last Tuesday of every month we always go out for a couple of beers and speak heavily in favor of the language that we like the most. There are people who seem to need types to code, I will include myself in this group, while others seem to do fine with languages without types as for example Clojure, Erlang, Elixir, … My former workmate, Brandon Lucas, keeps trolling on how you can’t model a state-machine with types, and until I wrote this post, I would totally agree.

What you normally see in blog post when this topic is explained is something similar to this (I will draw some ASCII art to give a better understanding):

                           +: State
                           #: Transition
                          
                           +--------------------------+
                           |   TurnedOn (On Switch)   |
                           +--------------------------+
                                ʌ              |
                                |              v
                           #----------#   #-----------#
                           |  TurnOn  |   |  TurnOff  |
                           #----------#   #-----------#
                                ʌ               |
                                |               v
                           +--------------------------+
                           |  Turnedoff (Off Switch)  |
                           +--------------------------+

1
2
3
4
5
6
7
8
9
10
11
12
module WhatYouNormallySee =
    type State = On | Off
    
    // Bug due to lack of testing
    // Note: ALWAYS use FsCheck, F# implementation of Haskells QuickCheck
    let transition = function
        | On  -> On
        | Off -> On
    
    let transitionFixed = function
        | On  -> Off
        | Off -> On

What is represented here is a state machine for a light switch. The state is defined as a sum type (algebraic data type) of the two values it can be. But, then when you need to perform the state transition, you would see how people fallback to a function to handle this logic.

In my example, I have deliberately introduced a bug in the transition function just to prove why this approach is problematic.

This is one of the misconceptions that you hear people talking about when they make the transition to functional programming languages. They think just because they have modeled the domain with a few sum and product types (algebraic data types) it’s all good and you can then claim absolute sentences like: “Make illegal states unrepresentable” and “Making Impossible States Impossible” and therefore you probably don’t need to test that part of the code, which is obviously a wrong misconception of what the authors tries to point out.

We need to be very thoughtful (and mostly careful) when we make those kind of statements, specially due to the audiences that might receive (conceive) these messages.

Note: I’m not dishing neither “Yaron Minsky” nor “Richard Feldman” as I have a HUGE respect for both on their work on OCaml and Elm respectively.

Use the type system instead of functions

So how can we move the logic from the function into the type domain by using the type system?

Well firstly we will need to introduce the following three simple concepts:

Phantom Types: Are parametrised types whose parameters do not all appear on the right-hand side of its definition. Example: type 'a Foo = Bar.
Function Types: Define a function signature as a type. Example for the identity function: type 'a Id = 'a -> 'a.
Not accessible Sum Type Case Constructors: By hiding the underlying case constructors for a given sum type, you can ensure that only specific parts of the code can instantiate your type. Example: type FooBar = private | Foo of int | Bar of float

Lets see how I use them to re-model the light switch state machine:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
module Light =
    type 'a Switch = private | State
    
    and TurnedOn  = On  Switch
    and TurnedOff = Off Switch
    
    and On  = On
    and Off = Off
    
    and TurnOn  = TurnedOff -> TurnedOn
    and TurnOff = TurnedOn  -> TurnedOff
    
    module Switch =
        let private initHelper = State
        let private turnHelper = fun _ -> State
        
        let initOn  : TurnedOn  = initHelper
        let initOff : TurnedOff = initHelper
        
        let turnOn  : TurnOn    = turnHelper
        let turnOff : TurnOff   = turnHelper
    
    module Output =
        // Expensive call cos of .NET Type Reflection
        let state (x:'a Switch)  =
            match typedefof<'a> with
                | t when t = typedefof<On>  -> "on"
                | t when t = typedefof<Off> -> "off"
                | _________________________ -> "invalid type"

> 
module Light = begin
  type 'a Switch = private | State
  and TurnedOn = On Switch
  and TurnedOff = Off Switch
  and On = | On
  and Off = | Off
  and TurnOn = TurnedOff -> TurnedOn
  and TurnOff = TurnedOn -> TurnedOff
  module Switch = begin
    val private initHelper : 'a Switch
    val private turnHelper : 'a -> 'b Switch
    val initOn : TurnedOn
    val initOff : TurnedOff
    val turnOn : TurnOn
    val turnOff : TurnOff
  end
  module Output = begin
    val state : x:'a Switch -> string
  end
end

We combine the concepts 1. and 3. to define the State type, which we limit to only two states: TurnedOn and TurnedOff, which also requires to introduce two type terms: On and Off.

Finally, we just need to expand our domain with the transition types, which we can use concept 2. to create two transition states: TurnOn and TurnOff, which will subsequently require to have the opposite state as input parameter.

That’s it. Now our domain model contains all the logic while our functions just are pure interfaces with no logic whatsoever, see both helper functions, for the initXXX and turnXXX functions. The functions just return the internal State type, which gets tagged by the type definitions. Pretty nifty right?

And we can be sure that no invalid State is created because we ensured that it can’t be instantiated from outside the module (and sub modules). So even though type 'a Switch is a generic type, we have limited only to the two states mentioned before.

The only minor issue is that type abbreviation (alias) in F# are erased at compile time and therefore not available at runtime, as Marcus Griep points out in the following tweet, therefore it’s a bit more difficult to output the currently state (see in next coding blocks how this can be overcome).

Demo:

So lets see how its used:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
open Light

let on =
    Switch.initOff
    |> Switch.turnOn

let off =
    on
    |> Switch.turnOff

let error =
    off
    // |> Switch.turnOff
    (* error FS0001: Type mismatch. Expecting a
           TurnedOff -> 'a    
       but given a
           TurnOff    
       The type 'Off' does not match the type 'On' *)

// on = off
(* error FS0001: Type mismatch. Expecting a
       TurnedOn    
   but given a
       TurnedOff    
   The type 'On' does not match the type 'Off' *)

on  |> Output.state
off |> Output.state

Produces the following output:

> val on : TurnedOn
> val off : TurnedOff
> val error : TurnedOff
> val it : string = "on"
> val it : string = "off"

A bit more complex example where we just want to automate the switch to turn on/off a couple of times in a row. To be able to do this, we introduce the Either sum type for better readability, but the built-in Choice<'a,'b> F# type could be used as well. This construct will also allow us to make a better output printer than the one that is based on .NET Reflection as we have a guarantee of which types go in to the Left and Right wrappers.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
// You can disable this warning by using '--mlcompatibility' or '--nowarn:62'
#nowarn "62" 

module Util =
    type ('a,'b) Either = Right of 'a | Left of 'b

open Util
open Light

let blinking : (TurnedOn,TurnedOff) Either -> (TurnedOn,TurnedOff) Either =
    function
        | Right on  -> on  |> Switch.turnOff |> Left
        | Left  off -> off |> Switch.turnOn  |> Right

// Or just "on" or "off" as we have the certainty of the types and it's a lot
// cheaper than .NET Reflection
let sprint : (TurnedOn,TurnedOff) Either -> string = function
    | Right s -> s |> Output.state // or just "on"
    | Left  s -> s |> Output.state // or just "off"

let foldHelper = function
    | [   ] -> fun _ -> [                   ]
    | x::xs -> fun _ -> blinking x :: x :: xs

([ Left off ], [ 1 .. 15 ])
||> List.fold foldHelper
|> List.map sprint
|> List.iter (printf "%s ")

> 
module Util = begin
  type ('a,'b) Either =
    | Right of 'a
    | Left of 'b
end

> 
val blinking :
  _arg1:(TurnedOn,TurnedOff) Either -> (TurnedOn,TurnedOff) Either

> 
val sprint : _arg1:(TurnedOn,TurnedOff) Either -> string

> 
val foldHelper :
  _arg1:(TurnedOn,TurnedOff) Either list ->
    ('a -> (TurnedOn,TurnedOff) Either list)

> on off on off on off on off on off on off on off on off val it : unit = ()

Conclusion:

I hope I can convince others that it is possible to model a state machine exclusively by using the type system, while keeping the logic out of the function layer. It uses a few type tricks that are present in F# but probably also in other ML alike languages.

Note: Don’t forget to ALWAYS use FsCheck, F# implementation of Haskells QuickCheck, even if you use this kind of approach. We are all human and therefore can fail. If you just remember this last part, You would make me a happy person.

References:

Wikipedia:
- Finite-state machine