带类型别名混乱的RankNTypes [英] RankNTypes with type aliases confusion

问题描述

我试图理解类型约束是如何处理类型别名的。首先，假设我有下一个类型的别名：

  type NumList a = Num a => [a] 
  

我有下一个功能：

  addFirst :: a  - > NumList a  - > NumList 
 addFirst x（y：_）= x + y 
  

错误：

  Type.hs：9：13：错误：
•（数字a）没有实例一个模式
可能的修正：
在
的上下文中添加（Num a）类型签名：
 addFirst :: a  - > NumList a  - > a 
•在模式中：y：_ 
在'addFirst'的等式中：ad 
  

这是显而易见的。这个问题已经在这里描述：

我明白为什么我们需要 { - ＃LANGUAGE RankNTypes＃ - } 这样的类型别名可以工作，为什么前面的例子不起作用。但是我不明白的是为什么下一个例子编译得很好（在ghc 8上）：

  prepend :: a  - > NumList a  - > NumList a 
 prepend =（:) 
  

当然，它在 ghci 如果我尝试传递错误的值：

 λ：prepend 1 [] 
 [1] 
λ：前置xx[] 
 
<互动>：3：1：错误：
•（Num [Char]）没有实例出现从'prepend'
的使用•当实例化'it'时，最初推断为
，这个overly-general类型：
 NumList [Char] 
 NB：这个实例化可以由单态限制引起的。 
  

看起来像在运行时延迟的类型类型检查：（$ / b
$ b

此外，一些简单和似乎是相同的代码段不会编译：

  first :: NumList a  - > a 
 first = head 
  

并产生下一个错误：

  Type.hs：12：9：error：
•（数量a）
没有实例可能的修正：
在
的上下文中添加（Num a）类型签名：
 first :: NumList a  - > a 
•在表达式中：head 
在'first'的等式：first = head 
  

有人可以解释一下这里发生了什么吗？在函数类型检查与否的一致性方面。

解决方案

（

不是真的，这可能有点令人惊讶，因为ause你在加载文件后在ghci 中得到类型错误。但是可以这样解释：文件本身非常好，但这并不意味着您可以使用其中定义的函数构建的表达式都是很好的类型。

更高级的多态性与它无关。 （+）例如在前奏中定义，但如果您尝试在ghci中评估 2 +argh你也会得到一个类型错误：

 没有使用'+ '
在表达式中：2 +argh
在'it'的等式中：it = 2 +argh
  

现在让我们看看 first 有什么问题：它声称给定一个 NumList a ，它可以产生一个 a ，不问任何问题。但我们知道如何轻松地构建 NumList a ！事实上， Num a 约束意味着 0 是 a 并使 [0] 完全有效 NumList a 。这意味着，如果第一被接受，那么所有类型将被占有：



  first :: NumList a  - > a 
 first = head 
 
 elt :: a 
 elt = first [0] 
  

特别是 Void ：



  argh :: Void 
 argh = elt 
  

确实是啊！

I'm trying to understand how type constraints work with type aliases. First, let's assume I have next type alias:

type NumList a = Num a => [a]

And I have next function:

addFirst :: a -> NumList a -> NumList
addFirst x (y:_) = x + y

This function fails with next error:

Type.hs:9:13: error:
    • No instance for (Num a) arising from a pattern
      Possible fix:
        add (Num a) to the context of
          the type signature for:
            addFirst :: a -> NumList a -> a
    • In the pattern: y : _
      In an equation for ‘addFirst’: ad

Which is obvious. This problem already described here:

Understanding a rank 2 type alias with a class constraint

And I understand why we need {-# LANGUAGE RankNTypes #-} for such type aliases to work and why previous example doesn't work. But what I don't understand is why next example compiles fine (on ghc 8):

prepend :: a -> NumList a -> NumList a
prepend = (:)

Of course it fails in ghci if I try to pass wrong value:

λ: prepend 1 []
[1]
λ: prepend "xx" []

<interactive>:3:1: error:
    • No instance for (Num [Char]) arising from a use of ‘prepend’
    • When instantiating ‘it’, initially inferred to have
      this overly-general type:
        NumList [Char]
      NB: This instantiation can be caused by the monomorphism restriction.

Seems like type type checking delayed at runtime :(

Moreover, some simple and seems to be the same piece of code doesn't compile:

first :: NumList a -> a
first = head

And produces next error:

Type.hs:12:9: error:
    • No instance for (Num a)
      Possible fix:
        add (Num a) to the context of
          the type signature for:
            first :: NumList a -> a
    • In the expression: head
      In an equation for ‘first’: first = head

Can somebody explain what is going on here? I expect some consistency in whether function type checks or not.

解决方案

Seems like type type checking delayed at runtime :(

Not really. Here it's may be a bit surprising because you get the type error in ghci after having loaded the file. However it can be explained: the file itself is perfectly fine but that does not mean that all the expressions you can build up using the functions defined in it will be well-typed.

Higher-rank polymorphism has nothing to do with it. (+) for instance is defined in the prelude but if you try to evaluate 2 + "argh" in ghci, you'll get a type-error too:

No instance for (Num [Char]) arising from a use of ‘+’
In the expression: 2 + "argh"
In an equation for ‘it’: it = 2 + "argh"

Now, let's see what the problem is with first: it claims that given a NumList a, it can produce an a, no questions asked. But we know how to build NumList a out of thin air! Indeed the Num a constraints means that 0 is an a and makes [0] a perfectly valid NumList a. Which means that if first were accepted then all the types would be inhabited:

first :: NumList a -> a
first = head

elt :: a
elt = first [0]

In particular Void would be too:

argh :: Void
argh = elt

Argh indeed!

这篇关于带类型别名混乱的RankNTypes的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！