В 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
Почему это?
