键入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