[SOLVED] Understanding of dependant types machines in Idris

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