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

Question

我有一堆函数可用于Vector,即具有类型强制长度的列表.

我试图让我的类型更容易编写,即不是写作

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在一个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

由于各种神秘的原因(类型级别的lambdas会破坏与实例解析和推理相关的各种事情 - 想象你是否可以定义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的新约束种类,您可以完全避免使用单独的类型,只需定义约束同义词:

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包使用相同的一般概念.大量的类和大型上下文可能使错误消息非常混乱并减慢编译速度,但这是类型级hackery的本质.但是,如果您将基本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

这应该允许你完全消除上下文,但是使向量上的操作定义有点棘手.