制作在自身上运行其输入的函数时出现无限类型错误答案

【问题标题】：Getting infinite type error when making function that runs its input on itself制作在自身上运行其输入的函数时出现无限类型错误
【发布时间】：2021-12-26 07:33:18
【问题描述】：

我试图弄清楚为什么这段代码没有按预期工作。

我想创建一个函数run，它将某个函数作为输入并返回应用于自身的函数。

run::(t1->t2)->t2
run a = a a

包含的类型应该是通用的，因为我希望它适用于任何东西，但是当我尝试时遇到无限类型错误，我不知道为什么。

【问题讨论】：

为 lambda 演算创建类型系统以使 ω 和 Ω 无法表达的目的不是吗？
你能显示一个你想传递给run的函数吗？结果应该是什么？

标签： haskell functional-programming typeerror

【解决方案1】：

你说a :: t1 -> t2。这意味着它的参数应该具有t1 类型。然后将其应用于自身，a a。这意味着它的参数是a。

所以现在我们有一个等式：参数应该具有t1 类型（因为它是a 的参数）和t1 -> t2 类型（因为它是a）：

t1 ~ t1 -> t2
   ~ (t1 -> t2) -> t2
   ~ ((t1 -> t2) -> t2) -> t2
   ~ (((t1 -> t2) -> t2) -> t2) -> t2
   ~ ...

每一行都在前一行的基础上，将t1 替换为它对应的t1 -> t2。没有有限类型满足给定的等式。

【讨论】：

【解决方案2】：

如果你想在 Haskell 中写出 (λx.xx) (λx.xx) 或 Y 组合器的等价物，可以这样做：

Prelude> newtype F t2 = Wrap {unwrap :: F t2 -> t2}
Prelude> run x = (unwrap x) x
Prelude> :t run
run :: F t2 -> t2
Prelude> run (Wrap run)
^C
Interrupted.
Prelude> myFix f = run (Wrap (\x -> f ((unwrap x) x)))
Prelude> factorial = myFix (\fac n -> if n == 0 then 1 else n * fac (n - 1))
Prelude> factorial 5
120

添加和删除 newtype 包装器在运行时是无操作的。

Haskell 不允许这种没有 data 或 newtype 包装器的自引用（“无限”）类型。自动推断无限类型是可能的，并且不会使类型系统比现在更加不一致，但是无限类型并不是很有用，而且它们经常意外地出现在真正不应该类型检查的错误代码中，所以他们被拒绝可能会更好。

【讨论】：

【解决方案3】：

你写

run::(t1->t2)->t2
run a = a a

因为a是函数的参数，

a :: t1 -> t2

现在您将a 应用到a。 a 的参数有t1 类型，所以我们必须有

a :: t1

唯一有意义的是t1 是否与t1 -> t2 相同。所以这意味着

t1
= t1 -> t2
= (t1 -> t2) -> t2
= ((t1 -> t2) -> t2) -> t2
= ...

这可能就是您的无限类型错误的来源。我不知道为什么你没有得到一个更简单的错误，说 t1 与 t1 -> t2 不同。

所以...你不能完全在 Haskell 中调用一个函数。您可以小心地做一些类似的事情。但是你如何做到这一点将取决于你想要完成什么。

【讨论】：

"我不知道为什么你没有得到一个更简单的错误，说 t1 与 t1 -> t2 不一样"这不是因为这两种类型 是 i> 同样，如果我们允许 t2 ~ (t1 -> t2)?
@amalloy，我们不能允许这样做，因为这两种类型都是参数。如果我写foo :: a -> b; foo = id，那将不会进行类型检查，因为我们不能只允许a ~ b。