Idris中的接口实例的接口约束

问题描述

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

我想为Num写一个Vect接口实例，但要特别为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

是否有一种方法来约束接口的实现，或者有更好的方法来实现此目的，例如使用依赖类型？

解决方法

在Idris中，您（几乎）与haskell一样

Num a => Num (Vect n a) where

与许多事情类似，它在http://0.0.0.0:6405中，但显然不在文档中。