В Morte (реализация исчисления конструкций) это выражение хорошо типизировано: $ morte ( λ(Nat : *) -> λ(Zero : Nat) -> Zero ) (∀(a : *) -> (a -> a) -> a -> a) (λ(a : *) -> λ(Succ : a -> a) -> λ(Zero : a) ->...