约束消失的事例：上位类型的怪事

Question

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

此问题是 RankNTypes with type aliases confusion 的后续问题。那里的问题归结为像这样的函数类型...

{-# 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 cannot be moved outside of the type of the second argument（如果我们有 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.

然而，在这里使用 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 的统一方式没有更近的距离——假设这样的事情真的发生了，这是我完全不确定的事情。那么，当约束以这种方式看似消失时，如何准确描述正在发生的事情？

Answer 1

哦，更奇怪了：

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

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

嗯，很明显那是假的。 sleight3 不能为字符串提供这样的 num 实例，而且绝对不能为 Void。但它也 实际上 不需要因为，就像你说的那样，永远不会评估应用该约束的参数。回想一下，约束多态值本质上只是字典参数的函数。 sleight3 只是承诺在它实际开始使用 y 之前提供这样一个字典，但是它不会以任何方式使用 y，所以没关系。

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

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

同样，参数函数显然不可能产生 Int，因为不存在 Void 值来评估它。但这也不是必需的，因为 f 被简单地忽略了！

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

约束消失的事例：上位类型的怪事

The case of the disappearing constraint: Oddities of a higher-rank type

haskell

types

type-constraints

higher-rank-types