Interface constraints for interface instances in Idris

Question

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?

joel joel · Accepted Answer · 2020-10-29T17:01:11

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.

Interface constraints for interface instances in Idris

1 Answers