2

有谁知道类型推断问题如何

E > hd (cons 1 nil) : α0

与打字环境

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

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

任何帮助将不胜感激！

4

1 回答 1

2

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

第三，在必须成立的类型变量之间生成一组方程。您可以自下而上、自上而下或以其他方式执行此操作。见海伦，巴斯蒂安。顶级质量类型错误消息。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

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

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

于 2008-12-19T20:33:18.913 回答