prolog - 键入 Y 组合器

Question

http://muaddibspace.blogspot.com/2008/01/type-inference-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