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

Question

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

{-# 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 的建议选择了语言扩展来编译代码。整个结构的灵感来自 How to make fixed-length vectors instance of Applicative? .

当我尝试使用它时，问题就开始了:

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

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

• 无法推断(Applicative (Vector n))
因使用“<*>”而产生
从上下文:Num t
受 ... 的实例声明约束

• 在表达式中:(+) v <> v'
在“+”的等式中: v + v' = (+) v <> v'
在“Num (Vector n t)”的实例声明中

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

知道发生了什么吗？在链接的问题中，同样的技巧似乎有效!？ (在第一行添加 KindSignatures 没有帮助，如果没有 FlexibleInstances/Contexts 我会收到编译器错误。)

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以这种方式适用于所有 n s, 所有 Vector n t s 是 Num 的成员给定 Num t ，与 n 的值无关，但它必须是 instance 签名的一部分宣言。