re-order the vending machine example

[neilvyas]

I think this ordering makes more clear that developing total state machines in idris looks something like

1. represent the state with an enumerated type (or something more complicated)
2. represent a specification for state transitions using a GAD(D?)T of commands, with the types encoding pre- and post-conditions.
3. Implement handlers that attempt to run the corresponding commands but are total over the state, i.e. the handlers never cause the program to crash, and the handlers must satisfy the pre-conditions of all commands they invoke. Also, implement some sort of abstract event loop (machineLoop in this case).
4. implement a concrete interpreter (runMachine and run in this case).

and in particular emphasizes that the specification is almost completely distinct from the implementation, with the specification focused on conveying correctness through pre- and post-conditions and the implementation focusing on totality or handling failure cases or whatever.

Yes, it is distinct from the book, but whatever.

Also, this is literally my first day with the idris book so let me know if I'm wildly off-base. Thanks so much for all this work! I'm really excited for the day when I can use idris, or something like it, in production.

[neilvyas]

e: I also had a comment about the Effects library but then read the aside after listing 13.9.

I'd also like to know how you can deal with indexed state, e.g. your state is a mapping of usernames -> pull requests and you'd like to assert some pre-conditions in the commands like "is this user present (in the list/dictionary)" or "this user has at least one pull request" or whatever, handling the failure cases in the handlers.