如何在 Haskell 中编写自应用函数？答案

【问题标题】：How can I write self-application function in Haskell?如何在 Haskell 中编写自应用函数？
【发布时间】：2017-03-20 06:12:27
【问题描述】：

我尝试了以下代码，但它会产生类型错误。

sa f = f f

• Occurs check: cannot construct the infinite type: t ~ t -> t1
• In the first argument of ‘f’, namely ‘f’
  In the expression: f f
  In an equation for ‘sa’: sa f = f f
• Relevant bindings include
    f :: t -> t1
      (bound at fp-through-lambda-calculus-michaelson.hs:9:4)
    sa :: (t -> t1) -> t1
      (bound at fp-through-lambda-calculus-michaelson.hs:9:1)

【问题讨论】：

你认为sa应该有什么类型？请记住，Haskell 中的所有术语都必须具有类型。另外，你想解决什么问题？
@Alec 我不知道，它需要一个可以带函数的函数？我只是在学习 lambda 演算，想知道如何在 Haskell 中表达它。我认为 Haskell 会很好地检查每个示例，但我立即陷入困境。也许 Lisp 或 Scheme 更容易达到这个目的。
这与您使用哪种语言无关。尝试在类型化的 lambda 演算中构造这个函数，并思考它应该有什么类型。我们会遇到类似的问题，不能构造无限类型
这很重要。您可以在 Lisp 和 Scheme 中轻松做到这一点，因为它们是动态类型的。

标签： haskell lambda-calculus

【解决方案1】：

使用新类型来构造无限类型。

newtype Eventually a = NotYet (Eventually a -> a)

sa :: Eventually a -> a
sa eventually@(NotYet f) = f eventually

在 GHC 中，eventually 和 f 将是内存中的同一个对象。

【讨论】：

此外，这可能会触发known bug in GHC，从而使内联发生分歧。 GHC 开发人员出于务实的原因不会修复此问题，IIRC 使用{-# NOINLINE as #-} 有一个简单的解决方法，以便禁用关键功能的内联。
@Daniel Wagner，谢谢，但我如何将这个 sa 应用于身份功能 id ？当我尝试类似:type NotYet Main.id 时，我仍然会遇到类型错误
@YoshihiroTanaka，这是一个单一类型的自我应用程序。在self应用id id中，两个id的类型不同。更明确地说是它的(id :: (A -> A) -> (A -> A)) (id :: A -> A)（对于任何类型A）。因此，您不能使用sa，因为sa 应用于自身的东西不是多态的。

【解决方案2】：

我认为在 Haskell 中没有一个可以适用于所有术语的自应用函数。自应用是类型化 lambda 演算中的一个特殊事物，它通常会逃避类型化。这与通过自应用我们可以表达定点组合子这一事实有关，当将其视为逻辑系统时，它会在类型系统中引入不一致（参见 Curry-Howard 对应）。

您询问是否将其应用于id 函数。在self应用id id中，两个id的类型不同。更明确地说是(id :: (A -> A) -> (A -> A)) (id :: A -> A)（对于任何类型A）。我们可以为id函数专门设计一个自应用程序：

sa :: (forall a. a -> a) -> b -> b
sa f = f f

ghci> :t sa id
sa id :: b -> b

效果很好，但受到其类型的限制。

使用RankNTypes，您可以创建类似这样的自应用函数系列，但您将无法创建一个通用的自应用函数，这样sa t 将是良好类型的，而当且仅当t t类型良好（至少在 GHC 的核心演算所基于的 System Fω（“F-omega”）中不是这样）。

原因，如果你正式地计算它（可能），那么我们可以得到sa sa，它没有范式，并且已知 Fω 正在归一化（当然，直到我们添加 fix）。

【讨论】：

感谢您的帮助！我是 Haskell 的新手，甚至不知道我必须添加 {-# LANGUAGE RankNTypes #-}。它现在可以工作了:-)
还想添加一个链接到 2002 年以来 Haskell 类型检查器上的相关帖子：link

【解决方案3】：

这是因为无类型的 lambda 演算在某种程度上比 Haskell更强大。或者，换句话说，无类型的 lambda 演算没有类型系统。因此，它没有健全的类型系统。而 Haskell 确实有一个。

这不仅出现在自我应用中，而且出现在涉及无限类型的任何情况下。试试这个，例如：

i x = x
s f g x = f x (g x)
s i i

令人惊讶的是，类型系统如何发现看似无害的表达式 s i i 不应该在健全的类型系统中被允许。因为，如果被允许，则可以自行申请。

【讨论】：