Определение экземпляра фактора для тензорного типа (Idris)

Question

Недавно я изучал Идрис и решил, что попробую написать простую библиотеку тензоров. Я начал с определения типа.

data Tensor : Vect n Nat -> Type -> Type 
    Scalar : a -> Tensor [] a 
    Dimension : Vect n (Tensor d a) -> Tensor (n::d) a 

Как вы можете видеть, тип Tensor параметризуется Vect из Nat с описывающих размеры тензора, и тип, описывающий его содержимое. Все идет нормально. Затем я решил попробовать сделать Tensor тип Functor.

instance Functor (Tensor d) where 
    map f (Scalar x) = f x 
    map f (Dimension x) = map f x 

И Идрис дал мне следующую ошибку.

Unifying `b` and `Tensor [] b` would lead to infinite type 

Хорошо. Из ошибки я понял, что, может быть, проблема в том, что первый шаблон map был слишком специфичным (т. Е. Принимал бы только скаляры, когда объявление типа карты таково, что оно принимает любой тензор). Это показалось странным, но я решил, что попробую переписать его с помощью инструкции with.

dimensions : {d : Vect n Nat} -> Tensor d a -> Vect n Nat 
dimensions {d} _ = d 

instance Functor (Tensor d) where 
    map f t with (dimensions t) 
    map f (Scalar x) | []  = f x 
    map f (Dimension x) | (_::_) = map f x 

Но у меня такая же ошибка. У меня довольно много опыта в Haskell, но я до сих пор не совсем привык к жаргону, который используется в типично типизированном программировании в целом и, в частности, Идрисе, поэтому всякая помощь в понимании сообщения об ошибке была бы весьма признательна.

Answer 1

(Примечание: от Idris 0.10 ключевое слово instance устарело и должно быть просто опущено).

Задача состоит в том, чтобы применить функцию ко всем элементам в конструкторах Scalar, но в остальном оставить структуру неизменной. Итак, нам нужно нанести Scalar на Scalar и Dimension на Dimension, а так как Dimension содержит вектор рекурсивных вхождений, мы должны использовать map для доступа к ним.

Functor (Tensor d) where 
    map f (Scalar x)  = Scalar (f x) 
    map f (Dimension xs) = Dimension (map (map f) xs) 

Так, в map (map f) xs, первый map для отображения над Vect и map f является рекурсивным вызовом.