如何在Haskell中编写自我应用程序功能？

Question

我尝试了以下代码,但它会生成类型错误.

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)

Answer 1

使用newtype构造无限类型.

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

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

在GHC,eventually并且f将在存储器中的相同对象.

Answer 2

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

\n\n

您询问如何将其应用到该id函数中。在self应用中id id，两者id有不同的类型。更明确地说，它是(id :: (A -> A) -> (A -> A)) (id :: A -> A)（对于任何类型A）。我们可以制作一个专门针对该功能设计的自助应用程序id：

\n\n

sa :: (forall a. a -> a) -> b -> b\nsa f = f f\n\nghci> :t sa id\nsa id :: b -> b\n

\n\n

它工作得很好，但受到其类型的限制。

\n\n

使用RankNTypes你可以创建像这样的自应用函数系列，但是你将无法创建一个通用的自应用函数，这样当它sa t类型良好时t t（至少在 System F 中不行） \xcf\x89（“F-omega”），GHC 的核心演算所基于）。

\n\n

原因是，如果你正式地（可能）计算出来，那么我们可以得到sa sa，它没有范式，并且 F\xcf\x89 已知是标准化的（fix当然，直到我们添加）。

\n