Haskell 中 fx = fx 类型的理由是什么?

发布于 2024-10-15 15:15:39 字数 116 浏览 3 评论 0原文

Haskell 给出了 fx = f x 的类型 t1 -> t,但有人可以解释为什么吗?

并且,任何其他不等价的函数是否有可能具有相同的类型?

Haskell gives f x = f x the type of t1 -> t, but could someone explain why?

And, is it possible for any other, nonequivalent function to have this same type?

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(2

饭团 2024-10-22 15:15:39

好的,从函数定义 fx = f x 开始,我们一步一步看一下可以推断出 f 的类型。

从一个完全未指定的类型变量 a 开始。我们还能推断出更多吗?是的,我们观察到 f 是一个带有一个参数的函数,因此我们可以将 a 更改为两个未知类型变量之间的函数,我们将其称为 b -> c.无论 b 代表什么类型,都是参数 x 的类型,而无论 c 代表什么类型,都必须是右侧的类型的定义。

从右边我们能看出什么?好吧,我们有 f,它是对我们正在定义的函数的递归引用,因此它的类型仍然是 b ->; c,其中两个类型变量与 f 的定义相同。我们还有 x,它是一个绑定在 f 定义内的变量,类型为 b。将 f 应用于 x 类型检查,因为它们共享相同的未知类型 b,结果为 c >。

此时,所有内容都组合在一起并且没有其他限制,我们可以将类型变量设置为“正式”,从而得到最终类型 b ->; c 其中两个变量都是 Haskell 中常见的隐式通用量化类型变量。

换句话说,f 是一个函数,它接受任何类型的参数并返回任何类型的值。它如何返回任何可能的类型?它不能,而且我们可以观察到对它的求值只会产生无限递归。

出于同样的原因,任何具有相同类型的函数在求值时从不返回的意义上都是“等效的”。

一个更直接的版本是完全删除参数:

foo :: a
foo = foo

...这也是普遍量化的并表示任何类型的值。这几乎相当于未定义

Okay, starting from the function definition f x = f x, let's step through and see what we can deduce about the type of f.

Start with a completely unspecified type variable, a. Can we deduce more than that? Yes, we observe that f is a function taking one argument, so we can change a into a function between two unknown type variables, which we'll call b -> c. Whatever type b stands for is the type of the argument x, and whatever type c stands for must be the type of the right-hand side of the definition.

What can we figure out about the right-hand side? Well, we have f, which is a recursive reference to the function we're defining, so its type is still b -> c, where both type variables are the same as for the definition of f. We also have x, which is a variable bound within the definition of f and has type b. Applying f to x type checks, because they're sharing the same unknown type b, and the result is c.

At this point everything fits together and with no other restrictions, we can make the type variables "official", resulting in a final type of b -> c where both variables are the usual, implicitly universally quantified type variables in Haskell.

In other words, f is a function that takes an argument of any type and returns a value of any type. How can it return any possible type? It can't, and we can observe that evaluating it produces only an infinite recursion.

For the same reason, any function with the same type will be "equivalent" in the sense of never returning when evaluated.

An even more direct version is to remove the argument entirely:

foo :: a
foo = foo

...which is also universally quantified and represents a value of any type. This is pretty much equivalent to undefined.

你又不是我 2024-10-22 15:15:39
f x = undefined

具有 (alpha) 等效类型 f :: t ->一个。


如果您好奇,Haskell 的类型系统源自 Hindley–Milner。非正式地,类型检查器从最允许的类型开始,然后统一各种约束,直到剩下的内容一致(或不一致)。在这种情况下,最通用的类​​型是 f :: t1 -> t,并且没有额外的限制。

进行比较

f x = f (f x)

与推断类型 f :: t -> t,因为统一了左侧f的参数类型和右侧外部f的参数类型。

f x = undefined

has the (alpha) equivalent type f :: t -> a.


If you're curious, Haskell's type system is derived from Hindley–Milner. Informally, the typechecker starts off with the most permissive types for everything, and unifies the various constraints until what remains is consistent (or not). In this case, the most general type is f :: t1 -> t, and there's no additional constraints.

Compare to

f x = f (f x)

which has inferred type f :: t -> t, due to unifying the types of the argument of f on the LHS and the argument to the outer f on the RHS.

~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文