带有类型别名混淆的RankNTypes

Question

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

type NumList a = Num a => [a]

我有下一个函数：

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

此函数失败，并显示下一个错误：

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

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

Understanding a rank 2 type alias with a class constraint

我理解为什么我们需要{-# LANGUAGE RankNTypes #-}才能让这种类型别名工作，以及为什么前面的例子不能工作。但我不明白的是，为什么下一个示例(在ghc 8上)编译得很好：

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

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

λ: 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.

看起来像在运行时延迟的类型检查:(

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

first :: NumList a -> a
first = head

并产生下一个错误：

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

有人能解释一下这是怎么回事吗？我希望在是否进行函数类型检查时保持一定的一致性。

Answer 1

看起来像在运行时延迟的类型检查:(

不怎么有意思。这里可能有点令人惊讶，因为在加载文件后，您会在ghci中得到类型错误。然而，可以解释:文件本身是完全没有问题的，但这并不意味着您可以使用其中定义的函数构建的所有表达式都是类型良好的。

更高级别的多态性与此无关。例如，(+)是在前言中定义的，但是如果你试图在ghci中计算2 + "argh"，你也会得到一个类型错误：

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

现在，让我们看看first的问题是什么:它声称给定一个NumList a，它可以生成一个a，这是没有问题的。但是我们知道如何凭空构建NumList a！实际上，Num a约束意味着0是一个a，并使[0]成为一个完全有效的NumList a。这意味着如果first被接受，那么所有类型都将被居住：

first :: NumList a -> a
first = head

elt :: a
elt = first [0]

特别是，Void也会是：

argh :: Void
argh = elt

啊，的确！