Free group monad

Question

In category theory, a monad is the composition of two adjoint functors. For example, the Maybe monad is the free pointed-set functor composed with the forgetful functor. Likewise, the List monad is the free monoid functor composed with the forgetful functor.

Monoid is one of the simplest algebraic structures, so I wonder if programming can benefit from more complex ones. I didn't find the free group monad in standard Haskell packages, so I'll define it here

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

The == operator is defined such that NegCons x (PosCons x y) == y. Accordingly, in length :: FreeGroup a -> Int, each PosCons is counted +1 and each NegCons -1 (it is the only group morphism to Int that values +1 on each PosCons).

As in lists (free monoids), concat is just multiplication and map is the functorial lift of functions. So the monad instance of FreeGroup is exactly the same as that of List.

Does the free group monad have any programming uses ? Also, there is often an interpretation of a monad as a value in a context : for List the context would be choice or uncertainty. Is there such an interpretation for the free group monad ?

How about free rings and vector spaces (which are always free) ?

For any algebraic structure S, the existence of a categorical free functor FS :: Set -> S means the existence of a function Haskell calls fold :

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

It lifts a function on the basis a to an S-morphism on the free object FS a. The usual foldr function is a specialization of foldMonoid (called foldMap in Haskell, for some reason I don't quite get), the monoid being the set of functions b -> b with composition as multiplication.

For the sake of completeness, here is the monad instance of 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

To define NegCons x (PosCons x y) == y, you need an Eq instance for the a in FreeGroup a. You cannot force that. I doubt FreeGroup is a monad in haskell. — Franky
It's the same for lists : instance Eq a => Eq [a]. The monad definition doesn't need the == operator, I just spoke of it the explain the link between PosCons and NegCons. — V. Semeria
You cannot have an Eq constraint here like in the example you gave in the comment because for Monad you don't have "access" to the type argument. You cannot put an Eq constraint on instance Monad FreeGroup where .... I guess this could work if you avoid equality by not having the Monad instance put it in any sort of normal form. — David Young
The operation you're obviously missing is the one that shows that group operations factor through the free group. In Haskell terms, this is probably best expressed as type instance Element (FreeGroup a) = a and then instance Eq a => MonoFoldable (FreeGroup a) where .... The ofoldMap implementation will have to collapse positive and negative elements appropriately. You'll probably also want normalize :: Eq a => FreeGroup a -> FreeGroup a. The need to normalize manually, and track normalization without help from the type checker, is probably the biggest barrier to making this useful. — dfeuer

trevor cook trevor cook · Accepted Answer · 2017-01-19T20:35:10

"Does the free group monad have any programming uses ?"

Due to the lack of answers over the last four months, I suppose the answer is 'no, not really'. But it is an interesting question, and since it is based on fundamental maths concepts it seems to me (also) that it should.

First I note that the proposed free group functionality could also just as easily be implemented with a list of Either a 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

This is a nice definition, since we ensure that our free group is just a monoid with a little extra structure. It calls out that the free group is just a composition of the free monoid with another functor (What's the name? Not the Either a b bifunctor but a functor F a = L a | R a). We also ensure that the free group monad instance is consistent with the monad instance of the free monoid. That is, monads on the free group which operate on terms which happen to all be positive should behave like the monads over the free monoid, correct?

Ultimately however, if we ever want to reduce inverses we need an Eq a instance. We will need to work at the term level, pure type level information is not enough. This makes the type level distinction between the free monoid and free group unhelpful--as far as i can see. At least with out dependent typing.

For the sake of discussion on actual programming uses, I'll attempt (but fail) to provide a plausible use case.

Imagine a text editor which uses the "Ctrl" key to signal command sequences. Any key sequence pressed while holding "Ctrl" are modeled as negatives (negative cons (:-:)) in the FreeGroup. So the free group term 'a':+:'b':+:'b':-:'a':-:[] could be used to model emacs behavior which writes "ab", moves the cursor back a character, and then to the beginning of the line. Such a design is nice. We can easily embed commands and macros in a stream without some special reserved escape characters.

However, this example fails as a proper use case, since we would expect 'a':+:'b':+:'b':-:'a':-:[] to be the same program as [], which it isn't. Moreover, its easy enough to instead just wrap each list term in an Either as discussed above.

Free group monad

1 Answers