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

You need to sign in to view this topic

This topic created in 4302 days ago, the information mentioned may be changed or developed.

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

hindlery

milner

类型

7 replies • 2014-10-20 05:58:18 +08:00

ffffwh

Oct 20, 2014

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

tan90ds

Oct 20, 2014

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

ffffwh

Oct 20, 2014

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

实例化是啥意思？

ffffwh

Oct 20, 2014

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

tan90ds

Oct 20, 2014

@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

Oct 20, 2014 via iPhone

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

tan90ds

Oct 20, 2014

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