如何为强制长度为2 ^ n的向量类型定义可用的Applicative实例

Question

对于某些应用程序，我需要长度为$ 2 ^ n $的向量。为了使长度与某些操作相匹配，我使用ist应用实例定义了我的类型，如下所示：

{-# LANGUAGE GADTs, DataKinds, FlexibleInstances, FlexibleContexts #-}
data Nat = Z | N Nat
data Vector n t where
  S :: t -> Vector Z t
  V :: Vector n t -> Vector n t -> Vector (N n) t

instance Functor (Vector n) where
  fmap f (S t ) = S (f t)
  fmap f (V t t') = V (fmap f t) (fmap f t')

instance Applicative (Vector Z) where
  pure = S
  S f <*> S a = S (f a)

instance Applicative (Vector n) => Applicative (Vector (N n)) where
  pure a = let a' = pure a in V a' a'
  V f f' <*> V a a' = V (f <*> a) (f' <*> a')

我根据ghci的建议选择了语言扩展，以使代码得以编译。整个结构的灵感来自于如何使Applicative的定长向量实例化？。

当我尝试使用它时，麻烦开始了：

instance Num t => Num (Vector n t) where
  v + v' = (+) <$> v <*> v'
  (*) = undefined
  abs = undefined
  signum = undefined
  fromInteger = undefined
  negate = undefined

添加这些行会触发以下错误：

•无法从上下文中推断出由于使用'<*>'而引起的（应用（向量n））：...

•在表达式中：（+）v < > v'在'+'的方程式中：v + v'=（+）v < > v'在'Num（Vector nt）'的实例声明中

我在Windows 7上使用Haskell Platform 8.0.2-a。

知道发生了什么吗？在链接的问题中，同样的技巧似乎有效！（在第一行中添加KindSignatures无济于事，并且如果没有FlexibleInstances / Context，我会收到一个编译器错误。）

Answer 1

您应该在Num (Vector n t)实例声明中添加类型约束，该约束指定Vector n a是的实例Applicative，否则不能(<*>)在此处使用。

因此，您可以使用以下方法解决问题：

instance (Num t, Applicative (Vector n)) => Num (Vector n t) where
  v + v' = (+) <$> v <*> v'
  -- ...

在这里，我们这样说，Vector n t是的一个实例Num给出的t是一个实例Num，并且Vector n是的一个实例Applicative。

由于您instance Applicative以Vector n对所有ns都适用的方式为您定义了your ，因此所有Vector n ts都是Num给定的成员Num t，而与的值无关n，但它必须是instance声明签名的一部分。