了解 Idris 中的依赖类型机器

Question

我试图按照这书中的自动售货机示例进行操作。因此，沿着门示例的脚步，我想用更简单版本的自动售货机来复制相同的场景。因此，在定义以下内容后：

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

我想表达的概念是，给定一个包含两块巧克力的自动售货机，那么只有我插入两次硬币才能购买两次，然后自动售货两次。尽管如此，运行以下代码仍会导致后续错误

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

检查 machineProg 右侧的预期类型时 MachineCmd () (0, 2) (0, 0)

之间的类型不匹配 机器命令() （磅、巧克力） （英镑、巧克力）（InsertCoin 类型） 和 _ -> _ （InsertCoin 是否应用于太多参数？）

具体来说： 之间的类型不匹配 MachineCmd ()（磅、巧克力） 和 \uv => _ -> uv

如果我尝试将两个操作管道化在一起，我会遇到类似的错误。虽然以下程序是正确的：

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

下面这个，显然在语法上与前一个相同，并且遵循书中的门示例，会引发类似的错误：

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

检查 machineProg 右侧的预期类型时 MachineCmd () (0, 0) (0, 0)

之间的类型不匹配 MachineCmd () (磅, 巧克力) (0, 巧克力) (GetCoins 类型) 和 _ -> _ （GetCoins 是否应用于太多参数？）

具体来说： 之间的类型不匹配 MachineCmd ()（磅、巧克力） 和 \uv => _ -> uv

令我困惑、无法继续推进的部分是解释如何解决“应用于太多参数？”问题。事实上，门的明显简单示例（我正在尝试修改以获得前者）在语法和类型上都是正确的：

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

谢谢你

Answer 1

显然，这只是一个语法错误，规定任何后续操作都应始终出现在新行中。按如下方式修复后，似乎可以工作。

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