diff --git a/Test.hs b/Test.hs
--- a/Test.hs
+++ b/Test.hs
@@ -1,4 +1,5 @@
 module Test where
 
 import Generics.Pointless.Examples.Examples
-import Generics.Pointless.Examples.GHood
+import Generics.Pointless.Examples.Observe
+import Debug.Observe
diff --git a/pointless-haskell.cabal b/pointless-haskell.cabal
--- a/pointless-haskell.cabal
+++ b/pointless-haskell.cabal
@@ -1,5 +1,5 @@
 Name:            pointless-haskell
-Version:         0.0.1
+Version:         0.0.2
 License:         BSD3
 License-file:    LICENSE
 Author:          Alcino Cunha <alcino@di.uminho.pt>, Hugo Pacheco <hpacheco@di.uminho.pt>
@@ -16,18 +16,14 @@
 extra-source-files: README, Test.hs
 
 Build-type: Simple
-Cabal-Version:  >=1.2
+Cabal-Version:  >= 1.2.3
 
 Flag splitBase
   Description:          Choose the new smaller, split-up base package.
 
 Library
   Hs-Source-Dirs: src
-  Build-Depends:        base, GHood, haskell98, process
-  if flag(splitBase)
-    Build-Depends:      base >= 3, array >= 0.1, pretty >= 1.0
-  else
-    Build-Depends:      base < 3
+  Build-Depends:        base >= 3 && < 5, GHood, haskell98, process
   exposed-modules:
         Generics.Pointless.Combinators
         Generics.Pointless.Functors,
@@ -35,6 +31,10 @@
         Generics.Pointless.Observe.Functors,
         Generics.Pointless.Observe.RecursionPatterns,
         Generics.Pointless.Examples.Examples,
-        Generics.Pointless.Examples.Observe
+        Generics.Pointless.Examples.Observe,
+        Generics.Pointless.Fctrable,
+        Generics.Pointless.MonadCombinators,
+        Generics.Pointless.Bifunctors,
+        Generics.Pointless.Bifctrable
 
