5

我已经定义了以下 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]

如果不是很明显，我正在尝试实现一个简单的向量空间。所有向量空间都需要向量加法，所以我想通过 makeVector和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

这样的事情是否可能，或者有没有其他方法可以为此目的使用模式匹配？

4

2 回答 2

4

您正在寻找的东西（在这种情况下令人困惑）Vector也被命名为 a 。通常，这些用于依赖类型的语言中，您可以在其中编写类似的内容

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

但这远非有效的 Haskell（或任何语言）。一些最近对 GHC 的扩展开始启用这种表达方式，但它们还没有实现。

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

于 2013-10-19T20:09:47.120 回答
4

只是添加到另一个答案中的示例 - 这几乎已经在 GHC 7.6 中有效：

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators #-}

import GHC.TypeLits

data Vector (n :: Nat) a where
    Nil  :: Vector 0 a
    Cons :: a -> Vector n a -> Vector (n + 1) a

该代码编译得很好，它只是不像你希望的那样工作。让我们在 ghci 中检查一下：

*Main> :t Nil
Nil :: Vector 0 a

目前很好...

*Main> :t Cons "foo" Nil
Cons "foo" Nil :: Vector (0 + 1) [Char]

嗯，这有点奇怪......为什么它说(0 + 1)而不是1？

*Main> :t Cons "foo" Nil :: Vector 1 String

<interactive>:1:1:
    Couldn't match type `0 + 1' with `1'
    Expected type: Vector 1 String
      Actual type: Vector (0 + 1) String
    In the return type of a call of `Cons'
    In the expression: Cons "foo" Nil :: Vector 1 String

呃。哎呀。这就是为什么它说(0 + 1)而不是1. 它不知道那些是一样的。这将在 GHC 7.8 中修复（至少这种情况会），这将是由于......在几个月内，我想？

于 2013-10-19T23:06:56.373 回答