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

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

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

Как видите, тип Tensor параметризуется Vect из Nats, описывающих размеры тензора, и типом, описывающим его содержимое. Все идет нормально. Затем я решил попробовать сделать тип 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, но я все еще не совсем привык к жаргону, используемому в программировании с зависимой типизацией в целом и в Идрисе в частности, поэтому я буду очень признателен за любую помощь в понимании сообщения об ошибке.


idris
person Kwarrtz    schedule 21.05.2016    source источник

Ответы (1)


arrow_upward
3
arrow_downward

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

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

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 - это рекурсивный вызов.

person András Kovács    schedule 21.05.2016