State machines in types

door.idr

-- Version 1, no possible failure

  openDoor : { [DOOR Closed] ==> [DOOR Open] } Eff ()
  openDoor = call OpenDoor
  
  closeDoor : { [DOOR Open] ==> [DOOR Closed] } Eff ()
  closeDoor = call CloseDoor
  
  knock : { [DOOR Closed] } Eff ()
  knock = call Knock
  
  doorProg : { [DOOR Closed] } Eff ()
  doorProg = do knock
                openDoor
                closeDoor
               
-- Version 2, door might jam

  openDoor : { [DOOR Closed] ==>
               {jammed} [DOOR (case jammed of
                                    Jammed => Closed
                                    OK => Open)] } Eff Jam
  openDoor = call OpenDoor
  
  closeDoor : { [DOOR Open] ==> [DOOR Closed] } Eff ()
  closeDoor = call CloseDoor
  
  knock : { [DOOR Closed] } Eff ()
  knock = call Knock
  
  doorProg : { [STDIO, DOOR Closed] } Eff ()
  doorProg = do knock
                OK <- openDoor | Jammed => putStrLn "Jammed!"
                putStrLn "Successfully opened"
                closeDoor