上回书说到

f:α→β ≡ B (B (B β M)) (= α)

可以使用组合子写出如下演绎规则对应的归约规则。

FαβM, αN ⊢ β(MN)

在α和β都是简单类型时这是可行的。但是如果是mltt怎么办呢，比如Π。

Curry在icl里区分两种F-obs，一种叫F-simple，就是ground type，基本类型；另一种叫F-composite，函数都是F-composite。

如果stlc仅使用蕴含片段，函数类型全是α→β的简单类型嵌套形式，那直觉蕴含和线性蕴含没有很大区别，每次mp或cut规则，都是消费掉一对(= α)和α。

但如果是Π，情况就不一样了。我们参照G组合子（Π等价）规则来看：

GαβM, αN ⊢ βN(MN)

这里第一个问题是N被复制了。这时候我们需要问一下βN如果使用显式类型时该如何理解。β在这里显然是一个F-composite，因为它能应用在N上。但是显式类型的写法里，βN是不允许的，因为N没有被正确标注类型。

我们希望看到的结果应该是β α N (MN)，这意味着Π的组合子表达式会相当复杂，因为要隔着很远把α N复制到β后面。我们动用λ形式

Π ≡ λx.λy.B (B (B (β x y) M))(= α) x y

才是符合要求的Π；当它应用在α N上时得到

λx.λy.(B (B (B (β x y) M))(= α) x y) α N
= B (B (B (β α N) M))(= α) α N

经过一系列归约后可以得到

β α N (MN)

此时因为β本身是一个函数，它可能可以展开成

(B (B (B β' M))(= α)) α N (MN)

或者它自己也是依赖类型，这里α N会再次被复制。

++++

这里看到归约和演绎规则的更多不同。首先当然还是要凑语法的形式。其次，归约是有顺序的，比如前面的Π的定义就出现了先归约外围还是先归约依赖类型的问题。

第三点，可能也是最重要的。当试图转换演绎规则到归约规则时，规则的类型线性性立刻显露出来。α是N的类型，如果N要复制，α也必须复制。在λ的形式上，这种复制就是简单的replicate，如果用组合子的话，S可以用于复制。

++++

还有一个简单一点的方式是开始只复制α，最后再复制N，此时把内层的B改成了S。这也是Curry的F改成G时的变化。

Π ≡ λx.B (B (S (β x) M))(= α) x

于是

(λx.B (B (S (β x) M)) (= α) x) α N
= B (B (S (β α) M)) (= α) α N
= B (S (β α) M) (= α α) N
= S (β α) M N
= β α N (MN)

这似乎是更好的做法因为归约序的问题也得以解决。(β α)即使发生归约也只是消去了(= α α)，然后就停住了，没有N，类型检查通过后不会继续归约。

只抽象一个x还是能手写算算的。最终这个Π的定义是

Π ≡ S (S (KB) [S (S(KS)β) (KM)]) (= α)

++++

从这些表达式可以看出，显式类型组合子的做法中，并不是类型和项交替排列的。类型确实可以混在项里一起写。