ADT theory “代数数据类型（ADT）是在简单类型 λ-演算（或系统 F）的基础上，通过引入积类型（Product）与和类型（Sum）的组合，并允许递归定义（µ），从而构造出结构化数据的一种类型系统扩展。它本质上是范畴论中的初始代数（Initial Algebra），对应逻辑学中的归纳类型。” Product types比如 pair 类型，本质上是把两个类型做了乘积。比如类型 L...

https://stanford-cs242.github.io/f19/ Lambda Calculus 自由变量 (Free Variables): 外层 lamdba 函数没有声明的变量 Closed Term / Conbinator: 没有自由变量的 term Alpha Conversion: 参数别名的修改，例如 λx. x 等价于 λy. y Beta Red...

TL;DR combinator 函数必须不含自由变量，combinator 之间可以组合 Y combinator 解决了匿名函数不能递归调用自身的问题 （在不能给函数命名的 lambda caculus 中也可以递归了） What is Combinator? A combinator is just a lambda expressions with no free varia...