是否可以在现代 Haskell 中定义 Omega 组合子（λx.xx）？

Question

堆栈！是否可以在现代 Haskell 中定义 Omega 组合子（λx.xx）？我想，Haskell98 的类型系统旨在使这样的事情变得不可能，但是现代扩展呢？

Answer 1

您不能直接在 Haskell 中表示 omega。很少有类型系统可以代表自我应用程序，而 Haskell 的类型系统不是其中之一。但是您可以对无类型的 lambda 演算进行编码并模拟 omega 和 self 应用程序，如下所示：

data Scott = Scott { apply :: Scott -> Scott }

omega = Scott $ \x -> apply x x

现在您可以说apply omega omega 并获得非终止计算。如果你想在 GHCi 中尝试一下，你可能需要下面的 Show 实例

instance Show Scott where
  show (Scott _) = "Scott"

Answer 2

不，但有点。这里要欣赏的是，Haskell 在newtype 声明中支持无限制递归。根据 Haskell 的语义，newtype 是定义的类型与其实现类型之间的同构。所以例如这个定义：

newtype Identity a = Identity { runIdentity :: a }

...断言Identity a 和a 类型是同构的。根据定义，构造函数Identity :: a -> Identity a 和观察者runIdentity :: Identity a -> a 是相反的。

所以从 svenningsson 的答案中借用 Scott 类型名称，定义如下：

newtype Scott = Scott { apply :: Scott -> Scott }

...断言Scott 类型与Scott -> Scott 同构。因此，虽然您不能将 Scott 直接应用于自身，但您可以使用同构来获取其 Scott -> Scott 对应项并将其应用于原始对象：

omega :: Scott -> Scott
omega x = apply x x

或者稍微有趣一点：

omega' :: (Scott -> Scott) -> Scott
omega' f = f (Scott f)

...这是一个固定点组合器类型！这个技巧可以适应在 Haskell 中编写 Y 组合器的一个版本：

module Fix where

newtype Scott a = Scott { apply :: Scott a -> a }

-- | This version of 'fix' is fundamentally the Y combinator, but using the
-- 'Scott' type to get around Haskell's prohibition on self-application (see
-- the expression @apply x x@, which is @x@ applied to itself).  Example:
--
-- >>> take 15 $ fix ([1..10]++)
-- [1,2,3,4,5,6,7,8,9,10,1,2,3,4,5]
fix :: (a -> a) -> a
fix f = (\x -> f (apply x x)) (Scott (\x -> f (apply x x)))

Answer 3

嗯，你可以定义：

{-# LANGUAGE Rank2Types #-}

omega :: (forall a . a) -> b
omega x = x x

然而这几乎没有用，因为唯一可以作为参数传递的值是undefined，所以你根本不能将它用作组合子。甚至omega omega 也无法进行类型检查。

要注意的是，为了让 x x 进行类型检查，您必须输入 x 类型为 T = t -> s 并且 t 与 T 统一（这样您就可以将 x 传递给本身）。但这基本上意味着t 必须是类型变量，并且参数必须是完全多态的，从而使函数无用。