有没有人一个想法如何的类型推断问题类型推断统一问题
E > hd (cons 1 nil) : α0
与定型环境
E={
hd : list(α1) → α1 ,
cons : α2 → list(α2) → list(α2),
nil : list(α3),
1 : int
}
可以在统一的问题被转移?
任何帮助真的很感谢!
有没有人一个想法如何的类型推断问题类型推断统一问题
E > hd (cons 1 nil) : α0
与定型环境
E={
hd : list(α1) → α1 ,
cons : α2 → list(α2) → list(α2),
nil : list(α3),
1 : int
}
可以在统一的问题被转移?
任何帮助真的很感谢!
首先,重命名类型变量,以便表达式中的变量都不会与键入环境中的变量发生冲突。 (在你的例子中,自从表达式引用{a0}开始,并且键入环境引用{a1,a2,a3},这已经完成。其次,使用新的类型变量,为你的每个子表达式创建一个类型变量表达,产生类似:。
nil : a4
1 : a5
cons : a6
(cons 1 nil) : a7
hd : a8
hd (cons 1 nil) : a0 // already had a type variable
第三,生成一组类型变量之间的等式必须持有您可以从下往上做到这一点,从上而下,或者以其他方式为广泛的见Heeren, Bastiaan. Top Quality Type Error Messages. 2005.详细说明你为什么想要选择这种或那种方式,这将导致如下所示:
a4 = list(a3) // = E(nil)
a5 = int // = E(1)
a6 = a2 -> list(a2) -> list(a2) // = E(cons)
// now it gets tricky, since we need to deal with application for the first time
a5 = a2 // first actual param of cons matches first formal param of cons
a4 = list(a2) // second actual param of cons matches type of second formal param of cons
a7 = list(a2) // result of (cons 1 nil) matches result type of cons with 2 params
a8 = list(a1) -> a1 // = E(hd)
// now the application of hd
a7 = list(a1) // first actual param of hd matches type of first formal param of hd
a0 = a1 // result of hd (cons 1 nil) matches result type of hd with 1 param
请注意,如果两次使用类型环境中的相同函数,我们需要更多的新类型变量(在上面的第二步中)与之统一,以便我们不会意外地调用所有的调用使用相同的类型。我不确定如何更清楚地解释这部分,对不起。在这里,我们处于一个简单的情况,因为高清和高清只能使用一次。
第四,统一这些方程,导致(如果我没有弄错)是这样的:
a4 = list(int)
a5 = int
a6 = int -> list(int) -> list(int)
a7 = list(int)
a8 = list(int) -> int
a0 = int
飘柔,你现在知道每个子表达式在你的原始表达式类型。 (公平的警告,我在这些事情上有点自己的业余爱好,而且我可能已经在这里做了一个印刷错误或无意中在某处作弊。)