这是一个创建于 3680 天前的主题，其中的信息可能已经有所发展或是发生改变。
当把一个 type scheme 实例（instance）化的时候，是不是要把所有 universally quantified variable （就是那些前边带 $\forall$ 的）都替换成某个具体的 type？还是可以只替换一部分？
 |
1
ffffwh 2014-10-20 04:15:48 +08:00
我什么都不懂。
不过你一说全称量词好像在王垠的《Hindley-Milner 类型系统的根本性错误》见过 |
 |
2
tan90ds OP @ffffwh 他的那篇文我看到了。我只是初学，总不能门都还没摸到就想着踢 HM 的馆子……
我只是奇怪为啥都搜不到什么正经的对 HM 的描述，学的时候是用英文学的，教授没给教材，中文的术语也不知道是哪个……一头雾水 |
|
3
ffffwh 2014-10-20 04:49:11 +08:00  1
type scheme是指类型标记吧，像foldr :: (x->z)->z->[x]->z。
全称量词好像一般省略了，具体该放哪儿不明。 实例化是啥意思？ |
|
4
ffffwh 2014-10-20 04:50:35 +08:00
修正
(x->z->z)->z->[x]->z |
|
5
tan90ds OP @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，这就叫实例化（可能正式的中文名不是这个） |
 |
6
keyanzhang 2014-10-20 05:38:51 +08:00 via iPhone
还没有学到这里……只是好奇，是否方便透露您在哪所学校？这是一节怎样的课程？
|
|
7
tan90ds OP @keyanzhang 学校是很普通的美本。这节是入门级的讲程序语言的课程，从有限自动机讲起，然后讲正则表达式、形式语言、函数式编程用 OCaml 讲了两周，现在在研究 HM 类型系统，以后会用 OCaml 写它自己的 parser。
|
Select Language