为什么3和x（被分配了3）在Haskell中具有不同的推断类型？ [英] Why do 3 and x (which was assigned 3) have different inferred types in Haskell?

问题描述

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

考虑下面的例子：

 前奏> ：t 3 
 3 ::（Num t）=> t 
前奏>让x = 3 
 Prelude> ：tx 
x :: Integer 
  

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

链接摘要：

阅读以下全部故事的答案;这里只是一个链接总结：

1. GHC类型默认值： Haskell报告部分
   4.3.4


2. GHCi的扩展类型默认值：使用GHCi部分
   2.4.5
3. 
   
4. 单形限制： Haskell
   wiki

解决方案

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

  let x = 5 
  

您可以对变量进行顶级定义。 MR坚持认为，如果没有类型签名的话，这样的定义应该通过为未解决的类型变量选择（希望）合适的默认实例来专用于单形值。相比之下，当您使用：t 来请求推断类型时，不会强制实施此类限制或默认设置。所以

 > ：t 3 
 3 ::（Num t）=> t 
  

因为 3 的确超载：它被任何数字类型承认。违约规则选择 Integer 作为默认数值类型，所以

 > ;让x = 3 
> ：tx 
x :: Integer 
  

现在让我们关掉MR。

 > ：set -XNoMonomorphismRestriction 
>让y = 3 
> ：t y 
 y ::（Num t）=> t 
  

没有MR，定义就像它的多态一样，就像 3 。只要检查...

 > ：t y *（2.5 :: Float）
 y *（2.5 :: Float）:: Float 
> ：ty *（3 :: Int）
y *（3 :: Int）:: Int 
  

请注意，根据随$提供的 fromInteger 方法，多态 y = 3 相关的 Num 实例。也就是说， y 不与 3 的特定表示相关联，而是用于构造 3 。天真地编译，这是一个缓慢的秘诀，有些人认为这是MR的动机。

我（在本地假装是）单态限制是一个更小或更大的邪恶。我总是为顶级定义编写类型签名，所以对于我想要达到的目标和MR是没有歧义的。

尝试了解类型系统是如何工作的，将类型推断的方面分开是非常有用的。

1. ‘遵循计划 将多态定义专门用于特定的用例：一个相当强大的约束解决问题，需要通过反向链接进行基本的统一和实例解析;猜测计划，概括类型以将多态类型方案分配给没有类型签名的定义：这非常脆弱，而且您越多移过基本的Hindley-Milner规范，使用类型类，具有更高级别的多态性，使用GADT时，陌生的东西就会变成。

b

学习第一部分的工作原理并理解第二部分困难的原因是很好的。类型推断中的许多怪异与第二种类型有关，并且启发式方法如单形性限制试图在含糊不清的情况下提供有用的默认行为。


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:

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

解决方案

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

1. ‘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

2. ‘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.

这篇关于为什么3和x（被分配了3）在Haskell中具有不同的推断类型？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！