为什么`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参数类型（an Enum a）与外观类型i（a Num a）之间的不匹配。

我现在开始意识到我的问题必须来自一个错误的假设：“一旦i被推断为i :: Num a => a，那么i就别无其他 ”。因此，我很困惑地看到succ i评估没有错误。

Enum a除了明确声明的内容外，GHC似乎也在推断。

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

此类型是模棱两可的，但它满足GHCi 默认规则中的条件：

找到所有未解决的约束。然后：

• 找到形式为(C a)where a的类型变量，并将这些约束划分为共享公共类型变量的组a。

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

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

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

• 现在，对于其余的每个组G，ty依次尝试使用默认类型列表中的每种类型；设置a = ty是否可以完全解决G中的约束。如果是这样，则默认a为ty。

• 将单元类型()和列表类型[]添加到标准类型列表的开头，这些类型在进行类型默认设置时会尝试使用。

默认的默认类型列表（sic）是（带有last子句的附加内容）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可以是别的（即不适合此类型的任何东西），但可以与较不通用（更具体）的类型一起使用：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。

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

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

Prelude> f x = succ x + 1

将使用两个约束来推断类型：

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

因此，似乎函数的推理规则比变量的规则更严格？

由于单态性限制，实际上是相反的方式（默认情况下不在GHCi中）。您实际上很幸运没有在这里遇到问题，但是答案已经足够长了。搜索该词应给您解释。

GHC是说my_succ :: forall a. Num a => a -> a并给予forall a没有出现在既不类型的签名i也不是x。

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

Haskell类型签名被隐式量化。使用language选项时ExplicitForAll，关键字forall使我们能够准确地说出这是什么意思。例如：

g :: b -> b

意味着：

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

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