Idris 中接口实例的接口约束

Question

我刚开始学习来自 Haskell 的 Idris，我正在尝试编写一些简单的线性代数代码。

我想为Vect 编写一个Num 接口实例，但专门为Vect n a 编写，约束条件是a 有一个Num 实例。

在 Haskell 中，我会像这样编写一个类型类实例：

instance Num a => Num (Vect n a) where
  (+) a b = (+) <$> a <*> b
  (*) a b = (*) <$> a <*> b
  fromInteger a = a : Nil

但是阅读 Idris interface docs 似乎并没有提到对接口实例的约束。

我能做的最好的事情如下，这可以预见地导致编译器哀叹a 不是数字类型：

Num (Vect n a) where
  (+) Nil Nil = Nil
  (+) (x :: xs) (y :: ys) = x + y :: xs + ys
  (*) Nil Nil = Nil
  (*) (x :: xs) (y :: ys) = x * y :: xs * ys
  fromInteger i = Vect 1 (fromInteger i)

我可以通过使用Num 约束（不可移植）或在命名空间中重载(+)（感觉有点笨拙）创建自己的向量类型来解决这个问题：

namespace Vect
  (+) : Num a => Vect n a -> Vect n a -> Vect n a
  (+) xs ys = (+) <$> xs <*> ys

有没有办法约束接口实现，或者有更好的方法来实现这一点，例如使用依赖类型？

Answer 1

在 Idris 中，你会做（几乎）与 haskell 相同的操作

Num a => Num (Vect n a) where

就像很多事情一样，这在 the book 中，但显然不在文档中。