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.5
+Version:         0.0.6
 License:         BSD3
 License-file:    LICENSE
 Author:          Alcino Cunha <alcino@di.uminho.pt>, Hugo Pacheco <hpacheco@di.uminho.pt>
@@ -23,7 +23,7 @@
 
 Library
   Hs-Source-Dirs: src
-  Build-Depends:        base >= 3 && < 5, GHood, haskell98, process
+  Build-Depends:        base >= 3 && < 5, GHood, haskell98, process, syb >= 0.1.0.2
   exposed-modules:
         Generics.Pointless.Combinators
         Generics.Pointless.Functors,
@@ -37,4 +37,4 @@
         Generics.Pointless.Bifunctors,
         Generics.Pointless.Bifctrable
 
-  extensions: TypeFamilies, TypeOperators, ScopedTypeVariables, UndecidableInstances, FlexibleInstances, FlexibleContexts, EmptyDataDecls, GADTs
+  extensions: TypeFamilies, TypeOperators, ScopedTypeVariables, UndecidableInstances, FlexibleInstances, FlexibleContexts, DeriveDataTypeable, EmptyDataDecls, GADTs
diff --git a/src/Generics/Pointless/Bifunctors.hs b/src/Generics/Pointless/Bifunctors.hs
--- a/src/Generics/Pointless/Bifunctors.hs
+++ b/src/Generics/Pointless/Bifunctors.hs
@@ -57,22 +57,43 @@
 type instance BRep (g :*| h) a = BRep g a  :*: BRep h a
 type instance BRep (g :@| h) a = BRep g a :@: BRep h a
 
+-- | The polytypic bifunctor zipping combinator.
+-- Just maps over the polymorphic parameter. To map over the recursive parameter we can use @fzip@.
+
+
+
+
+
+
+
 class Bifunctor (f :: * -> * -> *) where
-   bmap :: BFix f -> (a -> b) -> (x -> y) -> Rep (BRep f a) x -> Rep (BRep f b) y
+   bmap :: Ann (BFix f) -> (a -> b) -> (x -> y) -> Rep (BRep f a) x -> Rep (BRep f b) y
+   bzip :: Ann x -> Ann (BFix f) -> (a -> c) -> (Rep (BRep f a) x,Rep (BRep f c) x) -> Rep (BRep f (a,c)) x
 
 instance Bifunctor BId where
    bmap _ p f = f
+   bzip x _ create = fst
 instance Bifunctor (BConst t) where
    bmap _ p f = id
+   bzip x _ create = fst
 instance Bifunctor BPar where
    bmap _ p f = p
+   bzip x _ create = id
 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)
+   bmap _ p f (Left x) = Left (bmap (ann :: Ann (BFix g)) p f x)
+   bmap _ p f (Right x) = Right (bmap (ann :: Ann (BFix h)) p f x)
+   bzip (x::Ann x) _ create = (l -|- r) . dists
+       where l = bzip x g create \/ bmap g (id /\ create) idx . fst
+             r = bmap h (id /\ create) idx . fst \/ bzip x h create
+             idx = id :: x -> x
+             g = ann::Ann (BFix g)
+             h = ann::Ann (BFix h)
 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)
+   bmap _ p f (x,y) = (bmap (ann :: Ann (BFix g)) p f x,bmap (ann ::Ann (BFix h)) p f y)
+   bzip x _ create = (bzip x (ann::Ann (BFix g)) create >< bzip x (ann::Ann (BFix h)) create) . distp
 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
+   bmap _ p f x = bmap (ann :: Ann (BFix g)) p (bmap (ann :: Ann (BFix h)) p f) x
+   bzip = fail "not defined"
 
 type B d a x = Rep (BRep (BF d) a) x
 
@@ -80,8 +101,8 @@
     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
+pbmap :: Bifunctor (BF d) => Ann (d a) -> (a -> b) -> (x -> y) -> B d a x -> B d b y
+pbmap (_::Ann (d a)) p f = bmap (ann :: Ann (BFix (BF d))) p f
 
 -- * Fixpoint combinators
 
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
@@ -19,7 +19,19 @@
 module Generics.Pointless.Combinators where
 
 import Prelude hiding (or,and)
+import qualified Data.Generics as G
 
+-- * Type annotations
+
+-- type annotation
+data Ann a
+ann = _L
+vnn :: a -> Ann a
+vnn _ = ann
+
+instance Show (Ann a) where
+    show = const "ann"
+
 -- * Terminal object
 
 -- | The bottom value for any type.
@@ -29,7 +41,7 @@
 
 -- | The final object.
 -- The only possible value of type 'One' is '_L'.
-data One
+data One deriving G.Typeable
 
 instance Show One where
     show _ = "_L"
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
@@ -36,7 +36,7 @@
 
 -- | Definition of algebraic addition as an anamorphism in the point-wise style.
 addAnaPW :: (Int,Int) -> Int
-addAnaPW = ana (_L::Int) h 
+addAnaPW = ana (ann::Ann Int) h 
    where h (0,0) = Left _L 
          h (n,0) = Right (n-1,0) 
          h (0,m) = Right (0,m-1) 
@@ -44,7 +44,7 @@
 
 -- | Defition of algebraic addition as an anamorphism.
 addAna :: (Int,Int) -> Int
-addAna = ana (_L::Int) f
+addAna = ana (ann::Ann Int) f
    where f = (bang -|- (id >< zero \/ (zero >< id \/ succ >< id))) . aux . (out >< out)
          aux = coassocr . (distl -|- distl) . distr
 
@@ -53,25 +53,25 @@
 
 -- | Definition of algebraic addition as an hylomorphism.
 addHylo :: (Int,Int) -> Int
-addHylo = hylo (_L::From Int) f g
+addHylo = hylo (ann::Ann (From Int)) f g
    where f = id \/ succ
          g = (snd -|- id) . distl . (out >< id)
 
 -- | Definition of algebraic addition as an accumulation.
 addAccum :: (Int,Int) -> Int
-addAccum = accum (_L::Int) f t
+addAccum = accum (ann::Ann Int) f t
    where t = (fst -|- id >< succ) . distl
          f = (snd \/ fst) . distl
 
 addApoPW :: (Int,Int) -> Int
