haskell - 我在这个本来是微不足道的高级多态性练习中做错了什么？

Question

一年多以前，我问了一个问题 How to use a proxy in Haskell ，从那以后我少量使用了 RankNTypes GHC 扩展。问题是每次我尝试使用它时，我都会收到奇怪的错误消息并在代码中乱窜，直到它们消失。否则我放弃。

显然，我并不真正了解 Haskell 中的高级多态性。为了解决这个问题，我决定直接用最简单的例子，测试我所有的假设，看看我是否能给自己一个 Eureka 时刻。

第一个假设 - 更高等级的多态性不是标准 Haskell 98(或 2010？)功能的原因是，如果您接受一些许多程序员甚至不会注意到的不那么明显的限制，则不需要它.我可以定义 rank 1 和 rank 2 多态函数，乍一看，它们是等价的。如果我将它们加载到 GHCi 并使用相同的参数调用它们，它们将给出相同的结果。

所以 - 简单的示例函数......

{-# LANGUAGE RankNTypes #-}

rank0 :: [Int] -> Bool
rank0 x = null x

rank1a :: [a] -> Bool
rank1a x = null x

rank1b :: forall a. [a] -> Bool
rank1b x = null x

rank2 :: (forall a. [a]) -> Bool
rank2 x = null x

和 GHCi session ...

GHCi, version 7.4.2: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :load example01
[1 of 1] Compiling Main             ( example01.hs, interpreted )
Ok, modules loaded: Main.
*Main>

到目前为止没有错误 - 良好的开始。接下来，使用空列表参数测试每个函数...

*Main> rank0 []
True
*Main> rank1a []
True
*Main> rank1b []
True
*Main> rank2 []
True
*Main>

老实说，我有点惊讶 rank1a和 rank1b函数在这种情况下起作用。列表不知道它包含什么类型的元素，函数也不知道，但肯定必须决定类型来进行调用吗？我期望需要在某处提供明确的签名。

不过，这并不是 ATM 的真正问题，而且结果似乎很有希望。接下来，非空列表...

*Main> rank0 [1,2,3]
False
*Main> rank1a [1,2,3]
False
*Main> rank1b [1,2,3]
False
*Main> rank2 [1,2,3]

<interactive>:10:8:
    No instance for (Num a)
      arising from the literal `1'
    In the expression: 1
    In the first argument of `rank2', namely `[1, 2, 3]'
    In the expression: rank2 [1, 2, 3]
*Main>

哦，亲爱的 - 当参数知道更多关于它的类型时，似乎 rank 2 版本不喜欢它。不过，也许问题只是文字 1等是多态的...

*Main> rank2 ([1,2,3] :: [Int])

<interactive>:11:8:
    Couldn't match type `a' with `Int'
      `a' is a rigid type variable bound by
          a type expected by the context: [a] at <interactive>:11:1
    Expected type: [a]
      Actual type: [Int]
    In the first argument of `rank2', namely `([1, 2, 3] :: [Int])'
    In the expression: rank2 ([1, 2, 3] :: [Int])
*Main>

错误是不同的，但它仍然不起作用，我仍然不明白这些错误消息。

与各种理论混在一起，我的一个想法是，也许我需要告诉 GHC “忘记”列表的一些静态类型。根据这个理论，我尝试了各种方法，包括...

*Main> [1,2,3] :: [a]

<interactive>:12:2:
    No instance for (Num a1)
      arising from the literal `1'
    In the expression: 1
    In the expression: [1, 2, 3] :: [a]
    In an equation for `it': it = [1, 2, 3] :: [a]
*Main>

好的，GHCi 不知道我在说什么。如果 GHCi 只需要确切知道要忘记哪种类型，我也尝试过......

*Main> ([1,2,3] :: [Int]) :: [a]

<interactive>:15:2:
    Couldn't match type `a1' with `Int'
      `a1' is a rigid type variable bound by
           an expression type signature: [a1] at <interactive>:15:1
    Expected type: [a]
      Actual type: [Int]
    In the expression: ([1, 2, 3] :: [Int]) :: [a]
    In an equation for `it': it = ([1, 2, 3] :: [Int]) :: [a]
*Main>

我希望得到一个错误，以至于 GHCi 不知道如何 show具有被遗忘类型的值。我不知道如何用“被遗忘的”静态类型构造一个列表，我什至不确定这是否有意义。

在这一点上，我并没有尝试对更高级别的多态性做任何有用的事情。这里的重点是能够调用 rank2具有非空列表的函数，并了解为什么它与其他函数的工作方式不完全相同。我想自己一步一步地解决这个问题，但现在我完全陷入了困境。

Answer 1

让我们想想rank2的类型是什么方法。

rank2 :: (forall a. [a]) -> Bool
rank2 x = null x

rank2 的第一个参数需要是 forall a. [a] 类型的东西. forall在这里最外层意味着获得这样一个值的人可以选择 a。 .把它想象成把一个类型作为一个额外的参数。

所以，为了给 rank2 提供一些东西作为参数。 ，它需要是一个列表，其元素可以是 rank2的内部实现的任何类型可能想要。由于无法想象出这种任意类型的值，因此唯一可能的输入是 []或包含 undefined 的列表.

将此与 rank1b 进行对比:

rank1b :: forall a. [a] -> Bool
rank1b x = null x

这里 forall已经是最外层了，所以谁用 rank1b自己可以选择类型。

一个可行的变体是这样的:

rank2b :: (forall a. Num a => [a]) -> Bool
rank2b x = null x

现在你可以给它传递一个数字文字列表，它们是多态的 Num实例。另一种选择是这样的:

rank2c :: (forall a. [a -> a]) -> Bool
rank2c x = null x

这是有效的，因为你确实可以想出 forall a. a -> a 类型的值。 ，特别是函数 id .