I am just starting to learn Idris coming from Haskell, and I'm trying to write some simple linear algebra code.
I want to write a Num interface instance for Vect, but specifically for Vect n a with the constraint that a has a Num instance.
In Haskell I would write a typeclass instance like this:
instance Num a => Num (Vect n a) where
(+) a b = (+) <$> a <*> b
(*) a b = (*) <$> a <*> b
fromInteger a = a : Nil
But reading the Idris interface docs does not seem to mention constraints on interface instances.
The best I can do is the following, which predictably causes the compiler to lament about a not being a numeric type:
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)
I can work around this by creating my own vector type with a Num constraint (which isn't portable) or by overloading (+) in a namespace (which feels a little clunky):
namespace Vect
(+) : Num a => Vect n a -> Vect n a -> Vect n a
(+) xs ys = (+) <$> xs <*> ys
Is there a way to constrain interface implementations, or is there a better way to accomplish this, eg using dependent types?
In Idris, you'd do (almost) the same as haskell
Num a => Num (Vect n a) where
Like a number of things, this is in the book but not, apparently, in the docs.