prolog - 键入 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。由于自我应用是 Y 组合器的一部分，因此也不可能给它一个类型。

不幸的是，许多 Prolog 系统允许为A = A -> B. 这发生在许多原因上，要么 Prolog 系统允许循环术语，那么统一就会成功，甚至可以进一步处理生成的绑定。或者 Prolog 系统不允许循环项，则取决于它是否实现发生检查。如果发生检查打开，则统一不会成功。如果发生检查关闭，则统一可能会成功，但无法进一步处理生成的绑定，很可能导致打印中的堆栈溢出或进一步的统一。

所以我猜这种类型的循环统一发生在使用的 Prolog 系统的给定代码中，它被忽视了。

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

最好的祝福

PS：以下 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)