为什么 3 和 x（被分配为 3）在 Haskell 中具有不同的推断类型？

发布于 2024-11-29 14:40:38 字数 762 浏览 0 评论 0原文

Haskell 中的类型推断有一点学习曲线（至少可以这么说！）。开始学习它的一个好方法是通过简单的例子。因此，以下是类型推断的“hello world”。

考虑以下示例：

Prelude> :t 3
3 :: (Num t) => t
Prelude> let x = 3
Prelude> :t x
x :: Integer

问题是：为什么 3 和 x 有不同的类型？

链接摘要：

阅读下面的答案以了解完整的故事；这里只是一个链接摘要：

GHC 类型默认： Haskell Report 部分 4.3.4
GHCi 的扩展类型默认：使用 GHCi 部分 2.4.5
单态限制： Haskell 维基百科

原文

Type inference in Haskell has a bit of a learning curve (to say the least!). A good way to start learning it is with simple examples. So, the following is a bit of a "hello world" for type inference.

Consider the following example:

Prelude> :t 3
3 :: (Num t) => t
Prelude> let x = 3
Prelude> :t x
x :: Integer

The question is thus: Why do 3 and x have different types?

Link Summary:

Read the answers below for the full story; here's just a link summary:

GHC type defaulting: Haskell Report section
4.3.4
GHCi's extended type defaulting: Using GHCi section
2.4.5
Monomorphic Restriction: Haskell
wiki

分享到QQ

分享到微博

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

发布评论

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

只有影子陪我不离不弃 2024-12-06 14:40:38

这里还有另一个因素，在 acfoltzer 包含的一些链接中提到过，但可能值得在这里明确说明。您遇到了单态限制的影响。当您说

let x = 5

您对变量进行顶级定义时。 MR 坚持认为，当这些定义没有类型签名时，应该通过为未解析的类型变量选择（希望）合适的默认实例来专门化为单态值。相比之下，当您使用 :t 请求推断类型时，不会施加此类限制或默认值。因为

> :t 3
3 :: (Num t) => t

3 确实是重载的：任何数字类型都承认它。默认规则选择 Integer 作为默认数字类型，所以

> let x = 3
> :t x
x :: Integer

现在让我们关闭 MR。

> :set -XNoMonomorphismRestriction
> let y = 3
> :t y
y :: (Num t) => t

如果没有 MR，定义就尽可能多态，就像 3 一样重载。只是检查...

> :t y * (2.5 :: Float)
y * (2.5 :: Float) :: Float
> :t y * (3 :: Int)
y * (3 :: Int) :: Int

请注意，根据相关 NumfromInteger 方法，多态 y = 3 在这些用途中的专门化有所不同> 实例。也就是说，y 并不与 3 的特定表示相关联，而是与用于构造 3 的表示的方案相关联。天真的编译，这是缓慢的秘诀，一些人将其视为 MR 的动机。

对于单态限制是大恶还是小恶的争论，我（局部假装）保持中立。我总是为顶级定义编写类型签名，因此我想要实现的目标没有任何歧义，并且 MR 不是重点。

当尝试学习类型系统如何工作时，将类型推断的各个方面分开非常有用，

“遵循计划”，将多态定义专门针对特定用例：一个相当强大的约束解决问题，需要基本统一以及通过回链进行实例解析；
“猜测计划”，泛化类型以将多态类型方案分配给没有类型签名的定义：这是非常脆弱的，并且越多地越过基本的 Hindley-Milner 规则，具有类型类，具有更高的-等级多态性，有了 GADT，事情就变得更奇怪了。

了解第一个方法是如何运作的，并了解为什么第二个方法很困难，这是很好的做法。类型推断中的许多奇怪之处都与第二个相关，并且与诸如单态限制之类的启发式方法相关，这些启发式方法试图在面对歧义时提供有用的默认行为。

There's another factor here, mentioned in some of the links which acfoltzer includes, but it might be worth making explicit here. You're encountering the effect of the monomorphism restriction. When you say

let x = 5

you make a top-level definition of a variable. The MR insists that such definitions, when otherwise unaccompanied by a type signature, should be specialized to a monomorphic value by choosing (hopefully) suitable default instances for the unresolved type variables. By contrast, when you use :t to ask for an inferred type, no such restriction or defaulting is imposed. So

> :t 3
3 :: (Num t) => t

because 3 is indeed overloaded: it is admitted by any numeric type. The defaulting rules choose Integer as the default numeric type, so

> let x = 3
> :t x
x :: Integer

But now let's switch off the MR.

> :set -XNoMonomorphismRestriction
> let y = 3
> :t y
y :: (Num t) => t

Without the MR, the definition is just as polymorphic as it can be, just as overloaded as 3. Just checking...

> :t y * (2.5 :: Float)
y * (2.5 :: Float) :: Float
> :t y * (3 :: Int)
y * (3 :: Int) :: Int

