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

Question

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

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

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

我要宣布一个新类(class) 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 之类的操作转到 Maybe向量。

因此，v必有样* -> * , 和 i实物* .

但是，当我尝试用这样的向量实例化它时:

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'

现在，我对类型级编程非常陌生，而且我知道我很可能以一种非常落后的方式来做这件事。是否可以实例化这样的类型同义词？是否有任何类型向导对实现我的目标的更好方法提出建议？

Answer 1

这里的问题是 Vec2和 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就好像它是一个完全成熟的类型构造函数，类型为 * -> * ;它实际上是一个类型级别的“宏”，只能完全应用。

但是，您可以将类型同义词定义为部分应用程序本身:

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

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

如果您的 Vec3类型实际上看起来像

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

或类似的，那你就不走运了；您必须使用 newtype如果你想给出任何实例，包装器。 (另一方面，您应该能够完全避免直接在这些类型上定义实例，而是提供 Nil 和 Cons 的实例，而允许您使用 Vec3 作为实例。)

请注意，使用 GHC 7.4 的新 constraint kinds ，您可以完全避免使用单独的类型，而只需定义一个约束同义词:

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 使用了相同的一般思想。包裹。大量的类和大的上下文会使错误消息非常困惑并减慢编译速度，但这就是类型级黑客的本质。但是，如果您有一个基数 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

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