Haskell state machines -- impossible states unrepresentable :D

Main.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}

module Main where

import Data.Function ((&))

data Locked
data Open
data Closed

data Door s where
  Locked :: Door Locked
  Closed :: Door Closed
  Opened :: Door Open

deriving instance (Show (Door s))

initial :: Door Locked
initial = Locked

unlock :: Door Locked -> Door Closed
unlock = const Closed

open :: Door Closed -> Door Open
open = const Opened

close :: Door Open -> Door Closed
close = const Closed

lock :: Door Closed -> Door Locked
lock = const Locked

-- More complex now

data Parked
data Idling
data FirstGear
data SecondGear
data ThirdGear
data Stalled

data Car s where
  Parked :: Car Parked
  Idling :: Car Idling
  FirstGear :: Car FirstGear
  SecondGear :: Car SecondGear
  ThirdGear :: Car ThirdGear
  Stalled :: Car Stalled

deriving instance (Show (Car s))

data Parkable car where
  ParkableIdling :: Car Idling -> Parkable (Car Idling)
  ParkableFirstGear :: Car FirstGear -> Parkable (Car FirstGear)

park :: Parkable car -> Car Parked
park = const Parked

type family Ignite car where
  Ignite (Car Stalled) = Car Stalled
  Ignite (Car Parked) = Car Idling

data Ignitable car where
  IgnitableStalled :: Car Stalled -> Ignitable (Car Stalled)
  IgnitableParked :: Car Parked -> Ignitable (Car Parked)

ignite :: Ignitable car -> Ignite car
ignite IgnitableStalled{} = Stalled
ignite IgnitableParked{} = Idling

idle :: Car FirstGear -> Car Idling
idle = const Idling

data UpShiftable car where
  UpShiftableIdling :: Car Idling -> UpShiftable (Car Idling)
  UpShiftableFirst :: Car FirstGear -> UpShiftable (Car FirstGear)
  UpShiftableSecond :: Car SecondGear -> UpShiftable (Car SecondGear)

type family UpShift car where
  UpShift (Car Idling) = Car FirstGear
  UpShift (Car FirstGear) = Car SecondGear
  UpShift (Car SecondGear) = Car ThirdGear

shiftUp :: UpShiftable car -> UpShift car
shiftUp UpShiftableIdling{} = FirstGear
shiftUp UpShiftableFirst{} = SecondGear
shiftUp UpShiftableSecond{} = ThirdGear

data DownShiftable car where
  DownShiftableSecond :: Car SecondGear -> DownShiftable (Car SecondGear)
  DownShiftableThird :: Car ThirdGear -> DownShiftable (Car ThirdGear)

type family DownShift car where
  DownShift (Car SecondGear) = Car FirstGear
  DownShift (Car ThirdGear) = Car SecondGear

shiftDown :: DownShiftable car -> DownShift car
shiftDown DownShiftableSecond{} = FirstGear
shiftDown DownShiftableThird{} = SecondGear

carInitial :: Car Parked
carInitial = Parked

main :: IO ()
main = do
  print $ initial & unlock & open
  print $ initial & unlock & open & close & lock
  -- The following won't compile
  -- print $ initial & open & unlock

  print $
    carInitial
      & ignite . IgnitableParked
      & shiftUp . UpShiftableIdling
      & shiftUp . UpShiftableFirst
      & shiftDown . DownShiftableSecond
      & idle
      & park . ParkableIdling

  -- The following won't compile
  -- print $
  --   carInitial
  --     & ignite . IgnitableParked
  --     & shiftUp . UpShiftableIdling
  --     & shiftUp . UpShiftableFirst
  --     & idle
  --     & park . ParkableIdling