Note that the polymorphic y = 3 is being differently specialized in these uses, according to the fromInteger method supplied with the relevant Num instance. That is, y is not associated with a particular representation of 3, but rather a scheme for constructing representations of 3. Naïvely compiled, that's a recipe for slow, which some people cite as a motivation for the MR.

I'm (locally pretending to be) neutral on the debate about whether the monomorphism restriction is a lesser or greater evil. I always write type signatures for top-level definitions, so there is no ambiguity about what I'm trying to achieve and the MR is beside the point.

When trying to learn how the type system works, it's really useful to separate the aspects of type inference which

‘follow the plan’, specializing polymorphic definitions to particular use cases: a fairly robust matter of constraint-solving, requiring basic unification and instance resolution by backchaining; and
‘guess the plan’, generalizing types to assign a polymorphic type scheme to a definition with no type signature: that's quite fragile, and the more you move past the basic Hindley-Milner discipline, with type classes, with higher-rank polymorphism, with GADTs, the stranger things become.

It's good to learn how the first works, and to understand why the second is difficult. Much of the weirdness in type inference is associated with the second, and with heuristics like the monomorphism restriction trying to deliver useful default behaviour in the face of ambiguity.

回复收藏 0 原文

黎歌 2024-12-06 14:40:38

出现这种情况是因为 GHCi 中的默认类型，如所讨论的此处，这里，此处，以及这里，等等。不幸的是，这似乎很难搜索，因为在您知道“类型默认”这个短语之前，有很多方法可以描述这种行为。

更新：哦。删除了不好的例子。

回复收藏 0 原文

贪了杯 2024-12-06 14:40:38

由于没有其他人提到为什么存在单态限制，我想我应该添加Haskell 的历史：对类的懒惰。

6.2 单态限制早期争议的一个主要来源是所谓的“单态限制”。认为
genericLength 具有以下重载类型：
genericLength :: Num a =>; [b]->一个 
现在考虑这个定义：
<前><代码>f xs = (len, len)
其中 len = genericLength xs
看起来 len 应该只计算一次，但是
它实际上可以计算两次。为什么？因为我们可以推断类型
len :: (Num a) =>;一个；当通过字典传递脱糖时
翻译后，len 变成一个函数，每个函数都会调用一次
出现len，每个都可能用于不同的类型。
休斯强烈主张默默地复制是不可接受的
以此方式计算。他的论点是由他的一个计划激发的
所写的运行速度比他预期的要慢得多。（这是
诚然，我们使用了一个非常简单的编译器，但我们不愿意制作
性能差异如此之大取决于编译器
优化。）
经过多次辩论，委员会通过了
现在臭名昭著的单态限制。简单地说，它说
定义看起来不像函数（即没有参数
左侧）在任何重载类型中都应该是单态的
变量。在此示例中，规则强制同时使用 len
在两次出现时都键入，这解决了性能问题。
程序员可以为 len 提供显式类型签名，如果
需要多态行为。
单态限制是
显然是语言上的缺陷。它似乎会咬住每一个新的 Haskell
程序员通过产生意外或模糊的错误消息。
人们对替代方案进行了很多讨论。格拉斯哥 Haskell 编译器
（GHC，第 9.1 节）提供了一个标志：
-fno-单态限制
完全取消限制。但这么长的时间里，并没有真正
令人满意的替代方案已经出现。

我发现这篇论文对单态限制的基调非常有趣。

Since nobody else has mentioned why there's a monomorphism restriction, I thought I'd add this bit from A History of Haskell: Being Lazy With Class.

6.2 The monomorphism restriction A major source of controversy in the early stages was the so-called “monomorphism restriction.” Suppose
that genericLength has this overloaded type:
genericLength :: Num a => [b] -> a 
Now consider this deﬁnition:
f xs = (len, len) 
     where len = genericLength xs 
It looks as if len should be computed only once, but
it can actually be computed twice. Why? Because we can infer the type
len :: (Num a) => a; when desugared with the dictionary-passing
translation, len becomes a function that is called once for each
occurrence of len, each of which might used at a different type.
Hughes argued strongly that it was unacceptable to silently duplicate
computation in this way. His argument was motivated by a program he
had written that ran exponentially slower than he expected. (This was
admittedly with a very simple compiler, but we were reluctant to make
performance differences as big as this dependent on compiler
optimisations.)
Following much debate, the committee adopted the
now-notorious monomorphism restriction. Stated brieﬂy, it says that a
deﬁnition that does not look like a function (i.e. has no arguments on
the left-hand side) should be monomorphic in any overloaded type
variables. In this example, the rule forces len to be used at the same
type at both its occurrences, which solves the performance problem.
The programmer can supply an explicit type signature for len if
polymorphic behaviour is required.
The monomorphism restriction is
manifestly a wart on the language. It seems to bite every new Haskell
programmer by giving rise to an unexpected or obscure error message.
There has been much discussion of alternatives. The Glasgow Haskell Compiler
(GHC, Section 9.1) provides a ﬂag:
-fno-monomorphism-restriction
to suppress the restriction altogether. But in all this time, no truly
satisfactory alternative has evolved.