统一问题的类型推断 [英] Type inference to unification problem

问题描述

让任何人知道类型推断问题如何

Has anyone an idea how the type inference problem

E > hd (cons 1 nil) : α0

具有打字环境

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

在统一问题上可以转让吗?

can be transferred in an unification problem?

任何帮助将不胜感激！

推荐答案

首先，重命名类型变量，以使表达式中的任何变量都不会与类型化环境中的变量发生冲突. (在您的示例中，这已经完成，因为表达式引用了{a0}，而键入环境引用了{a1，a2，a3}.

First, rename type variables so that none of the variables in your expression collide with variables in the typing environment. (In your example, this is already done since the expression references { a0 }, and the typing environment references { a1, a2, a3 }.

其次，使用新的类型变量，为表达式中的每个子表达式创建一个类型变量，产生如下内容:

Second, using new type variables, make a type variable for every subexpression within your expression, producing something like:

nil : a4
1 : a5
cons : a6
(cons 1 nil) : a7
hd : a8
hd (cons 1 nil) : a0 // already had a type variable

第三，在必须保持的类型变量之间生成一组方程式.您可以从下至上，从上至下或其他方式执行此操作.请参阅巴斯蒂安Heeren.最高质量类型错误消息. 2005.详细介绍了为什么您可能想选择一种或另一种方式.这将导致类似:

Third, generate a set of equations among type variables which must hold. You can do this from the bottom up, from the top down, or in other ways. See Heeren, Bastiaan. Top Quality Type Error Messages. 2005. for extensive details on why you might want to choose one way or another. This will result in something like:

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都只使用一次.

Note carefully that if the same function was used from the type environment twice, we would need more new type variables (in the second step, above) to unify with, so that we wouldn't accidentally make all calls to cons use the same type. I'm not sure how to explain this part more clearly, sorry. Here we are in the easy case since hd and cons are each only used once.

第四，统一这些方程，得到(如果我没有记错的话):

Fourth, unify these equations, resulting in (if I haven't made a mistake) something like:

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

很高兴，您现在知道原始表达式中每个子表达式的类型.

Rejoice, you now know the type of every subexpression in your original expression.

(警告，在这些问题上，我本人还是一个业余爱好者，我很可能犯了印刷错误，或者在这里的某个地方无意中被骗了.)

(Fair warning, I'm somewhat of an amateur myself in these matters, and I may well have made a typographical error or inadvertently cheated somewhere here.)

这篇关于统一问题的类型推断的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！