为什么`suc a`在`is :: 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：

找出所有未解决的约束。那么：

• 查找格式为(C a) 的那些，其中a 是一个类型变量，并将这些约束划分为共享一个公共类型变量a 的组。

在这种情况下，只有一组：(Enum a, Num a)。

• 仅保留其中至少一个类是交互式类（定义如下）的组。

保留该组，因为Num 是一个交互式类。

• 现在，对于剩余的每个组 G，依次尝试默认类型列表中的每个类型 ty；如果设置a = ty 将允许完全解决 G 中的约束。如果是这样，默认a 为ty。

• 单元类型() 和列表类型[] 被添加到在进行类型默认时尝试的标准类型列表的开头。

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

因此，当您执行Prelude> succ i 来实际评估此表达式时（注意:t 不会评估它得到的表达式），a 设置为Integer（此列表中的第一个满足约束条件），并且结果打印为2。

你可以通过更改默认值来查看原因：

Prelude> default (Double)
Prelude> succ 1
2.0

对于更新的问题：

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

i 什么都不是.即使有很多同时出现在一个表达式中：

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

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

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

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

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

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

那是因为您指定了不允许这样做的签名。如果您不提供签名，则没有理由推断Num 约束。但是例如

Prelude> f x = succ x + 1

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

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

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

由于monomorphism restriction（默认情况下不在 GHCi 中），它实际上是相反的。没有在这里遇到它实际上已经有点幸运了，但是答案已经足够长了。搜索这个词应该会给你解释。

GHC 说 my_succ :: forall a. Num a => a -> a 并且给定的 forall a 没有出现在 i 和 x 的类型签名中。

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

Haskell type signatures are implicitly quantified. 当使用语言选项ExplicitForAll 时，关键字forall 可以让我们准确说出这意味着什么。例如：

g :: b -> b

意思是：

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

（另外，你只需要ExplicitForAll 而不是RankNTypes 来写下forall a. Num a => a。）