Created
October 31, 2014 15:11
-
-
Save edwinb/792e8d11ab71ccbdbebc to your computer and use it in GitHub Desktop.
State machines in types
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- 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 | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment