消失约束的情况：更高级别类型的奇怪 [英] The case of the disappearing constraint: Oddities of a higher-rank type

问题描述

下面介绍的所有实验均使用GHC 8.0.1完成。

这个问题是对类型别名混乱的RankNTypes 。那里的问题归结为像这样的功能类型......

  { - ＃LANGUAGE RankNTypes＃ - } 
 
 sleight1 :: a  - > （Num a => [a]） - > a 
 sleight1 x（y：_）= x + y 
  

...这是被类型检查程序拒绝......

  ThinAir.hs：4：13：error：
 * （数字a）由格式
引起可能的修正：
在
的上下文中添加（数字a）
的数字签名sleight1 :: a  - > （Num a => [a]） - > a 
 *在模式中：y：_ 
在'sleight1'的等式中：sleight1 x（y：_）= x + y 
  

...因为更高级的约束 Num a a - > a - >>（数字a = 1），则不可能移动到第二个参数的类型外 > [a]））。这样做，我们最终试图给已经量化的变量添加一个更高级别的约束条件，即：

pre $ sleight1 :: forall a。 a - > （Num a => [a]） - > a


完成这个概述后，我们可能会尝试简化示例。让我们将（+）替换为不需要 Num 的东西，然后将有问题的参数的类型从的结果：

  sleight2 :: a  - > （数字b => b） - > a 
 sleight2 xy = const xy 
  

这不能像以前一样工作（save for ）

  ThinAir.hs：7：24：error：
 *没有实例对于由于使用'y'引起的（Num b）
可能的修正：
在
的上下文中添加（Num b）类型签名：
 sleight2 :: a - > （数字b => b） - > a 
 *在'​​const'的第二个参数中，即'y'
在表达式中：const xy 
在'sleight2'的等式中：sleight2 xy = const xy 
失败，模块加载：无。 
  

然而，在这里使用 const 不必要，所以我们可以尝试自己编写实现：

  sleight3 :: a  - > （数字b => b） - > a 
 sleight3 xy = x 
  

令人惊讶的是，这真的有用！

  Prelude> ：r 
 [1的1]编译主（ThinAir.hs，解释）
好​​吧，模块加载：主。 
 * Main> ：t sleight3 
 sleight3 :: a  - > （数字b => b） - > a 
 * Main> sleight3 1 2 
 1 
  

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

  * Main>我不太确定如何做到这一点。我不太清楚如何做到这一点。我不知道如何做到这一点。理解。也许我们可以这样说，就像我们可以玩耍 undefined 一样，只要我们从不评估它，一个不可满足的约束可以坚持在一个类型中，只要它不是用于统一右侧的任何地方。然而，这感觉就像是一个非常弱的类比，特别是因为我们通常认为非严格性是一种涉及价值而不是类型的概念。此外，这让我们无法从掌握世界中的情况字符串与统一> Num b => b   - 假设实际上发生了这样的事情，这一点我并不确定。那么，什么是一个准确的描述，当一个约束似乎以这种方式消失时，发生了什么？ 
 
解决方案
变得更加怪异：
  Prelude> sleight3 1（wat+man）
 1 
 Prelude Data.Void> sleight3 1（37 :: Void）
 1 
  
请参阅 / em>该参数上的实际 Num 约束。只是，因为（正如chi已经评论过的） b 处于协变位置，所以这不是您在调用 sleight3 。相反，您可以选择任何类型的 b ，然后不管它是什么， sleight3 将会提供一个 Num 它的实例！
 
 
 
好吧，显然这是假的。  sleight3  不能为字符串提供这样一个num实例，绝对不是为 Void 。但它实际上并不需要，因为，就像你说的那样，这个约束所适用的论据从来没有被评估过。回想一下，约束多态值本质上只是字典参数的函数。  sleight3 只是承诺在它实际使用 y 之前提供这样的字典，但是它不会' t 以任何方式使用 y ，所以没关系。
 
 
 
