统一问题的类型推断答案

【问题标题】：Type inference to unification problem统一问题的类型推断
【发布时间】：2008-12-09 13:58:49
【问题描述】：

有谁知道类型推断问题是怎么回事

E > hd (cons 1 nil) : α0

与打字环境

                E={
                   hd : list(α1 ) → α1 ,
                   cons : α2 → list(α2 ) → list(α2 ),
                   nil : list(α3 ),
                   1 : int
                }

可以在统一问题中转移吗？

任何帮助将不胜感激！

【问题讨论】：

标签： lambda type-inference unification

【解决方案1】：

首先，重命名类型变量，使表达式中的变量不会与类型环境中的变量发生冲突。（在您的示例中，这已经完成，因为表达式引用 { 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

请注意，如果两次从类型环境中使用相同的函数，我们将需要更多新的类型变量（在上面的第二步中）来统一，这样我们就不会意外地使所有对 cons 的调用都使用同一类型。我不确定如何更清楚地解释这部分，抱歉。这里我们处于简单的情况，因为 hd 和 cons 都只使用一次。

第四，统一这些方程，结果（如果我没有弄错的话）如下：

a4 = list(int)
a5 = int
a6 = int -> list(int) -> list(int)
a7 = list(int)
a8 = list(int) -> int
a0 = int

庆幸，您现在知道原始表达式中每个子表达式的类型。

（公平的警告，我自己在这些事情上有点业余，我很可能在这里犯了印刷错误或无意中被骗了。）

【讨论】：