I have a deep thought on Monad and Comonad in haskell today. I feel it necessary to write down something to keep my mind active. Let’s first introduce the Monad.
A Monad is an abstraction of a series of function, such as a->a , a->s->a, a->s->(a,s),etc. We name them as Identity, Reader, State respectively. A Monad have two morphisms, an id and a bind which can glue any two functions in the group together. Let me explain why we should take care of this kind of abstraction. Generally speaking, programming is nothing but combining various of functions togther to work as people once intended. From some small and trustable functions , a bigger one grows. So the key to programming is combining. For any two function, one as f::a->b, one as g::b->c , we know from the math world there’s a combinator, little circle, who can give us an h::a->c, after being fed with f and g. We often wrote it down as h = f. g. In Haskell, as the same in math, all the function are pure, which means for some f::a->b, as long as f is fed with the same a , the same b is produced. In our practical programming , this does make f less usefull. There’s no global variable, thus we cannot return something varies with the it! There’s no pointer, thus we cannot change the input! These functions are too pure to be work in our unpure world. Of course, here I don’t means f is less powerfull, it actually can do as much as unpure functions, say in C++ or Java, can do. We can always pass the thing need to be changed to f as an argument and out as a result, then pass it to g. But this make our figure ache. After several really smart people had figure aches, they found that abstraction and liberate us from striking keyborad for trivial functions! Simply speeking, we introduce a indirect layer for the functions. We say the type of f now turns into a->m b, where m is a type constructor, and m b is totally a new type having some relation with b. For Identity ,Reader or State Monad, m is for any a (a), for any a (s->a), for any a (s-> (a,s)) respectively. All the problem we have to face now is how to define the little circle to compose these functions of the type a->m b. Still take f::a->m b and g::b->m c as example. let h = f .’ g
(def) h = f .’ g = a->(f a >>= b-> g b)
Here, we introduce the >>= combinator. It should be easy to understand h, which take an a of the type a, feed f with this a. Noting that (b->g b) equals to g, we use >>= to combine (f a) and g, where the underlying meaning of >>= should be extracting a b from f a and feed g with b, producing a result of m c. OK, we finally have h of a->m c. If we look into the type of the >>=, it is exactly m a->(a->m b)->m b. OK, here is another question, what kind of such m can make out function of a->m b composable? The answer is that if m is in the monad category, we can find such a >>= and a identity function to make things composable.
Now it is the time to introduce Comonad, Comonad is the dual of monad in category. I don’t know category at all, so I won’t explain anything about category. What I’ll do here is to dig something interesting with a comonad. Recalling that monad means a->m b, comonad means w a->b, where w is also a type constructor as m.
What cofused me today is wether (t->a)->b is comonadic. (t->a) can stand for a variable which varies to t, which is the core of FRP. Sigfpe once mention that FRP could be comonadic, using arrow could be over-abstracted. So I made myself stuck into the comonadic world. But finally what I understand is that (t->a)->b is not comonadic. Time-varied variable is (t->a), but functions based on them should be of (t->a)->(t->b), for that we can never extract a b from (t->a). I was deadly disappointed! The second thing confused me is the cobind, the dual of bind. Since i have no experence in category, I make some mistakes in understanding their types.
(def) cobind :: (w a->b)->w a->w b
I doubted its correctness, and thought it should be something like cobind’ :: a->(w a->b)->b.
(wrong def) f .’ g = a->(f a>>=b -> g b) , the same as the previous one.
But in fact, it’s wrong.
(right def) r .’ g = a->(g (cobind f a)
Now I list two comonad. The explanation will be given in the future post. I’m too sleep to write anything.
1. [a]->b is comonadic.
2. Tree a->b is comonadic.
3. Ptr a->b is comonadic.