Sample Haskell StateMachine

StateMachineProgA.idr

-- Example is presented in Marko's talk
-- https://dimjasevic.net/marko/2018/02/12/gave-a-talk-on-types-in-programming/index.html

-- This is original source in Idris
-- https://gitlab.com/mdimjasevic/uloga-tipova/blob/master/StateMachineProg-done.idr

data Grade' = A | B | C | D | E

data EssayS = Unassigned
            | Assigned
            | Writing
            | Reviewing
            | Done

data EssayCmd : Type -> EssayS -> EssayS -> Type where
  Assign   : EssayCmd () Unassigned Assigned
  Start    : EssayCmd () Assigned Writing
  Consult  : EssayCmd () state state
  Review   : EssayCmd () Writing Reviewing
  SendBack : EssayCmd () Reviewing Writing
  Grade    : Grade' -> EssayCmd Grade' Reviewing Done
  
  Pure     : ty -> EssayCmd ty state state
  (>>=)    : EssayCmd a state1 state2 ->
             (a -> EssayCmd b state2 state3) ->
             EssayCmd b state1 state3

essayProg1 : EssayCmd () Unassigned Assigned
essayProg1 = do
  Consult
  Consult
  Assign

essayProg2 : EssayCmd () Writing Writing
essayProg2 = do
  Review
  SendBack

essayProg3 : EssayCmd Grade' Reviewing Done
essayProg3 = SendBack >>= const Review >>= \_ => Grade C

essayTy : EssayCmd a s1 s2 -> Type
essayTy (Grade x) = (String, Int)
essayTy Consult   = ()
essayTy _         = String
  
r1 : essayTy Start
r1 = "Essay is started"

r2 : essayTy (Grade A)
r2 = ("Essay is done", 1)

r3 : essayTy Consult
r3 = ()

StateMachineProgB.hs

{-# LANGUAGE GADTs, TypeInType, TypeFamilies, TypeOperators, UndecidableInstances, PolyKinds #-}

module SampleStateMachine () where

import Data.Kind (Type)

data Grade' = A | B | C | D | E

data EssayS = Unassigned
            | Assigned
            | Writing
            | Reviewing
            | Done

data EssayCmd :: Type -> EssayS -> EssayS -> Type where
  Assign   :: EssayCmd () Unassigned Assigned
  Start    :: EssayCmd () Assigned Writing
  Consult  :: EssayCmd () state state
  Review   :: EssayCmd () Writing Reviewing
  SendBack :: EssayCmd () Reviewing Writing
  Grade    :: Grade' -> EssayCmd Grade' Reviewing Done

type family (>>=) (x :: EssayCmd a state1 state2) (y :: ay -> EssayCmd b state2 state3) :: EssayCmd b state1 state3

type family Const (x :: a) :: b -> a

type family EssayProg1 :: EssayCmd () Unassigned Assigned where
  EssayProg1 = Consult >>= Const Assign

type family EssayProg2 :: EssayCmd () Writing Writing where
  EssayProg2 = Review >>= Const SendBack

type family EssayProg3 :: EssayCmd Grade' Reviewing Done where
  EssayProg3 = SendBack >>= Const Review >>= Const Grade C

type family EssayTy (x :: EssayCmd a s1 s2) :: Type where
  EssayTy (Grade x) = (String, Int)
  EssayTy Consult   = ()
  EssayTy _         = String

r1 :: EssayTy Start
r1 = "Essay is started"

r2 :: EssayTy (Grade A)
r2 = ("Essay is done", 1)

r3 :: EssayTy Consult
r3 = ()