-  extensions: TypeFamilies, TypeOperators, ScopedTypeVariables, UndecidableInstances, FlexibleInstances, FlexibleContexts, EmptyDataDecls
+  extensions: TypeFamilies, TypeOperators, ScopedTypeVariables, UndecidableInstances, FlexibleInstances, FlexibleContexts, EmptyDataDecls, GADTs
diff --git a/src/Generics/Pointless/Bifctrable.hs b/src/Generics/Pointless/Bifctrable.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Pointless/Bifctrable.hs
@@ -0,0 +1,54 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Pointless.Bifctrable
+-- Copyright   :  (c) 2009 University of Minho
+-- License     :  BSD3
+--
+-- Maintainer  :  hpacheco@di.uminho.pt
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Pointless Haskell:
+-- point-free programming with recursion patterns as hylomorphisms
+-- 
+-- This module defines a class of representable bifunctors.
+--
+-----------------------------------------------------------------------------
+
+module Generics.Pointless.Bifctrable where
+
+import Prelude hiding (Functor(..),fmap)
+import Generics.Pointless.Bifunctors
+import Generics.Pointless.Combinators
+
+-- | Functor GADT for polytypic recursive bifunctions.
+-- At the moment it does not rely on a @Typeable@ instance for constants.
+data Bifctr (f :: * -> * -> *) where
+    BI :: Bifctr BId
+    BK :: Bifctr (BConst c)
+    BP :: Bifctr BPar
+    (:*!|) :: (Bifunctor f,Bifunctor g) => Bifctr f -> Bifctr g -> Bifctr (f :*| g)
+    (:+!|) :: (Bifunctor f,Bifunctor g) => Bifctr f -> Bifctr g -> Bifctr (f :+| g)
+    (:@!|) :: (Bifunctor f,Bifunctor g) => Bifctr f -> Bifctr g -> Bifctr (f :@| g)
+
+-- | Class of representable bifunctors.
+class (Bifunctor f) => Bifctrable (f :: * -> * -> *) where
+    bctr :: Bifctr f
+instance Bifctrable BId where
+    bctr = BI
+instance Bifctrable (BConst c) where
+    bctr = BK
+instance Bifctrable BPar where
+    bctr = BP
+instance (Bifunctor f,Bifctrable f,Bifunctor g,Bifctrable g) => Bifctrable (f :*| g) where
+    bctr = (:*!|) bctr bctr
+instance (Bifunctor f,Bifctrable f,Bifunctor g,Bifctrable g) => Bifctrable (f :+| g) where
+    bctr = (:+!|) bctr bctr
+
+-- | The fixpoint of a representable bifunctor.
+fixB :: Bifctr f -> BFix f
+fixB (_::Bifctr f) = (_L :: BFix f)
+
+-- | The representation of the fixpoint of a representable functor.
+fctrB :: Bifctrable f => BFix f -> Bifctr f
+fctrB (_::BFix f) = bctr :: Bifctr f
diff --git a/src/Generics/Pointless/Bifunctors.hs b/src/Generics/Pointless/Bifunctors.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Pointless/Bifunctors.hs
@@ -0,0 +1,145 @@
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Pointless.Bifunctors
+-- Copyright   :  (c) 2009 University of Minho
+-- License     :  BSD3
+--
+-- Maintainer  :  hpacheco@di.uminho.pt
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Pointless Haskell:
+-- point-free programming with recursion patterns as hylomorphisms
+-- 
+-- This module defines polymorphic data types as fixed points of bifunctor.
+-- Pointless Haskell works on a view of data types as fixed points of functors, in the same style as the PolyP (<http://www.cse.chalmers.se/~patrikj/poly/polyp/>) library.
+-- Instead of using an explicit fixpoint operator, a type function is used to relate the data types with their equivalent functor representations.
+--
+-----------------------------------------------------------------------------
+
+module Generics.Pointless.Bifunctors where
+
+import Generics.Pointless.Combinators
+import Generics.Pointless.Functors
+
+-- * Bifunctors
+
+newtype BId a x = BId {unBId :: x}
+newtype BConst t a x = BConst {unBConst :: t}
+newtype BPar a x = Par {unPar :: a}
+infixr 5 :+|
+data (g :+| h) a x = BInl (g a x) | BInr (h a x)
+infixr 6 :*|
+data (g :*| h) a x = BProd (g a x) (h a x)
+infixr 9 :@|
+newtype (g :@| h) a x = BComp {unBComp :: g a (h a x)}
+
+newtype BFix f = BFix { unBFix :: f (BFix f) (BFix f) }
+
+type family BF (f :: * -> *) :: * -> * -> *
+
+type family BRep (f :: * -> * -> *) a :: (* -> *)
+
+-- | Representation of bifunctors with the @Rep@ functor representation class.
+type instance Rep (BId a) x = x
+type instance Rep ((BConst t) a) x = t
+type instance Rep (BPar a) x = a
+type instance Rep ((g :+| h) a) x = Rep (g a) x `Either` Rep (h a) x
+type instance Rep ((g :*| h) a) x = (Rep (g a) x,Rep (h a) x)
+type instance Rep ((g :@| h) a) x = Rep (g a) (Rep (h a) x)
+
+-- | Representation of bifunctors with the @BRep@ bifunctor representation class.
+type instance BRep BId a = Id
+type instance BRep (BConst t) a = Const t
+type instance BRep BPar a = Const a
+type instance BRep (g :+| h) a = BRep g a :+: BRep h a
+type instance BRep (g :*| h) a = BRep g a  :*: BRep h a
+type instance BRep (g :@| h) a = BRep g a :@: BRep h a
+
+class Bifunctor (f :: * -> * -> *) where
+   bmap :: BFix f -> (a -> b) -> (x -> y) -> Rep (BRep f a) x -> Rep (BRep f b) y
+
+instance Bifunctor BId where
+   bmap _ p f = f
+instance Bifunctor (BConst t) where
+   bmap _ p f = id
+instance Bifunctor BPar where
+   bmap _ p f = p
+instance (Bifunctor g,Bifunctor h) => Bifunctor (g :+| h) where
+   bmap _ p f (Left x) = Left (bmap (_L :: BFix g) p f x)
+   bmap _ p f (Right x) = Right (bmap (_L :: BFix h) p f x)
+instance (Bifunctor g,Bifunctor h) => Bifunctor (g :*| h) where
+   bmap _ p f (x,y) = (bmap (_L :: BFix g) p f x,bmap (_L :: BFix h) p f y)
+instance (Bifunctor g,Bifunctor h) => Bifunctor (g :@| h) where
+   bmap _ p f x = bmap (_L :: BFix g) p (bmap (_L :: BFix h) p f) x
+
+type B d a x = Rep (BRep (BF d) a) x
+
+class Bimu d where
+    binn :: B d a (d a) -> d a
+    bout :: d a -> B d a (d a)
+
+pbmap :: Bifunctor (BF d) => d a -> (a -> b) -> (x -> y) -> B d a x -> B d b y
+pbmap (_::d a) p f = bmap (_L :: BFix (BF d)) p f
+
+-- * Fixpoint combinators
+
+data BI x = FixBId
+
+type instance BF BI = BId
+
+instance Bimu BI where
+   binn = id
+   bout = id
+
+data BK a x = FixBConst {unFixBConst :: a}
+
+type instance BF (BK a) = BConst a
+
+instance Bimu (BK a) where
+   binn = FixBConst
+   bout = unFixBConst
+
+infixr 5 :+!|
+data ((a :: * -> *) :+!| (b :: * -> *)) x = FixBSum {unFixBSum :: B (a :+!| b) x ((a :+!| b) x)}
+
+type instance BF (a :+!| b) = BF a :+| BF b
+
+instance Bimu (a :+!| b) where
+   binn = FixBSum
+   bout = unFixBSum
+
+infixr 6 :*!|
+data ((a :: * -> *) :*!| (b :: * -> *)) x = FixBProd {unFixBProd :: B (a :*!| b) x ((a :*!| b) x)}
+
+type instance BF (a :*!| b) = BF a :*| BF b
+
+instance Bimu (a :*!| b) where
+   binn = FixBProd
+   bout = unFixBProd
+
+infixr 9 :@!|
+data ((a :: * -> *) :@!| (b :: * -> *)) x = FixBComp {unFixBComp :: B (a :@!| b) x ((a :@!| b) x)}
+
+type instance BF (a :@!| b) = BF a :@| BF b
+
+instance Bimu (a :@!| b) where
+   binn = FixBComp
+   bout = unFixBComp
+
+-- * Default definitions for commonly used data types
+
+--instance (Bimu d, Rep (PF (d a)) (d a) ~ BRep (BF d) a (d a)) => Mu (d a) where
+--    inn = binn
+--    out = bout
+
+-- ** Lists
+
+type instance BF [] = BConst One :+| BPar :*| BId
+
+instance Bimu [] where
+    binn (Left _) = []
+    binn (Right (x,xs)) = x:xs
+    bout [] = Left _L
+    bout (x:xs) = Right (x,xs)
diff --git a/src/Generics/Pointless/Combinators.hs b/src/Generics/Pointless/Combinators.hs
--- a/src/Generics/Pointless/Combinators.hs
+++ b/src/Generics/Pointless/Combinators.hs
@@ -43,7 +43,7 @@
 
 -- | Converts elements into points.
 pnt :: a -> One -> a
-pnt x = \_ -> x
+pnt = const
 
 -- * Products
 
@@ -87,6 +87,14 @@
 -- | The application combinator.
 app :: (a -> b, a) -> b
 app (f,x) = f x
+
+-- | The left exponentiation combinator.
+lexp :: (a -> b) -> (b -> c) -> (a -> c)
+lexp f = curry (app . (id >< f))
+
+-- | The right exponentiation combinator.
+rexp :: (b -> c) -> (a -> b) -> (a -> c)
+rexp f = curry (f . app)
 
 infix 0 !
 -- | The infix combinator for a constant point.
diff --git a/src/Generics/Pointless/Examples/Examples.hs b/src/Generics/Pointless/Examples/Examples.hs
--- a/src/Generics/Pointless/Examples/Examples.hs
+++ b/src/Generics/Pointless/Examples/Examples.hs
@@ -39,7 +39,7 @@
 addAnaPW = ana (_L::Int) h 
    where h (0,0) = Left _L 
          h (n,0) = Right (n-1,0) 
-         h (0,n) = Right (0,n-1) 
+         h (0,m) = Right (0,m-1) 
          h (n,m) = Right (n,m-1)
 
 -- | Defition of algebraic addition as an anamorphism.
@@ -59,10 +59,16 @@
 
 -- | Definition of algebraic addition as an accumulation.
 addAccum :: (Int,Int) -> Int
-addAccum = accum (_L::Int) t f
+addAccum = accum (_L::Int) f t
    where t = (fst -|- id >< succ) . distl
          f = (snd \/ fst) . distl
 
+addApoPW :: (Int,Int) -> Int
+addApoPW = apo (_L :: Int) h
+    where h (0,0) = Left _L
+          h (n,0) = Right $ Right $ n-1
+          h (n,m) = Right $ Left (n,m-1)
+
 -- | Definition of algebraic addition as an apomorphism.
 addApo :: (Int,Int) -> Int
 addApo = apo (_L::Int) h
@@ -174,7 +180,7 @@
 -- | Definition of the binary partitioning of a number as an hylomorphism.
 bp :: Int -> Int
 bp 0 = 1
-bp n = if (odd n) then bp (n-1) else bp (n-1) + bp (div n 2)
+bp n = if odd n then bp (n-1) else bp (n-1) + bp (div n 2)
 
 -- | The fixpoint of the functor representing trees with maximal branching factor of two.
 type BTree = K One :+!: (I :+!: (I :*!: I))
@@ -197,7 +203,7 @@
          oi = uncurry pi . ((pred . (`div` 2)) >< id)
          h = (id -|- succ /\ id) . out
          pi 0 x = x 
-         pi k x = case (outr x) of
+         pi k x = case outr x of
             Right (_,y) -> pi (pred k) y
 
 -- ** Average
@@ -217,7 +223,7 @@
 
 -- | Pre-defined wrapping of an element into a list.
 wrap :: a -> [a]
-wrap x = x:[]
+wrap = (:[])
 
 -- | Definition of wrapping in the point-free style.
 wrapPF :: a -> [a]
@@ -236,7 +242,7 @@
 
 -- | Definition of the tail of a list as an anamorphism.
 tailCata :: [a] -> [a]
-tailCata = fst . (cata (_L::[a]) (f /\ inn . (id -|- id >< snd)))
+tailCata = fst . cata (_L::[a]) (f /\ inn . (id -|- id >< snd))
    where f = ([]!) \/ snd . snd
 
 -- | Definition of the tail of a list as a paramorphism.
@@ -272,7 +278,7 @@
 
 -- | Definition of list length as a catamorphism.
 lengthCata :: [a] -> Int
-lengthCata = cata (_L) f
+lengthCata = cata _L f
     where f = zero \/ succ . snd
 
 -- ** Filtering
@@ -300,7 +306,7 @@
 
 -- | Generation of a downwards list as an anamorphism.
 downtoAna :: Int -> [Int]
-downtoAna = ana (_L) f
+downtoAna = ana _L f
    where f = (bang -|- (id /\ pred)) . ((==0) ?)
 
 -- | Ordered list insertion as an apomorphism.
@@ -368,7 +374,7 @@
 -- | Definition of list mapping as a catamorphism.
 mapCata :: [a] -> (a -> b) -> [b]
 mapCata = cata (_L::[a]) f
-   where f = (([]!)!) \/ (curry (cons . (app . swap >< app) . ((fst >< id) /\ (snd >< id))))
+   where f = (([]!)!) \/ curry (cons . (app . swap >< app) . ((fst >< id) /\ (snd >< id)))
 
 -- | Definition of list reversion as a catamorphism.
 reverseAna :: [a] -> [a]
@@ -439,7 +445,7 @@
 -- | Definition of the subsequences of a list as a catamorphism.
 subsequences :: Eq a => [a] -> [[a]]
 subsequences = cata (_L::[a]) f
-   where f = cons . (nil /\ nil) \/ (uncurry union) . (snd /\ subsOp . swap . (wrap >< id))
+   where f = cons . (nil /\ nil) \/ uncurry union . (snd /\ subsOp . swap . (wrap >< id))
          subsOp (r,l) = map (l++) r
 
 -- ** Concatenation
@@ -475,7 +481,7 @@
 -- | Sorted concatenation of two lists as an hylomorphism.
 merge :: (Ord a) => ([a],[a]) -> [a]
 merge = hylo (_L::NeList [a] a) f g
-   where g = ((id \/ id) -|- ((id \/ id) . (assocr -|- (assocr . (swap >< id) . assocl)) . (id >< cons -|- cons >< id) . (((uncurry (<)) . (fst >< fst))?) )) . coassocl . (snd -|- (((cons . fst) -|- id) . distr . (id >< out))) . distl . (out >< id)
+   where g = ((id \/ id) -|- ((id \/ id) . (assocr -|- (assocr . (swap >< id) . assocl)) . (id >< cons -|- cons >< id) . ((uncurry (<) . (fst >< fst))?) )) . coassocl . (snd -|- (((cons . fst) -|- id) . distr . (id >< out))) . distl . (out >< id)
          f = id \/ cons
 
 -- ** Summation
@@ -494,7 +500,7 @@
 
 -- | Definition of integer multiplication as a catamorphism.
 multCata :: [Int] -> Int
-multCata = cata (_L) f
+multCata = cata _L f
 	    where f = (1!) \/ prod
 
 -- ** Predicates
@@ -502,7 +508,7 @@
 -- Test if a list is sorted as a paramorphism.
 sorted :: (Ord a) => [a] -> Bool
 sorted = para (_L::[a]) f
-    where f = true \/ (uncurry (&&)) . ((true . bang \/ (uncurry (<=)) . (id >< head)) . ((null . snd)?) >< id) . assocl . (id >< swap)
+    where f = true \/ uncurry (&&) . ((true . bang \/ uncurry (<=) . (id >< head)) . ((null . snd)?) >< id) . assocl . (id >< swap)
 
 -- ** Edit distance
 
@@ -534,7 +540,7 @@
          g' ((a,b),(x1,(x2,x3))) = min m1 (min m2 m3)
             where m1 = succ x1
                   m2 = succ x2
-                  m3 = add (x3,if (a==b) then 0 else 1)
+                  m3 = add (x3,if a==b then 0 else 1)
          h ([],bs) = Left bs
          h (as,[]) = Left as
          h (a:as,b:bs) = Right ((a,b),((as,b:bs),((a:as,bs),(as,bs))))
@@ -547,7 +553,7 @@
          g' ((a,b),(x1,(x2,x3))) = min m1 (min m2 m3)
             where m1 = succ x1
                   m2 = succ x2
-                  m3 = add (x3,if (a==b) then 0 else 1)
+                  m3 = add (x3,if a==b then 0 else 1)
          o :: Int -> F (EditDistL a) (Histo (EditDistL a) Int) -> F (EditDist a) Int
          o n ((as,bs),Left _) = Left []
          o n (([],bs),Right x) = Left bs
@@ -559,7 +565,7 @@
          h cs (a:as,bs) = ((a:as,bs),Right (as,bs))
          pi :: Int -> Histo (EditDistL a) Int -> Histo (EditDistL a) Int
          pi 0 x = x
-         pi k x = case (outr x) of
+         pi k x = case outr x of
             (_,Right y) -> pi (pred k) y
          j = outl
 
@@ -680,7 +686,7 @@
 -- | Calculate the height of a leaf tree as a catamorphism.
 height :: LTree a -> Int
 height = cata (_L::LTree a) f
-    where f = (0!) \/ (succ . (uncurry max))
+    where f = (0!) \/ (succ . uncurry max)
 
 -- * Rose Trees
 
diff --git a/src/Generics/Pointless/Fctrable.hs b/src/Generics/Pointless/Fctrable.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Pointless/Fctrable.hs
@@ -0,0 +1,53 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Pointless.Fctrable
+-- Copyright   :  (c) 2009 University of Minho
+-- License     :  BSD3
+--
+-- Maintainer  :  hpacheco@di.uminho.pt
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Pointless Haskell:
+-- point-free programming with recursion patterns as hylomorphisms
+-- 
+-- This module defines a class of representable functors.
+--
+-----------------------------------------------------------------------------
+
+module Generics.Pointless.Fctrable where
+
+import Prelude hiding (Functor(..),fmap)
+import Generics.Pointless.Functors
+import Generics.Pointless.Combinators
+
+-- | Functor GADT for polytypic recursive functions.
+-- At the moment it does not rely on a @Typeable@ instance for constants.
+data Fctr (f :: * -> *) where
+    I :: Fctr Id
+    K :: Fctr (Const c)
+    (:*!:) :: (Functor f,Functor g) => Fctr f -> Fctr g -> Fctr (f :*: g)
+    (:+!:) :: (Functor f,Functor g) => Fctr f -> Fctr g -> Fctr (f :+: g)
+    (:@!:) :: (Functor f,Functor g) => Fctr f -> Fctr g -> Fctr (f :@: g)
+
+-- | Class of representable functors.
+class (Functor f) => Fctrable (f :: * -> *) where
+    fctr :: Fctr f
+instance Fctrable Id where
+    fctr = I
+instance Fctrable (Const c) where
+    fctr = K
+instance (Functor f,Fctrable f,Functor g,Fctrable g) => Fctrable (f :*: g) where
+    fctr = (:*!:) fctr fctr
+instance (Functor f,Fctrable f,Functor g,Fctrable g) => Fctrable (f :+: g) where
+    fctr = (:+!:) fctr fctr
+instance (Functor f,Fctrable f,Functor g,Fctrable g) => Fctrable (f :@: g) where
+    fctr = (:@!:) fctr fctr
+
+-- | The fixpoint of a representable functor.
+fixF :: Fctr f -> Fix f
+fixF (_::Fctr f) = (_L :: Fix f)
+
+-- | The representation of the fixpoint of a representable functor.
+fctrF :: Fctrable f => Fix f -> Fctr f
+fctrF (_::Fix f) = fctr :: Fctr f
diff --git a/src/Generics/Pointless/Functors.hs b/src/Generics/Pointless/Functors.hs
--- a/src/Generics/Pointless/Functors.hs
+++ b/src/Generics/Pointless/Functors.hs
@@ -20,8 +20,8 @@
 
 module Generics.Pointless.Functors where
 
-import Generics.Pointless.Combinators
 import Prelude hiding (Functor(..))
+import Generics.Pointless.Combinators
 
 -- * Functors
 
@@ -31,7 +31,7 @@
 newtype Id x = Id {unId :: x}
 
 -- | Constant functor.
-newtype Const t x = Const {unConst :: t}
+newtype Const t x = Cons {unCons :: t}
 
 -- | Sum of functors.
 infixr 5 :+:
@@ -39,14 +39,14 @@
 
 -- | Product of functors.
 infixr 6 :*:
-data (g :*: h) x = g x :*: h x
+data (g :*: h) x = Prod (g x) (h x)
 
 -- | Composition of functors.
 infixr 9 :@:
 newtype (g :@: h) x = Comp {unComp :: g (h x)}
 
 -- | Explicit fixpoint operator.
-newtype Fix f = Fix { -- | The unfolding of the fixpoint of a functor is a the functor applied to its fixpoint.
+newtype Fix f = Fix { -- | The unfolding of the fixpoint of a functor is the functor applied to its fixpoint.
 	                   --
 	                   -- 'unFix' is specialized with the application of 'Rep' in order to subsume functor application
                          unFix :: Rep f (Fix f)
@@ -117,7 +117,7 @@
 -- ^ The composition functor applies in the nesting of the mapping function to the nested functor applications
 
 instance Functor [] where
-   fmap _ f l = map f l
+   fmap _ = map
 -- ^ The list functor maps the specific 'map' function over lists of types
 
 -- | Short alias to express the structurally equivalent sum of products for some data type
@@ -205,7 +205,19 @@
 cons :: (a,[a]) -> [a]
 cons = inn . inr
 
--- ** Int
+-- ** Natural Numbers
+
+data Nat = Zero | Succ Nat deriving (Eq,Show)
+
+type instance PF Nat = Const One :+: Id
+
+instance Mu Nat where
+    inn (Left _) = Zero
+    inn (Right n) = Succ n
+    out Zero = Left _L
+    out (Succ n) = Right n
+
+-- ** Int (positive only)
 
 type instance PF Int = Const One :+: Id
 
diff --git a/src/Generics/Pointless/MonadCombinators.hs b/src/Generics/Pointless/MonadCombinators.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Pointless/MonadCombinators.hs
@@ -0,0 +1,64 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Pointless.MonadCombinators
+-- Copyright   :  (c) 2009 University of Minho
+-- License     :  BSD3
+--
+-- Maintainer  :  hpacheco@di.uminho.pt
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Pointless Haskell:
+-- point-free programming with recursion patterns as hylomorphisms
+-- 
+-- This module lifts many standard combinators used for point-free programming to combinators over monads.
+--
+-----------------------------------------------------------------------------
+
+module Generics.Pointless.MonadCombinators where
+
+import Generics.Pointless.Combinators
+import Control.Monad
+
+-- | The left-to-right monadic binding combinator.
+infixl 1 <<=
+(<<=) :: Monad m => (a -> m b) -> m a -> m b
+(<<=) f m = m >>= f
+
+-- | Higher-order monadic binding.
+bind :: Monad m => (a -> m b,m a) -> m b
+bind (f,m) = f <<= m
+
+-- | The monadic left exponentiation combinator.
+mlexp :: Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
+mlexp f = curry (bind . (id >< f))
+
+-- | The monadic right exponentiation combinator.
+mrexp :: Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)
+mrexp f = curry ((f <<=) .  app)
+
+-- | The monadic sum combinator.
+infix 5 -||-
+(-||-) :: Monad m => (a -> m b) -> (c -> m d) -> (Either a c -> m (Either b d))
+(-||-) f g = (return . inl <=< f) \/ (return . inr <=< g)
+
+-- | The strength combinator for strong monads.
+-- In Haskell, every monad is a strong monad: <http://comonad. com/reader/2008/deriving-strength-from-laziness/>.
+mstrength :: Monad m => (b,m a) -> m (b,a)
+mstrength = uncurry (<<=) . (comp . (const return /\ dist) >< id)
+    where dist = curry id
+
+-- | The monadic fusion combinator.
+-- Performs left-to-right distribution of a strong monad over a product.
+mfuse :: Monad m => (m a,m b) -> m (a,b)
+mfuse = uncurry (<<=) . (curry (mstrength . swap) >< id) . swap
+
+-- | The monadic split combinator.
+infix 6  /|\
+(/|\) :: Monad m => (a -> m b) -> (a -> m c) -> a -> m (b,c)
+(/|\) f g = mfuse . (f /\ g)
+
+-- | The monadic product combinator.
+infix 7  >|<
+(>|<) :: Monad m => (a -> m c) -> (b -> m d) -> (a,b) -> m (c,d)
+f >|< g = f . fst /|\ g . snd
diff --git a/src/Generics/Pointless/Observe/Functors.hs b/src/Generics/Pointless/Observe/Functors.hs
--- a/src/Generics/Pointless/Observe/Functors.hs
+++ b/src/Generics/Pointless/Observe/Functors.hs
@@ -23,11 +23,12 @@
 import Debug.Observe
 import Data.Typeable
 import Prelude hiding (Functor(..))
+import Control.Monad hiding (Functor(..))
 
 -- * Definition of generic observations
 
 instance Typeable One where
-   typeOf _ = (mkTyCon "One") `mkTyConApp` []
+   typeOf _ = mkTyCon "One" `mkTyConApp` []
 
 -- | Class for mapping observations over functor representations.
 class FunctorO f where
@@ -41,20 +42,20 @@
 instance FunctorO Id where
    functorOf _ = "Id"
    watch _ _ _ = ""
-   fmapO _ f x = f x
+   fmapO _ f = f
 
 instance (Typeable a,Observable a) => FunctorO (Const a) where
    functorOf _ = "Const " ++ show (typeOf (_L::a))
    watch _ _ _ = ""
-   fmapO _ f x = thunk x
+   fmapO _ f = thunk
 
 
 instance (FunctorO f, FunctorO g) => FunctorO (f :+: g) where
    functorOf _ = "(" ++ functorOf (_L::Fix f) ++ ":+:" ++ functorOf (_L::Fix g) ++ ")"
    watch _ _ (Left _) = "Left"
    watch _ _ (Right _) = "Right"
-   fmapO _ f (Left x) = fmapO (_L::Fix f) f x >>= return . Left
-   fmapO _ f (Right x) = fmapO (_L::Fix g) f x >>= return . Right
+   fmapO _ f (Left x) = liftM Left (fmapO (_L::Fix f) f x)
+   fmapO _ f (Right x) = liftM Right (fmapO (_L::Fix g) f x)
 
 instance (FunctorO f, FunctorO g) => FunctorO (f :*: g) where
    functorOf _ = "(" ++ functorOf (_L::Fix f) ++ ":*:" ++ functorOf (_L::Fix g) ++ ")"
@@ -65,17 +66,12 @@
 
 instance (FunctorO g, FunctorO h) => FunctorO (g :@: h) where
    functorOf _ = "(" ++ functorOf (_L::Fix g) ++ ":@:" ++ functorOf (_L::Fix h) ++ ")"
-   watch _ (x::x) a = watch (_L::Fix g) (_L::Rep h x) a
-   fmapO _ f x = fmapO (_L::Fix g) (fmapO (_L::Fix h) f) x
-
---w :: Fix (g:@:h) -> x -> Rep (g:@:h) x -> String
---w (_::Fix (g:@:h)) (r::x) (x) = watch (_L::Fix g) (aux x) x
---   where aux :: Rep (g:@:h) x -> Rep h x
---         aux _ = _L
+   watch _ (x::x) = watch (_L::Fix g) (_L::Rep h x)
+   fmapO _ = fmapO (_L::Fix g) . fmapO (_L::Fix h)
 
 -- | Polytypic mapping of observations.
 omap :: FunctorO (PF a) => a -> (x -> ObserverM y) -> F a x -> ObserverM (F a y)
-omap (_::a) f = fmapO (_L::Fix (PF a)) f
+omap (_::a) = fmapO (_L::Fix (PF a))
 
 instance Observable One where
    observer = observeBase
@@ -84,19 +80,19 @@
    observer FixId = send "" (fmapO (_L :: Fix Id) thunk FixId)
 
 instance (Typeable a,Observable a) => Observable (K a) where
-   observer (FixConst a) = send "" (fmapO (_L::Fix (Const a)) thk a >>= return . FixConst)
+   observer (FixConst a) = send "" (liftM FixConst (fmapO (_L::Fix (Const a)) thk a))
       where thk = thunk :: a -> ObserverM a
 
 instance (FunctorO (PF a),FunctorO (PF b)) => Observable (a :+!: b) where
-   observer (FixSum f) = send "" (fmapO (_L::Fix (PF a :+: PF b)) thk f >>= return . FixSum)
+   observer (FixSum f) = send "" (liftM FixSum (fmapO (_L::Fix (PF a :+: PF b)) thk f))
       where thk = thunk :: a :+!: b -> ObserverM (a :+!: b)
 
 instance (FunctorO (PF a), FunctorO (PF b)) => Observable (a :*!: b) where
-   observer (FixProd f) = send "" (fmapO (_L::Fix (PF a :*: PF b)) thk f >>= return . FixProd)
+   observer (FixProd f) = send "" (liftM FixProd (fmapO (_L::Fix (PF a :*: PF b)) thk f))
       where thk = thunk :: a :*!: b -> ObserverM (a :*!: b)
 
 instance (FunctorO (PF a), FunctorO (PF b)) => Observable (a :@!: b) where
-   observer (FixComp f) = send "" (fmapO (_L::Fix (PF a :@: PF b)) thk f >>= return . FixComp)
+   observer (FixComp f) = send "" (liftM FixComp (fmapO (_L::Fix (PF a :@: PF b)) thk f))
       where thk = thunk :: a :@!: b -> ObserverM (a :@!: b)
 
 -- NOTE: The following commented instance causes overlapping problems with the specific ones defined for base types (One,Int,etc.).
@@ -108,7 +104,7 @@
 --      where thk = thunk :: a -> ObserverM a
 
 instance (Functor f, FunctorO f) => Observable (Fix f) where
-   observer (Fix x) = send (watch (_L::Fix f) (_L::Fix f) x) (fmapO (_L::Fix f) thk x >>= return . Fix)
+   observer (Fix x) = send (watch (_L::Fix f) (_L::Fix f) x) (liftM Fix (fmapO (_L :: Fix f) thk x))
       where thk = thunk :: Fix f -> ObserverM (Fix f)
 
 
diff --git a/src/Generics/Pointless/Observe/RecursionPatterns.hs b/src/Generics/Pointless/Observe/RecursionPatterns.hs
--- a/src/Generics/Pointless/Observe/RecursionPatterns.hs
+++ b/src/Generics/Pointless/Observe/RecursionPatterns.hs
@@ -39,7 +39,7 @@
 
 -- | Redefinition of anamorphisms as observable hylomorphisms.
 anaO :: (Mu b,Functor (PF b), FunctorO (PF b)) => b -> (a -> F b a) -> a -> b
-anaO b f = hyloO b inn f
+anaO b = hyloO b inn
 
 -- | Redefinition of paramorphisms as observable hylomorphisms.
 paraO :: (Mu a,Functor (PF a), FunctorO (PF a), Observable a, Typeable a) => a -> (F a (b,a) -> b) -> a -> b
diff --git a/src/Generics/Pointless/RecursionPatterns.hs b/src/Generics/Pointless/RecursionPatterns.hs
--- a/src/Generics/Pointless/RecursionPatterns.hs
+++ b/src/Generics/Pointless/RecursionPatterns.hs
@@ -53,13 +53,13 @@
 --  Anamorphisms resembles the dual of iteration and, hence, define the inverse of catamorphisms.
 -- Instead of consuming recursive types, they produce values of those types.
 ana :: (Mu b,Functor (PF b)) => b -> (a -> F b a) -> a -> b
-ana b f = hylo b inn f
+ana b = hylo b inn
 
 -- | Recursive definition of an anamorphism.
 anaRec :: (Mu b,Functor (PF b)) => b -> (a -> F b a) -> a -> b
 anaRec b f = inn . pmap b (anaRec b f) . f
 
--- | The functor of intermediate type of a paramorphism is the functor of the consumed type 'a'
+-- | The functor of the intermediate type of a paramorphism is the functor of the consumed type 'a'
 -- extended with an extra annotation to itself in recursive definitions.
 type Para a = a :@!: (I :*!: K a)
 
@@ -79,13 +79,13 @@
    where idA :: a -> a
          idA = id
 
--- | The functor of intermediate type of a paramorphism is the functor of the generated type 'b'
+-- | The functor of the intermediate type of an apomorphism is the functor of the generated type 'b'
 -- with an alternative annotation to itself in recursive definitions.
 type Apo b = b :@!: (I :+!: K b)
 
 -- | Definition of an apomorphism as an hylomorphism.
 --
--- Apomorphisms are the dual recursion patterns of paramorphisms, and therefore they can express functions defined by primitive corecursion.
+-- Apomorphisms are the dual recursion patterns of paramorphisms, and therefore they can express functions defined by primitive corecursion.
 --
 -- They were introduced independently in <http://www.cs.ut.ee/~varmo/papers/nwpt97.ps.gz> and /Program Construction and Generation Based on Recursive Types, MSc thesis/.
 apo :: (Mu b,Functor (PF b)) => b -> (a -> F b (Either a b)) -> a -> b
@@ -95,7 +95,7 @@
 
 -- | Recursive definition of an apomorphism.
 apoRec :: (Mu b,Functor (PF b)) => b -> (a -> F b (Either a b)) -> a -> b
-apoRec (b::b) f = (inn . pmap b (idB \/ idB) . pmap b (apoRec b f -|- idB) . f)
+apoRec (b::b) f = inn . pmap b (idB \/ idB) . pmap b (apoRec b f -|- idB) . f
    where idB :: b -> b
          idB = id
 
@@ -120,8 +120,8 @@
 -- Accumulations <http://www.fing.edu.uy/~pardo/papers/wcgp02.ps.gz> are binary functions that use the second parameter to store intermediate results.
 --
 -- The so called "accumulation technique" is tipically used in functional programming to derive efficient implementations of some recursive functions.
-accum :: (Mu a,Functor (PF d)) => d -> ((F a a,b) -> F d (a,b)) -> (F (Accum d b) c -> c) -> (a,b) -> c
-accum (d::d) g f = hylo (_L :: Accum d b) f ((g /\ snd) . (out >< id))
+accum :: (Mu a,Functor (PF a)) => a -> (F (Accum a b) c -> c) -> ((F a a,b) -> F a (a,b)) -> (a,b) -> c
+accum (a::a) f g = hylo (_L :: Accum a b) f ((g /\ snd) . (out >< id))
 
 -- | In histomorphisms we add an extra annotation 'c' to the base functor of type 'a'.
 type Histo a c = K c :*!: a