haskell - 试图让我的 GADT 成为 Num 的实例，但在构造函数之间乘法时遇到问题

Question

这是我的 GADT：

data Vector v where
    Zero    :: (Num a, Eq a, Show a) => Vector a
    Scalar  :: (Num a, Eq a, Show a) => a -> Vector a
    Vector  :: (Num a, Eq a, Show a) => [a] -> Vector [a]
    TVector :: (Num a, Eq a, Show a) => [a] -> Vector [a]

基本上，它表示一个向量，其中包含属于类型类 Num、Eq 和 Show 的元素。

我希望 Vector 本身是一个 Num，所以我执行以下操作：

instance Num (Vector v) where
    (Zero) + (Zero) = Zero
    -- etc
    (Vector a) * (Scalar b) = Vector $ map (* b) a -- This does not work

当我运行代码时，我得到：

Could not deduce (a ~ [a])
    from the context (v ~ [a], Num a, Eq a, Show a)
      bound by a pattern with constructor
                 Vector :: forall a. (Num a, Eq a, Show a) => [a] -> Vector [a],
               in an equation for `*'

为什么会发生这种情况，我该如何解决？

Answer 1

(*) :: Num a => a -> a -> a，即参数的类型必须相同；但是ScalarandVector构造函数给你不同的类型。因此，可以实现(*)andZero构造Scalar函数，以及VectorandTVector构造函数，但不能实现它们的组合。

如果您希望类型的v参数Vector表示向量的元素类型，则只需将VectorandTVector构造函数更改为 returnVector a而不是Vector [a]：

data Vector v where
    ...
    Vector  :: (Num a, Eq a, Show a) => [a] -> Vector a
    TVector :: (Num a, Eq a, Show a) => [a] -> Vector a

您还可以使用ConstraintKinds扩展名缩写重复的类约束：

type EqNumShow a = (Eq a, Num a, Show a)

大概有一个更好的名字来表达你为什么想要那些特定的约束。