Idris中依赖类型自动售货机代码的参数匹配错误排查

问题重现 #

参考《Type-Driven Development with Idris》的自动售货机示例，定义了以下类型：

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

尝试编写状态从(0,2)流转到(0,0)的程序时，出现类型错误：

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

同样，连续调用两次GetCoins也会触发类似错误：

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

而类似结构的Door示例却能正常运行：

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

错误原因 #

Idris的Do语法中，同一行内的空格会被解析为函数参数传递。你在do块里把多个命令写在同一行（比如InsertCoin InsertCoin），Idris会认为你是把第二个InsertCoin作为第一个InsertCoin的参数调用，但InsertCoin本身是一个不需要参数的命令构造器，因此触发“参数过多”的类型不匹配。

Door示例能正常运行，是因为每个命令都单独占一行，Idris会自动将其解析为>>=串联的绑定操作。

修复方案 #

在Do块中，每个命令必须单独占一行，或者用分号;分隔不同命令。

正确的自动售货机程序 #

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

连续两次GetCoins的正确写法 #

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

或者用分号分隔（语法合法但不推荐）：

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

验证 #

修复后的代码会正确完成状态流转：

1. InsertCoin：(0,2) → (1,2)
2. InsertCoin：(1,2) → (2,2)
3. Vend：(2,2) → (1,1)
4. Vend：(1,1) → (0,0)

符合预期的类型约束，类型检查可以通过。

内容的提问来源于stack exchange，提问作者jackb