Как сделать Vect n Int экземпляром Monoid

Question

В Идрисе Vect n a представляет собой тип данных, представляющий вектор n длины, содержащий элементы типа a. Представьте себе, у меня есть функция:

foo : Int -> Vect 4 Int 
foo n = [n-1, n, n+1, n*4] 

Тело функции не имеет значения, это может быть все, что возвращает вектор 4 Ints. Теперь я хочу, чтобы использовать эту функцию concatMap следующим образом:

bar : Vect n Int -> Vect (4*n) Int 
bar vals = concatMap foo vals 

Bar это функция, которая принимает вектор Int длины п и возвращает единица длиной 4 * п.

Тип подписи concatMap является:

Prelude.Foldable.concatMap : Foldable t => Monoid m => (a -> m) -> t a -> m 

И поэтому, если я пытаюсь скомпилировать бар, я получаю ошибку:

When elaborating right hand side of bar: 
    Can't resolve type class Monoid (Vect (plus n (plus n (plus n (plus n 0)))) Int) 

Это означает, что Vect п Int не является экземпляром моноидом. Чтобы сделать это экземпляр моноиде, мне нужно реализовать:

Prelude.Algebra.neutral : Monoid a => a 

Однако, к сожалению, я не знаю, как это сделать. Список реализует моноид, следующим образом:

instance Monoid (List a) where 
    neutral = [] 

Но если я пытаюсь реализовать моноид с нейтральным = [] для Vect п Int, я получаю сообщение об ошибке:

When elaborating right hand side of Prelude.Algebra.Vect n Int instance of Prelude.Algebra.Monoid, method neutral: 
| Can't unify 
|   Vect 0 Int 
| with 
|   Vect n Int 
| 
| Specifically: 
|   Can't unify 
|     0 
|   with 
|     n 

Так мне было интересно, как бы Я собираюсь реализовать моноид для Vect?

Answer 1

Вы не можете реализовать моноид, чтобы вы могли записать это выражение с помощью concatMap. Подумайте о подписании concatMap:

(Foldable t, Monoid m) => (a -> m) -> t a -> m 

Обратите внимание, что m должен быть то же Monoid в обоих возвращаемый тип функционального аргумента (a -> m) и возвращаемый тип всей функции. Однако это не тот случай для Vect n a. Рассмотрим выражение:

concatMap foo vals 

Здесь foo будет иметь тип a -> Vect 4 a и результат concatMap, что вы хотите это типа Vect (4*n) a где n является длина исходного вектора. Но это не может соответствовать concatMap типа, потому что у вас есть применение concatMap, который требует типа как:

(Foldable t, Monoid m, Monoid m1) => (a -> m) -> t a -> m1 

, где могут быть результат Моноид и значение, возвращаемый функцией различных типов, в то время как concatMap навязывает вам использовать такой же тип.

[a] и Vect n a совершенно различны, потому что []делает не включают длину в типе, и это позволяет написать concatMap функции.Фактически это позволяет сделать экземпляр Monoid для [] и конкатенацию как двоичный оператор.

При запуске крепления длины к типу эта возможность исчезает, потому что вы не можете смешивать различные длины больше, и, таким образом, Vect n a сделать не образуют моноид для конкатенации. Оператор конкатенации переходит в тип a -> b -> c в общем случае, и в частности его тип для Vect s равен Vect n a -> Vect m a -> Vect (n+m) a, что явно отличается от его типа для списков: [a] -> [a] ->[a].

---

При этом, ошибка вы сообщили в связи с тем, что при написании экземпляр для Monoid класса Vect n a значение neutral должно быть типа Vect n a но [] имеет тип Vect 0 a.

Однако вы можете создать экземпляр для класса Monoid за Vect n a. Если элементы такого вектора являются моноидами, то вы можете создать моноид таких векторов.

В этом случае он neutral вектор должен быть длиной n, и единственное разумное значение, которое вы можете дать его элементов является neutral элементов Monoid. В принципе, вы хотите, чтобы neutral от Vect n a был replicate n neutral.

Тогда двоичная операция для Monoid будет элементарным применением операции между элементами.

Так что пример будет выглядеть примерно так:

instance Monoid a => Monoid (Vect n a) where 
    neutral = replicate n neutral 

instance Semigroup a => Semigroup (Vect n a) where 
    Nil <+> Nil = Nil 
    (x :: xs) <+> (y :: ys) = (x <+> y) :: (xs <+> ys) 

К сожалению, я не Идрис пользователь/программист, так что я не могу сказать вам точно, как правильно писать такой код. Вышеизложенное является просто псевдокодом типа Haskell, чтобы дать представление о концепциях.