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

V2EX = way to explore

V2EX 是一个关于分享和探索的地方

现在注册

已注册用户请登录

这是一个创建于 3695 天前的主题，其中的信息可能已经有所发展或是发生改变。

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

hindlery

milner

类型

7 条回复 • 2014-10-20 05:58:18 +08:00

ffffwh

2014-10-20 04:15:48 +08:00

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

tan90ds

2014-10-20 04:30:14 +08:00

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

ffffwh

2014-10-20 04:49:11 +08:00

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

实例化是啥意思？

ffffwh

2014-10-20 04:50:35 +08:00

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

tan90ds

2014-10-20 05:02:34 +08:00

@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

2014-10-20 05:38:51 +08:00 via iPhone

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

tan90ds

2014-10-20 05:58:18 +08:00

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