Sunday, July 01, 2012

From Monads to Monoids in a small category


(Added 06/09/12: clarification about the nature of ' m a' from the point of view of C.Theory)

Let's start with the definition of a small category with a morphism defined by 'm' between set of objects 'a' and 'm b'. The simplest category definition would be:

{-# LANGUAGE FlexibleInstances #-}
import Data.Monoid
import Control.Monad

class Category  m a b where
 morph:: a ->  m b


Here 'm b'  is the codomain of the morphism which depends on the category instance. More on this at the end of the post. .

The other two requisites for a category according with this are an identity operation and associativity of the morphism. The first is guaranteed in Haskell by the polymorphic function 'id'.


id :: a -> a
id x = x

Lett´s modify the signature of 'id' slightly to match the Category definition as such:

return :: a -> m a

The second condition, associativity, is guaranteed by the nature of the forward chaining of operations in any programming language. (if not where that way, it would be impossible the denotational semantics of imperative languages in terms of monads, I guess)



The definition of functor According to this :



Let C and D be categories. A functor F from C to D is a mapping that:

  • associates to each object  an object ,
  • associates to each morphism  a morphism


So the morphism (a -> m b) may meet the first condition. This morphism  maps elements from the set ‘a’ to elements in the set ‘m b’. The second condition is the one defined in the Haskell instance of functor:


instance Functor a where

 fmap :: (a -> b) -> (m a ->  m b)


When a and b are the same, then we have a functor.which maps elements in ‘a’ to elements in ‘m a’  (a -> m a). But are 'a' and 'm a' the same? It seems that it is not the case, but I will talk about it later.

The functor category has functors as elements and natural transformations as morphisms, Additionally, the functors have a double nature as maps between points in ‘a’ (a -> ma) and as maps between morphisms (fmap) .  But a monoid is defined over elements of the set, and a monad works with morphisms (a -> m b), so we are interested on the set of elements with signature  (a -> m a) , to describe the Monoid instance for these elements.


If we try to construct the Monoid instance for any morphisms (a -> m a) . This instance demands that 'm' is a monad, that is, that the morphisms of m must  compose according with the monad laws:


instance Monad m => Monoid  (a -> m a) where
   mappend f g= \x -> do
                          y <-  f x
                          g y
   mempty=   \x -> return x

The definition of mappend is equivalent to the Kleisli operator in a Monad

(>=>) :: (a -> m b) -> (b -> m c) -> (a -> m c)
f >=> g = \x -> f x >>= g


In this case, a b and c are the same sets:

The Monoid instance e of morphisms that meet the Monad laws can be written as:

instance Monad m => Monoid  (a -> m a) where
   mappend = (>=>)
   mempty  = return

This typechecks in Haskell. But does this set (a -> m a) of maps between elements from the endofunctors have the necessary  reflexive and associative properties for being a Monoid? If you compare (1) the asociativite and identity laws of a Monoid, when applied to the morphisms between (a -> m a)  objects,  with (2) the monad laws you will conclude that (1) and (2)  are identical, and thus only the monadic morohisms form a Monoid,

The Monoid is defined within the subset of morphisms (a -> m a) which are part of the functor category, not with the set 'a' as such.  The return operation in a Monad correspond with the identity morphism in the set of such  morphisms. 



While in the IO monad, the morphisms (a -> IO a) refer to the same set ‘a’ in the domain and the codomain, (a -> Maybe a)  has one additional element (Nothing) which is terminal. 

In the case of List monad, the morphisms of the monad (a -> [a]) 'm a' is [a]. It sems quite different at first sight, But a list, as seen from the point of view of the list category, is a list of alternative arrows in the set 'a' (see the previous post).

for example the expression

f :: String -> [String]
f x= take 5 $ repeat x

can be considered as a endomorphism in the set of Strings that has five arrows. Then 'f' can be considered as a morphisn from 'a' to the set 'a' plus the empty list element (which is terminal)

'What is 'm a’ ?. Seen from the point of view of category theory, it is 'a' plus some terminal element(s).

What about the generalization for the morphisms of any ( a -> m b) being a and b of any kind? The Monoid instance can be extended to a larger class of morphisms between any Typeabe objects by assuming a of type Dynamic. So implicitly, to any a -> m b as long as a and b are Typeable:


instance Monad m => Monoid  (Dynamic -> m Dynamic) where
   mappend = (>=>)
   mempty  = return
If any 'a' with morphisms (a -> m a) is a Category, Then, I guess, the set of Typeable objects with the morphisms (Dynamic -> m Dynamic) is a Category

Even it can be extended to the endofunctors of the set of elements of any type:

data AllTypes = forall a . AllTypes a


instance Monad m => Monoid  (AllTypes-> m AllTypes) where
   mappend = (>=>)
   mempty  = return


Which implicity is a Monoid instance for any (a -> m b)

Am I wrong?. Did I miss something?