RankNTypes：是什么导致了这个错误？答案

【问题标题】：RankNTypes: What is causing this error?RankNTypes：是什么导致了这个错误？
【发布时间】：2012-10-06 10:29:37
【问题描述】：

我一直在探索 Rank2Types 和 RankNTypes 以尝试熟悉它们。但我无法弄清楚为什么以下不起作用。

g :: (forall a. forall b. a -> b) -> x -> y -> (u,v)
g p x y = (p x, p y)

这个定义被编译器接受，但是当我尝试使用它时它失败了：

ghci> g id 1 2

<interactive>:35:3:
    Couldn't match type `a' with `b'
      `a' is a rigid type variable bound by
          a type expected by the context: a -> b at <interactive>:35:1
      `b' is a rigid type variable bound by
          a type expected by the context: a -> b at <interactive>:35:1
    Expected type: a -> b
      Actual type: a -> a
    In the first argument of `g', namely `id'
    In the expression: g id 1 2

我很难理解为什么 a->a 不是预期的 a->b 可接受的类型。

【问题讨论】：

对于all a 和b，您需要a -> b 类型的函数。由于id 是forall a. a -> a 类型（即它只满足a ~ b 的第一个签名）它不是g 的有效输入。

标签： haskell types ghc

【解决方案1】：

对于所有类型a 和b，forall a. forall b. a -> b 类型的函数必须能够获取a 类型的值并产生b 类型的值。因此，例如，必须可以输入Int 并输出String。

如果输入Int，则无法从id 中获得String - 您只能返回与输入相同的类型。所以id 不是forall a. forall b. a -> b 类型。事实上，没有类型类约束就不可能有该类型的全部功能。

事实证明，你可以使用 ConstraintKinds 做一些接近（ish）你想要的事情，但它写起来既不美观也不美观：

这个想法是用约束参数化g，这些约束指定x、y、u和v需要满足哪些条件，以及x和u之间的关系和在y 和v 之间需要。由于我们在所有情况下都不需要所有这些约束，因此我们还引入了两个虚拟类型类（一个用于对单个参数的约束，一个用于“关系约束”），以便我们可以将它们用作不需要约束的约束（如果我们自己不指定约束，GHC 将无法推断约束）。

一些示例约束使这一点更清楚：

如果我们传入id作为函数，x必须等于u并且y必须等于v。 x、y、u 或 v 没有单独的限制。
如果我们传入show，x 和y 必须是Show 和u 的实例，v 必须等于String。 x和u或y和v之间的关系没有限制。
如果我们传入read . show，x和y需要是Show和u的实例，v需要是Read的实例。同样没有限制它们之间的关系。
如果我们有一个类型类Convert a b where convert :: a -> b 并且我们传入convert，那么我们需要Convert x u 和Convert y v，并且对各个参数没有限制。

下面是实现这个的代码：

{-# LANGUAGE Rank2Types, ConstraintKinds, FlexibleInstances, MultiParamTypeClasses #-}

class Dummy a
instance Dummy a

class Dummy2 a b
instance Dummy2 a b

g :: forall c. forall d. forall e. forall x. forall y. forall u. forall v.
     (c x, c y, d u, d v, e x u, e y v) =>
     (forall a. forall b. (c a, d b, e a b) => a -> b) -> x -> y -> (u,v)
g p x y = (p x, p y)

下面是如何使用它：

使用show . read在不同类型的数字之间进行转换：

> (g :: (Show x, Show y, Read u, Read v, Dummy2 x u, Dummy2 y v) => (forall a. forall b. (Show a, Read b, Dummy2 a b) => a -> b) -> x -> y -> (u,v)) (read . show) 1 2 :: (Double, Int)
(1.0,2)

使用id:

> (g :: (Dummy x, Dummy y, x~u, y~v) => (forall a. forall b. (Dummy a, Dummy b, a~b) => a -> b) -> x -> y -> (u,v)) id 1 2.0
(1,2.0)

使用show：

> (g :: (Show x, Show y, String~u, String~v, Dummy2 x u, Dummy2 x y) => (forall a. forall b. (Show a, String~b, Dummy2 a b) => a -> b) -> x -> y -> (u,v)) show 1 2.0
("1","2.0")

如您所见，这非常冗长且难以阅读，因为您每次使用它时都需要为g 指定一个签名。没有这个，我认为不可能让 GHC 正确推断约束（或者至少我不知道如何）。

【讨论】：

那么，如何表达p的类型可以取任意类型并返回任意类型呢？即，它可以是id 或show 或(< 10) 等。给定函数的实现，它的类型应该是什么？
@PeterHall 你不能。此外，您将无法以任何方式传递show，因为x 和y 不是Show 的实例。
啊，我已经理解了一部分了。如果我需要参数是 Int 和 Bool 但结果是 (Int, String) 那么没有这样的函数可以满足这一点。编译器无法推断出这个事实，但它会拒绝我尝试的所有内容。
@PeterHall 没有 total 函数可以满足这一要求。像f x = f x（或简单的undefined）这样的东西可以很容易地满足这一点。如果您添加一些类型类约束，您甚至可以获得满足它的全部函数，例如 read . show 如果 x 和 y 是 Show 和 u 和 v 的实例 @ 的实例987654400@。使用 ConstraintKinds，你甚至可以让它变得有点通用/有用。你仍然无法让它按照你的想法去做。
@PeterHall 事实证明，使用 KindConstraints 可以做你想做的事，但我不推荐它。查看我的编辑。

【解决方案2】：

当您查看函数forall a. forall b. a -> b 时，这意味着它接受任何类型的值并且可以返回任何类型的值。假设 f 是这样一个函数，那么您可以将 f 1 提供给任何函数，或者将 f "hello" 提供给任何函数，因为 f 的返回类型仍然是多态的，而另一方面，一旦您给 id 一个值，返回类型是固定的（它将与输入值的类型相同），因此错误。

【讨论】：

谢谢，我知道了。要使其正常工作，始终需要一些其他类型约束。