haskell - 约束消失的情况: Oddities of a higher-rank type

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只是 promise 在实际使用之前提供这样的字典 y , 但随后它不使用 y无论如何，所以没关系。

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

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

同样，参数函数显然不可能产生 Int因为不存在 Void评估它的值(value)。但这也不是必需的，因为 f简直是无视!

相比之下， sleight2 x y = const x y有点用 y : const 的第二个参数只是 rank-0 类型，因此编译器需要在此时解析任何需要的字典。即使 const最终也抛出 y离开，它仍然“强制”足够的这个值来表明它不是很好的类型。