typesstate-machineidris

# Understanding of dependant types machines in Idris

I was trying to follow the example on the Vending machine from this book. So, walking on the footsteps of the Door example, I wanted to replicate the same scenario with a simpler version of the vending machine. Thus, after defining the following:

``````VendState : Type
VendState = (Nat, Nat)

data MachineCmd : Type ->
VendState ->
VendState ->
Type where
InsertCoin : MachineCmd () (pounds, chocs)     (S pounds, chocs)
Vend       : MachineCmd () (S pounds, S chocs) (pounds, chocs)
GetCoins   : MachineCmd () (pounds, chocs)     (Z, chocs)

Pure : ty -> MachineCmd ty state state
(>>=) : MachineCmd a state1 state2 ->
(a -> MachineCmd b state2 state3) ->
MachineCmd b state1 state3
``````

I wanted to express the concept that, given a vending machine containing two chocolate bars, then I can purchase two times only if I am inserting the coins for two times, for then vending this two times. Still, running the following code leads to the subsequent error

``````machineProg : MachineCmd () (0,2) (0,0)
machineProg = do InsertCoin InsertCoin Vend Vend
``````

When checking right hand side of machineProg with expected type MachineCmd () (0, 2) (0, 0)

Type mismatch between MachineCmd () (pounds, chocs) (S pounds, chocs) (Type of InsertCoin) and _ -> _ (Is InsertCoin applied to too many arguments?)

Specifically: Type mismatch between MachineCmd () (pounds, chocs) and \uv => _ -> uv

I'm getting a similar error if I'm trying to pipeline two actions together. While the following program will be correct:

``````machineProg : MachineCmd () (0,0) (0,0)
machineProg = do GetCoins
``````

the following one, apparently syntactically equivalent to the former one and complying to the door example from the book, will raise a similar error:

``````machineProg : MachineCmd () (0,0) (0,0)
machineProg = do GetCoins GetCoins
``````

When checking right hand side of machineProg with expected type MachineCmd () (0, 0) (0, 0)

Type mismatch between MachineCmd () (pounds, chocs) (0, chocs) (Type of GetCoins) and _ -> _ (Is GetCoins applied to too many arguments?)

Specifically: Type mismatch between MachineCmd () (pounds, chocs) and \uv => _ -> uv

The part that puzzles me, for which I cannot progress with this, is interpreting how to solve the "applied to too many arguments?" issue. In fact, the apparently simple example of the door (which I'm trying to modify to obtain the former) is syntactically and type correct:

``````data DoorState = DoorOpen | DoorClosed

data DoorCmd : Type -> DoorState -> DoorState -> Type where
Open : DoorCmd () DoorClosed DoorOpen
Close : DoorCmd () DoorOpen DoorClosed
RingBell : DoorCmd () DoorClosed DoorClosed

Pure : ty -> DoorCmd ty state state
(>>=) : DoorCmd a state1 state2 ->
(a -> DoorCmd b state2 state3) ->
DoorCmd b state1 state3

doorProg : DoorCmd () DoorClosed DoorClosed
doorProg = do RingBell
Open
Close
``````

Thank you

Solution

• Apparently, it was merely a syntax error, prescribing that any subsequent action should always appear in a new line. After fixing this as follows, it seems to work.

``````machineProg : MachineCmd () (0,2) (0,0)
machineProg = do InsertCoin
InsertCoin
Vend
Vend
``````