diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,31 @@
+Copyright (c) 2009, University of Minho
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * The names of contributors may not be used to endorse or promote
+      products derived from this software without specific prior
+      written permission. 
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,33 @@
+Pointless Lenses
+
+This cabal package can be installed with:
+
+$ cabal install pointless-lenses
+
+For a manual install, execute:
+
+$ runhaskell Setup.lhs configure
+$ runhaskell Setup.lhs build
+$ runhaskell Setup.lhs install
+
+You can now start playing with the example code that comes with the library, under Language.Pointless.Examples.Examples.
+The easiest way is to create a new module that imports some library modules
+
+module Test where
+
+import Test.QuickCheck.Test
+import Generics.Pointless.Lenses
+import Generics.Pointless.Lenses.Examples.Examples
+
+and interpret it
+
+$ ghci Test.hs
+
+We can now test the well-behavedness of some lens, for example:
+
+> quickCheck (wb filter_lns)
++++ OK, passed 100 tests.
+
+Or run some example and later check what it is actually doing:
+> exampleT
+Fst (1,'a')
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,3 @@
+#!/usr/bin/env runhaskell
+> import Distribution.Simple
+> main = defaultMain
diff --git a/Test.hs b/Test.hs
new file mode 100644
--- /dev/null
+++ b/Test.hs
@@ -0,0 +1,5 @@
+module Test where
+
+import Test.QuickCheck.Test
+import Generics.Pointless.Lenses
+import Generics.Pointless.Lenses.Examples.Examples
diff --git a/pointless-lenses.cabal b/pointless-lenses.cabal
new file mode 100644
--- /dev/null
+++ b/pointless-lenses.cabal
@@ -0,0 +1,31 @@
+Name:            pointless-lenses
+Version:         0.0.1
+License:         BSD3
+License-file:    LICENSE
+Author:          Alcino Cunha <alcino@di.uminho.pt>, Hugo Pacheco <hpacheco@di.uminho.pt>
+Maintainer:      Hugo Pacheco <hpacheco@di.uminho.pt>
+Synopsis:        Pointless Lenses library
+Description:
+	Pointless Lenses is library of bidirectional lenses (<http://www.cis.upenn.edu/~bcpierce/papers/newlenses-popl.pdf>) defined in the point-free style of programming.
+	Generic bidirectional lenses can be defined over inductive types by relying in a set of lifted lens combinators from the standard point-free combinators.
+	Virtually any recursive lens can be defined by combining the lenses for the recursion patterns of catamorphisms and anamorphism.
+	The library also provides QuickCheck procedures to test the well-behavedness of user-defined lens transformations.
+Homepage:        http://haskell.di.uminho.pt/wiki/Pointless+Lenses
+
+Category: Generics
+
+extra-source-files: README, Test.hs
+
+Build-type: Simple
+Cabal-Version:  >= 1.2.3
+
+Library
+  Hs-Source-Dirs: src
+  Build-Depends:        base >= 3 && < 5, pointless-haskell >= 0.0.2, haskell98, process
+  exposed-modules:
+        Generics.Pointless.Lenses.Combinators
+        Generics.Pointless.Lenses.RecursionPatterns,
+        Generics.Pointless.Lenses.Reader.RecursionPatterns
+        Generics.Pointless.Lenses.Examples.Examples
+
+  extensions: ScopedTypeVariables, FlexibleContexts, Rank2Types, TypeOperators, TypeFamilies
diff --git a/src/Generics/Pointless/Lenses/Combinators.hs b/src/Generics/Pointless/Lenses/Combinators.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Pointless/Lenses/Combinators.hs
@@ -0,0 +1,181 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Pointless.Lenses.Combinators
+-- Copyright   :  (c) 2009 University of Minho
+-- License     :  BSD3
+--
+-- Maintainer  :  hpacheco@di.uminho.pt
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Pointless Lenses:
+-- bidirectional lenses with point-free programming
+-- 
+-- This module lifts a standard set of point-free combinators into bidirectional lenses.
+--
+-----------------------------------------------------------------------------
+
+module Generics.Pointless.Lenses.Combinators where
+
+import Generics.Pointless.Lenses
+import Generics.Pointless.Combinators
+
+-- * Point-free lens combinators
+
+-- | The right exponentiation combinator as a lens.
+-- Applies a lens to the domain of a function.
+rexp_lns :: Lens b c -> Lens (a -> b) (a -> c)
+rexp_lns l = Lens get' put' create'
+    where get' = curry (get l . app)
+          put' = curry ((put l) . app . (split >< id))
+          create' = curry (create l . app)
+
+-- | The lens composition operator.
+infixr 9 .<
+(.<) :: Lens b a -> Lens c b -> Lens c a
+(.<) f g = Lens get' put' create'
+    where get' = get f . get g
+          put' = put g . (put f . (id >< get g) /\ snd)
+          create' = create g . create f
+
+-- | The @fst@ point-free combinator.
+fst_lns :: b -> Lens (a,b) a
+fst_lns b = Lens get' put' create'
+    where get' = fst
+          put' = id >< snd
+          create' = id /\ (b!)
+
+-- | The @snd@ point-free combinator.
+snd_lns :: a -> Lens (a,b) b
+snd_lns a = Lens get' put' create'
+    where get' = snd
+          put' = swap . (id >< fst)
+          create' = (a!) /\ id
+
+-- | The @><@ point-free combinator.
+infix 7 ><<
+(><<) :: Lens c a -> Lens d b -> Lens (c,d) (a,b)
+(><<) f g = Lens get' put' create'
+    where get' = get f >< get g
+          put' = (put f >< put g) . distp
+          create' = create f >< create g
+
+-- | The left-biased @\/@ point-free combinator.
+-- It chooses left values over right values in the @create@ direction.
+infix 4 .\/<
+(.\/<) :: Lens a c -> Lens b c -> Lens (Either a b) c
+(.\/<) f g = Lens get' put' create'
+    where get' = get f \/ get g
+          put' = (put f -|- put g) . distr
+          create' = inl . create f
+
+-- | The right-biased @\/@ point-free combinator.
+-- It chooses right values over left values in the @create@ direction.
+infix 4 \/.<
+(\/.<) :: Lens a c -> Lens b c -> Lens (Either a b) c
+(\/.<) f g = Lens get' put' create'
+    where get' = get f \/ get g
+          put' = (put f -|- put g) . distr
+          create' = inr . create g
+
+-- | The @-|-@ point-free combinator.
+infix 5 -|-<
+(-|-<) :: Lens c a -> Lens d b -> Lens (Either c d) (Either a b)
+(-|-<) f g = Lens get' put' create'
+    where get' = get f -|- get g
+          put' = ((put f \/ create f . fst) -|- (create g . fst \/ put g)) . dists
+          create' = create f -|- create g
+
+-- | The @-|-@ point-free combinator with user-defined backward behavior.
+sum_lns :: ((a,d) -> c) -> ((b,c) -> d) -> Lens c a -> Lens d b -> Lens (Either c d) (Either a b)
+sum_lns h i f g = Lens get' put' create'
+    where get' = get f -|- get g
+          put' = (put f -|- put g) . ((id \/ (fst /\ h)) -|- ((fst /\ i) \/ id)) . dists
+          create' = create f -|- create g
+
+-- | The @pnt@ point-free combinator.
+infix 0 !<
+(!<) :: c -> Lens c One
+(!<) c = Lens get' put' create'
+    where get' = bang
+          put' = snd
+          create' = (c!)
+
+-- | The @(a!) \/ f@ point-free expression, where @a@ is a constant and @f@ a function.
+infix 4 !\/<
+(!\/<) :: Eq a => a -> Lens c a -> Lens (Either c b) a
+(!\/<) a f = Lens get' put' create'
+    where get' = get f \/ (a!)
+          put' = (inl \/ coswap) . (id -|- (snd -|- create f . fst)) . (put f -|- (((==a) . fst)?)) . distr
+          create' = inl . create f
+
+-- | The @f \/ (a!)@ point-free expression, where @a@ is a constant and @f@ a function.
+infix 4 \/!<
+(\/!<) :: Eq a => a -> Lens b a -> Lens (Either c b) a
+(\/!<) a f = Lens get' put' create'
+    where get' = (a!) \/ get f
+          put' = (id \/ inr) . ((snd -|- create f . fst) -|- id) . ((((==a) . fst)?) -|- put f) . distr
+          create' = inr . create f
+
+-- * Point-free isomorphism combinators
+
+-- | The lens identity combinator.
+id_lns :: Lens c c
+id_lns = Lens id fst id
+
+-- | The product distribution combinator
+distp :: ((c,d),(a,b)) -> ((c,a),(d,b))
+distp = fst >< fst /\ snd >< snd
+
+-- | The @distp@ point-free combinator.
+distp_lns :: Lens ((c,d),(a,b)) ((c,a),(d,b))
+distp_lns = Lens distp (distp . fst) distp
+
+-- | The sum distribution combinator.
+dists :: (Either a b,Either c d) -> Either (Either (a,c) (a,d)) (Either (b,c) (b,d))
+dists = (distr -|- distr) . distl
+
+-- | The @dists@ point-free combinator.
+dists_lns :: Lens (Either a b,Either c d) (Either (Either (a,c) (a,d)) (Either (b,c) (b,d)))
+dists_lns = (distr_lns -|-< distr_lns) .< distl_lns
+
+-- | The @swap@ point-free combinator.
+swap_lns :: Lens (a,b) (b,a)
+swap_lns = Lens swap (swap . fst) swap
+
+-- | The @coswap@ point-free combinator
+coswap_lns :: Lens (Either a b) (Either b a)
+coswap_lns = Lens coswap (coswap . fst) coswap
+
+-- | The @distl@ point-free combinator.
+distl_lns :: Lens (Either a b, c) (Either (a,c) (b,c))
+distl_lns = Lens distl (undistl . fst) undistl
+
+-- | The @undistl@ point-free combinator.
+undistl_lns :: Lens (Either (a,c) (b,c)) (Either a b, c)
+undistl_lns = Lens undistl (distl . fst) distl
+
+-- | The @distr@ point-free combinator.
+distr_lns :: Lens (c, Either a b) (Either (c,a) (c,b))
+distr_lns = Lens distr (undistr . fst) undistr
+
+-- | The @undistr@ point-free combinator.
+undistr_lns :: Lens (Either (c,a) (c,b)) (c, Either a b)
+undistr_lns = Lens undistr (distr . fst) distr
+
+-- | The @assocl@ point-free combinator.
+assocl_lns :: Lens (a,(b,c)) ((a,b),c)
+assocl_lns = Lens assocl (assocr . fst) assocr
+
+-- | The @assocr@ point-free combinator.
+assocr_lns :: Lens ((a,b),c) (a,(b,c))
+assocr_lns = Lens assocr (assocl . fst) assocl
+
+-- | The @coassocl@ point-free combinator.
+coassocl_lns :: Lens (Either a (Either b c)) (Either (Either a b) c)
+coassocl_lns = Lens coassocl (coassocr . fst) coassocr
+
+-- | The @coassocr@ point-free combinator.
+coassocr_lns :: Lens (Either (Either a b) c) (Either a (Either b c))
+coassocr_lns = Lens coassocr (coassocl . fst) coassocl
+
diff --git a/src/Generics/Pointless/Lenses/Examples/Examples.hs b/src/Generics/Pointless/Lenses/Examples/Examples.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Pointless/Lenses/Examples/Examples.hs
@@ -0,0 +1,68 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Pointless.Lenses.Examples.Examples
+-- Copyright   :  (c) 2009 University of Minho
+-- License     :  BSD3
+--
+-- Maintainer  :  hpacheco@di.uminho.pt
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Pointless Lenses:
+-- bidirectional lenses with point-free programming
+-- 
+-- This module provides examples, examples and more examples.
+--
+-----------------------------------------------------------------------------
+
+module Generics.Pointless.Lenses.Examples.Examples where
+
+import Generics.Pointless.Combinators
+import Generics.Pointless.Functors
+import Generics.Pointless.Fctrable
+import Generics.Pointless.Bifunctors
+import Generics.Pointless.Bifctrable
+import Generics.Pointless.Lenses
+import Generics.Pointless.Lenses.Combinators
+import Generics.Pointless.Lenses.RecursionPatterns
+import Generics.Pointless.Lenses.Reader.RecursionPatterns
+
+-- | List length lens.
+length_lns :: a -> Lens [a] Nat
+length_lns a = nat_lns _L (\x -> id_lns -|-< snd_lns a)
+
+-- | List zipping lens.
+-- The aux transformation is merely for simplifying the constant argument
+zip_lns :: Either (Either One (b,[b])) (a,[a]) -> Lens ([a],[b]) [(a,b)]
+zip_lns c = ana_lns _L (((!<) c .< aux -|-< distp_lns) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns))
+    where aux = (fst_lns _L -|-< snd_lns _L) -|-< fst_lns _L
+
+-- | List filtering lens.
+-- The argument passed to @snd_lns@ can be undefined because it will never be used
+filter_lns :: Lens [Either a b] [a]
+filter_lns = cata_lns _L ((inn_lns .\/< snd_lns _L) .< coassocl_lns .< (id_lns -|-< distl_lns))
+
+-- | List mapping lens.
+map_lns :: Lens c a -> Lens [c] [a]
+map_lns f = nat_lns _L (\x -> id_lns -|-< f ><< id_lns)
+
+-- | Generic mapping example using user-defined concrete generators
+data T a = Fst a | Next (T a) deriving (Eq,Show)
+
+type instance BF T = BPar :+| BId
+type instance PF (T a) = Const a :+: Id
+
+instance Mu (T a) where
+    inn (Left x) = Fst x
+    inn (Right x) = Next x
+    out (Fst x) = Left x
+    out (Next x) = Right x
+
+aux :: T a -> a
+aux (Fst x) = x
+aux (Next x) = aux x
+
+tmap_lns l = gmap_lns' (aux . snd) snd l
+
+exampleT = put (tmap_lns (fst_lns 'c')) (Fst 1,(Next (Fst (2,'a'))))
+
diff --git a/src/Generics/Pointless/Lenses/Reader/RecursionPatterns.hs b/src/Generics/Pointless/Lenses/Reader/RecursionPatterns.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Pointless/Lenses/Reader/RecursionPatterns.hs
@@ -0,0 +1,137 @@
+
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Pointless.Lenses.Reader.RecursionPatterns
+-- Copyright   :  (c) 2009 University of Minho
+-- License     :  BSD3
+--
+-- Maintainer  :  hpacheco@di.uminho.pt
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Pointless Lenses:
+-- bidirectional lenses with point-free programming
+-- 
+-- This module provides catamorphism and anamorphism bidirectional combinators for the definition of recursive lenses.
+-- The implementations use a monad reader so that each lens combinator permits a more flexible environment.
+--
+-----------------------------------------------------------------------------
+
+module Generics.Pointless.Lenses.Reader.RecursionPatterns where
+
+import Prelude hiding (Functor(..),fmap)
+import Control.Monad hiding (Functor(..),fmap)
+import Control.Monad.Instances hiding (Functor(..),fmap)
+import Generics.Pointless.Combinators
+import Generics.Pointless.MonadCombinators
+import Generics.Pointless.Functors
+import Generics.Pointless.Fctrable
+import Generics.Pointless.Bifunctors
+import Generics.Pointless.Bifctrable
+import Generics.Pointless.RecursionPatterns
+import Generics.Pointless.Lenses
+import Generics.Pointless.Lenses.Combinators
+import Generics.Pointless.Lenses.RecursionPatterns
+
+-- | The functor mapping function @fmap@ as a more relaxed lens.
+-- The extra function allows user-defined behavior when creating default concrete F-values.
+fmap_lns' :: Fctrable f => Fix f -> ((a,Rep f c) -> c) -> Lens c a -> Lens (Rep f c) (Rep f a)
+fmap_lns' (f::Fix f) h l = Lens get' put' create'
+    where get' = fmap f (get l)
+          put' = fmap f (put l) . uncurry (fzip' (fctr :: Fctr f) h) . (id /\ snd)
+          create' = fmap f (create l)
+
+-- | The polytypic functor zipping combinator.
+-- Gives preference to the abstract (first) F-structure.
+fzip' :: Fctr f -> ((a,e) -> c) -> (Rep f a,Rep f c) -> (e -> Rep f (a,c))
+fzip' I create = return
+fzip' K create = return . fst
+fzip' (f :*!: g) create = (fzip' f create >|< fzip' g create) . distp
+fzip' (f :+!: g) create = (l -||- r) . dists
+    where l = fzip' f create \/ fcre' f create . fst
+          r = fcre' g create . fst \/ fzip' g create
+
+-- | The polytypic auxiliary function for @fzip'@.
+-- Similar to @fmap (id /\ create)@ but using a monad reader for the concrete reconstruction function.
+fcre' :: Fctr f -> ((a,e) -> c) -> Rep f a -> (e -> Rep f (a,c))
+fcre' I create = return /|\ curry create
+fcre' K create = return
+fcre' (f :*!: g) create = fcre' f create >|< fcre' g create
+fcre' (f :+!: g) create = fcre' f create -||- fcre' g create
+
+-- | The @ana@ recursion pattern as a more relaxed lens.
+-- For @ana_lns'@ to be a well-behaved lens, we MUST prove termination of |get| for each instance.
+ana_lns' :: (Mu b,Fctrable (PF b)) => ((b,a) -> a) -> Lens a (F b a) -> Lens a b
+ana_lns' (h::(b,a) -> a) l = Lens get' put' create'
+    where get' = ana b (get l)
+          put' = accum b  (put l) (uncurry gene)
+          gene = fzip' g h <=< curry (id >< get l)
+          create' = cata b (create l)
+          b = _L :: b
+          g = fctr :: Fctr (PF b)
+
+-- | The @cata@ recursion pattern as a more relaxed lens.
+-- For @cata_lns'@ to be a well-behaved lens, we MUST prove termination of |put| and |create| for each instance.
+cata_lns' :: (Mu a,Fctrable (PF a)) => ((b,a) -> a) -> (Lens (F a b) b) -> Lens a b
+cata_lns' (h::(b,a) -> a) l = Lens get' put' create'
+    where get' = cata a (get l)
+          put' = ana a (uncurry gene)
+          gene = fzip' f h <=< (lexp (fmap (fixF f) get' . out) . curry (put l) /|\ const out)
+          create' = ana a (create l)
+          a = _L :: a
+          f = fctr :: Fctr (PF a)
+
+-- | A more relaxed version of the recursion pattern for recursive functions that can be expressed both as anamorphisms and catamorphisms.
+-- Proofs of termination are dismissed.
+nat_lns' :: (Mu a,Mu b,Fctrable (PF b)) => ((b,a) -> a) -> NatLens (PF a) (PF b) -> Lens a b
+nat_lns' (h::(b,a) -> a) l = ana_lns' h (l a .< out_lns)
+    where a = _L :: a
+
+-- | A more relaxed version of the bifunctor mapping function @bmap@ as a lens.
+-- Cannot employ @NatLens@ because the extra function depends on the polymorphic type argument.
+bmap_lns' :: Bifctrable f => x -> BFix f -> ((a,Rep (BRep f c) x) -> c) -> Lens c a -> Lens (Rep (BRep f c) x) (Rep (BRep f a) x)
+bmap_lns' (x::x) (f::BFix f) h l = Lens get' put' create'
+    where get' = bmap f (get l) idx
+          put' = bmap f (put l) idx . uncurry (bzip' x (bctr :: Bifctr f) h) . (id /\ snd)
+          create' = bmap f (create l) idx
+          idx = id :: x -> x
+
+-- | A more relaxed version of the the polytypic bifunctor zipping combinator.
+bzip' :: x -> Bifctr f -> ((a,e) -> c) -> (Rep (BRep f a) x,Rep (BRep f c) x) -> (e -> Rep (BRep f (a,c)) x)
+bzip' x BI create = return . fst
+bzip' x BP create = return
+bzip' x BK create = return . fst
+bzip' x (f :*!| g) create = (bzip' x f create >|< bzip' x g create) . distp
+bzip' (x::x) (f :+!| g) create = (l -||- r) . dists
+    where l = bzip' x f create \/ bcre' x f create . fst
+          r = bcre' x g create . fst \/ bzip' x g create
+          idx = id :: x -> x
+
+bcre' :: x -> Bifctr f -> ((a,e) -> c) -> Rep (BRep f a) x -> (e -> (Rep (BRep f (a,c)) x))
+bcre' x BI create = return
+bcre' x BP create = return /|\ curry create
+bcre' x BK create = return
+bcre' x (f :*!| g) create = bcre' x f create >|< bcre' x g create
+bcre' x (f :+!| g) create = bcre' x f create -||- bcre' x g create
+
+-- | A more relaxed version of the generic mapping lens for parametric types with one polymorphic parameter.
+-- We do not define @gmap_lns'@ as a recursion pattern lens because we want to provide more control in the auxiliary functions.
+-- Using @bmap_lns'@ we would not get @(a,d c) -> c@ but instead @(a,B d c (d a)) -> c@.
+gmap_lns' :: (Mu (d a),Mu (d c),Fctrable (PF (d c)),Fctrable (PF (d a)),Bifctrable (BF d),
+              F (d a) (d c) ~ B d a (d c), F (d c) (d c) ~ B d c (d c),
+              F (d a) (d a) ~ B d a (d a),F (d c) (d a) ~ B d c (d a))
+          => ((a,d c) -> c) -> ((d a,d c) -> d c) -> Lens c a -> Lens (d c) (d a)
+gmap_lns' (h::(a,d c) -> c) i l = Lens get' put' create'
+    where get' = cata dc (inn . bmap (fixB b) (get l) idda)
+          put' = accum da gene (uncurry tau)
+          gene = inn . bmap (fixB b) (put l) iddc . uncurry (bzip' dc b h <=< curry (id >< out))
+          tau = fzip' f i <=< curry (id >< bmap (fixB b) (get l) iddc . out)
+          create' = cata da (inn . bmap (fixB b) (create l) iddc)
+          b = bctr :: Bifctr (BF d)
+          f = fctr :: Fctr (PF (d a))
+          da = _L :: d a
+          dc = _L :: d c
+          idda = id :: d a -> d a
+          iddc = id :: d c -> d c
+
+
diff --git a/src/Generics/Pointless/Lenses/RecursionPatterns.hs b/src/Generics/Pointless/Lenses/RecursionPatterns.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Pointless/Lenses/RecursionPatterns.hs
@@ -0,0 +1,112 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Generics.Pointless.Lenses.RecursionPatterns
+-- Copyright   :  (c) 2009 University of Minho
+-- License     :  BSD3
+--
+-- Maintainer  :  hpacheco@di.uminho.pt
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Pointless Lenses:
+-- bidirectional lenses with point-free programming
+-- 
+-- This module provides catamorphism and anamorphism bidirectional combinators for the definition of recursive lenses.
+--
+-----------------------------------------------------------------------------
+
+module Generics.Pointless.Lenses.RecursionPatterns where
+
+import Prelude hiding (Functor(..),fmap)
+
+import Generics.Pointless.Combinators
+import Generics.Pointless.Functors
+import Generics.Pointless.Fctrable
+import Generics.Pointless.Bifunctors
+import Generics.Pointless.Bifctrable
+import Generics.Pointless.RecursionPatterns
+import Generics.Pointless.Lenses
+import Generics.Pointless.Lenses.Combinators
+
+inn_lns :: Mu a => Lens (F a a) a
+inn_lns = Lens inn (out . fst) out
+
+out_lns :: Mu a => Lens a (F a a)
+out_lns = Lens out (inn . fst) inn
+
+-- | The functor mapping function @fmap@ as a lens.
+fmap_lns :: Fctrable f => Fix f -> Lens c a -> Lens (Rep f c) (Rep f a)
+fmap_lns (f::Fix f) l = Lens get' put' create'
+    where get' = fmap f (get l)
+          put' = fmap f (put l) . fzip (fctr :: Fctr f) (create l)
+          create' = fmap f (create l)
+
+-- | The polytypic functor zipping combinator.
+-- Gives preference to the abstract (first) F-structure.
+fzip :: Fctr f -> (a -> c) -> (Rep f a,Rep f c) -> Rep f (a,c)
+fzip I create = id
+fzip K create = fst
+fzip (f :*!: g) create = (fzip f create >< fzip g create) . distp
+fzip (f :+!: g) create = (l -|- r) . dists
+    where l = fzip f create \/ fmap (fixF f) (id /\ create) . fst
+          r = fmap (fixF g) (id /\ create) . fst \/ fzip g create
+
+-- | The @ana@ recursion pattern as a lens.
+-- For @ana_lns@ to be a well-behaved lens, we MUST prove termination of |get| for each instance.
+ana_lns :: (Mu b,Fctrable (PF b)) => b -> Lens a (F b a) -> Lens a b
+ana_lns (b::b) l = Lens get' put' create'
+    where get' = ana b (get l)
+          put' = accum b  (put l) (fzip g create' . (id >< get l))
+          create' = cata b (create l)
+          g = fctr :: Fctr (PF b)
+
+-- | The @cata@ recursion pattern as a lens.
+-- For @cata_lns@ to be a well-behaved lens, we MUST prove termination of |put| and |create| for each instance.
+cata_lns :: (Mu a,Fctrable (PF a)) => a -> (Lens (F a b) b) -> Lens a b
+cata_lns (a::a) l = Lens get' put' create'
+    where get' = cata a (get l)
+          put' = ana a (fzip f create' . (put l . (id >< fmap (fixF f) get') /\ snd) . (id >< out))
+          create' = ana a (create l)
+          f = fctr :: Fctr (PF a)
+
+-- | The recursion pattern for recursive functions that can be expressed both as anamorphisms and catamorphisms.
+-- Proofs of termination are dismissed.
+nat_lns :: (Mu a,Mu b,Fctrable (PF b)) => a -> NatLens (PF a) (PF b) -> Lens a b
+nat_lns a l = ana_lns _L (l a .< out_lns)
+
+binn_lns :: Bimu d => Lens (B d a (d a)) (d a)
+binn_lns = Lens binn (bout . fst) bout
+
+bout_lns :: Bimu d => Lens (d a) (B d a (d a))
+bout_lns = Lens bout (binn . fst) binn
+
+-- | The bifunctor mapping function @bmap@ as a lens.
+bmap_lns :: Bifctrable f => BFix f -> Lens c a -> NatLens (BRep f c) (BRep f a)
+bmap_lns (f::BFix f) l (x::x) = Lens get' put' create'
+    where get' = bmap f (get l) idx
+          put' = bmap f (put l) idx . bzip x (bctr :: Bifctr f) (create l)
+          create' = bmap f (create l) idx
+          idx = id :: x -> x
+
+-- | The polytypic bifunctor zipping combinator.
+-- Just maps over the polymorphic parameter. To map over the recursive parameter we can use @fzip@.
+bzip :: x -> Bifctr f -> (a -> c) -> (Rep (BRep f a) x,Rep (BRep f c) x) -> Rep (BRep f (a,c)) x
+bzip x BI create = fst
+bzip x BP create = id
+bzip x BK create = fst
+bzip x (f :*!| g) create = (bzip x f create >< bzip x g create) . distp
+bzip (x::x) (f :+!| g) create = (l -|- r) . dists
+    where l = bzip x f create \/ bmap (fixB f) (id /\ create) idx . fst
+          r = bmap (fixB g) (id /\ create) idx . fst \/ bzip x g create
+          idx = id :: x -> x
+
+-- | Generic mapping lens for parametric types with one polymorphic parameter.
+-- Cannot be defined using @nat_lns@ because of the required equality constraints between functors and bifunctors.
+-- This could, however, be overcome by defining specific recursive combinators for bifunctors.
+gmap_lns :: (Mu (d c),Mu (d a),Fctrable (PF (d c)),Bifctrable (BF d),
+             F (d a) (d a) ~ B d a (d a),
+             F (d c) (d a) ~ B d c (d a))
+         => d a -> Lens c a -> Lens (d c) (d a)
+gmap_lns (da::d a) l = cata_lns _L (inn_lns .< (bmap_lns (fixB f) l) da)
+    where f = bctr :: Bifctr (BF d)
+