请问这里有熟悉 Hindlery-Milner 类型系统的么？

[tan90ds]

当把一个 type scheme 实例（instance）化的时候，是不是要把所有 universally quantified variable （就是那些前边带 $\forall$ 的）都替换成某个具体的 type？还是可以只替换一部分？

[ffffwh]

我什么都不懂。
不过你一说全称量词好像在王垠的《Hindley-Milner 类型系统的根本性错误》见过

[tan90ds]

@ffffwh 他的那篇文我看到了。我只是初学，总不能门都还没摸到就想着踢 HM 的馆子……
我只是奇怪为啥都搜不到什么正经的对 HM 的描述，学的时候是用英文学的，教授没给教材，中文的术语也不知道是哪个……一头雾水

[ffffwh]

type scheme是指类型标记吧，像foldr :: (x->z)->z->[x]->z。
全称量词好像一般省略了，具体该放哪儿不明。

实例化是啥意思？

[ffffwh]

修正
(x->z->z)->z->[x]->z

[tan90ds]

@ffffwh type scheme 是用在polymorphic 类型系统里的，大概是：
\forall alpha_1 alpha_2 ... alpha_n.tau 这样
这个东西是用来在类型推导时给 alpha type 确定一个具体的类型的，比如用OCaml写：
(fun x -> x) (1, true)，相当于 Haskell 的 \x->x，类型是 'a -> 'a。
在推导的时候，'a 会被分别确定为 Int 和 Bool，这就叫实例化（可能正式的中文名不是这个）

[keyanzhang]

还没有学到这里……只是好奇，是否方便透露您在哪所学校？这是一节怎样的课程？

[tan90ds]

@keyanzhang 学校是很普通的美本。这节是入门级的讲程序语言的课程，从有限自动机讲起，然后讲正则表达式、形式语言、函数式编程用 OCaml 讲了两周，现在在研究 HM 类型系统，以后会用 OCaml 写它自己的 parser。