关于 Morte（结构演算）打字的困惑

Question

在Morte（构造演算的实现）中，这个表达式的类型很好：

$ morte
(  λ(Nat : *)
-> λ(Zero : Nat)
-> Zero
)
(∀(a : *) ->  (a ->  a) ->  a ->  a)
(λ(a : *) ->  λ(Succ : a ->  a) ->  λ(Zero : a) ->  Zero) 
^D
∀(a : *) → (a → a) → a → a

λ(a : *) → λ(Succ : a → a) → λ(Zero : a) → Zero

但这个明显等价的表达式不是：

$ morte
(  λ(Nat : *)
-> (  λ(Zero : Nat)
   -> Zero)
   (λ(a : *) ->  λ(Succ : a ->  a) ->  λ(Zero : a) ->  Zero)
)
(∀(a : *) ->  (a ->  a) ->  a ->  a)
^D
morte: 
Context:
Nat : *

Expression: (λ(Zero : Nat) → Zero) (λ(a : *) → λ(Succ : a → a) → λ(Zero : a) → Zero)

Error: Function applied to argument of the wrong type

Expected type: Nat
Argument type: ∀(a : *) → ∀(Succ : a → a) → ∀(Zero : a) → a

这是为什么？

Answer 1

你只是放错了括号。交换第 4 行和第 5 行，输入检查通过。