连接自定义矢量

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)