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

• Can you examplify how you actually run this? Dec 15 '15 at 9:32
• I'm looking at how to improve the above functions using "path-dependent" types in the "Idris way," i.e. the idiomatic way to write each of the above functions in Idris Dec 15 '15 at 16:47
• As Idris is not exactly a common language, I think providing a little more information on how to run it would help you get some answer. I.e. is there online compilers for Idris? What is input and output from your program. Dec 15 '15 at 16:49
• Does your code actually work? I'm getting various error messages when trying to run it at www.tryidris.org Dec 15 '15 at 20:58

2 Answers

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.

• "To implement this you would need another state variable like coinInSlot in addition to the bars and pounds" no, you should add that state as a type index. That's the whole point: the type-level indices should be the ones restricting available operations, so you get a static, type check-time error if you try to e.g. return the coin from an idle machine. Jul 11 '18 at 3:29

You can index your Machine type by a (type-level) state to statically disallow certain operations. For example, suppose you only want to allow filling the machine with new chocolate bars when it's Idle. You can do that with

module VendingMachine

%default total

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

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

data MachineState = Idle | Vending
data Machine : (s : MachineState) -> Type where
IdleMachine : Choc -> Machine Idle
VendingMachine : Choc -> Pounds -> Machine Vending

init : Machine Idle
init = IdleMachine 0

fill : Choc -> Machine Idle -> Machine Idle
fill ns (IdleMachine bars) = IdleMachine (ns + bars)


Of course, the other operations also need to pay attention to the machine state. Inserting a coin starts a Vending transaction, and getting the change ends it:

insertCoin : Machine s -> Machine Vending
insertCoin (IdleMachine bars) = VendingMachine 1 bars
insertCoin (VendingMachine ps bars) = VendingMachine (1 + ps) bars

getChange : Machine Vending -> Machine Idle
getChange (VendingMachine n bars) = IdleMachine bars


The only tricky bit is vending itself, since after vending a chocolate bar, you will either remain in the transaction (if the balance is positive), or you go back to idle. This requires a bit more elbow grease, but nothing too complicated: vend0 just implements the vending logic, and nextState goes from zero-balance to idle, allowing vend to be written simply as a composition of the two:

vend0 : Machine Vending -> Machine Vending
vend0 (VendingMachine (S ps) (S bars)) = VendingMachine ps bars
vend0 (VendingMachine ps bars)         = VendingMachine ps bars

NextState : Machine Vending -> MachineState
NextState (VendingMachine Z bars) = Idle
NextState (VendingMachine (S ps) bars) = Vending

nextState : (m : Machine Vending) -> Machine (NextState m)
nextState (VendingMachine Z bars) = IdleMachine bars
nextState (VendingMachine (S ps) bars) = VendingMachine (S ps) bars

vend : (m : Machine Vending) -> Machine (NextState (vend0 m))
vend m = nextState $vend0 m  This nicely disallows definitions like ohNoWhatAreYouDoing : Machine ?s ohNoWhatAreYouDoing = fill 42$ insertCoin $init  or noSeriouslyWhatsWrongWithYou : Machine ?s noSeriouslyWhatsWrongWithYou = getChange$ vend $insertCoin$ fill 42 \$ init