9

我一直在探索 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。

4

2 回答 2

10

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

如果你输入一个- 你只能得到你输入String的相同类型。所以不是类型。事实上，没有类型类约束就不可能有该类型的全部功能。idIntidforall a. forall b. a -> b

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

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

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

  • 如果我们id作为函数传入，x必须等于u且y必须等于v。x,y或u单独没有限制v。
  • 如果我们传入show, xandy必须是 and 的实例并且Show必须等于. 和或和之间的关系没有限制。uvStringxuyv
  • 如果我们传入read . show, xandy需要是 和 的实例并且Show需要是. 再次对它们之间的关系没有限制。uvRead
  • 如果我们有一个类型类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 正确推断约束（或者至少我不知道如何）。

于 2012-10-16T10:45:08.050 回答
4

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

于 2012-10-16T10:50:14.053 回答