haskell - 为什么 `succ i` 在 `i::Num a => a` 处有效(而不是 `Enum a` )？

Question

这似乎适用于 GHCi 和 GHC。我将首先展示一个使用 GHCi 的示例。

给定的 i 类型已推断如下:

Prelude> i = 1
Prelude> :t i
i :: Num p => p

鉴于 succ 是在 Enum 上定义的函数:

Prelude> :i Enum
class Enum a where
  succ :: a -> a
  pred :: a -> a
  -- …OMITTED…

并且 Num 不是 Enum 的“子类”(如果我可以使用这个术语的话):

class Num a where
  (+) :: a -> a -> a
  (-) :: a -> a -> a
-- …OMITTED…

为什么succ i不返回错误？

Prelude> succ i
2 -- works, no error

我希望 :type i 被推断为:

Prelude> i = 1
Prelude> :type i
i :: (Enum p, Num p) => p

(我正在使用“GHC v. 8.6.3”)

添加:

阅读 @RobinZigmond 评论和 @AlexeyRomanov 答案后，我注意到 1 可以解释为多种类型之一和多种类之一。感谢@AlexeyRomanov 的回答，我对用于决定用于不明确表达式的类型的默认规则有了更多了解。

但是我不认为 Alexey 的回答完全解决了我的问题。我的问题是关于 i 的类型。这与 succ i 的类型无关。

这是关于 succ 参数类型(Enum a)和 i 的表观类型(Num a )。

我现在开始意识到我的问题一定源于一个错误的假设:“一旦 i 被推断为 i::Num a => a ，那么 i 可以是没有别的'。因此，我很困惑地看到 succ i 的评估没有错误。

除了显式声明的内容之外，GHC 似乎还推断了 Enum a。

x :: Num a => a
x = 1
y = succ x -- works

但是，当类型变量作为函数出现时，它不会添加 Enum a:

my_succ :: Num a => a -> a
my_succ z = succ z -- fails compilation

对我来说，附加到函数的类型约束似乎比应用于变量的类型约束更严格。

GHC 正在说 my_succ::forall a。 Num a => a -> a 并给出forall a 没有出现在 i 和 x 的类型签名中我认为这意味着 GHC 不会再推断任何类对于 my_succ 类型。

但这似乎又是错误的:我已经用以下内容检查了这个想法(我第一次输入RankNTypes)，显然GHC仍然推断Enum a:

{-# LANGUAGE RankNTypes #-}

x :: forall a. Num a => a
x = 1
y = succ x

看来函数的推理规则比变量的推理规则更严格？

Answer 1

是的，succ i的类型按照您的预期推断出来:

Prelude> :t succ i
succ i :: (Enum a, Num a) => a

该类型不明确，但满足 the defaulting rules 中的条件对于 GHCi:

Find all the unsolved constraints. Then:

• Find those that are of form (C a) where a is a type variable, and partition those constraints into groups that share a common type variable a.

在本例中，只有一组:(Enum a, Num a) .

• Keep only the groups in which at least one of the classes is an interactive class (defined below).

保留该组，因为 Num是一个互动类(class)。

• Now, for each remaining group G, try each type ty from the default-type list in turn; if setting a = ty would allow the constraints in G to be completely solved. If so, default a to ty.

• The unit type () and the list type [] are added to the start of the standard list of types which are tried when doing type defaulting.

默认的默认类型列表(原文如此)是(带有最后一个子句的添加内容)default ((), [], Integer, Double) 。

所以当你这样做时Prelude> succ i要实际计算此表达式(注意 :t 不会计算它得到的表达式)， a设置为Integer (此列表中的第一个满足约束条件)，结果打印为 2 .

您可以通过更改默认值来查看原因:

Prelude> default (Double)
Prelude> succ 1
2.0

对于更新的问题:

I'm now starting to realise that my question must stem from a wrong assumption: 'that once i is inferred to be i :: Num a => a, then i can be nothing else'. Hence I was puzzled to see succ i was evaluated without errors.

i可以是其他(即没有不适合此类型的内容)，但它可以与不太通用(更具体)的类型一起使用:Integer , Int 。即使其中许多同时出现在一个表达式中:

Prelude> (i :: Double) ^ (i :: Integer)
1.0

这些用途不会影响 i 的类型本身:它已经定义并且类型固定。到目前为止还好吗？

嗯，添加约束也会使类型更加具体，所以(Num a, Enum a) => a比 (Num a) => a 更具体:

Prelude> i :: (Num a, Enum a) => a
1

因为当然任何类型 a满足 (Num a, Enum a) 中的两个约束满足 Num a .

However it is not adding Enum a when the type variable appears as a function:

那是因为您指定了不允许的签名。如果你不签名，就没有理由推断Num约束。但例如

Prelude> f x = succ x + 1

将推断具有两个约束的类型:

Prelude> :t f
f :: (Num a, Enum a) => a -> a

So it seems that inference rules for functions are stricter than the ones for variables?

实际上是相反的，因为 monomorphism restriction (默认情况下不在 GHCi 中)。实际上你很幸运没有在这里遇到它，但答案已经足够长了。搜索该术语应该会给您解释。

GHC is saying my_succ :: forall a. Num a => a -> a and given forall a doesn't appear in the type-signature of neither i nor x.

这是一条红鲱鱼。我不确定为什么它显示在一种情况下而不是另一种情况下，但所有情况下都有 forall a幕后花絮:

Haskell type signatures are implicitly quantified. When the language option ExplicitForAll is used, the keyword forall allows us to say exactly what this means. For example:

g :: b -> b

means this:

g :: forall b. (b -> b)

(此外，您只需要 ExplicitForAll 而不是 RankNTypes 来写下 forall a. Num a => a 。)