Бесплатная групповая монада

В теории категорий aa monad представляет собой композицию из двух сопряженных функторов. Например, монада Maybe может быть свободным указательным функтором, составленным с забывчивым функтором. Аналогично, Монада Списка - это свободный моноидный функтор, составленный с забывчивым функтором.

Моноид - одна из простейших алгебраических структур, поэтому я задаюсь вопросом, может ли программирование извлечь выгоду из более сложных. Я не нашел бесплатную групповую монаду в стандартных пакетах Haskell, поэтому я определю ее здесь.

data FreeGroup a = Nil | PosCons a (FreeGroup a) | NegCons a (FreeGroup a)

Оператор == определяется так, что NegCons x (PosCons x y) == y. Соответственно, в length :: FreeGroup a -> Int каждый PosCons подсчитывается +1 и каждый NegCons -1 (это единственный морфизм группы для Int, что значения +1 на каждом PosCons).

Как и в списках (свободные моноиды), concat является просто умножением, а map является функториальным лифтом функций. Таким образом, экземпляр monad FreeGroup точно такой же, как у List.

Использует ли свободная групповая монада какое-либо программирование? Кроме того, часто существует интерпретация монады как значения в контексте: для List контекст будет выбором или неопределенностью. Существует ли такая интерпретация для свободной монады?

Как насчет свободных колец и векторных пространств (которые всегда свободны)?

Для любой алгебраической структуры S существование категорического свободного функтора FS :: Set -> S означает существование функции, которую Haskell вызывает fold:

foldS :: S s => (a -> s) -> FS a -> s

Он поднимает функцию на основе a на S -морфизм на свободном объекте FS a. Обычная функция foldr является специализацией foldMonoid (называемой foldMap в Haskell, по какой-то причине я не совсем понимаю), моноид - это набор функций b -> b с составом как умножение.

Для полноты, вот пример монады FreeGroup:

mult :: FreeGroup a -> FreeGroup a -> FreeGroup a
mult Nil x = x
mult x Nil = x
mult (PosCons x y) z = PosCons x (mult y z)
mult (NegCons x y) z = NegCons x (mult y z)

inverse :: FreeGroup a -> FreeGroup a
inverse Nil = Nil
inverse (PosCons x y) = mult (inverse y) (NegCons x Nil)
inverse (NegCons x y) = mult (inverse y) (PosCons x Nil)

groupConcat :: FreeGroup (FreeGroup a) -> FreeGroup a
groupConcat Nil = Nil
groupConcat (PosCons x l) = mult x (groupConcat l)
groupConcat (NegCons x l) = mult (inverse x) (groupConcat l)

instance Functor FreeGroup where
  fmap f Nil = Nil
  fmap f (PosCons x y) = PosCons (f x) (fmap f y)
  fmap f (NegCons x y) = NegCons (f x) (fmap f y)

instance Applicative FreeGroup where
  pure x = PosCons x Nil
  fs <*> xs = do { f <- fs; x <- xs; return $ f x; }

instance Monad FreeGroup where
  l >>= f = groupConcat $ fmap f l

Ответы

Ответ 1

"Использует ли свободная групповая монада какое-либо программирование?"

Из-за отсутствия ответов за последние четыре месяца, я полагаю, что ответ "нет, а не действительно". Но это интересный вопрос, и поскольку он основан на фундаментальных математических концепциях, мне кажется (также), что он должен.

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

type FreeGroupT a = [Either a a]

fgTofgT :: FreeGroup a -> FreeGroupT a
fgTofgT Nil = []
fgTofgT (a :+: as) = Right a : fgToList as
fgTofgT (a :-: as) = Left a : fgToList as

fgTTofg :: FreeGroupT a -> FreeGroup a
fgTTofg [] = Nil
fgTTofg (Right a : as) = a :+: fgTTofg as
fgTTofg (Left a : as) = a :-: fgTTofg as

--using (:-:) instead of NegCons
--and   (:+:) instead of PosCons

Это хорошее определение, так как мы гарантируем, что наша свободная группа является просто моноидом с небольшой дополнительной структурой. Он гласит, что свободная группа - это всего лишь композиция свободного моноида с другим функтором (какое имя? Нет, либо b bifunctor, но и функтор F a = L a | R a). Мы также гарантируем, что экземпляр монады свободной группы согласуется с экземпляром монады свободного моноида. То есть, монады свободной группы, которые действуют на условиях, которые все бывают положительными, должны вести себя как монады над свободным моноидом, правильно?

В конечном счете, однако, если мы хотим уменьшить обратные, нам нужен экземпляр Eq a. Нам нужно будет работать на уровне термина, чистая информация о типе уровня недостаточно. Это делает различие уровня между свободным моноидом и свободной группой бесполезным - насколько я могу видеть. По крайней мере, без зависимого набора текста.

В целях обсуждения фактических применений программного обеспечения я попытаюсь (но не обязательно) предоставить правдоподобный вариант использования.

Представьте текстовый редактор, который использует клавишу "Ctrl", чтобы сигнализировать последовательности команд. Любая последовательность клавиш, нажатая при удерживании "Ctrl", моделируется как негативы (отрицательные минусы (: -:)) в FreeGroup. Таким образом, свободный член группы 'a':+:'b':+:'b':-:'a':-:[] может использоваться для моделирования поведения emacs, который записывает "ab", перемещает курсор назад символ, а затем в начало строки. Такой дизайн приятный. Мы можем легко вставлять команды и макросы в поток без каких-либо специальных зарезервированных escape-символов.

Однако этот пример не подходит для правильного использования, так как мы ожидаем, что 'a':+:'b':+:'b':-:'a':-:[] будет той же программой, что и [], а это не так. Более того, его достаточно просто, чтобы просто обернуть каждый член списка в Либо, как описано выше.