RankNTypes:导致此错误的原因是什么？

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的函数forall a. forall b. a -> b必须能够获取类型a的值并生成类型的值b.因此,例如,它必须能够投入Int并获得一个String.

你不能得到一个String出来的id,如果你把在Int-你永远只能拿回你把在同一类型,因此,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不能正确地推断出约束(或者至少我不知道如何).