使用此GADT进行模式匹配:

Question

我已经定义了以下GADT:

data Vector v where
    Zero    :: Num a => Vector a
    Scalar  :: Num a => a -> Vector a
    Vector  :: Num a => [a] -> Vector [a]
    TVector :: Num a => [a] -> Vector [a]

如果它不明显,我正在尝试实现一个简单的向量空间.所有向量空间都需要向量加法,所以我想通过make Vector和instanceof 来实现它Num.在向量空间中,添加不同长度的向量没有意义,这是我想要强制执行的.我认为这样做的一种方法是使用警卫:

instance Num (Vector v) where
    (Vector a) + (Vector b) | length a == length b =  
                                Vector $ zipWith (+) a b
                            | otherwise = 
                                error "Only add vectors with the same length."

这种方法没有什么问题,但我觉得必须有一种方法来实现模式匹配.也许一种方法是定义一个新的数据类型VectorLength,它看起来像这样:

data Length l where
    AnyLength   :: Nat a => Length a
    FixedLength :: Nat a -> Length a

然后,可以将长度组件添加到Vector数据类型,如下所示:

data Vector (Length l) v where
    Zero :: Num a => Vector AnyLength a
    -- ...
    Vector :: Num a => [a] -> Vector (length [a]) [a]

我知道这不是正确的语法,但这是我正在玩的一般想法.最后,您可以定义添加

instance Num (Vector v) where
    (Vector l a) + (Vector l b) = Vector $ zipWith (+) a b

这样的事情是可能的,还是有其他方法可以为此目的使用模式匹配？

Answer 1

您正在寻找的也是名为 a 的东西（在本例中令人困惑）Vector。一般来说，这些用于依赖类型语言，您可以编写类似的内容

data Vec (n :: Natural) a where
  Nil  :: Vec 0 a
  Cons :: a -> Vec n a -> Vec (n + 1) a

但这远非有效的 Haskell（或实际上任何语言）。GHC 的一些最新扩展已开始支持这种表达方式，但目前还没有实现。

您可能对固定向量感兴趣，它可以最好地近似相对稳定的 GHC 中可用的固定向量Vector。它在类型族和延续之间使用了许多技巧来创建固定大小向量的类。