diff --git a/Bench/Compositions.hs b/Bench/Compositions.hs
new file mode 100644
--- /dev/null
+++ b/Bench/Compositions.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
+
+import Control.LensFunction
+import Examples.Evaluator hiding (incL)
+
+import Criterion.Main
+import Control.Lens
+
+test n = unlift (\x -> iterate (lift incL) x !! n)
+  where
+    incL :: Lens' Int Int
+    incL = lens' $ \s -> (s + 1, (\v -> v - 1))
+
+test2 = unliftT (\(x:xs) -> foldl (lift2 addL) x xs)
+  where
+    addL :: Lens' (Int, Int) Int 
+    addL = lens' $ \(a,b) -> (a + b, \v -> (v - b, b))
+    
+
+
+
+put l s v = set l v s
+
+main = defaultMain [
+  bgroup "composition" [ bench "U10000000" $ nf (put (test 10000000) 0) 0
+                       , bench "U20000000" $ nf (put (test 20000000) 0) 0
+                       , bench "B5000"     $ nf (put test2 [0..5000]) 0
+                       , bench "B10000"    $ nf (put test2 [0..10000]) 0
+                       ]
+  ]
+
diff --git a/Bench/Eval.hs b/Bench/Eval.hs
new file mode 100644
--- /dev/null
+++ b/Bench/Eval.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
+
+import Control.LensFunction
+import Examples.Evaluator hiding (incL)
+
+import Criterion.Main
+
+import Control.DeepSeq
+import Control.Lens
+
+
+instance NFData a => NFData (Env a) where
+  rnf (Env xs) = rnf xs
+
+instance NFData a => NFData (Val a) where
+  rnf (VNum a)       = rnf a
+  rnf (VFun s e env) = rnf s `seq` rnf e `seq` rnf env
+
+instance NFData Exp where
+  rnf (ENum i)     = rnf i
+  rnf (EInc e)     = rnf e
+  rnf (EFun s e)   = rnf s `seq` rnf e
+  rnf (EApp e1 e2) = rnf e1 `seq` rnf e2
+  rnf (EVar e)     = rnf e
+
+
+expr1 = twice @@ twice @@ (twice @@ twice @@ twice @@ (twice @@ twice @@ twice @@ twice @@ inc)) @@ x 
+    where
+      twice = EFun "f" $ EFun "x" $
+                EVar "f"@@ (EVar "f" @@ EVar "x")
+      inc   = EFun "x" (EInc (EVar "x"))
+      x     = EVar "x"
+
+incL :: Lens' Int Int
+incL = lens' $ \s -> (s + 1, (\v -> v - 1))
+
+put l s v = set l v s 
+
+main = defaultMain [
+  bgroup "evalL" [ bench "E0"    $ nf (put (evalL expr) env0)        (VNum 0)
+                 , bench "E1000" $ nf (put (evalL expr) (envn 1000)) (VNum 0)
+                 , bench "E2000" $ nf (put (evalL expr) (envn 2000)) (VNum 0)
+                 , bench "E3000" $ nf (put (evalL expr) (envn 3000)) (VNum 0)
+     ]
+  ]
+
diff --git a/Control/LensFunction.hs b/Control/LensFunction.hs
new file mode 100644
--- /dev/null
+++ b/Control/LensFunction.hs
@@ -0,0 +1,220 @@
+{-# LANGUAGE RankNTypes #-}
+
+-- Required for sequenceL, if we use var Laarhoven repl.
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE Safe #-}
+
+{-|
+This module provides an "applicative" (functional) way of composing
+lenses through the data type 'L'. For example, this module enables us
+to define a "lens" version of 'unlines' as follows.
+
+@
+unlinesF :: [L s String] -> L s String
+unlinesF []     = new ""
+unlinesF (x:xs) = catLineF x (unlinesF xs)
+  where catLineF = lift2 catLineL
+
+catLineL :: Lens' (String, String) String
+catLineL = ...
+@
+
+To make a lens from such "lens functions", one can use unlifting
+functions ('unlift', 'unlift2', 'unliftT') as follows.
+
+@
+unlinesL :: Lens' [String] String
+unlinesL = unliftT unlinesF
+@
+
+The obtained lens works as expected (here 'Control.Lens.^.', 'Control.Lens.&'
+and 'Control.Lens..~' are taken from "Control.Lens").
+
+>>> ["banana", "orange", "apple"] ^. unlinesL
+"banana\norange\napple\n"
+>>> ["banana", "orange", "apple"] & unlinesL .~ "Banana\nOrange\nApple\n"
+["Banana","Orange","Apple"]
+
+One can understand that @L s a@ is an updatable @a@. 
+The type @[L s String] -> L s String@ of @unlinesF@ tells us that
+we can update only the list elements.
+Actually, insertion or deletion of lines to the view will fail, as below.
+
+>>> ["banana", "orange", "apple"] & unlinesL .~ "Banana\nOrange\nApple"
+*** Exception: ...
+>>> ["banana", "orange", "apple"] & unlinesL .~ "Banana\nOrange\nApple\n\n"
+*** Exception: ...
+
+If you want to reflect insertions and deletions, one have to write a
+function of type @L s [String] -> L s String@, which says that the
+list structure itself would be updatable. To write a function of this
+type, 'liftC' and 'liftC2' functions would be sometimes useful.
+
+@
+unlinesF' :: L s [String] -> L s String
+unlinesF' = liftC (foldWithDefault "" "\n") (lift catLineL')
+
+catLineL' :: Lens' (Either () (String,String)) String
+catLineL' = ...
+
+foldWithDefault :: a -> (Lens' (Either () (a,b)) b) -> Lens' [a] b
+foldWithDefault d f = ...
+@
+
+
+
+
+-}
+
+module Control.LensFunction
+       (
+
+       -- * Core Datatype
+         L() -- abstract
+
+       -- * Other constructors for @Lens'@
+       , lens'
+       -- * Functions handling pairs and containers
+       , unit, pair, list, sequenceL
+
+       -- * Lifting Functions 
+       , new, lift, lift2, liftT
+       , liftLens, liftLens'
+       -- * Unlifting Functions
+       , unlift, unlift2, unliftT
+
+       -- * Functions for Handling Observations
+       -- ** Core Monad
+       , R() -- abstract
+       -- ** Lifting Observations
+       , observe
+       , liftO, liftO2
+       -- ** Unlifting Functions 
+       , unliftM, unliftM2, unliftMT
+       -- * Lifting Functions for Combinators 
+       , liftC, liftC2 
+       , module Control.LensFunction.Exception
+       ) where
+
+import Control.LensFunction.Core
+import Control.LensFunction.Util
+import Control.LensFunction.Exception
+
+import Data.Traversable (Traversable)
+
+import Control.Exception
+
+import qualified Control.Lens as L 
+---------------------------------------------------------
+
+mName :: String
+mName = "Control.LensFunction"
+
+{- | 
+The nullary version of a lifting function. Since there is no source,
+every view generated by 'new' is not updatable.
+
+The function will throw 'ConstantUpdateException', if its view is
+updated. 
+-}
+new :: Eq a => a -> L s a
+new a = lift (lens' $ const (a, check a)) unit
+  where
+    check x x' = if x == x' then
+                   ()
+                 else
+                   throw (ConstantUpdateException $ mName ++ ".new")
+
+{- |
+The lifting function for binary lenses. 'unlift2' is a left inverse of this function. 
+
+prop> unlift2 (lift2 l) = l
+
+This function can be defined from 'lift' and 'pair' as below.
+
+prop> lift2 l x y = lift l (pair x y)
+
+NB: This is not a right inverse of 'unlift2'.
+
+prop> (\x y -> x) /= lift2 (unlift2 (\x y -> x))
+
+>>> set (unlift (\z -> (\x y -> x) z z)) "A" "B"
+"B"
+>>> set (unlift (\z -> lift2 (unlift2 (\x y -> x)) (z,z))) "A" "B"
+Error: ...
+-}
+lift2 :: L.Lens' (a,b) c -> (L s a -> L s b -> L s c)
+lift2 l x y = lift l (pair x y) 
+
+{- Derived Functions -}
+
+{- | Similar to @pair@, but this function is for lists. This is a
+derived function, because this can be defined by using 'lift' and
+'pair'.
+-}
+list :: [L s a] -> L s [a]
+list []     = lift (L.lens (\() -> [])
+                           (\() v -> case v of
+                                      [] -> ()
+                                      _  -> throw (ShapeMismatchException $ mName ++ ".list") ))
+              unit
+list (z:zs) = lift consL (pair z (list zs))
+  where
+    consL = L.lens (uncurry (:))
+                   (\_ z -> case z of
+                             (x:xs) -> (x,xs)
+                             _ -> throw (ShapeMismatchException $ mName ++ ".list"))
+
+{- | A data-type generic version of 'list'. The contraint @Eq (t ())@
+says that we can check the equivalence of shapes of containers @t@. -}
+sequenceL :: (Eq (t ()), Traversable t) => t (L s a) -> L s (t a)
+sequenceL x = lift (fillL x) $ list (contents x)
+  where
+    fillL t = L.lens (fill t)
+                     (\_ v -> if shape t == shape v then
+                                contents v
+                              else
+                                throw (ShapeMismatchException $ mName ++ ".sequenceL"))
+
+{-# SPECIALIZE sequenceL :: [L s a] -> L s [a] #-}              
+
+{- | A lifting function for lens combinators. One can understand that the
+     universal quantification for the second argument as closedness restriction. -}
+liftC :: Eq a => (L.Lens' a b -> L.Lens' c d) ->
+             (forall s. L s a -> L s b) ->
+             (forall s. L s c -> L s d)
+liftC c f = lift (c (unlift f))
+
+{- | Similar to 'liftC', but this function is for binary lens combinators.
+-}
+liftC2 :: (Eq a, Eq c) => (L.Lens' a b -> L.Lens' c d -> L.Lens' e f) 
+          -> (forall s. L s a -> L s b) 
+          -> (forall s. L s c -> L s d)
+          -> (forall s. L s e -> L s f)
+liftC2 c f g = lift (c (unlift f) (unlift g))
+
+----------------------------------------------------------
+{- | A datatype-generic version of 'lift2'-}
+liftT :: (Eq (t ()), Traversable t)
+         => L.Lens' (t a) b -> (forall s. t (L s a) -> L s b)
+liftT l xs = lift l (sequenceL xs)
+
+{- | Lifting of observations.
+A typical use of this function would be as follows. 
+
+@
+f x :: L s Int -> R s (L s B)
+f x = do b <- liftO (> 0) x 
+         if b then ... else ...           
+@
+
+-}
+liftO :: Eq w => (a -> w) -> L s a -> R s w
+liftO p x = observe (lift (L.lens p unused) x)
+  where
+    unused s v | v == p s  = s
+               | otherwise = error "This error cannot happen"
+
+{- | Lifting of binary observations -}
+liftO2 :: Eq w => (a -> b -> w) -> L s a -> L s b -> R s w
+liftO2 p x y = liftO (uncurry p) (x `pair` y) 
diff --git a/Control/LensFunction/Core.hs b/Control/LensFunction/Core.hs
new file mode 100644
--- /dev/null
+++ b/Control/LensFunction/Core.hs
@@ -0,0 +1,419 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
+{-# LANGUAGE IncoherentInstances #-}
+-- Required for unliftM, unliftM2, unliftMT, if we use var Laarhoven repl.
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+{-# LANGUAGE Trustworthy #-}
+
+module Control.LensFunction.Core where
+    
+import Prelude -- hiding ((.), id, sequence) 
+-- import Control.Category
+
+import Data.Traversable (Traversable)
+import Control.Applicative (Applicative, pure, (<*>))
+import Control.Monad (ap)
+
+import Control.LensFunction.Util
+import Control.LensFunction.Exception
+import Control.LensFunction.Internal
+
+import qualified Control.Lens as L (Lens', lens)
+
+import qualified Data.IntMap as IM
+
+import Data.Maybe (fromJust) 
+import Control.Exception 
+
+
+{- | 
+A variant of 'Control.Lens.lens'. Sometimes, this function would be
+easier to use because one can re-use a source information to define a "put". 
+-}
+lens' :: (s -> (v, v -> s)) -> L.Lens' s v
+lens' f = \u s -> let (v,r) = f s
+                  in fmap r (u v)
+{-# INLINE[1] lens' #-}
+
+{- |
+Just a composition of 'lift' and 'Control.Lens.lens'.
+Sometimes, this function would be more efficient than the composition
+due to eliminated conversion from the lens to the internal representation.
+
+Since both of the internal and the external representations are
+functions (= normal forms), we have to pay the conversion cost for
+each time when the lifted lens function is evaluated, even in the lazy
+evaluation.
+
+We actually has the RULE to make the composition of 'lift' and
+'Control.Lens.lens' to 'liftLens'. However, the rule may not be fired
+especially when profiling codes are inserted by GHC.
+-}
+liftLens :: (a -> b) -> (a -> b -> a) -> (forall s. L s a -> L s b)
+liftLens g p = liftI (lensI g p)
+
+{- |
+Just a composition of 'lift' and 'lens''. This function has the
+similar role to 'liftLens'.
+-}
+
+liftLens' :: (a -> (b, b -> a)) -> (forall s. L s a -> L s b)
+liftLens' f = liftI (lensI' f)
+
+
+
+dup :: Poset s => LensI s (s,s)
+dup = lensI' $ \s -> ((s,s), \(t,t') -> lub t t')
+{-# INLINE dup #-}
+
+
+{- | A type class for partially ordered sets, in which pairs are
+compaired componentwisely. Instead of having partial comparison
+operator, it provides an associative, commutative and idempotent
+operator, which can be partial like "join" in semilattice but can be
+partial.
+-}          
+class Poset s where
+    lub :: s -> s -> s -- ^ Operation to take LUB 
+
+data Tag a = O { unTag :: a } -- Original, or irrelevant
+           | U { unTag :: a } -- Updated, or relevant 
+
+instance Eq a => Poset (Tag a) where
+  lub (O a) (O b) | a == b = O a
+  lub (O _) (U b)          = U b
+  lub (U a) (O _)          = U a
+  lub (U a) (U b) | a == b = U a
+  lub _     _              = throw (NoLUBException "Control.LensFunction.lub")
+
+instance (Poset a, Poset b) => Poset (a,b) where
+  lub (a,b) (a',b') = (lub a a', lub b b')
+
+instance (Poset a, Eq (t ()), Traversable t) => Poset (t a) where
+  {-# SPECIALIZE lub :: Poset a => [a] -> [a] -> [a] #-}
+  lub t1 t2 = if shape t1 == shape t2 then
+                fill t1 (zipWith lub (contents t1) (contents t2))
+              else
+                throw (NoLUBException "Control.LensFunction.lub")
+  
+-- Internally used datastructure for a slightly first merge
+data Diff t a = Diff (t ())              -- Shape of the data -- Assumption: t is Traversable
+                     (IM.IntMap a)       -- Original mapping from indices to values 
+                     (IM.IntMap (Tag a)) -- Updated mapping 
+
+{-# SPECIALIZE toDiff :: [a] -> Diff [] a #-}
+toDiff :: Traversable t => t a -> Diff t a
+toDiff s = let om = IM.fromAscList $ zip [0..] (contents s)
+           in Diff (shape s) om IM.empty
+
+
+{-# SPECIALIZE fromDiff :: Diff [] a -> [a] #-}
+fromDiff :: Traversable t => Diff t a -> t a
+fromDiff (Diff sh om um) =
+  let cs = map (\i -> case IM.lookup i um of
+                       Just v  -> unTag v
+                       Nothing -> fromJust $ IM.lookup i om) [0..]
+  in fill sh cs 
+
+instance Eq a => Poset (Diff t a) where
+  lub (Diff t1 o1 m1) (Diff t2 o2 m2) -- Invariant: t1 == t2 and o1 == o2 
+    = Diff t1 o1 (IM.unionWith lub m1 m2)
+
+
+
+{- |
+An abstract type for "updatable" data. Bidirectional programming
+through our module is to write manipulation of this datatype.
+
+
+
+==== Categorical Notes
+
+The type constructor @L s@ together with 'lift', 'unit' and 'pair'
+defines a lax monoidal functor from the category of lenses to that of
+Haskell functions. The 'lift' function does transfor a lens to a
+function. The 'unit' and 'pair' functions are the core operations on
+this lax monoidal functor.  Any lifting functions defined in this
+module can be defined by these three functions.
+
+
+-}
+newtype L s a = L (Poset s => LensI s a)
+
+unL :: L s a -> (Poset s => LensI s a)
+unL (L s) = s
+{-# INLINE unL #-}
+
+
+{-
+f id' <<< tag <<< y
+vs.
+f y 
+
+lift2 id :: L s A -> L s B -> L s (A,B)
+
+f y = pair y y
+
+
+(y *** y) <<< dup 
+vs
+(id' *** id') <<< dup <<< tag <<< y
+
+y = (\x -> unTag y) (\_ v -> O v) --- NOT locally well-behaved
+
+put ((y *** y) <<< dup) s (s,v) = _|_
+
+put ((id' *** id') <<< dup <<< tag <<< y) s (s,v) = O v
+
+-}
+
+{- |
+The lifting function. Note that it forms a functor from the
+category of lenses to the category of sets and functions.
+
+'unlift' is a left-inverse of this function.
+
+prop> unlift (lift x) = x
+-}
+{-
+Notice that 'lift' is not a surjection. That is,
+there is a function such that @lift (unlift f) /= f@.
+However such a function cannot be constructed with `lift`.
+-}
+lift :: L.Lens' a b -> (forall s. L s a -> L s b)
+lift l = liftI (fromLens l)
+
+liftI :: LensI a b -> (forall s. L s a -> L s b)
+liftI h = \(L x) -> L (h <<< x)
+
+{-# NOINLINE[1]  lift #-}
+{-# INLINE       liftI #-}
+
+{- | A paring function of @L s a@-typed values.
+This function can be defined by 'lift2' as below.
+
+prop> pair = lift2 (lens id (const id)) 
+-}
+pair :: L s a -> L s b -> L s (a,b) 
+pair (L x) (L y) = L ((x *** y) <<< dup)
+
+{-# INLINE pair #-}
+
+
+{- |
+The unit element in the lifted world.
+
+Let @elimUnitL@ and @elimUnitR@ are lenses defined as follows.
+
+@
+elimUnitL = lens (\(x,()) -> x) (\_ x -> (x,()))
+elimUnitR = lens (\((),x) -> x) (\_ x -> ((),x))
+@
+
+Then, we have the following laws.
+
+prop> lift2 elimUnitL x unit = x
+prop> lift2 elimUnitR unit x = x
+-}
+unit :: L s ()
+unit = L $ lensI' (\s -> ( (), \() -> s ) )
+{-# INLINABLE unit #-}
+
+
+{- | The unlifting function, satisfying @unlift (lift x) = x@. -}
+unlift :: Eq a => (forall s. L s a -> L s b) -> L.Lens' a b
+unlift f = toLens $ unL (f id') <<< tag
+
+id' :: L (Tag s) s 
+id' = L $ lensI unTag (const U)
+{-# INLINE id' #-}
+
+tag :: LensI s (Tag s)
+tag = lensI O (const unTag)
+{-# INLINE tag #-}
+
+{- | The unlifting function for binary functions, satisfying
+     @unlift2 (lift2 x) = x@.
+-}
+unlift2 :: (Eq a, Eq b) => (forall s. L s a -> L s b -> L s c) -> L.Lens' (a,b) c
+unlift2 f = toLens $ unL (f fst' snd') <<< tag2
+
+
+fst' :: L (Tag a,b) a
+fst' = L $ lensI (unTag . fst) (\(_,b) a -> (U a, b))
+{-# INLINE fst' #-}
+
+snd' :: L (a, Tag b) b 
+snd' = L $ lensI (unTag . snd) (\(a,_) b -> (a, U b))
+{-# INLINE snd' #-}
+
+tag2 :: LensI (a,b) (Tag a, Tag b)
+tag2 = lensI (\(a,b) -> (O a, O b)) (\_ (a,b) -> (unTag a, unTag b))
+{-# INLINE tag2 #-}
+
+{- |
+The unlifting function for functions that manipulate data structures,
+satisfying @unliftT (liftT x) = x@ if @x@ keeps the shape.
+The constraint @Eq (t ())@ says that we can compare the shapes of
+given two containers. 
+
+-}
+unliftT :: (Eq a, Eq (t ()), Traversable t) =>
+           (forall s. t (L s a) -> L s b) -> L.Lens' (t a) b
+unliftT f = toLens $ 
+  lensI' $ \s -> let l = makeLens s
+                 in viewrefl l s 
+  where
+--    makeLens s = unL (f (projs (shape s))) <<< tagT
+    makeLens s = unL (f (projsV (shape s))) <<< diffL 
+
+tagT :: Functor f => LensI (f s) (f (Tag s))
+tagT = lensI (fmap O) (\_ -> fmap unTag)
+{-# INLINE tagT #-}
+
+diffL :: Traversable t => LensI (t a) (Diff t a)
+diffL = lensI' $ \s -> (toDiff s, fromDiff)
+{-# INLINE diffL #-}
+
+
+-- V is from Voigtlaender    
+projsV :: Traversable t => t b -> t (L (Diff t a) a)
+projsV sh =
+  let n = length (contents sh)
+  in fill sh $ map (projV sh) [0..n-1]
+
+projV :: Traversable t => t b -> Int -> L (Diff t a) a
+projV _ i = L $ lensI' $ \(Diff s o _) ->
+                           ( fromJust (IM.lookup i o),
+                             \v -> Diff s o (IM.singleton i (U v)))
+                          
+  
+     
+
+projs :: Traversable t => t b -> t (L (t (Tag a)) a)
+projs sh =
+  let n = length (contents sh)
+  in fill sh $ map (proj sh) [0..n-1] 
+
+
+proj :: Traversable t => t b -> Int -> L (t (Tag a)) a
+proj sh i = L $
+            lensI  (\s -> unTag (contents s !! i))
+                   (\s v -> fill sh (update i (U v) (contents s)))
+
+update :: Int -> a -> [a] -> [a]
+update 0 v (_:xs) = v:xs
+update i v (x:xs) = x:update (i-1) v xs 
+update _ _ _      = error "Invalid Index"
+
+-- TODO: TH Generator for lifting and unlifting functions. 
+
+
+---------------------------------------
+
+{- |
+An abstract monad used to keep track of observations.
+By this monad, we can inspect the value of 'L s a'-data.
+
+It is worth noting that we cannot change the inspection result to ensure
+the consistency property (aka PutGet in some context).
+
+
+-}
+newtype R s a = R { unR :: Poset s => s -> (a, s -> Bool) }
+
+instance Functor (R s) where
+  fmap f (R m) = R $ \s -> let (x, p) = m s in (f x, p)
+
+instance Monad (R s) where
+  return x = R $ const (x, const True)
+  R m >>= f = R $ \s -> let (x,c1) = m s
+                            (y,c2) = let R k = f x in k s
+                        in (y, \t -> c1 t && c2 t)
+
+instance Applicative (R s) where
+  pure  = return
+  (<*>) = ap
+
+      
+
+{- |
+A primitive used to define 'liftO' and 'liftO2'.
+With 'observe', one can inspect the current value of a lifted '(L s a)'-value
+as below.
+
+@
+f x :: L s A -> R s (L s B)
+f x = do viewX <- observe x
+         ... computation depending on 'viewX' ...
+@
+
+Once the 'observe' function is used in a lens function,
+the lens function becomes not able to change 
+change the "observed" value to ensure the correctness.
+
+-}
+observe :: Eq w => L s w -> R s w
+observe l = R $ \s ->  let w = get (unL l) s
+                       in (w, \s' -> get (unL l) s' == w)
+
+{-# INLINABLE observe #-}
+
+{- | A monadic version of 'unlift'. -}
+unliftM :: Eq a => (forall s. L s a -> R s (L s b)) -> L.Lens' a b
+unliftM f = toLens $ lensI' $ \src -> viewrefl (makeLens src) src 
+  where
+    makeLens src =
+      let (l,p) = unR (f id') (O src)
+          l'    = unL l <<< tag
+          put' s v =
+            let s' = put l' s v
+            in if p (O s') then
+                 s'
+               else
+                 throw (ChangedObservationException "Control.Lens.Function.unliftM")
+      in lensI (get l')  put'
+
+{- | A monadic version of 'unlift2'. -}
+unliftM2 :: (Eq a, Eq b) =>
+            (forall s. L s a -> L s b -> R s (L s c)) -> L.Lens' (a,b) c
+unliftM2 f = toLens $ lensI' $ \src -> viewrefl (makeLens src) src 
+  where
+    makeLens src =
+      let (l,p) = unR (f fst' snd') (get tag2 src)
+          l'    = unL l <<< tag2
+          put' s v =
+            let s' = put l' s v
+            in if p (get tag2 s') then
+                 s'
+               else
+                 throw (ChangedObservationException "Control.LensFunction.unliftM2")
+      in lensI (get l')  put'
+
+
+{- | A monadic version of 'unliftT'. -}
+unliftMT :: (Eq a, Eq (t ()), Traversable t) =>
+            (forall s. t (L s a) -> R s (L s b)) -> L.Lens' (t a) b
+unliftMT f = toLens $ lensI' $ \src -> viewrefl (makeLens src) src
+  where
+    makeLens src =
+      let (l,p) = unR (f (projsV (shape src))) (get diffL src)
+          l'    = unL l <<< diffL
+          -- (l,p) = unR (f (projs (shape s))) (get tagT s)
+          -- l'    = unL l <<< tagT
+          put' s v =
+            let s' = put l' s v
+            in if p (get diffL {- tagT -} s') then
+                 s'
+               else
+                 throw (ChangedObservationException "Control.LensFunction.unliftMT")
+      in lensI (get l')  put'
+           
+{-# RULES
+"lift/lens'"       forall x.   lift (lens' x)        = liftI (lensI' x)
+"lift/lens"        forall g p. lift (L.lens g p)     = liftI (lensI g p)
+"lens/fromLens"    forall g p. fromLens (L.lens g p) = lensI g p
+"lens'/fromLens"   forall f.   fromLens (lens' f)    = lensI' f
+  #-}
+
diff --git a/Control/LensFunction/Exception.hs b/Control/LensFunction/Exception.hs
new file mode 100644
--- /dev/null
+++ b/Control/LensFunction/Exception.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+
+module Control.LensFunction.Exception
+       (
+         SomeLensFunctionException(..),
+         NoLUBException(..),
+         ChangedObservationException(..),
+         ShapeMismatchException(..),
+         ConstantUpdateException(..)
+       ) where
+
+import Control.Exception
+import Data.Typeable (cast, Typeable)
+
+data SomeLensFunctionException
+  = forall e. Exception e => SomeLensFunctionException e
+  deriving Typeable
+
+instance Show SomeLensFunctionException where
+  show (SomeLensFunctionException e) = show e 
+
+instance Exception SomeLensFunctionException 
+
+lfToException :: Exception e => e -> SomeException
+lfToException = toException . SomeLensFunctionException
+
+lfFromException :: Exception e => SomeException -> Maybe e
+lfFromException x = do
+    SomeLensFunctionException a <- fromException x
+    cast a
+
+data NoLUBException = NoLUBException String deriving (Typeable)
+
+instance Show NoLUBException where
+  show (NoLUBException s) = s ++ ": No LUB"
+
+instance Exception NoLUBException where
+  toException   = lfToException
+  fromException = lfFromException
+
+data ChangedObservationException
+  = ChangedObservationException String
+  deriving Typeable
+
+instance Show ChangedObservationException where
+  show (ChangedObservationException s) = s ++ ": Changed Observation"
+
+instance Exception ChangedObservationException where
+  toException   = lfToException
+  fromException = lfFromException
+
+
+data ShapeMismatchException = ShapeMismatchException String
+                               deriving Typeable 
+
+instance Show ShapeMismatchException where
+  show (ShapeMismatchException s) = s ++ ": Shape Mismatch"
+
+instance Exception ShapeMismatchException where
+  toException   = lfToException
+  fromException = lfFromException
+
+data ConstantUpdateException = ConstantUpdateException String
+                               deriving Typeable 
+instance Show ConstantUpdateException where 
+  show (ConstantUpdateException s) = s ++ ": Update on Constant"
+
+instance Exception ConstantUpdateException where
+  toException   = lfToException
+  fromException = lfFromException
+  
+
+
+
+
diff --git a/Control/LensFunction/Internal.hs b/Control/LensFunction/Internal.hs
new file mode 100644
--- /dev/null
+++ b/Control/LensFunction/Internal.hs
@@ -0,0 +1,102 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE RankNTypes, ExistentialQuantification #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE BangPatterns #-}
+
+{- | Internal Representation of Lenses -}
+
+module Control.LensFunction.Internal
+       (
+         LensI(), get, put
+       , lensI, lensI', viewrefl
+       , fromLens
+       , toLens 
+       , (***), (<<<)
+       ) where
+
+import qualified Control.Lens as L 
+
+#ifdef __USE_VAN_LAARHOVEN__
+import Control.LensFunction.InternalL
+#else
+#endif 
+
+#ifndef __USE_VAN_LAARHOVEN__
+
+newtype Store v s = Store (v, v -> s)
+
+instance Functor (Store v) where
+  {-# INLINE fmap #-}
+  fmap = storeMap
+
+storeMap :: (a -> b) -> Store v a -> Store v b 
+storeMap f (Store (v, !g)) = Store (v, f . g)
+{-# INLINE storeMap #-}
+
+fromLens :: L.Lens' s v -> LensI s v
+fromLens lens = fromLens' lens -- the argument is necessary to pass the type check.
+
+fromLens' :: ((v -> Store v v) -> (s -> Store v s)) -> LensI s v 
+fromLens' l = 
+  -- lensI (getConst . l Const) (\s v -> L.runIdentity $ l (\_ -> L.Identity v) s)
+  let f = l (\v -> Store (v,id))
+  in LensI $ \s -> let Store !vr = f s
+                   in vr
+{-# INLINE fromLens' #-}                      
+
+toLens :: LensI s v -> L.Lens' s v
+toLens (LensI f) = \u s -> let (v, r) = f s
+                           in fmap r (u v)
+
+{-# INLINE[0] fromLens #-}
+{-# INLINE[0] toLens #-}
+
+{-# RULES
+"SPECIALIZE fromLens" forall (x :: L.Lens' s v). fromLens x = fromLens' (x :: (v -> Store v v) -> (s -> Store v s))
+  #-}
+
+{- |
+A variant of conventional representation. 
+-}
+newtype LensI s v = LensI { runLens :: s -> (v, v -> s) }
+
+get :: LensI s v -> s -> v
+get lens = fst . runLens lens
+{-# INLINE get #-}
+
+put :: LensI s v -> s -> v -> s
+put lens = snd . runLens lens
+{-# INLINE put #-}
+
+lensI :: (s -> v) -> (s -> v -> s) -> LensI s v
+lensI g p = LensI (\s -> (g s, p s))
+{-# INLINE lensI #-}
+
+lensI' :: (s -> (v, v -> s)) -> LensI s v
+lensI' = LensI
+{-# INLINE lensI' #-}
+
+viewrefl :: LensI s v -> s -> (v, v -> s)
+viewrefl = runLens
+{-# INLINE viewrefl #-}
+
+(<<<) :: LensI b c -> LensI a b -> LensI a c 
+y <<< x = LensI $ \s ->
+                  let !(v1, r1) = runLens x s
+                      !(v2, r2) = runLens y v1
+                  in (v2, r1 . r2)
+{-# INLINABLE (<<<) #-}
+
+(***) :: LensI a s -> LensI b t -> LensI (a,b) (s,t)
+x *** y = LensI $ \(a,b) ->
+                  let !(va, ra) = runLens x a
+                      !(vb, rb) = runLens y b
+                  in ((va,vb), \(va',vb') -> (ra va', rb vb'))
+
+{-# INLINABLE (***) #-}
+
+
+
+
+#endif 
+
diff --git a/Control/LensFunction/InternalL.hs b/Control/LensFunction/InternalL.hs
new file mode 100644
--- /dev/null
+++ b/Control/LensFunction/InternalL.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE Safe #-}
+
+{- | Lens in the van Laarhoven representation -}
+
+module Control.LensFunction.InternalL where
+
+import Control.Arrow (first, second)
+import Control.Applicative (Const(..))
+import Control.Monad.Identity 
+
+import qualified Control.Lens as L 
+
+
+type LensI s v = L.Lens' s v
+
+fromLens :: L.Lens' s v -> LensI s v 
+fromLens x = x
+{-# INLINE[2] fromLens #-}
+
+toLens :: LensI s v -> L.Lens' s v
+toLens x = x
+{-# INLINE[2] toLens #-}
+
+get :: LensI s v -> s -> v 
+get l = L.view l -- the argument is necessary to pass the type check.
+
+{-# INLINE get #-}
+
+put :: LensI s v -> s -> v -> s
+put lens = flip (L.set lens) 
+{-# INLINE put #-}
+
+newtype Store a b = Store { runStore :: (a, a -> b) }
+
+instance Functor (Store a) where
+  {-# INLINE fmap #-}
+  fmap f (Store (a, r)) = Store (a, f . r)
+
+viewrefl :: LensI s v -> (s -> (v, v -> s))
+viewrefl lens s = runStore $ lens (\v -> Store (v, id)) s  
+{-# INLINE viewrefl #-}
+
+
+lensI :: (s -> v) -> (s -> v -> s) -> LensI s v
+lensI = L.lens
+{-# INLINE lensI #-}
+
+lensI' :: (s -> (v, v -> s)) -> LensI s v
+lensI' h = \f s -> let (v,r) = h s
+                       in fmap r (f v)
+{-# INLINE lensI' #-}
+
+(***) :: LensI a b -> LensI a' b' -> LensI (a,a') (b,b')
+x *** y = L.alongside x y
+{-# INLINE (***) #-}
+
+(<<<) = flip (.)
+{-# INLINE (<<<) #-}
diff --git a/Control/LensFunction/Util.hs b/Control/LensFunction/Util.hs
new file mode 100644
--- /dev/null
+++ b/Control/LensFunction/Util.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE Trustworthy #-}
+
+module Control.LensFunction.Util where
+
+import Data.Traversable (Traversable)
+import qualified Data.Traversable as T
+import qualified Data.Foldable as F
+
+import qualified Control.Monad.State as St 
+
+contents :: Traversable t => t a -> [a] 
+contents = F.toList
+
+fill :: Traversable t => t b -> [a] -> t a
+fill t = St.evalState (T.traverse next t)
+  where
+    next _ = do (y:ys) <- St.get
+                St.put ys
+                return y
+
+{-# INLINABLE[2] fill #-}
+{-# INLINABLE[2] contents #-}                
+{-# RULES
+"fill/list"     fill = fillList
+"contents/list" contents = id :: [a] -> [a]
+  #-}
+fillList :: [a] -> [b] -> [b]
+fillList _ ys = ys
+
+shape :: Functor f => f a -> f ()
+shape = fmap (const ()) 
diff --git a/Examples/Evaluator.hs b/Examples/Evaluator.hs
new file mode 100644
--- /dev/null
+++ b/Examples/Evaluator.hs
@@ -0,0 +1,68 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
+
+module Examples.Evaluator where
+
+import Control.LensFunction
+
+import Data.Traversable (Traversable)
+import Data.Foldable    (Foldable) 
+
+import Control.Lens
+
+data Exp = ENum Integer
+         | EInc Exp 
+         | EFun String Exp 
+         | EApp Exp Exp 
+         | EVar String
+           deriving (Eq, Show)
+
+data Val a = VNum a 
+           | VFun String Exp (Env a)
+             deriving (Eq, Functor, Foldable, Traversable, Show) 
+
+newtype Env a = Env [(String, Val a)]
+              deriving (Eq, Functor, Foldable, Traversable, Show) 
+
+lkup x (Env env) = case lookup x env of
+                    Just v -> v
+                    Nothing -> error $ "Undefined variable: " ++ x
+xtnd (x,e) (Env env) = Env $ (x,e):env
+
+incL = lens' $ \s -> (s + 1, \v -> v - 1)
+
+eval :: Exp -> Env (L s Integer) -> Val (L s Integer)
+eval (ENum n) env = VNum (new n)
+eval (EInc e) env =
+  let VNum n = eval e env
+  in VNum (lift incL n)
+eval (EFun x e) env =
+  VFun x e env
+eval (EApp e1 e2) env =
+  let VFun x e env' = eval e1 env
+      v2 = eval e2 env
+  in eval e (xtnd (x,v2) env')
+eval (EVar x) env = lkup x env
+
+infixl 9 @@ -- @@ is left associative
+(@@) = EApp
+
+expr = twice @@ twice @@ twice @@ twice @@ inc @@ x 
+    where
+      twice = EFun "f" $ EFun "x" $
+                EVar "f"@@ (EVar "f" @@ EVar "x")
+      inc   = EFun "x" (EInc (EVar "x"))
+      x     = EVar "x"
+
+evalL e = unliftT (\env -> sequenceL $ eval e env)
+
+env0   = Env [("x", VNum 3)]
+envn n = Env $ [("x", VNum 3)] ++ [  ("y" ++ show i, VNum i)  | i <- [1..n] ]
+
+{-
+*Examples.Evaluator> env0 ^. evalL expr
+VNum 65539
+*Examples.Evaluator> env0 & evalL expr .~ (VNum 0)
+Env [("x",VNum (-65536))]
+-}
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, Kazutaka Matsuda
+
+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.
+
+    * Neither the name of Kazutaka Matsuda nor the names of other
+      contributors may 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/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/app-lens.cabal b/app-lens.cabal
new file mode 100644
--- /dev/null
+++ b/app-lens.cabal
@@ -0,0 +1,198 @@
+name:     app-lens
+version:  0.1.0.0
+synopsis: applicative (functional) bidirectional programming beyond composition chains 
+
+description:
+   A bidirectional transformation connects data in difference formats,
+   maintaining consistency amid separate updates. The "lens"
+   programming language---with Kmett's Haskell lens package being
+   one of the most influentials---is a solution to this problem.
+   .
+   Many lens implementations (including Kmett's Haskell library) only
+   support the point-free style of programming. Though concise at times,
+   this style becomes less handy when programs get more complicated. 
+   .  
+   This module provides the infrastructure for programming complex
+   bidirectional transformations, by representing lenses as functions
+   that are subject to the normal applicative-style programming.  For
+   example, let us consider the 'unlines' functions and to define a
+   lens version of it. In our framework we can program through pattern
+   matching and explicit recursion as in normal functional programming.
+   .
+   > unlinesF :: [L s String] -> L s String
+   > unlinesF []     = new ""
+   > unlinesF (x:xs) = catLineF x (unlinesF xs)
+   >    where catLineF = lift2 catLineL
+   .   
+   Here, @lift2 :: Lens' (a,b) c -> (forall s. L s a -> L s b -> L s
+   c)@ and @new :: a -> (forall s. L s a)@ lift lenses to functions.
+   The former is for binary lenses and the latter is for constant
+   lenses.  We can then apply lenses as functions, alleviating the
+   need of specialized combinators. In the above, we omitted the
+   definition of a primitive lens @catLineL :: Lens' (String, String)
+   String@ that concatenates two strings with a newline in between.   
+   .
+   Simply unlifting ('unlift', 'unlift2', 'unliftT') such "lens functions"
+   gives us the desired lenses. 
+   .   
+   > unlinesL :: Lens' [String] String
+   > unlinesL = unliftT unlinesF
+   .
+   The obtained lens works as expected.
+   .
+   .
+   >>> ["banana", "orange", "apple"] ^. unlinesL
+   "banana\norange\napple\n"
+   >>> ["banana", "orange", "apple"] & unlinesL .~ "Banana\nOrange\nApple\n"
+   ["Banana","Orange","Apple"]
+   .
+   .   
+   One may prefer to define @unliftF@ with 'foldr'. Indeed, we can
+   use 'foldr' as below because @catLineF@ and @unlinesF@ are simply
+   Haskell functions.
+   .
+   > unliftF = foldr (lift2 catLineL) (new "") 
+   .
+   Here, the program is written in a point-free manner similar to that
+   of the other lens frameworks. But note that this 'foldr' is just
+   Haskell's 'foldr', instead of a special combinator for lenses.
+   .
+   More examples can be found at \"Examples\" in the source code
+   <https://bitbucket.org/kztk/app-lens/downloads>.
+   . 
+   === Remark
+   .
+   The applicative-style programming is possible in our implementation 
+   because a function representation different from Kmett's is used for lenses.
+   As a result, when we program record-field access chains such as 
+   .
+   > src .^ l1 . l2 
+   > src & l1 . l2 .~ tgt' 
+   .
+   The order of composition is inverted in our implementation. 
+   .
+   > src .^ unlift (lift l2 . lift l1)
+   > src & unlift (lift l2 . lift l1) .~ tgt' 
+   .
+   This difference causes slight inconvenience for record updates, but is 
+   crucial in allowing the applicative-style lens programming we
+   aim for.    
+
+
+license:             BSD3
+license-file:        LICENSE
+
+homepage:            https://bitbucket.org/kztk/app-lens
+bug-reports:         https://bitbucket.org/kztk/app-lens/issues
+tested-with:         GHC == 7.8.3
+
+author:              Kazutaka Matsuda
+copyright:           (c) Kazutaka Matsuda, 2015
+maintainer:          kztk@ecei.tohoku.ac.jp
+category:            Data, Lenses
+build-type:          Simple
+cabal-version:       >=1.10
+
+
+
+Flag UseVanLaarhoven
+  Description: Use Control.Lens.Lens' as internal representations.
+               (1.5 times speed up for 'lift' but 1000 times slow down for 'lift2')
+  Default:     False 
+
+Library
+  exposed-modules:
+    Control.LensFunction, 
+    Control.LensFunction.Exception
+  
+  other-modules: 
+    Control.LensFunction.Core, 
+    Control.LensFunction.Util 
+    Control.LensFunction.Internal    
+  
+  if flag(useVanLaarhoven)
+    other-modules: Control.LensFunction.InternalL
+    cpp-options: -D__USE_VAN_LAARHOVEN__
+
+  other-extensions:    
+    RankNTypes, NoMonomorphismRestriction, 
+    FlexibleInstances, FlexibleContexts, UndecidableInstances, 
+    IncoherentInstances, CPP, ExistentialQuantification, 
+    DeriveDataTypeable, DeriveFunctor, DeriveFoldable, DeriveTraversable
+  
+  build-depends:  
+    base       >=4.7   && < 4.8, 
+    containers >=0.5   && < 0.6, 
+    mtl        >=2.2   && < 2.3,
+    lens       >=4     && < 4.12
+
+  default-language: Haskell2010
+
+-- Executable prof
+--   Main-is: Bench/Prof.hs
+--   Build-Depends:
+--      app-lens, 
+--      base,
+--      mtl, 
+--      containers, 
+--      lens, 
+--      deepseq >= 1.3 && < 2, 
+--      criterion >= 1.1 && < 2
+--
+--
+--   if flag(useVanLaarhoven)
+--     cpp-options: -D__USE_VAN_LAARHOVEN__
+--
+--   ghc-options: -O2 -rtsopts 
+--   ghc-prof-options: -prof -auto-all -rtsopts "-with-rtsopts=-p -s"
+--   default-language:    Haskell2010
+
+
+Benchmark compositions
+  type: exitcode-stdio-1.0
+  Main-is: Bench/Compositions.hs
+  Build-Depends: 
+     app-lens, 
+     base,
+     mtl, 
+     containers, 
+     lens, 
+     deepseq >= 1.3 && < 1.4, 
+     criterion >= 1.1 && < 1.2
+
+
+  if flag(useVanLaarhoven)
+    cpp-options: -D__USE_VAN_LAARHOVEN__
+
+  ghc-options: -rtsopts -O2
+  ghc-prof-options: -prof -rtsopts 
+  default-language:    Haskell2010
+
+Benchmark eval
+  type: exitcode-stdio-1.0
+  Main-is: Bench/Eval.hs
+  Build-Depends: 
+     app-lens, 
+     base,
+     mtl, 
+     containers, 
+     lens,
+     deepseq >= 1.3 && < 1.4, 
+     criterion >= 1.1 && < 1.2
+
+  other-modules: 
+     Examples.Evaluator
+
+  if flag(useVanLaarhoven)
+    cpp-options: -D__USE_VAN_LAARHOVEN__
+
+  ghc-options: -rtsopts -O2
+  ghc-prof-options: -prof -rtsopts 
+  default-language:    Haskell2010
+
+source-repository head
+   type:     git
+   location: https://bitbucket.org/kztk/app-lens
+
+
+