约束消失的情况：更高等级类型的怪异

下面描述的所有实验都是使用 GHC 8.0.1 完成的。

这个问题是后续问题具有类型别名混淆的 RankNTypes https://stackoverflow.com/q/40252867/2751851。那里的问题归结为像这样的函数类型......

{-# LANGUAGE RankNTypes #-}

sleight1 :: a -> (Num a => [a]) -> a
sleight1 x (y:_) = x + y

...被类型检查器拒绝...

ThinAir.hs:4:13: error:
    * No instance for (Num a) arising from a pattern
      Possible fix:
        add (Num a) to the context of
          the type signature for:
            sleight1 :: a -> (Num a => [a]) -> a
    * In the pattern: y : _
      In an equation for `sleight1': sleight1 x (y : _) = x + y

...因为更高阶的约束Num a 不能移动到第二个参数的类型之外 https://stackoverflow.com/a/14593131/2751851（如果我们有的话就有可能a -> a -> (Num a => [a])反而）。既然如此，我们最终尝试为整个事情已经量化的变量添加一个更高等级的约束，即：

sleight1 :: forall a. a -> (Num a => [a]) -> a

完成这个重述后，我们可能会尝试稍微简化一下这个例子。我们来替换一下(+)用不需要的东西Num，并将有问题的参数的类型与结果的类型分开：

sleight2 :: a -> (Num b => b) -> a
sleight2 x y = const x y

这不像以前那样工作（除了错误消息中的细微变化）：

ThinAir.hs:7:24: error:
    * No instance for (Num b) arising from a use of `y'
      Possible fix:
        add (Num b) to the context of
          the type signature for:
            sleight2 :: a -> (Num b => b) -> a
    * In the second argument of `const', namely `y'
      In the expression: const x y
      In an equation for `sleight2': sleight2 x y = const x y
Failed, modules loaded: none.

Using const然而，这里可能是不必要的，所以我们可以尝试自己编写实现：

sleight3 :: a -> (Num b => b) -> a
sleight3 x y = x

令人惊讶的是，这确实有效！

Prelude> :r
[1 of 1] Compiling Main             ( ThinAir.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t sleight3
sleight3 :: a -> (Num b => b) -> a
*Main> sleight3 1 2
1

更奇怪的是，似乎并没有真正的Num对第二个参数的约束：

*Main> sleight3 1 "wat"
1

我不太确定如何使其易于理解。也许我们可以这么说，就像我们可以杂耍一样undefined只要我们从不评估它，一个不可满足的约束就可以很好地保留在类型中，只要它不用于右侧任何地方的统一。然而，这感觉像是一个相当弱的类比，特别是考虑到我们通常理解的非严格性是一个涉及值而不是类型的概念。此外，这并没有让我们更接近于理解世界是如何发生的。String与Num b => b——假设这样的事情真的发生了，但我完全不确定。那么，当约束似乎以这种方式消失时，对正在发生的情况的准确描述是什么？

哦，事情变得更奇怪了：

Prelude> sleight3 1 ("wat"+"man")
1
Prelude Data.Void> sleight3 1 (37 :: Void)
1

看那边is一个实际的Num对该论点的限制。只是，因为（正如 chi 已经评论的那样）b处于协变位置，这不是您在调用时必须提供的约束sleight3。相反，您可以选择任何类型b，那么无论它是什么，sleight3将提供一个Num举个例子吧！

嗯，显然那是假的。sleight3 can't为字符串提供这样的 num 实例，并且绝对不是为Void。但它也没有actually需要，因为就像你说的那样，应用该约束的参数永远不会被评估。回想一下，约束多态值本质上只是字典参数的函数。sleight3只是承诺在实际使用之前提供这样一本字典y，但随后它doesn't use y无论如何，所以没关系。

它基本上与这样的函数相同：

defiant :: (Void -> Int) -> String
defiant f = "Haha"

同样，参数函数显然不可能产生一个Int因为不存在Void对其进行评估的价值。但这也不是必需的，因为f根本就被忽略了！

相比之下，sleight2 x y = const x y有点用y：第二个参数const只是一个 0 级类型，因此编译器需要在此时解析任何所需的字典。即使const最终也抛出y即使这样，它仍然“强制”足够多的值，以表明它的类型不正确。