-addApoPW = apo (_L :: Int) h
+addApoPW = apo (ann :: Ann 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
+addApo = apo (ann::Ann Int) h
    where h = (id -|- coswap) . coassocr . (fst -|- inn >< id) . distr . (out >< out)
          
 -- ** Product
@@ -82,7 +82,7 @@
 
 -- | Definition of algebraic product as an hylomorphism
 prodHylo :: (Int,Int) -> Int
-prodHylo = hylo (_L::[Int]) f g
+prodHylo = hylo (ann::Ann [Int]) f g
    where f = zero \/ add
          g = (snd -|- fst /\ id) . distr . (id >< out)
 
@@ -94,7 +94,7 @@
 
 -- | Definition of 'greater than' as an hylomorphism.
 gtHylo :: (Int,Int) -> Bool
-gtHylo = hylo (_L :: From Bool) f g
+gtHylo = hylo (ann :: Ann (From Bool)) f g
     where g = ((((False!) \/ (True!)) \/ (False!)) -|- id) . coassocl . (distl -|- distl) . distr . (out >< out)
 	  f = id \/ id
 
@@ -118,18 +118,18 @@
 
 -- | Definition of the factorial function as an hylomorphism.
 factHylo :: Int -> Int
-factHylo = hylo (_L :: [Int]) f g
+factHylo = hylo (ann :: Ann [Int]) f g
    where g = (id -|- succ /\ id) . out
          f = one \/ prod
 
 -- | Definition of the factorial function as a paramorphism.
 factPara :: Int -> Int
-factPara = para (_L::Int) f
+factPara = para (ann::Ann Int) f
    where f = one \/ (prod . (id >< succ))
 
 -- | Definition of the factorial function as a zygomorphism.
 factZygo :: Int -> Int
-factZygo = zygo (_L::Int) inn f
+factZygo = zygo (ann::Ann Int) inn f
    where f = one \/ (prod . (id >< succ))
 
 -- ** Fibonnaci
@@ -155,19 +155,19 @@
 
 -- | Definition of the fibonacci function as an hylomorphism.
 fibHylo :: Int -> Int
-fibHylo = hylo (_L :: BSTree) f g
+fibHylo = hylo (ann :: Ann BSTree) f g
    where f = zero \/ (one \/ add)
          g = (id -|- ((id -|- succ /\ id) . out)) . out
          
 
 -- | Definition of the fibonacci function as an histomorphism.
 fibHisto :: Int -> Int
-fibHisto = histo (_L::Int) f
+fibHisto = histo (ann::Ann Int) f
    where f = (zero \/ (one . snd \/ add . (id >< outl)) . distr . out)
 
 -- | Definition of the fibonacci function as a dynamorphism.
 fibDyna :: Int -> Int
-fibDyna = dyna (_L::Int) f g
+fibDyna = dyna (ann::Ann Int) f g
    where f = (zero \/ (one . snd \/ add . (id >< outl)) . distr . out)
          g = out
 
@@ -187,14 +187,14 @@
 
 -- | Definition of the binary partitioning of a number as an hylomorphism.
 bpHylo :: Int -> Int
-bpHylo = hylo (_L :: BTree) g h
+bpHylo = hylo (ann :: Ann BTree) g h
    where g = one \/ (id \/ add)
          h = (id -|- h') . out
          h' = (id -|- id /\ (`div` 2) . succ) . (even?)
 
 -- | Definition of the binary partitioning of a number as a dynamorphism.
 bpDyna :: Int -> Int
-bpDyna = dyna (_L :: [Int]) (g . o) h
+bpDyna = dyna (ann :: Ann [Int]) (g . o) h
    where g = one \/ (id \/ add)
          o = id -|- oj
          oj = (o1 -|- o2) . ((odd . fst)?)
@@ -214,7 +214,7 @@
 
 -- | Definition of the average of a set of integers as a catamorphism.
 averageCata :: [Int] -> Int
-averageCata = uncurry div . cata (_L::[Int]) f
+averageCata = uncurry div . cata (ann::Ann [Int]) f
    where f = (zero \/ add . (id >< fst)) /\ (zero \/ succ . snd . snd)
 
 -- * Lists
@@ -242,12 +242,12 @@
 
 -- | 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 (ann::Ann [a]) (f /\ inn . (id -|- id >< snd))
    where f = ([]!) \/ snd . snd
 
 -- | Definition of the tail of a list as a paramorphism.
 tailPara :: [a] -> [a]
-tailPara = para (_L::[a]) f
+tailPara = para (ann::Ann [a]) f
    where f = ([]!) \/ snd . snd
 
 -- ** Length
@@ -267,7 +267,7 @@
 
 -- | Definition of list length as an hylomorphism.
 lengthHylo :: [a] -> Int
-lengthHylo = hylo (_L::Int) f g
+lengthHylo = hylo (ann::Ann Int) f g
    where f = inn
          g = (id -|- snd) . out
 
@@ -290,18 +290,18 @@
 
 -- | Definition of list filtering as an catamorphism.
 filterCata :: (a -> Bool) -> [a] -> [a]
-filterCata p = cata (_L::[a]) f
+filterCata p = cata (ann::Ann [a]) f
    where f = (nil \/ (cons \/ snd)) . (id -|- ((p . fst)?))
 
 -- ** Generation
 
 -- | Generation of infinite lists as an anamorphism.
 repeatAna :: a -> [a]
-repeatAna = ana (_L::[a]) (inr . (id /\ id))
+repeatAna = ana (ann::Ann [a]) (inr . (id /\ id))
 
 -- | Finite replication of an element as an anamorphism.
 replicateAna :: (Int,a) -> [a]
-replicateAna = ana (_L::[a]) h
+replicateAna = ana (ann::Ann [a]) h
    where h = (bang -|- snd /\ id) . distl . (out >< id)
 
 -- | Generation of a downwards list as an anamorphism.
@@ -311,36 +311,36 @@
 
 -- | Ordered list insertion as an apomorphism.
 insertApo :: Ord a => (a,[a]) -> [a]
-insertApo = apo (_L::[a]) f
+insertApo = apo (ann::Ann [a]) f
    where f = inr. undistr . (inr \/ (inr \/ inl)) . ((id >< nil) -|- ((id >< cons) . assocr -|- assocr . (swap >< id)) . distl . ((le?) >< id) . assocl) . distr . (id >< out)
          le = uncurry (<=)
 
 -- | Ordered list insertion as a paramorphism.
 insertPara :: Ord a => (a,[a]) -> [a]
-insertPara (x,l) = para (_L::[a]) f l
+insertPara (x,l) = para (ann::Ann [a]) f l
    where f = wrap . (x!) \/ ((x:) . cons . (id >< snd) \/ cons . (id >< fst)) . (((x <=) . fst)?)
 
 -- | Append an element to the end of a list as an hylomorphism.
 snoc :: (a,[a]) -> [a]
-snoc = hylo (_L::NeList a a) f g
+snoc = hylo (ann::Ann (NeList a a)) f g
    where g = (fst -|- subr) . distr . (id >< out)
          f = wrap \/ cons
 
 -- | Append an element to the end of a list as an apomorphism.
 snocApo :: (a,[a]) -> [a]
-snocApo = apo (_L::[a]) h
+snocApo = apo (ann::Ann [a]) h
    where h = inr . undistr . coswap . (id >< nil  -|-  assocr . (swap >< id) . assocl) . distr . (id >< out)
 
 -- ** Extraction
 
 -- | Creates a bubble from a list. Used in the bubble sort algorithm.
 bubble :: (Ord a) => [a] -> Either One (a,[a])
-bubble = cata (_L::[a]) f
+bubble = cata (ann::Ann [a]) f
    where f = id -|- ((id >< ([]!)) \/ ((id >< cons) . assocr . (id \/ (swap >< id)) . ((uncurry (<) . fst) ?) . assocl)) . distr
 
 -- | Extraction of a number of elements from a list as an anamorphism.
 takeAna :: (Int,[a]) -> [a]
-takeAna = ana (_L::[a]) h
+takeAna = ana (ann::Ann [a]) h
    where h = (bang -|- assocr . (swap >< id) . assocl) . aux . (out >< out)
          aux = coassocl . (distl -|- distl) . distr
 
@@ -354,7 +354,7 @@
 
 -- | Definition for partitioning a list at a specified element as an hylomorphism.
 partitionHylo :: (Ord a) => (a,[a]) -> ([a],[a])  
-partitionHylo = hylo (_L::[(a,a)]) f g
+partitionHylo = hylo (ann::Ann [(a,a)]) f g
    where g = (snd -|- ((id >< fst) /\ (id >< snd))) . distr . (id >< out)
          f = (nil /\ nil) \/ (((cons >< id) . assocl . (snd >< id) \/ (id >< cons) . ((fst . snd) /\ (id >< snd)) . (snd >< id)) . ((gt . fst)?))
 
@@ -362,13 +362,13 @@
 
 -- | Incremental summation as a catamorphism.
 isum :: [Int] -> [Int]
-isum = cata (_L::[Int]) f
+isum = cata (ann::Ann [Int]) f
    where f = nil \/ isumOp . swap . (id >< cons . (zero . bang /\ id))
          isumOp (l,x) = map (x+) l
 
 -- | Incrementation the elements of a list by a specified value as a catamorphism.
 fisum :: [Int] -> Int -> [Int]
-fisum = cata (_L::[Int]) f
+fisum = cata (ann::Ann [Int]) f
     where f = pnt (nil . bang) \/ comp . swap . (curry add >< (cons .) . split . (pnt id . bang /\ id))
 
 data Some a = Wrap a | Insert a (Some a) deriving (Eq,Show)
@@ -395,19 +395,19 @@
 
 -- | Definition of list mapping as a catamorphism.
 mapCata :: [a] -> (a -> b) -> [b]
-mapCata = cata (_L::[a]) f
+mapCata = cata (ann::Ann [a]) f
    where f = (([]!)!) \/ curry (cons . (app . swap >< app) . ((fst >< id) /\ (snd >< id)))
 
 -- | Definition of list reversion as a catamorphism.
 reverseCata :: [a] -> [a]
-reverseCata = cata (_L::[a]) f 
+reverseCata = cata (ann::Ann [a]) f 
     where f = nil \/ (cat . swap . (wrap >< id))
 
 -- | Linear version of reverse using accumulations
 reverseAccum l = reverseAccum' (l,[])
 
 reverseAccum' :: ([a],[a]) -> [a]
-reverseAccum' = accum (_L ::[a]) h tau
+reverseAccum' = accum (ann ::Ann [a]) h tau
     where h = (snd \/ snd . fst) . distl
           tau = (fst -|- aux) . distl
           aux = assocr . (id >< cons) . distp . ((id /\ id) >< id) . assocr
@@ -417,36 +417,36 @@
     where g = id \/ id
           h = (snd -|- aux) . distl . (out >< id)
           aux = (id >< inn . inr) . assocr . (swap >< id)
-          t = _L :: K [a] :+!: I
+          t = ann :: Ann (K [a] :+!: I)
 
 -- | Definition of the quicksort algorithm as an hylomorphism.
 qsort :: (Ord a) => [a] -> [a]
-qsort = hylo (_L::Tree a) f g
+qsort = hylo (ann::Ann (Tree a)) f g
    where g = (id -|- (fst /\ partition)) . out
          f = nil \/ (cat . (id >< cons) . assocr . (swap >< id) . assocl)
 
 -- | Definition of the bubble sort algorithm as an anamorphism.
 bsort :: (Ord a) => [a] -> [a]
-bsort = ana (_L::[a]) bubble
+bsort = ana (ann::Ann [a]) bubble
 -- | Definition of the insertion sort algorithm as a catamorphism.
 isort :: (Ord a) => [a] -> [a]
-isort = cata (_L::[a]) (nil \/ insertApo)
+isort = cata (ann::Ann [a]) (nil \/ insertApo)
 
 -- Auxiliary split function for the merge sort algorithm.
 msplit :: [a] -> ([a],[a])
-msplit = cata (_L::[a]) f
+msplit = cata (ann::Ann [a]) f
     where f = (nil /\ nil) \/ (swap . (cons >< id) . assocl)
 
 -- Definition of the merge sort algorithm as an hylomorphism.
 msort :: (Ord a) => [a] -> [a]
-msort = hylo (_L::(K One :+!: K a) :+!: (I :*!: I)) f g
+msort = hylo (ann::Ann ((K One :+!: K a) :+!: (I :*!: I))) f g
     where g = coassocl . (id -|- (fst -|- msplit . cons) . ((null . snd)?)) . out 
 	  f = (([]!) \/ wrap) \/ merge
 
 -- | Definition of the heap sort algorithm as an hylomorphism.
 hsort :: (Ord a) => [a] -> [a]
 hsort = hylo f g h
-    where f = _L ::(K One :+!: K a) :+!: (K a :*!: (I :*!: I)) 
+    where f = ann :: Ann ((K One :+!: K a) :+!: (K a :*!: (I :*!: I)))
 	  h = coassocl . (id -|- (fst -|- hsplit . cons) . ((null . snd)?)) . out
 	  g = (([]!) \/ wrap) \/ cons . (id >< merge)
 
@@ -459,7 +459,7 @@
 
 -- | Malcolm downwards accumulations on lists.
 malcolm :: ((b, a) -> a) -> a -> [b] -> [a]
-malcolm o e = map (cata (_L::[b]) ((e!) \/ o)) . malcolmAna' cons . (id /\ nil . bang)
+malcolm o e = map (cata (ann::Ann [b]) ((e!) \/ o)) . malcolmAna' cons . (id /\ nil . bang)
 
 -- | Malcom downwards accumulations on lists as an anamorphism.
 malcolmAna :: ((b, a) -> a) -> a -> [b] -> [a]
@@ -467,14 +467,14 @@
 
 -- | Uncurried version of Malcom downwards accumulations on lists as an anamorphism.
 malcolmAna' :: ((b, a) -> a) -> ([b], a) -> [a]
-malcolmAna' o = ana (_L::[a]) g
+malcolmAna' o = ana (ann:: Ann [a]) g
    where g = (fst -|- (snd /\ (id >< o) . assocr . (swap >< id))) . distl . (out >< id)
 
 -- ** Zipping
 
 -- | Definition of the zip for lists of pairs as an anamorphism.
 zipAna :: ([a],[b]) -> [(a,b)]
-zipAna = ana (_L::[(a,b)]) f
+zipAna = ana (ann::Ann [(a,b)]) f
    where f = (bang -|- ((fst >< fst) /\ (snd >< snd))) . aux . (out >< out)
          aux = coassocl . (distl -|- distl) . distr
 
@@ -482,7 +482,7 @@
 
 -- | Definition of the subsequences of a list as a catamorphism.
 subsequences :: Eq a => [a] -> [[a]]
-subsequences = cata (_L::[a]) f
+subsequences = cata (ann::Ann [a]) f
    where f = cons . (nil /\ nil) \/ uncurry union . (snd /\ subsOp . swap . (wrap >< id))
          subsOp (r,l) = map (l++) r
 
@@ -494,7 +494,7 @@
 
 -- | List concatenation as a catamorphism.
 catCata :: [a] -> [a] -> [a]
-catCata = cata (_L::[a]) f
+catCata = cata (ann::Ann [a]) f
    where f = (id!) \/ (comp . (curry cons >< id))
 
 -- | The fixpoint of the list functor with a specific terminal element.
@@ -502,7 +502,7 @@
 
 -- | List concatenation as an hylomorphism.
 catHylo :: ([a],[a]) -> [a]
-catHylo = hylo (_L::NeList [a] a) f g
+catHylo = hylo (ann::Ann (NeList [a] a)) f g
    where g = (snd -|- assocr) . distl . (out >< id)
          f = id \/ cons
 
@@ -513,12 +513,12 @@
 
 -- | Definition of lists-of-lists concatenation as an anamorphism.
 concatCata :: [[a]] -> [a]
-concatCata = cata (_L::[[a]]) g
+concatCata = cata (ann::Ann[[a]]) g
    where g = ([]!) \/ cat
 
 -- | Sorted concatenation of two lists as an hylomorphism.
 merge :: (Ord a) => ([a],[a]) -> [a]
-merge = hylo (_L::NeList [a] a) f g
+merge = hylo (ann::Ann (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)
          f = id \/ cons
 
@@ -526,7 +526,7 @@
 
 -- | Definition of inter addition as a catamorphism.
 sumCata :: [Int] -> Int
-sumCata = cata (_L::[Int]) f
+sumCata = cata (ann::Ann [Int]) f
    where f = (0!) \/ add
 
 -- ** Multiplication
@@ -545,7 +545,7 @@
 
 -- Test if a list is sorted as a paramorphism.
 sorted :: (Ord a) => [a] -> Bool
-sorted = para (_L::[a]) f
+sorted = para (ann::Ann [a]) f
     where f = true \/ uncurry (&&) . ((true . bang \/ uncurry (<=) . (id >< head)) . ((null . snd)?) >< id) . assocl . (id >< swap)
 
 -- ** Edit distance
@@ -572,7 +572,7 @@
 
 -- | The edit distance algorithm as an hylomorphism.
 editdistHylo :: Eq a => ([a],[a]) -> Int
-editdistHylo (x::([a],[a])) = hylo (_L::EditDist a) g h x
+editdistHylo (x::([a],[a])) = hylo (ann::Ann (EditDist a)) g h x
    where g :: Eq a => F (EditDist a) Int -> Int
          g = length \/ g'
          g' ((a,b),(x1,(x2,x3))) = min m1 (min m2 m3)
@@ -585,7 +585,7 @@
 
 -- | The edit distance algorithm as a dynamorphism.
 editDistDyna :: Eq a => ([a],[a]) -> Int
-editDistDyna (l1::[a],l2) = dyna (_L :: EditDistL a) (g . o (length l1)) (h l1) (l1,l2)
+editDistDyna (l1::[a],l2) = dyna (ann :: Ann (EditDistL a)) (g . o (length l1)) (h l1) (l1,l2)
    where g :: Eq a => F (EditDist a) Int -> Int
          g = length \/ g'
          g' ((a,b),(x1,(x2,x3))) = min m1 (min m2 m3)
@@ -622,20 +622,20 @@
 
 -- | Definition of a stream sequence generator as an anamorphism. 
 generate :: Int -> Stream Int
-generate = ana (_L::Stream a) (id /\ succ)
+generate = ana (ann::Ann(Stream a)) (id /\ succ)
 
 -- | Identity o streams as an anamorphism.
 idStream :: Stream a -> Stream a
-idStream = ana (_L::Stream a) out
+idStream = ana (ann::Ann (Stream a)) out
 
 -- | Mapping over streams as an anamorphism.
 mapStream :: (a -> b) -> Stream a -> Stream b
-mapStream f = ana (_L::Stream b) g 
+mapStream f = ana (ann::Ann (Stream b)) g 
     where g = (f >< id) . out
 
 -- | Malcolm downwards accumulations on streams.
 malcolmS :: ((b,a) -> a) -> a -> Stream b -> Stream a
-malcolmS o e = mapStream (cata (_L::[b]) ((e!) \/ o)) . malcolmSAna' cons . (id /\ nil . bang)
+malcolmS o e = mapStream (cata (ann::Ann [b]) ((e!) \/ o)) . malcolmSAna' cons . (id /\ nil . bang)
 
 -- | Malcom downwards accumulations on streams as an anamorphism.
 malcolmSAna :: ((b,a) -> a) -> a -> Stream b -> Stream a
@@ -643,7 +643,7 @@
 
 -- | Uncurried version of Malcom downwards accumulations on streams as an anamorphism.
 malcolmSAna' :: ((b,a) -> a) -> (Stream b, a) -> Stream a
-malcolmSAna' o = ana (_L::Stream a) g
+malcolmSAna' o = ana (ann::Ann (Stream a)) g
     where g = snd /\ swap . (o >< id) . assocl . (id >< swap) . assocr . (out >< id)
 
 -- | Promotes streams elements to streams of singleton elements.
@@ -652,7 +652,7 @@
 
 -- | Definition of parwise exchange on streams as a futumorphism.
 exchFutu :: Stream a -> Stream a
-exchFutu = futu (_L::Stream a) (f /\ (g . (h /\ i)))
+exchFutu = futu (ann::Ann (Stream a)) (f /\ (g . (h /\ i)))
    where f = headS . tailS
          g = innr
          h = headS
@@ -674,33 +674,33 @@
 
 -- | Counting the number of leaves in a binary tree as a catamorphism.
 nleaves :: Tree a -> Int
-nleaves = cata (_L::Tree a) f
+nleaves = cata (ann::Ann (Tree a)) f
     where f = (1!) \/ (add . snd)
 
 -- | Counting the number of nodes in a binary tree as a catamorphism.
 nnodes :: Tree a -> Int
-nnodes = cata (_L::Tree a) f
+nnodes = cata (ann::Ann (Tree a)) f
     where f = (0!) \/ (succ . add . snd)
 
 -- | Generation of a binary tree with a specified height as an anamorphism.
 genTree :: Int -> Tree Int
-genTree = ana (_L::Tree Int) f
+genTree = ana (ann::Ann (Tree Int)) f
     where f = (bang -|- (id /\ (pred /\ pred))) . ((==0)?)
 
 -- | The preorder traversal on binary trees as a catamorphism.
 preTree :: Tree a -> [a]
-preTree = cata (_L::Tree a) f
+preTree = cata (ann::Ann (Tree a)) f
     where f = ([]!) \/ (cons . (id >< cat))
 
 -- | The postorder traversal on binary trees as a catamorphism.
 postTree :: Tree a -> [a]
-postTree = cata (_L::Tree a) f
+postTree = cata (ann::Ann (Tree a)) f
     where f = ([]!) \/ (cat . swap . (wrap >< cat))
 
 -- * Leaf Trees
 
 -- | Datatype declaration of a leaf tree.
-data LTree a = Leaf a | Branch (LTree a) (LTree a)
+data LTree a = Leaf a | Branch (LTree a) (LTree a) deriving (Eq,Show)
 
 -- | The functor of a leaf tree.
 type instance PF (LTree a) = Const a :+: (Id :*: Id)
@@ -713,17 +713,17 @@
 
 -- | Extract the leaves of a leaf tree as a catamorphism.
 leaves :: LTree a -> [a]
-leaves = cata (_L::LTree a) f
+leaves = cata (ann::Ann (LTree a)) f
     where f = wrap \/ cat
 
 -- | Generation of a leaft tree of a specified height as an anamorphism.
 genLTree :: Int -> LTree Int
-genLTree = ana (_L::LTree Int) f
+genLTree = ana (ann::Ann (LTree Int)) f
     where f = ((0!) -|- (id /\ id)) . out
 
 -- | Calculate the height of a leaf tree as a catamorphism.
 height :: LTree a -> Int
-height = cata (_L::LTree a) f
+height = cata (ann::Ann (LTree a)) f
     where f = (0!) \/ (succ . uncurry max)
 
 -- * Rose Trees
@@ -740,17 +740,17 @@
 
 --	 The preorder traversal on rose trees as a catamorphism.
 preRose :: Rose a -> [a]
-preRose = cata (_L::Rose a) f
+preRose = cata (ann ::Ann (Rose a)) f
    where f = (cons . (id >< concat))
 
 -- | The postorder traversal on rose trees as a catamorphism.
 postRose :: Rose a -> [a]
-postRose = cata (_L::Rose a) f
-   where f = cat . swap . (wrap >< cata (_L::[[a]]) (nil \/ cat))
+postRose = cata (ann ::Ann (Rose a)) f
+   where f = cat . swap . (wrap >< cata (ann::Ann [[a]]) (nil \/ cat))
 
 -- | Generation of a rose tree of a specified height as an anamorphism.
 genRose :: Int -> Rose Int
-genRose = ana (_L::Rose Int) f
+genRose = ana (ann ::Ann (Rose Int)) f
    where f = ((id /\ ([]!)) \/ (id /\ downtoAna . pred)) . ((==0)?)
 
 
diff --git a/src/Generics/Pointless/Examples/Observe.hs b/src/Generics/Pointless/Examples/Observe.hs
--- a/src/Generics/Pointless/Examples/Observe.hs
+++ b/src/Generics/Pointless/Examples/Observe.hs
@@ -29,66 +29,66 @@
 
 -- | Definition of the observable length function as an hylomorphism.
 lengthHyloO :: Observable a => [a] -> Int
-lengthHyloO = hyloO (_L::Int) f g
+lengthHyloO = hyloO (ann::Ann Int) f g
    where f = inn
          g = (id -|- snd) . out
 
 -- | Definition of the observable length function as an anamorphism.
 lengthAnaO :: Observable a => [a] -> Int
-lengthAnaO = anaO (_L::Int) f
+lengthAnaO = anaO (ann::Ann Int) f
    where f = (id -|- snd) . out
 
 -- | Definition of the observable length function as a catamorphism.
 lengthCataO :: (Typeable a, Observable a) => [a] -> Int
-lengthCataO = cataO (_L :: [a]) g
+lengthCataO = cataO (ann ::Ann [a]) g
    where g = inn . (id -|- snd)
 
 -- | Definition of the observable factorial function as an hylomorphism.
 factHyloO :: Int -> Int
-factHyloO = hyloO (_L::[Int]) f g
+factHyloO = hyloO (ann::Ann [Int]) f g
     where g = (id -|- succ /\ id) . out
           f = one \/ prod
 
 -- | Definition of the observable factorial function as a paramorphism.
 factParaO :: Int -> Int
-factParaO = paraO (_L::Int) f
+factParaO = paraO (ann::Ann Int) f
     where f = one \/ prod . (id >< succ)
 
 -- | Definition of the observable factorial function as a zygomorphism.
 factZygoO :: Int -> Int
-factZygoO = zygoO (_L::Int) inn f
+factZygoO = zygoO (ann::Ann Int) inn f
    where f = one \/ (prod . (id >< succ))
 
 -- | Definition of the observable fibonacci function as an hylomorphism.
 fibHyloO :: Int -> Int
-fibHyloO = hyloO (_L::LTree One) f g
+fibHyloO = hyloO (ann::Ann (LTree One)) f g
     where g = (bang -|- pred /\ pred . pred) . ((<=1)?)
 	  f = one \/ add
 	
 -- | Definition of the observable fibonacci function as an histomorphism.
 fibHistoO :: Int -> Int
-fibHistoO = histoO (_L::Int) f
+fibHistoO = histoO (ann::Ann Int) f
    where f = (zero \/ (one . snd \/ add . (id >< outl)) . distr . out)
 
 -- | Definition of the observable fibonacci function as a dynamorphism.
 fibDynaO :: Int -> Int
-fibDynaO = dynaO (_L::Int) f g
+fibDynaO = dynaO (ann::Ann Int) f g
    where f = (zero \/ (one . snd \/ add . (id >< outl)) . distr . out)
          g = out
 
 -- | Definition of the observable quicksort function as an hylomorphism.
 qsortHyloO :: (Typeable a, Observable a, Ord a) => [a] -> [a]
-qsortHyloO = hyloO (_L::Tree a) f g
+qsortHyloO = hyloO (ann::Ann (Tree a)) f g
     where g = (id -|- fst /\ partition) . out
 	  f = nil \/ cat . (id >< cons) . assocr . (swap >< id) . assocl
 
 -- | Definition of the observable tail function as a paramorphism.
 tailParaO :: (Typeable a, Observable a) => [a] -> [a]
-tailParaO = paraO (_L::[a]) (nil \/ snd . snd)
+tailParaO = paraO (ann::Ann [a]) (nil \/ snd . snd)
 
 -- | Definition of the observable add function as an accumulation.
 addAccumO :: (Int,Int) -> Int
-addAccumO = accumO (_L::Int) t f
+addAccumO = accumO (ann::Ann Int) t f
     where t = (fst -|- id >< succ) . distl
 	  f = (snd \/ fst) . distl
 
diff --git a/src/Generics/Pointless/Fctrable.hs b/src/Generics/Pointless/Fctrable.hs
--- a/src/Generics/Pointless/Fctrable.hs
+++ b/src/Generics/Pointless/Fctrable.hs
@@ -27,6 +27,7 @@
 data Fctr (f :: * -> *) where
     I :: Fctr Id
     K :: Fctr (Const c)
+    L :: Fctr []
     (:*!:) :: (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)
@@ -38,6 +39,8 @@
     fctr = I
 instance Fctrable (Const c) where
     fctr = K
+instance Fctrable [] where
+    fctr = L
 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
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
@@ -21,6 +21,10 @@
 module Generics.Pointless.Functors where
 
 import Prelude hiding (Functor(..))
+import qualified Data.Generics as G
+import qualified Data.Typeable as G
+import qualified Data.Data as G
+import qualified Data.Functor as F
 import Generics.Pointless.Combinators
 
 -- * Functors
@@ -28,32 +32,42 @@
 -- ** Definition and operations over functors
 
 -- | Identity functor.
-newtype Id x = IdF {unIdF :: x}
+data Id x = IdF {unIdF :: x} deriving (Eq,Show,G.Typeable)
 
 -- | Constant functor.
-newtype Const t x = ConsF {unConsF :: t}
+data Const t x = ConsF {unConsF :: t} deriving (Eq,Show,G.Typeable)
 
 -- | Sum of functors.
 infixr 5 :+:
-data (g :+: h) x = InlF (g x) | InrF (h x)
+data (g :+: h) x = InlF (g x) | InrF (h x) deriving (Eq,Show)
 
+instance (G.Typeable (g x),G.Typeable (h x)) => G.Typeable ((g :+: h) x) where
+   typeOf _ = G.mkTyCon ":+:" `G.mkTyConApp` [G.typeOf (ann::g x),G.typeOf (ann::h x)]
+
 -- | Product of functors.
 infixr 6 :*:
-data (g :*: h) x = ProdF (g x) (h x)
+data (g :*: h) x = ProdF (g x) (h x) deriving (Eq,Show)
 
+instance (G.Typeable (g x),G.Typeable (h x)) => G.Typeable ((g :*: h) x) where
+   typeOf _ = G.mkTyCon ":*:" `G.mkTyConApp` [G.typeOf (ann::g x),G.typeOf (ann::h x)]
+
 -- | Composition of functors.
 infixr 9 :@:
-newtype (g :@: h) x = CompF {unCompF :: g (h x)}
+data (g :@: h) x = CompF {unCompF :: g (h x)} deriving (Eq,Show)
 
+instance (G.Typeable (g x),G.Typeable (h x)) => G.Typeable ((g :@: h) x) where
+   typeOf _ = G.mkTyCon ":@:" `G.mkTyConApp` [G.typeOf (ann::g x),G.typeOf (ann::h x)]
+
 -- | Explicit fixpoint operator.
-newtype Fix f = FixF { -- | The unfolding of the fixpoint of a functor is the functor applied to its fixpoint.
+newtype Fix f = Inn { -- | 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
-                         unFixF :: Rep f (Fix f)
+                         ouT :: Rep f (Fix f)
                     }
 
-instance Show (Rep f (Fix f)) => Show (Fix f) where
-   show (FixF f) = "(Fix " ++ show f ++ ")"
+instance ShowRep f => Show (Fix f) where
+    show f@(Inn r) = "(Fix " ++ showrep (vnn f) showfix r ++ ")"
+        where showfix = show :: Fix f -> String
 
 -- | Family of patterns functors of data types.
 --
@@ -90,43 +104,133 @@
 type instance Rep [] x = [x]
 -- ^ The application of the list functor to some type returns a list of the argument type.
 
+-- | A specific @Show@ class for functor representations that receives a show function for recursive instances.
+-- This avoids infinite loops in the type inference of fixpoints.
+class ShowRep f where
+    showrep :: Ann (Fix f) -> (x -> String) -> Rep f x -> String
+instance ShowRep Id where
+    showrep _ f x = f x
+instance Show t => ShowRep (Const t) where
+    showrep _ _ t = show t
+instance (ShowRep f,ShowRep g) => ShowRep (f :*: g) where
+    showrep (_ :: Ann (Fix (f :*: g))) f (x,y) = "("++l++","++r++")"
+        where l = showrep (ann :: Ann (Fix f)) f x
+              r = showrep (ann :: Ann (Fix g)) f y
+instance (ShowRep f,ShowRep g) => ShowRep (f :+: g) where
+    showrep (_ :: Ann (Fix (f :+: g))) f (Left x) = "(Left "++l++")"
+        where l = showrep (ann :: Ann (Fix f)) f x
+    showrep (_ :: Ann (Fix (f :+: g))) f (Right y) = "(Right "++r++")"
+        where r = showrep (ann :: Ann (Fix g)) f y
+instance (ShowRep f,ShowRep g) => ShowRep (f :@: g) where
+    showrep (_ :: Ann (Fix (f:@:g))) f x = showrep (ann :: Ann (Fix f)) r x
+        where r = showrep (ann :: Ann (Fix g)) f
+
+class ToRep f where
+    rep :: f x -> Rep f x
+    fun :: f x -> Ann (Fix f)
+    val :: f x -> Ann x
+    unrep :: Ann (Fix f) -> Ann x -> Rep f x -> f x
+
+instance ToRep [] where
+	rep l = l
+	fun l = ann
+	val l = ann
+	unrep _ _ l = l
+
+instance ToRep Id where
+    rep (IdF x) = x
+    fun _ = ann::Ann (Fix Id)
+    val (IdF (x::x)) = ann::Ann x
+    unrep _ _ x = IdF x
+instance ToRep (Const c) where
+    rep (ConsF x) = x
+    fun _ = ann::Ann (Fix (Const c))
+    val (ConsF _::Const c x) = ann::Ann x
+    unrep _ _ x = ConsF x
+instance (ToRep f,ToRep g) => ToRep (f :*: g) where
+    rep (ProdF x y) = (rep x,rep y)
+    fun _ = ann::Ann (Fix (f:*:g))
+    val (ProdF (x::f x) (y::g x)) = ann::Ann x
+    unrep (_::Ann (Fix (f:*:g))) a (x,y) = ProdF (unrep (ann::Ann (Fix f)) a x) (unrep (ann::Ann (Fix g)) a y)
+instance (ToRep f,ToRep g) => ToRep (f :+: g) where
+    rep (InlF l) = Left (rep l)
+    rep (InrF r) = Right (rep r)
+    fun _ = ann::Ann (Fix (f:+:g))
+    val (InlF (l::f x)) = ann::Ann x
+    val (InrF (r::g x)) = ann::Ann x
+    unrep (_::Ann (Fix (f:+:g))) a (Left l) = InlF (unrep (ann::Ann (Fix f)) a l)
+    unrep (_::Ann (Fix (f:+:g))) a (Right r) = InrF (unrep (ann::Ann (Fix g)) a r)
+instance (Functor f,F.Functor f,ToRep f,ToRep g) => ToRep (f :@: g) where
+    rep (CompF x) = rep $ F.fmap rep x
+    fun _ = ann::Ann (Fix (f:@:g))
+    val (CompF x::(f:@:g) x) = ann::Ann x
+    unrep (_::Ann (Fix (f:@:g))) a x = CompF $ (unrep (ann::Ann (Fix f)) (ann::Ann (g a))) $ fmap (ann::Ann (Fix f)) (unrep (ann::Ann (Fix g)) a) x
+
 -- | Polytypic 'Prelude.Functor' class for functor representations
 class Functor (f :: * -> *) where
-   fmap :: Fix f                          -- ^ For desambiguation purposes, the type of the functor must be passed as an explicit parameter to 'fmap'
+   fmap :: Ann (Fix f)                          -- ^ For desambiguation purposes, the type of the functor must be passed as an explicit parameter to 'fmap'
         -> (x -> y) -> Rep f x -> Rep f y -- ^ The mapping over representations
+   fzip :: Ann (Fix f) -> (a -> c) -> (Rep f a,Rep f c) -> Rep f (a,c)      -- ^ The polytypic functor zipping combinator.
+        -- Gives preference to the abstract (first) F-structure.
 
+instance F.Functor Id where
+   fmap f (IdF x) = IdF $ f x
 instance Functor Id where
    fmap _ f = f
+   fzip _ create = id
 -- ^ The identity functor applies the mapping function the argument type
 
+instance F.Functor (Const t) where
+   fmap f (ConsF x) = ConsF x
 instance Functor (Const t) where
    fmap _ f = id
+   fzip _ create = fst
 -- ^ The constant functor preserves the argument type
 
+instance (F.Functor g,F.Functor h) => F.Functor (g :+: h) where
+   fmap f (InlF x) = InlF (F.fmap f x)
+   fmap f (InrF x) = InrF (F.fmap f x)
 instance (Functor g,Functor h) => Functor (g :+: h) where
-   fmap _ f (Left x) = Left (fmap (_L :: Fix g) f x)
-   fmap _ f (Right x) = Right (fmap (_L :: Fix h) f x)
+   fmap (_::Ann (Fix (g:+:h))) f (Left x) = Left (fmap (ann :: Ann (Fix g)) f x)
+   fmap (_::Ann (Fix (g:+:h))) f (Right x) = Right (fmap (ann :: Ann (Fix h)) f x)
+   fzip (_::Ann (Fix (g:+:h))) create = (l -|- r) . dists
+    where l = fzip (ann::Ann (Fix g)) create \/ fmap (ann::Ann (Fix g)) (id /\ create) . fst
+          r = fmap (ann::Ann (Fix h)) (id /\ create) . fst \/ fzip (ann::Ann (Fix h)) create
 -- ^ The sum functor recursively applies the mapping function to each alternative
 
+instance (F.Functor g,F.Functor h) => F.Functor (g :*: h) where
+   fmap f (ProdF x y) = ProdF (F.fmap f x) (F.fmap f y)
 instance (Functor g,Functor h) => Functor (g :*: h) where
-   fmap _ f (x,y) = (fmap (_L :: Fix g) f x,fmap (_L :: Fix h) f y)
+   fmap (_::Ann (Fix (g:*:h))) f (x,y) = (fmap (ann :: Ann (Fix g)) f x,fmap (ann :: Ann (Fix h)) f y)
+   fzip (_::Ann (Fix (g:*:h))) create = (fzip (ann::Ann (Fix g)) create >< fzip (ann::Ann (Fix h)) create) . distp
 -- ^ The product functor recursively applies the mapping function to both sides
 
+instance (F.Functor g,F.Functor h) => F.Functor (g :@: h) where
+   fmap f (CompF x) = CompF $ F.fmap (F.fmap f) x
 instance (Functor g,Functor h) => Functor (g :@: h) where
-   fmap _ f x = fmap (_L :: Fix g) (fmap (_L :: Fix h) f) x
+   fmap (_::Ann (Fix (g:@:h))) f x = fmap (ann :: Ann (Fix g)) (fmap (ann :: Ann (Fix h)) f) x
+   fzip (_::Ann (Fix (g:@:h))) create = fmap g (fzip h create) . fzip g (fmap h create)
+    where g = ann::Ann (Fix g)
+          h = ann::Ann (Fix h)
 -- ^ The composition functor applies in the nesting of the mapping function to the nested functor applications
 
 instance Functor [] where
    fmap _ = map
+   fzip _ create = lzip create
 -- ^ The list functor maps the specific 'map' function over lists of types
 
+lzip :: (a -> c) -> ([a],[c]) -> [(a,c)]
+lzip create ([],lc) = []
+lzip create (a:la,[]) = (a,create a) : lzip create (la,[])
+lzip create (a:la,c:lc) = (a,c) : lzip create (la,lc)
+
 -- | Short alias to express the structurally equivalent sum of products for some data type
 type F a x = Rep (PF a) x
 
 -- | Polytypic map function
-pmap :: Functor (PF a) => a                          -- ^ A value of a data type that is the fixed point of the desired functor
+pmap :: Functor (PF a) => Ann a                          -- ^ A value of a data type that is the fixed point of the desired functor
                        -> (x -> y) -> F a x -> F a y -- ^ The mapping over the equivalent sum of products
-pmap (_::a) f = fmap (_L :: Fix (PF a)) f
+pmap (_::Ann a) f = fmap (ann:: Ann (Fix (PF a))) f
 
 -- | The 'Mu' class provides the value-level translation between data types and their sum of products representations
 class Mu a where
@@ -135,9 +239,15 @@
     -- | unpacks a data type into the equivalent sum of products
     out :: a -> F a a
 
+inn' :: Mu a => Ann a -> F a a -> a
+inn' _ = inn
+
+out' :: Mu a => Ann a -> a -> F a a
+out' _ = out
+
 instance Mu (Fix f) where
-   inn = FixF
-   out = unFixF
+   inn = Inn
+   out = ouT
 -- ^ Expanding/contracting the fixed point of a functor is the same as consuming/applying it's single type constructor
 
 -- ** Fixpoint combinators
@@ -207,7 +317,7 @@
 
 -- ** Natural Numbers
 
-data Nat = Zero | Succ Nat deriving (Eq,Show,Read)
+data Nat = Zero | Succ Nat deriving (Eq,Show,Read,G.Typeable,G.Data)
 
 type instance PF Nat = Const One :+: Id
 
@@ -232,6 +342,14 @@
 
 suck :: Int -> Int
 suck = inn . inr
+
+natInt :: Nat -> Int
+natInt Zero = 0
+natInt (Succ n) = succ (natInt n)
+
+intNat :: Int -> Nat
+intNat 0 = Zero
+intNat n = Succ (intNat $ pred n)
 
 -- ** Bool
 
diff --git a/src/Generics/Pointless/MonadCombinators.hs b/src/Generics/Pointless/MonadCombinators.hs
--- a/src/Generics/Pointless/MonadCombinators.hs
+++ b/src/Generics/Pointless/MonadCombinators.hs
@@ -43,7 +43,7 @@
 (-||-) 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/>.
+-- 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
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
@@ -21,78 +21,76 @@
 import Generics.Pointless.Combinators
 import Generics.Pointless.Functors
 import Debug.Observe
-import Data.Typeable
+import qualified Data.Generics as G
 import Prelude hiding (Functor(..))
 import Control.Monad hiding (Functor(..))
 
 -- * Definition of generic observations
 
-instance Typeable One where
-   typeOf _ = mkTyCon "One" `mkTyConApp` []
-
 -- | Class for mapping observations over functor representations.
 class FunctorO f where
    -- | Derives a type representation for a functor. This is used for showing the functor for reursion trees.
-   functorOf :: Fix f -> String
+   functorOf :: Ann (Fix f) -> String
    -- | Watch values of a functor. Since the fixpoint of a functor recurses over himself, we cannot use the 'Show' instance for functor values applied to their fixpoint.
-   watch :: Fix f -> x -> Rep f x -> String
+   watch :: Ann (Fix f) -> Ann x -> Rep f x -> String
    -- | Maps an observation over a functor representation.
-   fmapO :: Fix f -> (x -> ObserverM y) -> Rep f x -> ObserverM (Rep f y)
+   fmapO :: Ann (Fix f) -> (x -> ObserverM y) -> Rep f x -> ObserverM (Rep f y)
 
 instance FunctorO Id where
    functorOf _ = "Id"
    watch _ _ _ = ""
    fmapO _ f = f
 
-instance (Typeable a,Observable a) => FunctorO (Const a) where
-   functorOf _ = "Const " ++ show (typeOf (_L::a))
+instance (G.Typeable a,Observable a) => FunctorO (Const a) where
+   functorOf _ = "Const " ++ show (G.typeOf (_L::a))
    watch _ _ _ = ""
    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) = liftM Left (fmapO (_L::Fix f) f x)
-   fmapO _ f (Right x) = liftM Right (fmapO (_L::Fix g) f x)
+   functorOf (_::Ann (Fix (f:+:g))) = "(" ++ functorOf (ann::Ann (Fix f)) ++ ":+:" ++ functorOf (ann::Ann (Fix g)) ++ ")"
+   watch (_::Ann (Fix (f:+:g))) _ (Left _) = "Left"
+   watch (_::Ann (Fix (f:+:g))) _ (Right _) = "Right"
+   fmapO (_::Ann (Fix (f:+:g))) f (Left x) = liftM Left (fmapO (ann::Ann (Fix f)) f x)
+   fmapO (_::Ann (Fix (f:+:g))) f (Right x) = liftM Right (fmapO (ann::Ann (Fix g)) f x)
 
 instance (FunctorO f, FunctorO g) => FunctorO (f :*: g) where
-   functorOf _ = "(" ++ functorOf (_L::Fix f) ++ ":*:" ++ functorOf (_L::Fix g) ++ ")"
+   functorOf (_::Ann (Fix (f:*:g))) = "(" ++ functorOf (ann::Ann (Fix f)) ++ ":*:" ++ functorOf (ann::Ann (Fix g)) ++ ")"
    watch _ _ _ = ""
-   fmapO _ f (x,y) = do x' <- fmapO (_L :: Fix f) f x
-			y' <- fmapO (_L::Fix g) f y
-			return (x',y')
+   fmapO (_::Ann (Fix (f:*:g))) f (x,y) = do
+       x' <- fmapO (ann::Ann (Fix f)) f x
+       y' <- fmapO (ann::Ann (Fix g)) f y
+       return (x',y')
 
 instance (FunctorO g, FunctorO h) => FunctorO (g :@: h) where
-   functorOf _ = "(" ++ functorOf (_L::Fix g) ++ ":@:" ++ functorOf (_L::Fix h) ++ ")"
-   watch _ (x::x) = watch (_L::Fix g) (_L::Rep h x)
-   fmapO _ = fmapO (_L::Fix g) . fmapO (_L::Fix h)
+   functorOf (_::Ann (Fix (g:@:h))) = "(" ++ functorOf (ann::Ann (Fix g)) ++ ":@:" ++ functorOf (ann::Ann (Fix h)) ++ ")"
+   watch (_::Ann (Fix (g:@:h))) (x::Ann x) = watch (ann::Ann (Fix g)) (ann::Ann (Rep h x))
+   fmapO (_::Ann (Fix (g:@:h))) = fmapO (ann::Ann (Fix g)) . fmapO (ann::Ann (Fix h))
 
 -- | Polytypic mapping of observations.
-omap :: FunctorO (PF a) => a -> (x -> ObserverM y) -> F a x -> ObserverM (F a y)
-omap (_::a) = fmapO (_L::Fix (PF a))
+omap :: FunctorO (PF a) => Ann a -> (x -> ObserverM y) -> F a x -> ObserverM (F a y)
+omap (_::Ann a) = fmapO (ann::Ann (Fix (PF a)))
 
 instance Observable One where
    observer = observeBase
 
 instance Observable I where
-   observer FixId = send "" (fmapO (_L :: Fix Id) thunk FixId)
+   observer FixId = send "" (fmapO (ann :: Ann (Fix Id)) thunk FixId)
 
-instance (Typeable a,Observable a) => Observable (K a) where
-   observer (FixConst a) = send "" (liftM FixConst (fmapO (_L::Fix (Const a)) thk a))
+instance (G.Typeable a,Observable a) => Observable (K a) where
+   observer (FixConst a) = send "" (liftM FixConst (fmapO (ann::Ann (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 "" (liftM FixSum (fmapO (_L::Fix (PF a :+: PF b)) thk f))
+   observer (FixSum f) = send "" (liftM FixSum (fmapO (ann::Ann (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 "" (liftM FixProd (fmapO (_L::Fix (PF a :*: PF b)) thk f))
+   observer (FixProd f) = send "" (liftM FixProd (fmapO (ann::Ann (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 "" (liftM FixComp (fmapO (_L::Fix (PF a :@: PF b)) thk f))
+   observer (FixComp f) = send "" (liftM FixComp (fmapO (ann::Ann (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.).
@@ -105,7 +103,8 @@
 
 instance (Functor f, FunctorO f) => Observable (Fix f) where
 
-   observer (FixF x) = send (watch (_L::Fix f) (_L::Fix f) x) (liftM FixF (fmapO (_L :: Fix f) thk x))
+   observer (Inn x) = send (watch f f x) (liftM Inn (fmapO f thk x))
       where thk = thunk :: Fix f -> ObserverM (Fix f)
+            f = ann::Ann (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
@@ -29,61 +29,61 @@
 -- * Recursion patterns with observation of intermediate data structures
 
 -- | Redefinition of hylomorphisms with observation of the intermediate data type.
-hyloO :: (Mu b, Functor (PF b), FunctorO (PF b)) => b -> (F b c -> c) -> (a -> F b a) -> a -> c
-hyloO (b::b) g h = cata f g . observe ("Recursion Tree Functor: " ++ functorOf f) . ana f h
-   where f = _L :: Fix (PF b)
+hyloO :: (Mu b, Functor (PF b), FunctorO (PF b)) => Ann b -> (F b c -> c) -> (a -> F b a) -> a -> c
+hyloO (b::Ann b) g h = cata f g . observe ("Recursion Tree Functor: " ++ functorOf f) . ana f h
+   where f = ann :: Ann (Fix (PF b))
 
 -- | Redefinition of catamorphisms as observable hylomorphisms.
-cataO :: (Mu a, Functor (PF a), FunctorO (PF a)) => a -> (F a b -> b) -> a -> b
+cataO :: (Mu a, Functor (PF a), FunctorO (PF a)) => Ann a -> (F a b -> b) -> a -> b
 cataO a f = hyloO a f out
 
 -- | Redefinition of anamorphisms as observable hylomorphisms.
-anaO :: (Mu b,Functor (PF b), FunctorO (PF b)) => b -> (a -> F b a) -> a -> b
+anaO :: (Mu b,Functor (PF b), FunctorO (PF b)) => Ann b -> (a -> F b a) -> a -> b
 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
-paraO (a::a) f = hyloO (_L :: Para a) f (pmap a (idA /\ idA) . out)
+paraO :: (Mu a,Functor (PF a), FunctorO (PF a), Observable a, Typeable a) => Ann a -> (F a (b,a) -> b) -> a -> b
+paraO (a::Ann a) f = hyloO (ann :: Ann (Para a)) f (pmap a (idA /\ idA) . out)
    where idA :: a -> a
          idA = id
 
 -- | Redefinition of apomorphisms as observable hylomorphisms.
-apoO :: (Mu b,Functor (PF b), FunctorO (PF b), Observable b, Typeable b) => b -> (a -> F b (Either a b)) -> a -> b
-apoO (b::b) f = hyloO (_L :: Apo b) (inn . pmap b (idB \/ idB)) f
+apoO :: (Mu b,Functor (PF b), FunctorO (PF b), Observable b, Typeable b) => Ann b -> (a -> F b (Either a b)) -> a -> b
+apoO (b::Ann b) f = hyloO (ann :: Ann (Apo b)) (inn . pmap b (idB \/ idB)) f
    where idB :: b -> b
          idB = id
 
 -- | Redefinition of zygomorphisms as observable hylomorphisms.
-zygoO :: (Mu a, Functor (PF a), FunctorO (PF a), Observable b, Typeable b, F a (a,b) ~ F (Zygo a b) a) => a -> (F a b -> b) -> (F (Zygo a b) b -> b) -> a -> b
-zygoO a g f = aux a (_L :: b) g f
-   where aux :: (Mu a,Functor (PF a), FunctorO (PF a),Observable b, Typeable b, F a (a,b) ~ F (Zygo a b) a) => a -> b -> (F a b -> b) -> (F (Zygo a b) b -> b) -> a -> b
-         aux (a::a) (b::b) g f = hyloO (_L :: Zygo a b) f (pmap a (id /\ cata a g) . out)
+zygoO :: (Mu a, Functor (PF a), FunctorO (PF a), Observable b, Typeable b, F a (a,b) ~ F (Zygo a b) a) => Ann a -> (F a b -> b) -> (F (Zygo a b) b -> b) -> a -> b
+zygoO a g f = aux a (ann :: Ann b) g f
+   where aux :: (Mu a,Functor (PF a), FunctorO (PF a),Observable b, Typeable b, F a (a,b) ~ F (Zygo a b) a) => Ann a -> Ann b -> (F a b -> b) -> (F (Zygo a b) b -> b) -> a -> b
+         aux (a::Ann a) (b::Ann b) g f = hyloO (ann :: Ann (Zygo a b)) f (pmap a (id /\ cata a g) . out)
 
 -- | Redefinition of accumulations as observable hylomorphisms.
-accumO :: (Mu a,Functor (PF d), FunctorO (PF d), Observable b, Typeable b) => d -> ((F a a,b) -> F d (a,b)) -> (F (Accum d b) c -> c) -> (a,b) -> c
-accumO (d::d) g f = hyloO (_L :: Accum d b) f ((g /\ snd) . (out >< id))
+accumO :: (Mu a,Functor (PF d), FunctorO (PF d), Observable b, Typeable b) => Ann d -> ((F a a,b) -> F d (a,b)) -> (F (Accum d b) c -> c) -> (a,b) -> c
+accumO (d::Ann d) g f = hyloO (ann :: Ann (Accum d b)) f ((g /\ snd) . (out >< id))
 
 -- | Redefinition of histomorphisms as observable hylomorphisms.
-histoO :: (Mu a,Functor (PF a), FunctorO (PF a), Observable a) => a -> (F a (Histo a c) -> c) -> a -> c
-histoO (a::a) g = fst . outH . cataO a (inn . (g /\ id))
+histoO :: (Mu a,Functor (PF a), FunctorO (PF a), Observable a) => Ann a -> (F a (Histo a c) -> c) -> a -> c
+histoO (a::Ann a) g = fst . outH . cataO a (inn . (g /\ id))
    where outH :: Histo a c -> F (Histo a c) (Histo a c)
          outH = out
 
 -- | Redefinition of futumorphisms as observable hylomorphisms.
-futuO :: (Mu b,Functor (PF b), FunctorO (PF b), Observable b) => b -> (a -> F b (Futu b a)) -> a -> b
-futuO (b::b) g = anaO b ((g \/ id) . out) . innF . inl
+futuO :: (Mu b,Functor (PF b), FunctorO (PF b), Observable b) => Ann b -> (a -> F b (Futu b a)) -> a -> b
+futuO (b::Ann b) g = anaO b ((g \/ id) . out) . innF . inl
    where innF :: F (Futu b a) (Futu b a) -> Futu b a
          innF = inn
 
 -- | Redefinition of dynamorphisms as observable hylomorphisms.
-dynaO :: (Mu b, Functor (PF b), FunctorO (PF b), Observable b) => b -> (F b (Histo b c) -> c) -> (a -> F b a) -> a -> c
-dynaO (b::b) g h = fst . outH . hyloO b (inn . (g /\ id)) h
+dynaO :: (Mu b, Functor (PF b), FunctorO (PF b), Observable b) => Ann b -> (F b (Histo b c) -> c) -> (a -> F b a) -> a -> c
+dynaO (b::Ann b) g h = fst . outH . hyloO b (inn . (g /\ id)) h
    where outH :: Histo b c -> F (Histo b c) (Histo b c)
          outH = out
 
 -- | Redefinition of chronomorphisms as observable hylomorphisms.
-chronoO :: (Mu c,Functor (PF c), FunctorO (PF c)) => c -> (F c (Histo c b) -> b) -> (a -> F c (Futu c a)) -> a -> b
-chronoO (c::c) g h = fst . outH . hyloO c (inn . (g /\ id)) ((h \/ id) . out) . innF . inl
+chronoO :: (Mu c,Functor (PF c), FunctorO (PF c)) => Ann c -> (F c (Histo c b) -> b) -> (a -> F c (Futu c a)) -> a -> b
+chronoO (c::Ann c) g h = fst . outH . hyloO c (inn . (g /\ id)) ((h \/ id) . out) . innF . inl
    where outH :: Histo c b -> F (Histo c b) (Histo c b)
          outH = out
          innF :: F (Futu c a) (Futu c a) -> (Futu c a)
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
@@ -34,29 +34,29 @@
 import Prelude hiding (Functor(..))
 
 -- | Definition of an hylomorphism
-hylo :: Functor (PF b) => b -> (F b c -> c) -> (a -> F b a) -> a -> c
+hylo :: Functor (PF b) => Ann b -> (F b c -> c) -> (a -> F b a) -> a -> c
 hylo b g h = g . pmap b (hylo b g h) . h
 
 -- | Definition of a catamorphism as an hylomorphism.
 --
 -- Catamorphisms model the fundamental pattern of iteration, where constructors for recursive datatypes are repeatedly consumed by arbitrary functions.
 -- They are usually called folds.
-cata :: (Mu a,Functor (PF a)) => a -> (F a b -> b) -> a -> b
+cata :: (Mu a,Functor (PF a)) => Ann a -> (F a b -> b) -> a -> b
 cata a f = hylo a f out
 
 -- | Recursive definition of a catamorphism.
-cataRec :: (Mu a,Functor (PF a)) => a -> (F a b -> b) -> a -> b
+cataRec :: (Mu a,Functor (PF a)) => Ann a -> (F a b -> b) -> a -> b
 cataRec a f = f . pmap a (cataRec a f) . out
 
 -- | Definition of an anamorphism as an hylomorphism.
 --
 --  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 :: (Mu b,Functor (PF b)) => Ann b -> (a -> F b a) -> a -> b
 ana b = hylo b inn
 
 -- | Recursive definition of an anamorphism.
-anaRec :: (Mu b,Functor (PF b)) => b -> (a -> F b a) -> a -> b
+anaRec :: (Mu b,Functor (PF b)) => Ann b -> (a -> F b a) -> a -> b
 anaRec b f = inn . pmap b (anaRec b f) . f
 
 -- | The functor of the intermediate type of a paramorphism is the functor of the consumed type 'a'
@@ -68,14 +68,14 @@
 -- Paramorphisms supply the gene of a catamorphism with a recursively computed copy of the input.
 --
 -- The first introduction to paramorphisms is reported in <http://www.cs.uu.nl/research/techreps/repo/CS-1990/1990-04.pdf>.
-para :: (Mu a,Functor (PF a)) => a -> (F a (b,a) -> b) -> a -> b
-para (a::a) f = hylo (_L :: Para a) f (pmap a (idA /\ idA) . out)
+para :: (Mu a,Functor (PF a)) => Ann a -> (F a (b,a) -> b) -> a -> b
+para (a::Ann a) f = hylo (ann :: Ann (Para a)) f (pmap a (idA /\ idA) . out)
    where idA :: a -> a
          idA = id
 
 -- | Recursive definition of a paramorphism.
-paraRec :: (Mu a,Functor (PF a)) => a -> (F a (b,a) -> b) -> a -> b
-paraRec (a::a) f = f . pmap a (paraRec a f >< idA) . pmap a (idA /\ idA) . out
+paraRec :: (Mu a,Functor (PF a)) => Ann a -> (F a (b,a) -> b) -> a -> b
+paraRec (a::Ann a) f = f . pmap a (paraRec a f >< idA) . pmap a (idA /\ idA) . out
    where idA :: a -> a
          idA = id
 
@@ -88,14 +88,14 @@
 -- 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
-apo (b::b) f = hylo (_L :: Apo b) (inn . pmap b (idB \/ idB)) f
+apo :: (Mu b,Functor (PF b)) => Ann b -> (a -> F b (Either a b)) -> a -> b
+apo (b::Ann b) f = hylo (ann :: Ann (Apo b)) (inn . pmap b (idB \/ idB)) f
    where idB :: b -> b
          idB = id
 
 -- | 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 :: (Mu b,Functor (PF b)) => Ann b -> (a -> F b (Either a b)) -> a -> b
+apoRec (b::Ann b) f = inn . pmap b (idB \/ idB) . pmap b (apoRec b f -|- idB) . f
    where idB :: b -> b
          idB = id
 
@@ -107,10 +107,10 @@
 -- Zygomorphisms were introduced in <http://dissertations.ub.rug.nl/faculties/science/1990/g.r.malcolm/>.
 --
 -- They can be seen as the asymmetric form of mutual iteration, where both a data consumer and an auxiliary function are defined (<http://www.fing.edu.uy/~pardo/papers/njc01.ps.gz>).
-zygo :: (Mu a, Functor (PF a),F a (a,b) ~ F (Zygo a b) a) => a -> (F a b -> b) -> (F (Zygo a b) b -> b) -> a -> b
-zygo a g f = aux a (_L :: b) g f
-   where aux :: (Mu a,Functor (PF a),F a (a,b) ~ F (Zygo a b) a) => a -> b -> (F a b -> b) -> (F (Zygo a b) b -> b) -> a -> b
-         aux (a::a) (b::b) g f = hylo (_L :: Zygo a b) f (pmap a (id /\ cata a g) . out)
+zygo :: (Mu a, Functor (PF a),F a (a,b) ~ F (Zygo a b) a) => Ann a -> (F a b -> b) -> (F (Zygo a b) b -> b) -> a -> b
+zygo a g f = aux a (ann :: Ann b) g f
+   where aux :: (Mu a,Functor (PF a),F a (a,b) ~ F (Zygo a b) a) => Ann a -> Ann b -> (F a b -> b) -> (F (Zygo a b) b -> b) -> a -> b
+         aux (a::Ann a) (b::Ann b) g f = hylo (ann :: Ann (Zygo a b)) f (pmap a (id /\ cata a g) . out)
 
 -- | In accumulations we add an extra annotation 'b' to the base functor of type 'a'.
 type Accum a b = a :*!: K b
@@ -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 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))
+accum :: (Mu a,Functor (PF a)) => Ann a -> (F (Accum a b) c -> c) -> ((F a a,b) -> F a (a,b)) -> (a,b) -> c
+accum (a::Ann a) f g = hylo (ann :: Ann (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
@@ -130,8 +130,8 @@
 --
 -- Histomorphisms (<http://cs.ioc.ee/~tarmo/papers/inf.ps.gz>) capture the powerfull schemes of course-of-value iteration, and differ from catamorphisms for being able to apply the gene function at a deeper depth of recursion.
 -- In other words, they allow to reuse sub-sub constructor results.
-histo :: (Mu a,Functor (PF a)) => a -> (F a (Histo a c) -> c) -> a -> c
-histo (a::a) g = fst . outH . cata a (inn . (g /\ id))
+histo :: (Mu a,Functor (PF a)) => Ann a -> (F a (Histo a c) -> c) -> a -> c
+histo (a::Ann a) g = fst . outH . cata a (inn . (g /\ id))
    where outH :: Histo a c -> F (Histo a c) (Histo a c)
          outH = out
 
@@ -151,8 +151,8 @@
 -- Futumorphisms are the dual of histomorphisms and are proposed as 'cocourse-of-argument' coiterators by their creators (<http://cs.ioc.ee/~tarmo/papers/inf.ps.gz>).
 --
 -- In the same fashion as histomorphisms, it allows to seed the gene with multiple levels of depth instead of having to do 'all at once' with an anamorphism.
-futu :: (Mu b,Functor (PF b)) => b -> (a -> F b (Futu b a)) -> a -> b
-futu (b::b) g = ana b ((g \/ id) . out) . innF . inl
+futu :: (Mu b,Functor (PF b)) => Ann b -> (a -> F b (Futu b a)) -> a -> b
+futu (b::Ann b) g = ana b ((g \/ id) . out) . innF . inl
    where innF :: F (Futu b a) (Futu b a) -> Futu b a
          innF = inn
 
@@ -171,8 +171,8 @@
 -- Instead of following the recursion pattern of the input via structural recursion (as in histomorphisms),
 -- dynamorphisms allow us to reuse the annotated structure in a bottom-up approach and avoiding rebuilding
 -- it every time an annotation is needed, what provides a more efficient dynamic algorithm.
-dyna :: (Mu b, Functor (PF b)) => b -> (F b (Histo b c) -> c) -> (a -> F b a) -> a -> c
-dyna (b::b) g h = fst . outH . hylo b (inn . (g /\ id)) h
+dyna :: (Mu b, Functor (PF b)) => Ann b -> (F b (Histo b c) -> c) -> (a -> F b a) -> a -> c
+dyna (b::Ann b) g h = fst . outH . hylo b (inn . (g /\ id)) h
    where outH :: Histo b c -> F (Histo b c) (Histo b c)
          outH = out
 
@@ -184,8 +184,8 @@
 --
 -- The notion of chronomorphism is a recent recursion pattern (at least known as such).
 -- The first and single reference available is <http://comonad.com/reader/2008/time-for-chronomorphisms/>.
-chrono :: (Mu c,Functor (PF c)) => c -> (F c (Histo c b) -> b) -> (a -> F c (Futu c a)) -> a -> b
-chrono (c::c) g h = fst . outH . hylo c (inn . (g /\ id)) ((h \/ id) . out) . innF . inl
+chrono :: (Mu c,Functor (PF c)) => Ann c -> (F c (Histo c b) -> b) -> (a -> F c (Futu c a)) -> a -> b
+chrono (c::Ann c) g h = fst . outH . hylo c (inn . (g /\ id)) ((h \/ id) . out) . innF . inl
    where outH :: Histo c b -> F (Histo c b) (Histo c b)
          outH = out
          innF :: F (Futu c a) (Futu c a) -> (Futu c a)
@@ -197,7 +197,7 @@
 --
 -- After expanding the definitions of '.', '/\' and 'app' we see that this corresponds to the expected pointwise equation @'fix' f = f ('fix' f)@.
 fix :: (a -> a) -> a
-fix = hylo (_L :: K (a -> a) :*!: I) app (id /\ id)
+fix = hylo (ann :: Ann (K (a -> a) :*!: I)) app (id /\ id)
 
 -- | The combinator for isomorphic type transformations.
 --