统一问题的类型推断

发布于 2024-07-09 16:35:25 字数 349 浏览 11 评论 0原文

有谁知道如何

E > hd (cons 1 nil) : α0

将打字环境的

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

类型推断问题转移到统一问题中？

任何帮助将不胜感激！

原文

Has anyone an idea how the type inference problem

E > hd (cons 1 nil) : α0

with the typing environment

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

can be transferred in an unification problem?

Any help would really be appreciated!

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

蓝海似她心 2024-07-16 16:35:25

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

，在类型变量之间生成一组必须成立的方程。您可以从下往上、从上往下或以其他方式执行此操作。 .nl/bastiaan/phdthesis/" rel="nofollow noreferrer">Heeren, Bastiaan。顶级质量类型错误消息。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 use 进行所有调用我不知道如何更清楚地解释这部分，抱歉，我们处于简单的情况，因为 hd 和 cons 都只使用一次。

第四，统一这些方程，得到（如果我没有犯错的话）类似的结果：

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

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

（公平警告，我自己在这些问题上有点业余，我很可能犯了一个印刷错误或无意中在此处作弊。）

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

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

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.)

回复收藏 0 原文

~没有更多了~