声明参数化类型同义词的实例

我有很多适用于向量的函数，即具有类型强制长度的列表。

我试图让我的类型更容易编写，即而不是编写

foo :: (Fold Integer v, Map Integer Integer v v, ...) => ...

我正在宣布一个新班级NList所以我可以写foo :: NList v Integer => ...

（简化的）类如下所示：

class ( Fold (v i) i
      , Map i i (v i) (v i)
      , Map i (Maybe i) (v i) (v (Maybe i))
      ) => NList v i

正如您所看到的，我必须将“向量”类型与“项目”类型分开（即v从.....分离i）这样我就可以做类似的事情Map onto a Maybe vector.

像这样，v必须有种类* -> *, and i kind *.

然而，当我尝试用这样的向量实例化它时：

instance NList Vec2 Integer
instance NList Vec3 Integer
...

我收到以下错误：

Type synonym `Vec2' should have 1 argument, but has been given none
In the instance declaration for `NList Vec2 Integer'

现在，我对类型级编程非常陌生，并且我知道我可能会以非常落后的方式进行此操作。是否可以实例化这样的类型同义词？是否有任何类型向导可以提供更好的方法来实现我的目标的建议？

这里的问题是Vec2 and Vec3大概被声明为这样的：

type Vec2 a = Vec (S (S Z)) a
type Vec3 a = Vec (S (S (S Z))) a

由于各种神秘的原因，类型同义词不能部分应用（它们会导致类型级 lambda，这会严重破坏与实例解析和推理相关的各种事物 - 想象一下，如果您可以定义type Id a = a并使其成为一个实例Monad).

也就是说，你无法使Vec2任何事物的实例，因为你不能使用Vec2就好像它是一个成熟的类型构造函数，具有以下类型* -> *;它实际上是一个只能完全应用的类型级“宏”。

然而，你can将类型同义词定义为部分应用程序本身：

type Vec2 = Vec (S (S Z))
type Vec3 = Vec (S (S (S Z)))

这些是等效的，只是您的实例将被允许。

If your Vec3类型实际上看起来像

type Vec3 a = Cons a (Cons a (Cons a Nil)))

或类似的，那么你就不走运了；你必须使用newtype如果您想提供任何实例，请使用包装器。 （另一方面，您应该能够完全避免直接在这些类型上定义实例，方法是为Nil and Cons相反，允许您使用Vec3作为一个例子。）

请注意，GHC 7.4 的新功能约束种类 http://blog.omega-prime.co.uk/?p=127，您可以完全避免单独的类型，而只需定义一个约束同义词：

type NList v i =
    ( Fold (v i) i
    , Map i i (v i) (v i)
    , Map i (Maybe i) (v i) (v (Maybe i))
    )

就您的总体方法而言，它基本上应该可以正常工作；使用相同的一般思想Vec http://hackage.haskell.org/package/Vec包裹。大量的类和大的上下文可能会使错误消息变得非常混乱并减慢编译速度，但这就是类型级黑客的本质。不过，如果你有一定的基础Vec类型定义为通常的 GADT：

data Vec n a where
    Nil :: Vec Z a
    Succ :: a -> Vec n a -> Vec (S n) a

那么你实际上根本不需要任何类型类。如果它以其他方式定义，但仍然在类型级别自然参数化，那么您可以将所有类替换为一个类：

data Proxy s = Proxy

class Nat n where
    natElim
        :: ((n ~ Z) => r)
        -> (forall m. (n ~ S m, Nat m) => Proxy m -> r)
        -> Proxy n
        -> r

这应该允许您完全消除上下文，但使定义向量上的操作变得有点棘手。