Vending Machine in Idris

Type Driven Development with Idris demonstrates how Idris can be used to build a Finite State Machine for a vending machine.

Please critique my implementation. I'm new to dependent types, so I'm not sure if dependent types would enhance this implementation. In other words, if path-dependent types would significantly improve this FSM, then I'm not sure how.

module VendingMachine

-- Pounds is a form of currency/money
Pounds : Type
Pounds = Nat

-- the Machine dispenses/vends chocolate candy bars
Choc : Type
Choc = Nat

data Machine = Mach Pounds Choc

fill : Machine -> Nat -> Machine
fill (Mach ps bars) ns = Mach ps (bars + ns)

init : Machine
init = Mach 0 0

insertCoin : Machine -> Machine
insertCoin (Mach ps bars) = (Mach (ps + 1) bars)

vend : Machine -> Machine
vend (Mach Z bars)          = Mach Z bars
vend (Mach (S ps) (S bars)) = Mach ps bars

getChange : Machine -> Machine
getChange (Mach Z bars) = Mach Z bars
getChange (Mach n bars) = Mach 0 bars

I've tried searching and googling for variations on how to solve this kind of problem, and all the searches turn up either posts made by you or references to the original documentation and the Effects library. In other words, there is not much online documentation available for the Idris language, and I'm a little unsure as to whether it is worthwhile pursuing this language. However I can comment a little on general issues in your code and state machines:

• Naming is slightly inconsistent – For the types I would use Pounds and ChocolateBars (or Bars), with the corresponding pounds and bars when used as parameters

• Be consistent using either (S pounds) or (pounds + 1) - Try sticking to one specific notation to indicate the incremented version. The same goes for the use of Z or 0. Be consistent.

• What is the price of one chocolate bar? If it´s "1 pound" which the code related to vend it doesn't make sense to have a getChange variant. This is more of a removePounds method.

-
States are not interlinked – I would define more states, with actions clearly linked to the states. As it stands there is no connection between insertCoin, vend and possibly the getChange actions. All of these can be executed in an arbitrarily sequence depending on availability of pounds and bars in the vending machine.
Alternative version in pseudo code:

• Empty – An empty vending machine, with no money or no bars

• action: fill → state: Idle: Increases the quantity of bars

• Idle - A vending machine with no currently inserted money, but has bars

• action: insertCoin → state: ReadyForVending: changes the coinInSlot variable

• action: removePounds → state: Idle: Clears the pounds variable

• ReadyForVending – With inserted money, and bars

• action: vend → state: Idle: Removes one bars, and clears coinInSlot

• action: returnCoin → state: Idle: Clear the coinInSlot

To implement this you would need another state variable like coinInSlot in addition to the bars and pounds.

• Machine vs Mach is unclear – I'm not sure if you've gotten it quite correct with these, and at least the names are kind of confusing. I think rather than the strange extra notation of Mach I would've used Tuples or Records to describe the internal state, and this would simplify some of the following code as well.

• Use effects for the state machine – In the online compiler I found, there was not support for effects, but the documentation (and some slides/post/papers) I found indicates that to properly implement a state machine you should use the Effects library (hangman), which aren't supported in the online compilator.

I tried compiling a new version using the online compilator at http://www.tryidris.org, but there was loads of errors and it seemed a little unstable. In addition, when trying to get information from OP regarding how you actually are running your code, and expected output, I didn't get much response. As such, I've failed getting you alternate refactored code better implementing a type dependent state machine in Idris.

StackExchange Code Review Q#112408, answer score: 2