它基本上与这样的功能： 
 
 
  defiant ::（Void  - > Int） - >字符串
 defiant f =哈哈
  
同样，参数函数显然不可能屈服一个 Int ，因为不存在 Void 值来评估它。但是这也不是必需的，因为 f 被简单地忽略了！
 
 
 
相比之下， sleight2 xy = const xy  does not sorta use  y ：第二个参数 const 只是一个0级的类型，所以编译器需要在那个时候解析任何需要的字典。即使 const 最终还会抛出 y ，它仍然强迫这个值足以证明它是没有很好的类型。
 
All the experiments described below were done with GHC 8.0.1.

This question is a follow-up to RankNTypes with type aliases confusion. The issue there boiled down to the types of functions like this one...
{-# LANGUAGE RankNTypes #-}

sleight1 :: a -> (Num a => [a]) -> a
sleight1 x (y:_) = x + y
... which are rejected by the type checker...
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
... because the higher-rank constraint Num a cannot be moved outside of the type of the second argument (as would be possible if we had a -> a -> (Num a  => [a]) instead). That being so, we end up trying to add a higher-rank constraint to a variable already quantified over the whole thing, that is:
sleight1 :: forall a. a -> (Num a => [a]) -> a
With this recapitulation done, we might try to simplify the example a bit. Let's replace (+) with something that doesn't require Num, and uncouple the type of the problematic argument from that of the result:
sleight2 :: a -> (Num b => b) -> a
sleight2 x y = const x y
This doesn't work just like before (save for a slight change in the error message):
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 here, however, is perhaps unnecessary, so we might try writing the implementation ourselves:
sleight3 :: a -> (Num b => b) -> a
sleight3 x y = x
Surprisingly, this actually works!
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
Even more bizarrely, there seems to be no actual Num constraint on the second argument:
*Main> sleight3 1 "wat"
1
I'm not quite sure about how to make that intelligible. Perhaps we might say that, just like we can juggle undefined as long as we never evaluate it, an unsatisfiable constraint can stick around in a type just fine as long as it is not used for unification anywhere in the right-hand side. That, however, feels like a pretty weak analogy, specially given that non-strictness as we usually understand it is a notion involving values, and not types. Furthermore, that leaves us no closer from grasping how in the world String unifies with Num b => b -- assuming that such a thing actually happens, something which I'm not at all sure of. What, then, is an accurate description of what is going on when a constraint seemingly vanishes in this manner?
解决方案
Oh, it gets even weirder:
Prelude> sleight3 1 ("wat"+"man")
1
Prelude Data.Void> sleight3 1 (37 :: Void)
1
See, there is an actual Num constraint on that argument. Only, because (as chi already commented) the b is in a covariant position, this is not a constraint you have to provide when calling sleight3. Rather, you can just pick any type b, then whatever it is, sleight3 will provide a Num instance for it!

Well, clearly that's bogus. sleight3 can't provide such a num instance for strings, and most definitely not for Void. But it also doesn't actually need to because, quite like you said, the argument for which that constraint would apply is never evaluated. Recall that a constrained-polymorphic value is essentially just a function of a dictionary argument. sleight3 simply promises to provide such a dictionary before it actually gets to use y, but then it doesn't use y in any way, so it's fine.

It's basically the same as with a function like this:
defiant :: (Void -> Int) -> String
defiant f = "Haha"
Again, the argument function clearly can not possibly yield an Int because there doesn't exist a Void value to evaluate it with. But this isn't needed either, because f is simply ignored!

By contrast, sleight2 x y = const x y does kinda sorta use y: the second argument to const is just a rank-0 type, so the compiler needs to resolve any needed dictionaries at that point. Even if const ultimately also throws y away, it still "forces" enough of this value to make it evident that it's not well-typed.

                        
这篇关于消失约束的情况：更高级别类型的奇怪的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！