haskell - RankNTypes : What is causing this error?

Question

我刚刚探索了 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 来说不是可接受的类型。

Answer 1

对于所有类型a和b，对于所有a，类型为的函数。福奥尔湾a -> b 必须能够获取 a 类型的值并生成 b 类型的值。因此，例如，它必须能够放入 Int 并取出 String。

如果您输入 Int，则无法从 id 中获取 String - 您只能返回与您相同的类型所以对于all a来说，id不是类型。福奥尔湾a -> b。事实上，如果没有类型类约束，就不会有该类型的总函数。

<小时/>

事实证明，您可以使用 ConstraintKinds 做一些接近您想要的事情，但它写起来并不漂亮，使用起来也不漂亮:

这个想法是使用约束参数化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，其中convert::a -> b并且我们传入convert，那么我们需要Convert x u 和转换 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 。读取以在不同类型的数字之间进行转换:

> (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)

使用显示:

> (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 正确推断约束(或者至少我不知道如何推断)。