How can I encode and enforce legal FSM state transitions with a type system?

Question

Suppose I have a type Thing with a state property A | B | C,
and legal state transitions are A->B, A->C, C->A.

I could write:

transitionToA :: Thing -> Maybe Thing

which would return Nothing if Thing was in a state which cannot transition to A.

But I'd like to define my type, and the transition functions in such a way that transitions can only be called on appropriate types.

An option is to create separate types AThing BThing CThing but that doesn't seem maintainable in complex cases.

Another approach is to encode each state as it's own type:

data A = A Thing
data B = B Thing
data C = C Thing

and

transitionCToA :: C Thing -> A Thing

This seems cleaner to me. But it occurred to me that A,B,C are then functors where all of Things functions could be mapped except the transition functions.

With typeclasses I could create somthing like:

class ToA t where  
    toA :: t -> A Thing

Which seems cleaner still.

Are there other preferred approaches that would work in Haskell and PureScript?

Answer 1

Here's a fairly simple way that uses a (potentially phantom) type parameter to track which state a Thing is in:

{-# LANGUAGE DataKinds, KindSignatures #-}
-- note: not exporting the constructors of Thing
module Thing (Thing, transAB, transAC, transCA) where

data State = A | B | C
data Thing (s :: State) = {- elided; can even be a data family instead -}

transAB :: Thing A -> Thing B
transAC :: Thing A -> Thing C
transCA :: Thing C -> Thing A

transAB = {- elided -}
transAC = {- elided -}
transCA = {- elided -}