Блог

Я только начинаю изучать Idris из Haskell, и я пытаюсь написать какой-нибудь простой код линейной алгебры.

Я хочу написать экземпляр 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, похоже, не упоминаются ограничения на экземпляры интерфейса.

Лучшее, что я могу сделать, это следующее, что предсказуемо заставляет компилятор жаловаться 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
  

Как и многие другие вещи, это есть в книге, но, по-видимому, нет в документах.