不如去研究一下 Haskell 的 Hindley-Milner 多态类型系统？

HM 的 type inference 是纯 unification 的

没入门
告辞

那为什么不去研究下system F。。。

没入门

既然简单，我就不会叫 System F 这种晦涩的名字

多态系统可以解决，谁说 a 必须只能指代 函数a 或 量a 其中之一的？

JW 你跟我 brief 一下 Lambda 演算的基本 term 和 operation

不会

要不然我不清楚你说得到底是有引用背书的，还是你自己造的

没听说过草

还有term一说吗

指定理？

我都会自己造词了吗。。。

Lambda 演算是基于项(term) 的形式化系统，为什么没有 term？

Lambda calculus 代表的是一个语言的抽象方式（包括作用域）
以及求值的模式（beta-reducation 操作）

Lambda 演算本身不是完整的（准确的说应该是严重可扩展），但即便这样它也可以基于具名抽象引用自己的基元操作，构造新行为

Lambda 演算只有三种基本项，
Abstraction: λarg. body
上面我用的是 currying 的形式，多参函数可以变成许多单参函数
Application: (f x)
Variable: x
就是包含在 lexical scope 里的 name binding

这个是实现细节，我们谈的是基本技术

希腊字母和 bar
这个学术大佬真会写提纲，R=polymorphism U=strongness F=combination

我都忘记了它们和 一个立方体有啥大关联……

早就有结构体了

Haskell早就有record了