消失约束的情况:更高等级类型的奇数

Question

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

这个问题是RankNTypes的后续类型别名混淆.这个问题归结为像这样的函数类型......

{-# 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 不能移动到第二个参数的类型之外(如果我们有的话可能会这样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抛弃了它,它仍然"强迫"足够的这个价值,使它显然不是很好的类型.