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 :

-- A session type that enforces valid interactions with a vending machine.
%provide (VendingMachineSession : (Path -> Type)) with Protocol "vending-machine.txt"

-- An implementation of the protocol.
vendingMachine : VendingMachineSession ("waiting", "vended")
vendingMachine = do
--Action "hack" -> Won't compile as it's not a legal action described in vending-machine.txt.
  Action "pay"
  Action "return"
--Action "vend" -> Won't compile as it's not a legal action *in this state*.
  Action "pay"
  Action "select"
  Action "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" ["pay", "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", "vended")

When checking an application of constructor Protocol.>>=:
        Type mismatch between
                Command ()
                        (Choice [("pay", "waiting", "paid"),
                                 ("return", "paid", "waiting"),
                                 ("select", "paid", "selected"),
                                 ("vend", "selected", "vended")])
                        (locate "vend"
                                [("pay", "waiting", "paid"),
                                 ("return", "paid", "waiting"),
                                 ("select", "paid", "selected"),
                                 ("vend", "selected", "vended")])
                (Type of Action "vend")
        and
                Command ()
                        (Choice [("pay", "waiting", "paid"),
                                 ("return", "paid", "waiting"),
                                 ("select", "paid", "selected"),
                                 ("vend", "selected", "vended")])
                        ("waiting", "waiting")
                (Expected type)

        Specifically:
                Type mismatch between
                        locate "vend" [("pay", "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

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.

yurrriq / flying-spaghetti-monster Goto Github PK