输入 Y 组合符

Question

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

看起来不错，但随后他声称要为 Y 组合器分配一个类型......而实际上，向 lambda 演算添加类型的全部目的是拒绝为 Y 组合器之类的东西分配类型。

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

Answer 1

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

Answer 2

打字应该禁止自我应用，不应该找到一个类型 (t t). 。如果可能的话 t 会有一个类型 A -> B, ，我们会有 A = A -> B. 。由于 self 应用程序是 Y 组合器的一部分，因此也不可能为其指定类型。

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

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

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

此致

附：下面的 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)