Merge pull request #82 from coot/coyoneda-docs

Coyoneda docs - lets add some math ;)

Author: paf31

src/Data/Coyoneda.purs

@@ -26,7 +26,19 @@ data CoyonedaF f a i = CoyonedaF (i -> a) (f i)
 -- | The `Coyoneda` `Functor`.
 -- |
 -- | `Coyoneda f` is a `Functor` for any type constructor `f`. In fact,
--- | it is the _free_ `Functor` for `f`.
+-- | it is the _free_ `Functor` for `f`, i.e. any natural transformation
+-- | `nat :: f ~> g`, can be factor through `liftCoyoneda`.  The natural
+-- | transformation from `Coyoneda f ~> g` is given by `lowerCoyoneda <<<
+-- | hoistCoyoneda nat`:
+-- | ```purescript
+-- | lowerCoyoneda <<< hoistCoyoneda nat <<< liftCoyoneda $ fi
+-- | = lowerCoyoneda (hoistCoyoneda nat (Coyoneda $ mkExists $ CoyonedaF id fi))    (by definition of liftCoyoneda)
+-- | = lowerCoyoneda (coyoneda id (nat fi))                                         (by definition of hoistCoyoneda)
+-- | = unCoyoneda map (coyoneda id (nat fi))                                        (by definition of lowerCoyoneda)
+-- | = unCoyoneda map (Coyoneda $ mkExists $ CoyonedaF  id (nat fi))                (by definition of coyoneda)
+-- | = map id (nat fi)                                                              (by definition of unCoyoneda)
+-- | = nat fi                                                                       (since g is a Functor)
+-- | ```
 newtype Coyoneda f a = Coyoneda (Exists (CoyonedaF f a))
 
 instance eqCoyoneda :: (Functor f, Eq1 f, Eq a) => Eq (Coyoneda f a) where
@@ -55,6 +67,12 @@ instance bindCoyoneda :: Bind f => Bind (Coyoneda f) where
     liftCoyoneda $
       runExists (\(CoyonedaF k fi) -> lowerCoyoneda <<< f <<< k =<< fi) e
 
+-- | When `f` is a Monad then it is a functor as well.  In this case
+-- | `liftCoyoneda` is not only a functor isomorphism but also a monad
+-- | isomorphism, i.e. the following law holds
+-- | ```purescript
+-- | liftCoyoneda fa >>= liftCoyoneda <<< g = liftCoyoneda $ fa >>= g
+-- | ```
 instance monadCoyoneda :: Monad f => Monad (Coyoneda f)
 
 instance monadTransCoyoneda :: MonadTrans Coyoneda where
@@ -64,6 +82,12 @@ instance extendCoyoneda :: Extend w => Extend (Coyoneda w) where
   extend f (Coyoneda e) =
     runExists (\(CoyonedaF k fi) -> liftCoyoneda $ f <<< coyoneda k <<= fi) e
 
+-- | As in the monad case: if `w` is a comonad, then it is a functor, thus
+-- | `liftCoyoneda` is an iso of functors, but moreover it is an iso of
+-- | comonads, i.e. the following law holds:
+-- | ```purescript
+-- | g <<= liftCoyoneda w = liftCoyoneda $ g <<< liftCoyoneda <<= w
+-- | ```
 instance comonadCoyoneda :: Comonad w => Comonad (Coyoneda w) where
   extract (Coyoneda e) = runExists (\(CoyonedaF k fi) -> k $ extract fi) e
 
@@ -78,6 +102,21 @@ unCoyoneda :: forall f g a. (forall b. (b -> a) -> f b -> g a) -> Coyoneda f a -
 unCoyoneda f (Coyoneda e) = runExists (\(CoyonedaF k fi) -> f k fi) e
 
 -- | Lift a value described by the type constructor `f` to `Coyoneda f`.
+-- |
+-- | Note that for any functor `f` `liftCoyoneda` has a right inverse
+-- | `lowerCoyoneda`:
+-- | ```purescript
+-- | liftCoyoneda <<< lowerCoyoneda $ (Coyoneda e)
+-- | = liftCoyoneda <<< unCoyoneda map $ (Coyoneda e)
+-- | = liftCoyonead (runExists (\(CoyonedaF k fi) -> map k fi) e)
+-- | = liftCoyonead (Coyoneda e)
+-- | = coyoneda id (Coyoneda e)
+-- | = Coyoneda e
+-- | ```
+-- | Moreover if `f` is a `Functor` then `liftCoyoneda` is an isomorphism of
+-- | functors with inverse `lowerCoyoneda`:  we already showed that
+-- | `lowerCoyoneda <<< hoistCoyoneda id = lowerCoyoneda` is its left inverse
+-- | whenever `f` is a functor.
 liftCoyoneda :: forall f. f ~> Coyoneda f
 liftCoyoneda = coyoneda id