dependent type是可以用组合子算出来的

B(B(CBS)B)Ξ

来看看这个表达式能干什么，给它三个参数XYZ

B (B(CBS)B) Ξ X Y Z
(B(CBS)B) (ΞX) Y Z
B (CBS) B (ΞX) Y Z
C B S (B(ΞX)) Y Z
B (B(ΞX)) S Y Z
B (ΞX) (SY) Z
ΞX(SYZ)
∀u.Xu⊃SYZu
∀u.Xu⊃Yu(Zu)

++++

这个表达式之于马丁洛夫类型论，可以类比薛定谔方程之于量子力学了。[喵喵]