连接自定义向量

Question

我定义了一个向量：

{-# LANGUAGE GADTs, DataKinds, TypeFamilies, UndecidableInstances, TypeOperators #-}
data Nat = Z | S Nat
type family (+) (n :: Nat) (m :: Nat) :: Nat
type instance Z     + m = m
type instance (S n) + m = S (n + m)
type family (*) (n :: Nat) (m :: Nat) :: Nat
type instance Z * m = Z
type instance (S n) * m = n * m + m
data Vec (n :: Nat) a where
  VNil  :: Vec Z a
  VCons :: a -> Vec n a -> Vec (S n) a

并试图制作一个 vectorConcat，如下所示：

vectorConcat :: Vec m (Vec n a) -> Vec (m * n) a

但是，在尝试执行此操作时：

vectorAppend :: Vec n a -> Vec m a -> Vec (n + m) a
vectorAppend VNil         ys = ys
vectorAppend (VCons x xs) ys = VCons x (vectorAppend xs ys)
vectorConcat :: Vec m (Vec n a) -> Vec (m * n) a
vectorConcat VNil = VNil
vectorConcat (VCons x xs) = vectorAppend x (vectorConcat xs)

我收到以下错误，但不确定如何解决它：

Could not deduce (((n1 * n) + n) ~ (n + (n1 * n)))
from the context (m ~ 'S n1)
  bound by a pattern with constructor
             VCons :: forall a (n :: Nat). a -> Vec n a -> Vec ('S n) a,
           in an equation for `concatV'

我已经坚持了一段时间，想知道我是否可以找到任何方向。

Answer 1

GHC 并不真正了解关于算术的许多事实，特别是（在这种情况下）不知道加法是可交换的。教GHC这个事实也不容易。

但是，在这种特定情况下，您可以简单地手动交换(*)定义中的术语，然后事情就可以编译好了：

type instance (S n) * m = m + (n * m)