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

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

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

知道是怎么回事吗？在相关的问题中，同样的技巧似乎奏效了！？（在第一行添加KindSignature没有帮助，如果没有Flexible实例/上下文，我会得到一个编译器错误。）

Answer 1

我认为使用辅助类更好一点。我也倾向于liftA2而不是

class App' n where
  pure' :: a -> Vector n a

instance App' 'Z where
  pure' = S

instance App' n => App' ('N n) where
  pure' a = let a' = pure' a in V a' a'

liftA2'
  :: (a -> b -> c)
  -> Vector n a
  -> Vector n b
  -> Vector n c
liftA2' f = \xs -> go xs
  where
    go (S x) (S y) = S (f x y)
    go (V l1 r1) (V l2 r2) =
      V (go l1 l2) (go r1 r2)

instance App' n => Applicative (Vector n) where
  pure = pure'
  -- import Control.Applicative to get the liftA2 method
  liftA2 = liftA2'

Answer 2

您应该在您的Num（Vector n t）实例声明中添加一个类型约束，指定Vector n a是Applative的实例，否则您不能使用（

因此，您可以通过以下方式解决问题：

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

因此，我们在这里说，Vector n t是Num的一个实例，给定的t是Num的一个实例，Vector n是Applicative的一个实例。

由于您为您的Vector n定义了应用程序实例，因此它适用于所有Vector ns，因此所有Vector n ts都是给定Num t的成员，而不管n的值，但它需要是实例声明的签名的一部分。