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.6
+Version:         0.0.7
 License:         BSD3
 License-file:    LICENSE
 Author:          Alcino Cunha <alcino@di.uminho.pt>, Hugo Pacheco <hpacheco@di.uminho.pt>
@@ -27,6 +27,7 @@
   exposed-modules:
         Generics.Pointless.Combinators
         Generics.Pointless.Functors,
+        Generics.Pointless.HFunctors,
         Generics.Pointless.Fctrable,
         Generics.Pointless.RecursionPatterns,
         Generics.Pointless.Observe.Functors,
@@ -37,4 +38,4 @@
         Generics.Pointless.Bifunctors,
         Generics.Pointless.Bifctrable
 
-  extensions: TypeFamilies, TypeOperators, ScopedTypeVariables, UndecidableInstances, FlexibleInstances, FlexibleContexts, DeriveDataTypeable, EmptyDataDecls, GADTs
+  extensions: TypeFamilies, TypeOperators, ScopedTypeVariables, UndecidableInstances, FlexibleInstances, FlexibleContexts, DeriveDataTypeable, EmptyDataDecls, GADTs, Rank2Types
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
@@ -1,4 +1,3 @@
-
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Generics.Pointless.Functors
diff --git a/src/Generics/Pointless/HFunctors.hs b/src/Generics/Pointless/HFunctors.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Pointless/HFunctors.hs
@@ -0,0 +1,143 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Pointless.HFunctors
+-- Copyright   :  (c) 2011 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 higher-order functor.
+--
+-----------------------------------------------------------------------------
+
+module Generics.Pointless.HFunctors where
+
+import Generics.Pointless.Combinators
+import Generics.Pointless.Functors
+
+import Prelude hiding (Functor(..))
+import Data.Monoid
+
+-- | The type of natural transformations
+infixr 8 :~>
+type s :~> v = forall a. s a -> v a
+
+-- * Higher-order functors
+
+-- | Identity higher-order functor
+newtype Functor f => HId (f :: * -> *) a = IdH {unIdH :: f a}
+
+-- | Constant higher-order functor
+newtype HConst c (f :: * -> *) a = ConsH {unConsH :: c}
+
+-- | Parameter higher-order functor
+newtype HParam (f :: * -> *) a = HPar {unParH :: a}
+
+newtype Functor g => HFun (g :: * -> *) (f :: * -> *) a = HFun {unFunH :: g a}
+
+-- | Sum higher-order functor
+infixr 5 :+~:
+data ((g :: (* -> *) -> (* -> *)) :+~: (h :: (* -> *) -> (* -> *))) (f :: * -> *) a = InlH (g f a) | InrH (h f a)
+
+-- | Product higher-order functor
+infixr 6 :*~:
+data ((g :: (* -> *) -> (* -> *)) :*~: (h :: (* -> *) -> (* -> *))) (f :: * -> *) a = ProdH (g f a) (h f a)
+
+-- | Composition of a regular functor with an higher-order functor
+infixr 9 :@~:
+data ((g :: * -> *) :@~: (h :: (* -> *) -> (* -> *))) (f :: * -> *) a = CompH {unCompH :: g (h f a)}
+
+-- | The fixpoint of an higher-order functor is a regular functor
+newtype HFix (f :: (* -> *) -> (* -> *)) a = HInn { hOut :: (HRep f (HFix f)) a }
+
+-- | Annotations of higher-order functors, only to provide type-level information to the compiler
+data AnnH (f :: (* -> *) -> (* -> *))
+
+-- * Application of higher-order functors to a regular functor
+type family HRep (g :: (* -> *) -> (* -> *)) (f :: * -> *) :: * -> *
+
+type instance HRep HId f = f
+type instance HRep (HConst c) f = Const c
+type instance HRep HParam f = Id
+type instance HRep (HFun g) f = g
+type instance HRep (g :+~: h) f = HRep g f :+: HRep h f
+type instance HRep (g :*~: h) f = HRep g f :*: HRep h f
+type instance HRep (g :@~: h) f = g :@: HRep h f
+
+-- * Functor composition as the fixpoint of an higher-order functor (using the fixpoint of the first functor)
+
+type family App (f :: (* -> *) -> (* -> *)) (g :: * -> *) :: (* -> *) -> (* -> *)
+type instance App HId g = HId
+type instance App (HConst t) g = HConst t
+type instance App HParam g = HFun g
+type instance App (HFun h) g = HFun (h :@: g)
+type instance App (f :*~: g) h = App f h :*~: App g h
+type instance App (f :+~: g) h = App f h :+~: App g h
+type instance App (f :@~: g) h = f :@~: (App g h)
+
+type instance HF (f :@: g) = App (HF f) g
+
+-- * User-defined polymorphic types as fixed points of higher-order functors
+
+type family HF (t :: * -> *) :: (* -> *) -> (* -> *)
+type H t a = HRep (HF t) a
+
+class Hu (t :: * -> *) where
+    hinn :: (H t t) a -> t a
+    hout :: t a -> (H t t) a
+
+type instance HF [] = HConst One :+~: HParam :*~: HId
+instance Hu [] where
+    hout [] = InlF $ ConsF _L
+    hout (x:xs) = InrF $ ProdF (IdF x) xs
+    hinn (InlF (ConsF _)) = []
+    hinn (InrF (ProdF (IdF x) xs)) = x:xs
+
+type instance HF (HFix f) = f
+instance Hu (HFix f) where
+    hinn = HInn
+    hout = hOut
+
+-- * Foldable higher-order functors
+
+-- | Polymorphic monoid class
+class FMonoid f where
+    fzero :: f a
+    fplus :: f a -> f a -> f a
+
+instance (FMonoid f,FMonoid g) => FMonoid (f :*: g) where
+    fzero = ProdF fzero fzero
+    fplus (ProdF x1 x2) (ProdF y1 y2) = ProdF (fplus x1 y1) (fplus x2 y2)
+
+instance FMonoid f => FMonoid (f :@: g) where
+    fzero = CompF fzero
+    fplus (CompF x) (CompF y) = CompF (fplus x y)
+
+instance FMonoid [] where
+    fzero = mempty
+    fplus = mappend
+
+class HFoldable f where
+    reduce :: FMonoid g => AnnH f -> (HRep f g) :~> g
+    reduce' :: FMonoid g => AnnH f -> Ann (Fix g) -> (HRep f g) :~> g
+    reduce' annf anns = reduce annf
+
+instance HFoldable HId where
+    reduce _ ga = ga
+instance HFoldable (HConst a) where
+    reduce _ x = fzero
+instance HFoldable HParam where
+    reduce _ x = fzero
+instance HFoldable (HFun g) where
+    reduce _ x = fzero
+instance (HFoldable f,HFoldable g) => HFoldable (f :+~: g) where
+    reduce (_::AnnH (f :+~: g)) (InlF x) = reduce (ann::AnnH f) x
+    reduce (_::AnnH (f :+~: g)) (InrF y) = reduce (ann::AnnH g) y
+instance (HFoldable f,HFoldable g) => HFoldable (f :*~: g) where
+    reduce (_::AnnH (f :*~: g)) (ProdF x y) = reduce (ann::AnnH f) x `fplus` reduce (ann::AnnH g) y
+    
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
@@ -202,4 +202,4 @@
 -- | The combinator for isomorphic type transformations.
 --
 -- It can translate between types that share the same functor.
-nu d = (inn . pmap d nu . out) d
+nu d = inn . pmap d (nu d) . out