当前位置：文江博客话题详情

输入 Y 组合符

发布于 2024-09-19 16:44:57 字数 371 浏览 6 评论 0原文

http://muaddibspace.blogspot.com/2008 /01/type-inference-for-simply-typed-lambda.html 是 Prolog 中简单类型 lambda 演算的简洁定义。

看起来不错，但随后他声称要为 Y 组合器分配一个类型……而从真正意义上讲，向 lambda 演算添加类型的整个目的是拒绝为 Y 组合器之类的东西分配类型。

任何人都可以准确地看出他的错误或（更有可能的是）我的误解在哪里吗？

原文

分享到QQ

分享到微博

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

发布评论

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

酒与心事 2024-09-26 16:44:57

Y 组合器的基本形式

Y f = (\x -> f (x x)) (\x -> f (x x))

只是无法使用本文中提出的简单类型系统来键入。

还有其他更简单但有意义的示例，无法在该级别上键入：

例如，

test f = (f 1, f "Hello")

这显然适用于 test (\x -> x) 但我们无法给出更高级别的类型但

test :: (∀a . a -> a) -> (Int, String)

即使在更高级的类型系统中，例如允许上述操作的 Haskell GHCI 扩展，Y 仍然很难输入。

因此，考虑到递归的可能性，我们可以只需定义并使用 fix 组合器

fix f = f (fix f)

与 fix :: (a -> a) ->;一个

The Y combinator in its basic form

Y f = (\x -> f (x x)) (\x -> f (x x))

just cannot be typed using the simple type system proposed in the article.

There are other, much easier but meaningful examples that cannot be typed on that level:

Take e.g.

test f = (f 1, f "Hello")

This obviously works for test (\x -> x) but we cannot give the higher-ranked type that was required here, namely

test :: (∀a . a -> a) -> (Int, String)

But even in more advanced type systems like the GHCI extensions of Haskell which allow the above, Y is still hard to type.

So, given the possibility of recursion, we can just define and work using the fix combinator

fix f = f (fix f)

with fix :: (a -> a) -> a

回复收藏 0 原文

硪扪都還晓 2024-09-26 16:44:57

键入应该禁止 self 应用程序，应该不可能找到 (tt) 的类型。如果可能的话，t 将具有类型 A ->; B，我们就会有 A = A -> B。由于 self 应用程序是 Y 组合器的一部分，因此也不可能为其指定类型。

不幸的是，许多 Prolog 系统都允许 A = A -> A 的解决方案。 B。这种情况发生的原因有很多，要么 Prolog 系统允许循环项，那么统一就会成功，并且生成的绑定甚至可以进一步处理。或者Prolog系统不允许循环项，那么就看它是否实现了发生检查。如果发生检查已打开，则统一将不会成功。如果发生的检查关闭，则统一可能会成功，但无法进一步处理生成的绑定，很可能导致打印或进一步统一时堆栈溢出。

所以我猜想这种类型的循环统一发生在所使用的 Prolog 系统的给定代码中，并且没有被注意到。

解决该问题的一种方法是打开发生检查，或者通过显式调用 unify_with_occurrs_check/2 来替换代码中发生的任何统一。

最好的问候

P.S.：以下 Prolog 代码效果更好：

/**
 * Simple type inference for lambda expression.
 *
 * Lambda expressions have the following syntax:
 *    apply(A,B): The application.
 *    [X]>>A: The abstraction.
 *    X: A variable.
 *
 * Type expressions have the following syntax:
 *    A>B: Function domain
 *
 * To be on the save side, we use some unify_with_occurs_check/2.
 */

find(X,[Y-S|_],S) :- X==Y, !.
find(X,[_|C],S) :- find(X,C,S).

typed(C,X,T) :- var(X), !, find(X,C,S), 
                unify_with_occurs_check(S,T).
typed(C,[X]>>A,S>T) :- typed([X-S|C],A,T).
typed(C,apply(A,B),R) :- typed(C,A,S>R), typed(C,B,T), 
                unify_with_occurs_check(S,T).

以下是一些示例运行：

Jekejeke Prolog, Development Environment 0.8.7
(c) 1985-2011, XLOG Technologies GmbH, Switzerland
?- typed([F-A,G-B],apply(F,G),C).
A = B > C
?- typed([F-A],apply(F,F),B).
No
?- typed([],[X]>>([Y]>>apply(Y,X)),T).
T = _T > ((_T > _Q) > _Q)

Typing should disallow self application, it should not be possible to find a type for (t t). If it where possible then t would have a type A -> B, and we would have A = A -> B. Since self application is part of Y combinator, its also not possible to give a type to it.

Unfortunately many Prolog systems allow a solution for A = A -> B. This happens on many grounds, either the Prolog system allows circular terms, then the unification will succeed and the resulting bindings can even further be processed. Or the Prolog system does not allow circular terms, then it depends on whether it implements an occurs check. If the occurs check is on, then unification will not succeed. If the occurs check is off, then the unification might succeed but the resulting bindings can not further be processed, most likely leading to stack overflow in printing or further unifications.

So I guess a circular unification of this type happens in the given code by the used Prolog system and it gets unnoticed.

One way to solve the issue would be to either switch on the occurs check or to replace any of the occuring unifications in the code by an explicit call to unify_with_occurs_check/2.

Best Regards

P.S.: The following Prolog code works better:

/**
 * Simple type inference for lambda expression.
 *
 * Lambda expressions have the following syntax:
 *    apply(A,B): The application.
 *    [X]>>A: The abstraction.
 *    X: A variable.
 *
 * Type expressions have the following syntax:
 *    A>B: Function domain
 *
 * To be on the save side, we use some unify_with_occurs_check/2.
 */

find(X,[Y-S|_],S) :- X==Y, !.
find(X,[_|C],S) :- find(X,C,S).

typed(C,X,T) :- var(X), !, find(X,C,S), 
                unify_with_occurs_check(S,T).
typed(C,[X]>>A,S>T) :- typed([X-S|C],A,T).
typed(C,apply(A,B),R) :- typed(C,A,S>R), typed(C,B,T), 
                unify_with_occurs_check(S,T).

Here are some sample runs:

Jekejeke Prolog, Development Environment 0.8.7
(c) 1985-2011, XLOG Technologies GmbH, Switzerland
?- typed([F-A,G-B],apply(F,G),C).
A = B > C
?- typed([F-A],apply(F,F),B).
No
?- typed([],[X]>>([Y]>>apply(Y,X)),T).
T = _T > ((_T > _Q) > _Q)

回复收藏 0 原文

~没有更多了~