Free group monad
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 xy) == 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
"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 aa,
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 ab 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.
上一篇: 功能性编程与面向对象编程
下一篇: 自由组monad