-
02-10-2019 - |
题
http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html 是 Prolog 中简单类型 lambda 演算的简明定义。
看起来不错,但随后他声称要为 Y 组合器分配一个类型......而实际上,向 lambda 演算添加类型的全部目的是拒绝为 Y 组合器之类的东西分配类型。
任何人都可以准确地看出他的错误或(更有可能的是)我的误解在哪里吗?
解决方案
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
其他提示
打字应该禁止自我应用,不应该找到一个类型 (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)