Haskell 中 fx = fx 类型的理由是什么?
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 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱,如果其他用户或者作者回复了您的评论,将不能在第一时间通知您!
发布评论
评论(2)
好的,从函数定义
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
是一个函数,它接受任何类型的参数并返回任何类型的值。它如何返回任何可能的类型?它不能,而且我们可以观察到对它的求值只会产生无限递归。出于同样的原因,任何具有相同类型的函数在求值时从不返回的意义上都是“等效的”。
一个更直接的版本是完全删除参数:
...这也是普遍量化的并表示任何类型的值。这几乎相当于
未定义
。Okay, starting from the function definition
f x = f x
, let's step through and see what we can deduce about the type off
.Start with a completely unspecified type variable,
a
. Can we deduce more than that? Yes, we observe thatf
is a function taking one argument, so we can changea
into a function between two unknown type variables, which we'll callb -> c
. Whatever typeb
stands for is the type of the argumentx
, and whatever typec
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 stillb -> c
, where both type variables are the same as for the definition off
. We also havex
, which is a variable bound within the definition off
and has typeb
. Applyingf
tox
type checks, because they're sharing the same unknown typeb
, and the result isc
.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:
...which is also universally quantified and represents a value of any type. This is pretty much equivalent to
undefined
.具有 (alpha) 等效类型
f :: t ->一个。
如果您好奇,Haskell 的类型系统源自 Hindley–Milner。非正式地,类型检查器从最允许的类型开始,然后统一各种约束,直到剩下的内容一致(或不一致)。在这种情况下,最通用的类型是
f :: t1 -> t
,并且没有额外的限制。进行比较
与推断类型
f :: t -> t
,因为统一了左侧f
的参数类型和右侧外部f
的参数类型。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
which has inferred type
f :: t -> t
, due to unifying the types of the argument off
on the LHS and the argument to the outerf
on the RHS.