Flying Spaghetti Monster
An Idris type provider for communicating type-checkable protocols.
Usage
This is a verified session using the protocol described in vending-machine.txt:
%provide (VendingMachineSession : (Route -> Type)) with Protocol "vending-machine.txt"
-- An implementation of the protocol.
vendingMachine : VendingMachineSession ("waiting", const "waiting")
vendingMachine = do
--`Do "hack"` wouldn't compile, because it's not a legal action described in vending-machine.txt.
Do "insert-coin"
--`Do "vend"` wouldn't compile, because it's not a legal action *in this state*.
Do "insert-coin"
-- Some actions can fail, in which case the compiler checks all the paths end in the right state.
Success <- Try "select" | Failure => do Do "return"; Fail
Do "vend"If you try and use the illegal action "hack", you'll get the following compilation error:
Example.idr:27:10:When checking right hand side of vendingMachine with expected type
VendingMachineSession ("waiting", "vended")
When checking argument membership to constructor Protocol.Action:
Can't find a value of type
Elem "hack" ["insert-coin", "return", "select", "vend"]
The Idris compiler reads the description of the protocol and then type checks it. Even though the actions are specified by strings, Idris is able to verify that they're within the set of actions specified.
But that's not all. The Idris compiler is able to type check that the order of the actions fits the specified protocol. If you try and use the legal action "vend" at the wrong time, you'll get another compilation error.
It's a little long, but it clearly indicates that there's no "vend" action that has the appropriate source and destination states:
Example.idr:31:3:When checking right hand side of vendingMachine with expected type
VendingMachineSession ("waiting", const "waiting")
When checking an application of constructor Protocol.>>=:
Type mismatch between
Command ()
(Choice [("insert-coin", "waiting", "paid"),
("return", "paid", "waiting"),
("select", "paid", "selected"),
("vend", "selected", "vended")])
(locate "vend"
[("insert-coin", "waiting", "paid"),
("return", "paid", "waiting"),
("select", "paid", "selected"),
("vend", "selected", "vended")])
(Type of Action "vend")
and
Command ()
(Choice [("insert-coin", "waiting", "paid"),
("return", "paid", "waiting"),
("select", "paid", "selected"),
("vend", "selected", "vended")])
("waiting", "waiting")
(Expected type)
Specifically:
Type mismatch between
locate "vend" [("insert-coin", "waiting", "paid"),
("return", "paid", "waiting"),
("select", "paid", "selected"),
("vend", "selected", "vended")]
and
("waiting", "waiting")
Unification failure
See the example for more detail.
FFI
Idris Type Providers depend on a foreign function interface. That's turned off by default in the version of Idris on Stack. To install with it enabled:
stack install idris --flag idris:FFI --flag idris:extra-deps libffi-0.1
Building
You can build the example:
$ ./build
$ ./runexample
Todo
- Generate a finite state machine type from data.
- Supply the type via a type provider.
- Get the type error messages as good as they were before I started abstracting everything.
- Support transitions that can fail.
- Read the list of valid steps over HTTP.
- Use error reflection to improve error reporting.
- Package it.
- Set up a sample protocol registry.