这一篇非常炸裂的是有一种18世纪工程师暴力使用微积分的精神。它有一个第一眼完全无法接受的定义，就是 组合子或λ里的「应用」，MN，可以被解释成逻辑上逆蕴含，N⊃M；类似的一个项N和它的类型α的关系是 N ⊢ α 于是根据演绎定理有 ⊢ N⊃α 于是 ⊢ αN 在整个体系的规则推导上，完全不冲突，无论是非依赖类型还是依赖类型。Curry在书上写出过很多次 ⊢ξN 来表达F-obs ξ和其它组合子项N的关系，但他没有像我这种民科滥用的符号的勇气。[允悲][二哈][喵喵]