diff --git a/DDF/Bimap.hs b/DDF/Bimap.hs
--- a/DDF/Bimap.hs
+++ b/DDF/Bimap.hs
@@ -1,7 +1,27 @@
+{-# LANGUAGE NoImplicitPrelude, NoMonomorphismRestriction #-}
+
 module DDF.Bimap (module DDF.Bimap, module DDF.Prod, module DDF.Option) where
 
-import DDF.Map as Map
+import qualified DDF.Map as Map
 import DDF.Prod
 import DDF.Option
+import DDF.Int
+import qualified Data.Bimap as M
+import qualified Prelude as M
+import qualified Data.Map as M
 
-class Map.Map r => Bimap r where
+class (Int r, Map.Map r) => Bimap r where
+  size :: r h (M.Bimap a b -> M.Int)
+  lookupL :: (Map.Ord a, Map.Ord b) => r h (M.Bimap a b -> a -> Maybe b)
+  lookupR :: (Map.Ord a, Map.Ord b) => r h (M.Bimap a b -> b -> Maybe a)
+  empty :: r h (M.Bimap a b)
+  singleton :: r h ((a, b) -> M.Bimap a b)
+  toMapL :: r h (M.Bimap a b -> M.Map a b)
+  toMapR :: r h (M.Bimap a b -> M.Map b a)
+  insert :: (Map.Ord a, Map.Ord b) => r h ((a, b) -> M.Bimap a b -> M.Bimap a b) 
+  updateL :: (Map.Ord a, Map.Ord b) => r h ((b -> Maybe b) -> a -> M.Bimap a b -> M.Bimap a b)
+  updateR :: (Map.Ord a, Map.Ord b) => r h ((a -> Maybe a) -> b -> M.Bimap a b -> M.Bimap a b)
+
+lookupL2 = app2 lookupL
+size1 = app size
+insert2 = app2 insert
diff --git a/DDF/Bool.hs b/DDF/Bool.hs
--- a/DDF/Bool.hs
+++ b/DDF/Bool.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE NoImplicitPrelude, NoMonomorphismRestriction #-}
 module DDF.Bool (module DDF.Bool, module DDF.DBI) where
 
 import DDF.DBI
@@ -7,3 +7,7 @@
 class DBI r => Bool r where
   bool :: M.Bool -> r h M.Bool
   ite :: r h (a -> a -> M.Bool -> a)
+
+ite1 = app ite
+ite2 = app2 ite
+ite3 = app3 ite
diff --git a/DDF/Combine.hs b/DDF/Combine.hs
--- a/DDF/Combine.hs
+++ b/DDF/Combine.hs
@@ -1,10 +1,20 @@
-{-# LANGUAGE NoImplicitPrelude, TypeFamilies, TypeApplications, ScopedTypeVariables, NoMonomorphismRestriction #-}
+{-# LANGUAGE
+  NoImplicitPrelude,
+  TypeFamilies,
+  TypeApplications,
+  ScopedTypeVariables,
+  NoMonomorphismRestriction,
+  MultiParamTypeClasses,
+  FlexibleInstances,
+  FlexibleContexts
+#-}
 
 module DDF.Combine where
 
 import DDF.Meta.Interpreter
-import DDF.DLang
 import qualified DDF.Map as Map
+import DDF.Lang
+import qualified DDF.VectorTF as VTF
 
 instance (DBI l, DBI r) => DBI (Combine l r) where
   z = Combine z z
@@ -12,7 +22,6 @@
   app (Combine fl fr) (Combine xl xr) = Combine (app fl xl) (app fr xr)
   abs (Combine l r) = Combine (abs l) (abs r)
   hoas f = Combine (hoas $ \x -> case f (Combine x z) of Combine l _ -> l) (hoas $ \x -> case f (Combine z x) of Combine _ r -> r)
-  liftEnv (Combine l r) = Combine (liftEnv l) (liftEnv r)
 
 instance (Bool l, Bool r) => Bool (Combine l r) where
   bool x = Combine (bool x) (bool x)
@@ -33,6 +42,7 @@
   doubleMult = Combine doubleMult doubleMult
   doubleDivide = Combine doubleDivide doubleDivide
   doubleExp = Combine doubleExp doubleExp
+  doubleEq = Combine doubleEq doubleEq
 
 instance (Float l, Float r) => Float (Combine l r) where
   float x = Combine (float x) (float x)
@@ -53,8 +63,19 @@
   singleton = Combine Map.singleton Map.singleton
   alter = Combine Map.alter Map.alter
   mapMap = Combine Map.mapMap Map.mapMap
+  unionWith = Combine Map.unionWith Map.unionWith
 
 instance (Bimap l, Bimap r) => Bimap (Combine l r) where
+  size = Combine size size
+  empty = Combine empty empty
+  singleton = Combine singleton singleton
+  lookupL = Combine lookupL lookupL
+  lookupR = Combine lookupR lookupR
+  toMapL = Combine toMapL toMapL
+  toMapR = Combine toMapR toMapR
+  insert = Combine insert insert
+  updateL = Combine updateL updateL
+  updateR = Combine updateR updateR
 
 instance (Dual l, Dual r) => Dual (Combine l r) where
   dual = Combine dual dual
@@ -63,24 +84,62 @@
 instance (Unit l, Unit r) => Unit (Combine l r) where
   unit = Combine unit unit
 
-instance (Lang l, Lang r) => Lang (Combine l r) where
-  fix = Combine fix fix
+instance (Sum l, Sum r) => Sum (Combine l r) where
   left = Combine left left
   right = Combine right right
   sumMatch = Combine sumMatch sumMatch
-  exfalso = Combine exfalso exfalso
-  ioRet = Combine ioRet ioRet
-  ioBind = Combine ioBind ioBind
-  ioMap = Combine ioMap ioMap
+
+instance (Int l, Int r) => Int (Combine l r) where
+  int x = Combine (int x) (int x)
+  pred = Combine pred pred
+  isZero = Combine isZero isZero
+
+instance (Y l, Y r) => Y (Combine l r) where
+  y = Combine y y
+
+instance (List l, List r) => List (Combine l r) where
   nil = Combine nil nil
   cons = Combine cons cons
   listMatch = Combine listMatch listMatch
+
+instance (Functor l m, Functor r m) => Functor (Combine l r) m where
+  map = Combine map map
+
+instance (Applicative l m, Applicative r m) => Applicative (Combine l r) m where
+  pure = Combine pure pure
+  ap = Combine ap ap
+
+instance (Monad l m, Monad r m) => Monad (Combine l r) m where
+  bind = Combine bind bind
+  join = Combine join join
+
+instance (IO l, IO r) => IO (Combine l r) where
+  putStrLn = Combine putStrLn putStrLn
+
+instance (VTF.VectorTF l, VTF.VectorTF r) => VTF.VectorTF (Combine l r) where
+  zero = Combine VTF.zero VTF.zero
+  basis = Combine VTF.basis VTF.basis
+  plus = Combine VTF.plus VTF.plus
+  mult = Combine VTF.mult VTF.mult
+  vtfMatch = Combine VTF.vtfMatch VTF.vtfMatch
+
+instance (DiffWrapper l, DiffWrapper r) => DiffWrapper (Combine l r) where
+  diffWrapper = Combine diffWrapper diffWrapper
+  runDiffWrapper = Combine runDiffWrapper runDiffWrapper
+
+instance (Fix l, Fix r) => Fix (Combine l r) where
+  fix = Combine fix fix
+  runFix = Combine runFix runFix
+
+instance (FreeVector l, FreeVector r) => FreeVector (Combine l r) where
+  freeVector = Combine freeVector freeVector
+  runFreeVector = Combine runFreeVector runFreeVector
+
+instance (Lang l, Lang r) => Lang (Combine l r) where
+  exfalso = Combine exfalso exfalso
   runWriter = Combine runWriter runWriter
   writer = Combine writer writer
   double2Float = Combine double2Float double2Float
   float2Double = Combine float2Double float2Double
   state = Combine state state
   runState = Combine runState runState
-  putStrLn = Combine putStrLn putStrLn
-
-instance (DLang l, DLang r) => DLang (Combine l r) where
diff --git a/DDF/DBI.hs b/DDF/DBI.hs
--- a/DDF/DBI.hs
+++ b/DDF/DBI.hs
@@ -17,11 +17,11 @@
   DefaultSignatures,
   TypeOperators,
   TypeApplications,
-  PartialTypeSignatures
+  PartialTypeSignatures,
+  NoImplicitPrelude
 #-}
 
 module DDF.DBI (module DDF.DBI, module DDF.ImportMeta) where
-import qualified Prelude as P
 import DDF.ImportMeta
 
 class Monoid r m where
@@ -38,7 +38,6 @@
   -- Use lam to do automatic lifting of variables.
   hoas :: (r (a, h) a -> r (a, h) b) -> r h (a -> b)
   hoas f = abs $ f z
-  liftEnv :: r () x -> r h x
   com :: r h ((b -> c) -> (a -> b) -> (a -> c))
   com = lam3 $ \f g x -> app f (app g x)
   flip :: r h ((a -> b -> c) -> (b -> a -> c))
@@ -54,6 +53,9 @@
   let_ :: r h (a -> (a -> b) -> b)
   let_ = flip1 id
 
+class LiftEnv r where
+  liftEnv :: r () a -> r h a
+
 const1 = app const
 map2 = app2 map
 return = pure
@@ -66,14 +68,14 @@
 flip2 = app2 flip
 let_2 = app2 let_
 
-class Functor r f where
+class DBI r => Functor r f where
   map ::  r h ((a -> b) -> (f a -> f b))
 
 class Functor r a => Applicative r a where
   pure :: r h (x -> a x)
   ap :: r h (a (x -> y) -> a x -> a y)
 
-class (DBI r, Applicative r m) => Monad r m where
+class Applicative r m => Monad r m where
   bind :: r h (m a -> (a -> m b) -> m b)
   join :: r h (m (m a) -> m a)
   join = lam $ \m -> bind2 m id
@@ -83,7 +85,6 @@
 class BiFunctor r p where
   bimap :: r h ((a -> b) -> (c -> d) -> p a c -> p b d)
 
-app3 f a b c = app (app2 f a b) c
 com2 = app2 com
 
 class NT repr l r where
@@ -99,23 +100,37 @@
     conv = convS
 
 instance {-# OVERLAPPING #-} NT repr x x where
-    conv = P.id
+    conv x = x
 
 lam :: forall repr a b h. DBI repr =>
-  ((forall k. NT repr (a, h) k => repr k a) -> (repr (a, h)) b) -> repr h (a -> b)
+  ((forall k. NT repr (a, h) k => repr k a) -> (repr (a, h)) b) ->
+  repr h (a -> b)
 lam f = hoas (\x -> f $ conv x)
 
 lam2 :: forall repr a b c h. DBI repr =>
-  ((forall k. NT repr (a, h) k => repr k a) -> (forall k. NT repr (b, (a, h)) k => repr k b) -> (repr (b, (a, h))) c) -> repr h (a -> b -> c)
+  ((forall k. NT repr (a, h) k => repr k a) ->
+   (forall k. NT repr (b, (a, h)) k => repr k b) ->
+   (repr (b, (a, h))) c) ->
+  repr h (a -> b -> c)
 lam2 f = lam $ \x -> lam $ \y -> f x y
 
 lam3 f = lam2 $ \a b -> lam $ \c -> f a b c
 
+lam4 f = lam3 $ \a b c -> lam $ \d -> f a b c d
+
 app2 f a = app (app f a)
 
+app3 f a b = app (app2 f a b)
+
+app4 f a b c = app (app3 f a b c)
+
+app5 f a b c d = app (app4 f a b c d)
+
 plus2 = app2 plus
 
 noEnv :: repr () x -> repr () x
-noEnv = P.id
+noEnv x = x
 
-scomb2 = app2 scomb
+scomb2 = app2 scomb
+plus1 = app plus
+dup1 = app dup
diff --git a/DDF/DLang.hs b/DDF/DLang.hs
deleted file mode 100644
--- a/DDF/DLang.hs
+++ /dev/null
@@ -1,12 +0,0 @@
-{-# LANGUAGE
-  RankNTypes,
-  NoImplicitPrelude,
-  TypeOperators,
-  NoMonomorphismRestriction
-#-}
-
-module DDF.DLang (module DDF.DLang, module DDF.Lang) where
-
-import DDF.Lang
-
-class Lang r => DLang r where
diff --git a/DDF/Diff.hs b/DDF/Diff.hs
--- a/DDF/Diff.hs
+++ b/DDF/Diff.hs
@@ -6,40 +6,55 @@
   TypeApplications,
   FlexibleContexts,
   UndecidableInstances,
-  TypeFamilies
+  TypeFamilies,
+  MultiParamTypeClasses,
+  TypeOperators,
+  DataKinds
 #-}
 
 module DDF.Diff where
 
-import DDF.DLang
+import DDF.Lang
+import qualified Prelude as M
 import qualified Data.Map as M
 import qualified DDF.Map as Map
+import qualified Data.Bimap as M
+import qualified DDF.Meta.Dual as M
+import qualified DDF.VectorTF as VTF
+import qualified DDF.Meta.DiffWrapper as M.DW
+import qualified Data.Functor.Foldable as M
+import qualified DDF.Meta.FreeVector as M
 
+type instance DiffType v (l -> r) = DiffType v l -> DiffType v r
 instance DBI r => DBI (Diff r v) where
   z = Diff z
   s (Diff x) = Diff $ s x
   abs (Diff f) = Diff $ abs f
   app (Diff f) (Diff x) = Diff $ app f x
   hoas f = Diff $ hoas (\x -> runDiff $ f $ Diff x)
-  liftEnv (Diff x) = Diff $ liftEnv x
 
+type instance DiffType v M.Bool = M.Bool
 instance Bool r => Bool (Diff r v) where
   bool x = Diff $ bool x
   ite = Diff ite
 
+type instance DiffType v M.Char = M.Char
 instance Char r => Char (Diff r v) where
   char = Diff . char
 
+type instance DiffType v (l, r) = (DiffType v l, DiffType v r)
 instance Prod r => Prod (Diff r v) where
   mkProd = Diff mkProd
   zro = Diff zro
   fst = Diff fst
 
+type instance DiffType v (M.Dual l r) = M.Dual (DiffType v l) (DiffType v r)
 instance Dual r => Dual (Diff r v) where
   dual = Diff $ dual
   runDual = Diff $ runDual
 
-instance (Vector r v, Double r, Dual r) => Double (Diff r v) where
+type instance DiffType v M.Double = M.Dual M.Double v
+instance (Vector r v, Lang r) => Double (Diff r v) where
   double x = Diff $ mkDual2 (double x) zero
   doublePlus = Diff $ lam2 $ \l r ->
     mkDual2 (plus2 (dualOrig1 l) (dualOrig1 r)) (plus2 (dualDiff1 l) (dualDiff1 r))
@@ -53,7 +68,9 @@
       (divide2 (minus2 (mult2 (dualOrig1 r) (dualDiff1 l)) (mult2 (dualOrig1 l) (dualDiff1 r)))
         (mult2 (dualOrig1 r) (dualOrig1 r)))
   doubleExp = Diff $ lam $ \x -> let_2 (doubleExp1 (dualOrig1 x)) (lam $ \e -> mkDual2 e (mult2 e (dualDiff1 x)))
+  doubleEq = Diff $ lam2 $ \l r -> doubleEq2 (dualOrig1 l) (dualOrig1 r)
 
+type instance DiffType v M.Float = M.Dual M.Float v
 instance (Vector r v, Lang r) => Float (Diff r v) where
   float x = Diff $ mkDual2 (float x) zero
   floatPlus = Diff $ lam2 $ \l r ->
@@ -69,43 +86,126 @@
         (float2Double1 (mult2 (float2Double1 (dualOrig1 r)) (dualOrig1 r))))
   floatExp = Diff (lam $ \x -> let_2 (floatExp1 (dualOrig1 x)) (lam $ \e -> mkDual2 e (mult2 (float2Double1 e) (dualDiff1 x))))
 
+type instance DiffType v (Maybe l) = Maybe (DiffType v l)
 instance Option r => Option (Diff r v) where
   nothing = Diff nothing
   just = Diff just
   optionMatch = Diff optionMatch
 
+type instance DiffType v (M.Map k val) = M.Map (DiffType v k) (DiffType v val)
 instance Map.Map r => Map.Map (Diff r v) where
   empty = Diff Map.empty
   singleton = Diff Map.singleton
-  lookup :: forall h k a. Map.Ord k => Diff r v h (k -> M.Map k a -> Maybe a)
+  lookup :: forall h k a. Map.Ord k => Diff r v h (M.Map k a -> k -> Maybe a)
   lookup = withDict (Map.diffOrd (Proxy :: Proxy (v, k))) (Diff Map.lookup)
   alter :: forall h k a. Map.Ord k => Diff r v h ((Maybe a -> Maybe a) -> k -> M.Map k a -> M.Map k a)
   alter = withDict (Map.diffOrd (Proxy :: Proxy (v, k))) (Diff Map.alter)
   mapMap = Diff Map.mapMap
+  unionWith :: forall h k a. Map.Ord k => Diff r v h ((a -> a -> a) -> M.Map k a -> M.Map k a -> M.Map k a)
+  unionWith = withDict (Map.diffOrd (Proxy :: Proxy (v, k))) (Diff Map.unionWith)
 
+type instance DiffType v (M.Bimap a b) = M.Bimap (DiffType v a) (DiffType v b)
 instance Bimap r => Bimap (Diff r v) where
+  size = Diff size
+  toMapL = Diff toMapL
+  toMapR = Diff toMapR
+  lookupL :: forall h a b. (Map.Ord a, Map.Ord b) => Diff r v h (M.Bimap a b -> a -> Maybe b)
+  lookupL = withDict (Map.diffOrd (Proxy :: Proxy (v, a))) (withDict (Map.diffOrd (Proxy :: Proxy (v, b))) (Diff lookupL))
+  lookupR :: forall h a b. (Map.Ord a, Map.Ord b) => Diff r v h (M.Bimap a b -> b -> Maybe a)
+  lookupR = withDict (Map.diffOrd (Proxy :: Proxy (v, a))) (withDict (Map.diffOrd (Proxy :: Proxy (v, b))) (Diff lookupR))
+  empty = Diff empty
+  singleton = Diff singleton
+  insert :: forall h a b. (Map.Ord a, Map.Ord b) => Diff r v h ((a, b) -> M.Bimap a b -> M.Bimap a b)
+  insert = withDict (Map.diffOrd (Proxy :: Proxy (v, a))) (withDict (Map.diffOrd (Proxy :: Proxy (v, b))) (Diff insert))
+  updateL :: forall h a b. (Map.Ord a, Map.Ord b) => Diff r v h ((b -> Maybe b) -> a -> M.Bimap a b -> M.Bimap a b)
+  updateL = withDict (Map.diffOrd (Proxy :: Proxy (v, a))) (withDict (Map.diffOrd (Proxy :: Proxy (v, b))) (Diff updateL))
+  updateR :: forall h a b. (Map.Ord a, Map.Ord b) => Diff r v h ((a -> Maybe a) -> b -> M.Bimap a b -> M.Bimap a b)
+  updateR = withDict (Map.diffOrd (Proxy :: Proxy (v, a))) (withDict (Map.diffOrd (Proxy :: Proxy (v, b))) (Diff updateR))
 
+type instance DiffType v () = ()
 instance Unit r => Unit (Diff r v) where
   unit = Diff unit
 
-instance (Vector r v, Lang r) => Lang (Diff r v) where
-  fix = Diff fix
+type instance DiffType v (M.Either l r) = M.Either (DiffType v l) (DiffType v r)
+instance Sum r => Sum (Diff r v) where
   left = Diff left
   right = Diff right
   sumMatch = Diff sumMatch
-  exfalso = Diff exfalso
-  ioRet = Diff ioRet
-  ioBind = Diff ioBind
+
+instance Int r => Int (Diff r v) where
+  int = Diff . int
+  pred = Diff pred
+  isZero = Diff isZero
+
+instance Y r => Y (Diff r v) where
+  y = Diff y
+
+type instance DiffType v (M.IO l) = M.IO (DiffType v l)
+instance IO r => IO (Diff r v) where
+  putStrLn = Diff putStrLn
+
+type instance DiffType v [l] = [DiffType v l]
+instance List r => List (Diff r v) where
   nil = Diff nil
   cons = Diff cons
   listMatch = Diff listMatch
-  ioMap = Diff ioMap
+
+instance Functor r M.IO => Functor (Diff r v) M.IO where
+  map = Diff map
+
+instance Applicative r M.IO => Applicative (Diff r v) M.IO where
+  pure = Diff pure
+  ap = Diff ap
+
+instance Monad r M.IO => Monad (Diff r v) M.IO where
+  bind = Diff bind
+  join = Diff join
+
+instance (Vector r v, Lang r) => VTF.VectorTF (Diff r v) where
+  zero = Diff VTF.zero
+  basis = Diff VTF.basis
+  plus = Diff VTF.plus
+  mult = Diff $ VTF.mult `com2` dualOrig
+  vtfMatch = Diff $ lam4 $ \ze b p m -> VTF.vtfMatch4 ze b p $ lam $ \x -> app m (mkDual2 x zero)
+
+type instance DiffType v (M.DW.DiffWrapper a x) = M.DW.DiffWrapper (v ': a) x
+instance DiffWrapper r => DiffWrapper (Diff r v) where
+  diffWrapper = Diff diffWrapper
+  runDiffWrapper = Diff runDiffWrapper
+
+type instance DiffType v (M.Fix f) = M.DW.DiffWrapper '[v] (f (M.Fix f))
+instance DiffWrapper r => Fix (Diff r v) where
+  fix = Diff diffWrapper
+  runFix = Diff runDiffWrapper
+
+type instance DiffType v (M.FreeVector a b) = M.FreeVector (DiffType v a) (DiffType v b)
+instance FreeVector r => FreeVector (Diff r v) where
+  freeVector = Diff freeVector
+  runFreeVector = Diff runFreeVector
+
+type instance DiffType v Void = Void
+type instance DiffType v (Writer l r) = Writer (DiffType v l) (DiffType v r)
+type instance DiffType v (State l r) = State (DiffType v l) (DiffType v r)
+instance (Vector r v, Lang r) => Lang (Diff r v) where
+  exfalso = Diff exfalso
   writer = Diff writer
   runWriter = Diff runWriter
   float2Double = Diff $ bimap2 float2Double id
   double2Float = Diff $ bimap2 double2Float id
   state = Diff state
   runState = Diff runState
-  putStrLn = Diff putStrLn
 
-instance (Vector r v, DLang r) => DLang (Diff r v) where
+instance Map.Ord () where
+  diffOrd _ = Dict
+
+instance Map.Ord a => Map.Ord [a] where
+  diffOrd (_ :: Proxy (v, [a])) = withDict (Map.diffOrd (Proxy :: Proxy (v, a))) Dict
+
+instance Map.Ord l => Map.Ord (M.Dual l r) where
+  diffOrd (_ :: Proxy (v, M.Dual l r)) = withDict (Map.diffOrd (Proxy :: Proxy (v, l))) Dict
+
+instance Map.Ord M.Double where
+  diffOrd _ = Dict
+
+instance Map.Ord M.Float where
+  diffOrd _ = Dict
diff --git a/DDF/DiffWrapper.hs b/DDF/DiffWrapper.hs
new file mode 100644
--- /dev/null
+++ b/DDF/DiffWrapper.hs
@@ -0,0 +1,8 @@
+module DDF.DiffWrapper (module DDF.DiffWrapper, module DDF.DBI) where
+
+import DDF.DBI
+import DDF.Meta.DiffWrapper as DW
+
+class DBI r => DiffWrapper r where
+  diffWrapper :: r h (DW.FDiffType a x -> DW.DiffWrapper a x)
+  runDiffWrapper :: r h (DW.DiffWrapper a x -> DW.FDiffType a x)
diff --git a/DDF/Double.hs b/DDF/Double.hs
--- a/DDF/Double.hs
+++ b/DDF/Double.hs
@@ -1,11 +1,14 @@
-{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE
+  NoImplicitPrelude,
+  NoMonomorphismRestriction
+#-}
 
-module DDF.Double (module DDF.Double, module DDF.DBI) where
+module DDF.Double (module DDF.Double, module DDF.Bool) where
 
-import DDF.DBI
+import DDF.Bool
 import qualified Prelude as M
 
-class DBI r => Double r where
+class Bool r => Double r where
   double :: M.Double -> r h M.Double
   doubleZero :: r h M.Double
   doubleZero = double 0
@@ -16,3 +19,12 @@
   doubleMult :: r h (M.Double -> M.Double -> M.Double)
   doubleDivide :: r h (M.Double -> M.Double -> M.Double)
   doubleExp :: r h (M.Double -> M.Double)
+  doubleEq :: r h (M.Double -> M.Double -> M.Bool)
+
+doublePlus1 = app doublePlus
+doublePlus2 = app2 doublePlus
+doubleMinus2 = app2 doubleMinus
+doubleMult2 = app2 doubleMult
+doubleDivide2 = app2 doubleDivide
+doubleExp1 = app doubleExp
+doubleEq2 = app2 doubleEq
diff --git a/DDF/Eval.hs b/DDF/Eval.hs
--- a/DDF/Eval.hs
+++ b/DDF/Eval.hs
@@ -2,7 +2,8 @@
   NoImplicitPrelude,
   LambdaCase,
   TypeFamilies,
-  FlexibleContexts
+  FlexibleContexts,
+  MultiParamTypeClasses
 #-}
 
 module DDF.Eval where
@@ -17,7 +18,13 @@
 import qualified Data.Map as M.Map
 import qualified DDF.Meta.Dual as M
 import qualified DDF.Map as Map
-import DDF.DLang
+import qualified DDF.Meta.VectorTF as M.VTF
+import qualified Data.Bimap as M.Bimap
+import qualified DDF.VectorTF as VTF
+import qualified DDF.Meta.DiffWrapper as M.DW
+import qualified Data.Functor.Foldable as M
+import qualified DDF.Meta.FreeVector as M
+import DDF.Lang
 
 comb = Eval . M.const
 
@@ -26,7 +33,6 @@
   s (Eval a) = Eval $ a . M.snd
   abs (Eval f) = Eval $ \h a -> f (a, h)
   app (Eval f) (Eval x) = Eval $ \h -> f h $ x h
-  liftEnv (Eval x) = Eval $ \_ -> x ()
 
 instance Bool Eval where
   bool = comb
@@ -47,6 +53,7 @@
   doubleMult = comb (*)
   doubleDivide = comb (/)
   doubleExp = comb M.exp
+  doubleEq = comb (==)
 
 instance Float Eval where
   float = comb
@@ -66,11 +73,22 @@
 instance Map.Map Eval where
   empty = comb M.Map.empty
   singleton = comb M.Map.singleton
-  lookup = comb M.Map.lookup
+  lookup = flip1 $ comb M.Map.lookup
   alter = comb M.Map.alter
   mapMap = comb M.fmap
+  unionWith = comb M.Map.unionWith
 
 instance Bimap Eval where
+  size = comb M.Bimap.size
+  lookupL = flip1 $ comb M.Bimap.lookup
+  lookupR = flip1 $ comb M.Bimap.lookupR
+  toMapL = comb M.Bimap.toMap
+  toMapR = comb M.Bimap.toMapR
+  empty = comb M.Bimap.empty
+  singleton = comb $ \(a, b) -> M.Bimap.singleton a b
+  insert = comb $ \(a, b) -> M.Bimap.insert a b
+  updateL = comb M.Bimap.update
+  updateR = comb M.Bimap.updateR
 
 instance Dual Eval where
   dual = comb M.Dual
@@ -79,29 +97,71 @@
 instance Unit Eval where
   unit = comb ()
 
-instance Lang Eval where
-  fix = comb loop
-    where loop x = x $ loop x
+instance Sum Eval where
   left = comb M.Left
   right = comb M.Right
   sumMatch = comb $ \l r -> \case
                              M.Left x -> l x
                              M.Right x -> r x
-  exfalso = comb absurd
-  ioRet = comb M.return
-  ioBind = comb (>>=)
+
+instance Int Eval where
+  int = comb
+  pred = comb ((-) 1)
+  isZero = comb (== 0)
+
+instance Y Eval where
+  y = comb loop
+    where loop x = x $ loop x
+
+instance List Eval where
   nil = comb []
   cons = comb (:)
   listMatch = comb $ \l r -> \case
                             [] -> l
                             x:xs -> r x xs
-  ioMap = comb M.fmap
+
+instance Functor Eval M.IO where
+  map = comb M.fmap
+
+instance Applicative Eval M.IO where
+  pure = comb M.pure
+  ap = comb M.ap
+
+instance Monad Eval M.IO where
+  join = comb M.join
+  bind = comb (>>=)
+
+instance IO Eval where
+  putStrLn = comb M.putStrLn
+
+instance VTF.VectorTF Eval where
+  zero = comb M.VTF.Zero
+  basis = comb M.VTF.Basis
+  plus = comb M.VTF.Plus
+  mult = comb M.VTF.Mult
+  vtfMatch = comb $ \zr b p m -> \case
+                                 M.VTF.Zero -> zr
+                                 M.VTF.Basis t -> b t
+                                 M.VTF.Plus l r -> p l r
+                                 M.VTF.Mult l r -> m l r
+
+instance DiffWrapper Eval where
+  diffWrapper = comb M.DW.DiffWrapper
+  runDiffWrapper = comb M.DW.runDiffWrapper
+
+instance Fix Eval where
+  fix = comb M.Fix
+  runFix = comb M.unfix
+
+instance FreeVector Eval where
+  freeVector = comb M.FreeVector
+  runFreeVector = comb M.runFreeVector
+
+instance Lang Eval where
+  exfalso = comb absurd
   writer = comb (M.WriterT . M.Identity)
   runWriter = comb M.runWriter
   float2Double = comb M.float2Double
   double2Float = comb M.double2Float
   state = comb M.state
   runState = comb M.runState
-  putStrLn = comb M.putStrLn
-
-instance DLang Eval where
diff --git a/DDF/Fix.hs b/DDF/Fix.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Fix.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE NoMonomorphismRestriction, NoImplicitPrelude #-}
+
+module DDF.Fix (module DDF.Fix, module DDF.DBI) where
+
+import DDF.DBI
+import qualified Data.Functor.Foldable as M
+
+class DBI r => Fix r where
+  fix :: r h (f (M.Fix f) -> M.Fix f)
+  runFix :: r h (M.Fix f -> f (M.Fix f))
+
+fix1 = app fix
+runFix1 = app runFix
diff --git a/DDF/FreeVector.hs b/DDF/FreeVector.hs
new file mode 100644
--- /dev/null
+++ b/DDF/FreeVector.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+module DDF.FreeVector (module DDF.FreeVector, module DDF.DBI) where
+
+import DDF.DBI
+import qualified DDF.Meta.FreeVector as M
+
+class DBI r => FreeVector r where
+  freeVector :: r h ((b -> d) -> M.FreeVector b d)
+  runFreeVector :: r h (M.FreeVector b d -> (b -> d))
+
+freeVector1 = app freeVector
+runFreeVector1 = app runFreeVector
+runFreeVector2 = app2 runFreeVector
diff --git a/DDF/GDiff.hs b/DDF/GDiff.hs
--- a/DDF/GDiff.hs
+++ b/DDF/GDiff.hs
@@ -4,23 +4,24 @@
   InstanceSigs,
   ScopedTypeVariables,
   TypeFamilies,
-  TypeApplications
+  TypeApplications,
+  MultiParamTypeClasses,
+  FlexibleInstances,
+  FlexibleContexts
 #-}
 
-module DDF.GDiff (module DDF.Meta.Diff) where
-import DDF.DLang
+module DDF.GDiff where
+import DDF.Lang
 import qualified Prelude as M
-import DDF.Meta.Diff
 import DDF.Diff ()
-import qualified Data.Map as M
 import qualified DDF.Map as Map
+import qualified DDF.VectorTF as VTF
 
 instance DBI r => DBI (GDiff r) where
   z = GDiff (M.const z)
   s (GDiff x) = GDiff (\p -> s $ x p)
   app (GDiff f) (GDiff x) = GDiff (\p -> app (f p) (x p))
   abs (GDiff x) = GDiff (\p -> abs $ x p)
-  liftEnv (GDiff x) = GDiff (\p -> liftEnv $ x p)
 
 instance Bool r => Bool (GDiff r) where
   bool x = GDiff $ M.const $ bool x
@@ -38,14 +39,22 @@
   dual = GDiff $ M.const $ dual
   runDual = GDiff $ M.const $ runDual
 
-instance (Double r, Dual r) => Double (GDiff r) where
+instance Lang r => Double (GDiff r) where
   double x = GDiff $ M.const $ double x
   doublePlus = GDiff $ M.const $ doublePlus
   doubleMinus = GDiff $ M.const $ doubleMinus
   doubleMult = GDiff $ M.const $ doubleMult
   doubleDivide = GDiff $ M.const $ doubleDivide
   doubleExp = GDiff $ M.const $ doubleExp
+  doubleEq = GDiff $ M.const $ doubleEq
 
+instance Lang r => VTF.VectorTF (GDiff r) where
+  zero = GDiff $ M.const $ VTF.zero
+  basis = GDiff $ M.const $ VTF.basis
+  plus = GDiff $ M.const $ VTF.plus
+  mult = GDiff $ M.const $ VTF.mult
+  vtfMatch = GDiff $ M.const $ VTF.vtfMatch
+
 instance Lang r => Float (GDiff r) where
   float x = GDiff $ M.const $ float x
   floatPlus = GDiff $ M.const $ floatPlus
@@ -62,35 +71,75 @@
 instance Map.Map r => Map.Map (GDiff r) where
   empty = GDiff $ M.const Map.empty
   singleton = GDiff $ M.const Map.singleton
-  lookup :: forall h k a. Map.Ord k => GDiff r h (k -> M.Map k a -> Maybe a)
-  lookup = GDiff $ \(_ :: Proxy v) -> withDict (Map.diffOrd (Proxy :: Proxy (v, k))) Map.lookup
-  alter :: forall h k a. Map.Ord k => GDiff r h ((Maybe a -> Maybe a) -> k -> M.Map k a -> M.Map k a)
-  alter = GDiff $ \(_ :: Proxy v) -> withDict (Map.diffOrd (Proxy :: Proxy (v, k))) Map.alter
+  lookup = GDiff $ M.const Map.lookup
+  alter = GDiff $ M.const Map.alter
   mapMap = GDiff $ M.const Map.mapMap
+  unionWith = GDiff $ M.const Map.unionWith
 
 instance Bimap r => Bimap (GDiff r) where
+  size = GDiff $ M.const size
+  lookupL = GDiff $ M.const lookupL
+  lookupR = GDiff $ M.const lookupR
+  empty = GDiff $ M.const empty
+  singleton = GDiff $ M.const singleton
+  insert = GDiff $ M.const insert
+  updateL = GDiff $ M.const updateL
+  updateR = GDiff $ M.const updateR
+  toMapL = GDiff $ M.const toMapL
+  toMapR = GDiff $ M.const toMapR
 
 instance Unit r => Unit (GDiff r) where
   unit = GDiff $ M.const unit
 
-instance Lang r => Lang (GDiff r) where
-  fix = GDiff $ M.const fix
+instance Sum r => Sum (GDiff r) where
   left = GDiff $ M.const left
   right = GDiff $ M.const right
   sumMatch = GDiff $ M.const sumMatch
-  exfalso = GDiff $ M.const exfalso
-  ioRet = GDiff $ M.const ioRet
-  ioBind = GDiff $ M.const ioBind
+
+instance Int r => Int (GDiff r) where
+  int x = GDiff $ M.const $ int x
+  pred = GDiff $ M.const pred
+  isZero = GDiff $ M.const isZero
+
+instance Y r => Y (GDiff r) where
+  y = GDiff $ M.const y
+
+instance Functor r M.IO => Functor (GDiff r) M.IO where
+  map = GDiff $ M.const map
+
+instance Applicative r M.IO => Applicative (GDiff r) M.IO where
+  pure = GDiff $ M.const pure
+  ap = GDiff $ M.const ap
+
+instance Monad r M.IO => Monad (GDiff r) M.IO where
+  bind = GDiff $ M.const bind
+  join = GDiff $ M.const join
+
+instance IO r => IO (GDiff r) where
+  putStrLn = GDiff $ M.const putStrLn
+
+instance List r => List (GDiff r) where
   nil = GDiff $ M.const nil
   cons = GDiff $ M.const cons
   listMatch = GDiff $ M.const listMatch
-  ioMap = GDiff $ M.const ioMap
+
+instance DiffWrapper r => DiffWrapper (GDiff r) where
+  diffWrapper = GDiff $ M.const diffWrapper
+  runDiffWrapper = GDiff $ M.const runDiffWrapper
+
+instance DiffWrapper r => Fix (GDiff r) where
+  fix = GDiff $ M.const fix
+  runFix = GDiff $ M.const runFix
+
+instance FreeVector r => FreeVector (GDiff r) where
+  freeVector = GDiff $ M.const freeVector
+  runFreeVector = GDiff $ M.const runFreeVector
+
+instance Lang r => Lang (GDiff r) where
+  exfalso = GDiff $ M.const exfalso
   writer = GDiff $ M.const writer
   runWriter = GDiff $ M.const runWriter
   float2Double = GDiff $ M.const float2Double
   double2Float = GDiff $ M.const double2Float
   state = GDiff $ M.const state
   runState = GDiff $ M.const runState
-  putStrLn = GDiff $ M.const putStrLn
-
-instance DLang r => DLang (GDiff r) where
diff --git a/DDF/GInfDiff.hs b/DDF/GInfDiff.hs
deleted file mode 100644
--- a/DDF/GInfDiff.hs
+++ /dev/null
@@ -1,85 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
-
-module DDF.GInfDiff where
-
-import DDF.DLang
-import DDF.InfDiff ()
-import qualified DDF.Map as Map
-
-instance DBI r => DBI (GInfDiff r) where
-  z = GInfDiff $ \_ -> z
-  s (GInfDiff x) = GInfDiff $ s . x
-  abs (GInfDiff x) = GInfDiff $ abs . x
-  app (GInfDiff f) (GInfDiff x) = GInfDiff $ \p -> app (f p) (x p)
-  liftEnv (GInfDiff x) = GInfDiff $ liftEnv . x
-
-instance Dual r => Dual (GInfDiff r) where
-  dual = GInfDiff $ \_ -> dual
-  runDual = GInfDiff $ \_ -> runDual
-
-instance Bimap r => Bimap (GInfDiff r) where
-
-instance Lang r => Float (GInfDiff r) where
-  float x = GInfDiff $ \_ -> float x
-  floatPlus = GInfDiff $ \_ -> floatPlus
-  floatMinus = GInfDiff $ \_ -> floatMinus
-  floatMult = GInfDiff $ \_ -> floatMult
-  floatDivide = GInfDiff $ \_ -> floatDivide
-  floatExp = GInfDiff $ \_ -> floatExp
-
-instance (Dual r, Double r) => Double (GInfDiff r) where
-  double x = GInfDiff $ \_ -> double x
-  doublePlus = GInfDiff $ \_ -> doublePlus
-  doubleMinus = GInfDiff $ \_ -> doubleMinus
-  doubleMult = GInfDiff $ \_ -> doubleMult
-  doubleDivide = GInfDiff $ \_ -> doubleDivide
-  doubleExp = GInfDiff $ \_ -> doubleExp
-
-instance Char r => Char (GInfDiff r) where
-  char x = GInfDiff $ \_ -> char x
-
-instance Bool r => Bool (GInfDiff r) where
-  bool x = GInfDiff $ \_ -> bool x
-  ite = GInfDiff $ \_ -> ite
-
-instance Prod r => Prod (GInfDiff r) where
-  mkProd = GInfDiff $ \_ -> mkProd
-  zro = GInfDiff $ \_ -> zro
-  fst = GInfDiff $ \_ -> fst
-
-instance Option r => Option (GInfDiff r) where
-  nothing = GInfDiff $ \_ -> nothing
-  just = GInfDiff $ \_ -> just
-  optionMatch = GInfDiff $ \_ -> optionMatch
-
-instance Map.Map r => Map.Map (GInfDiff r) where
-  empty = GInfDiff $ \_ -> Map.empty
-  singleton = GInfDiff $ \_ -> Map.singleton
-  lookup = GInfDiff $ \_ -> Map.lookup
-  alter = GInfDiff $ \_ -> Map.alter
-  mapMap = GInfDiff $ \_ -> Map.mapMap
-
-instance Unit r => Unit (GInfDiff r) where
-  unit = GInfDiff $ \_ -> unit
-
-instance Lang r => Lang (GInfDiff r) where
-  fix = GInfDiff $ \_ -> fix
-  left = GInfDiff $ \_ -> left
-  right = GInfDiff $ \_ -> right
-  sumMatch = GInfDiff $ \_ -> sumMatch
-  exfalso = GInfDiff $ \_ -> exfalso
-  ioRet = GInfDiff $ \_ -> ioRet
-  ioBind = GInfDiff $ \_ -> ioBind
-  ioMap = GInfDiff $ \_ -> ioMap
-  writer = GInfDiff $ \_ -> writer
-  runWriter = GInfDiff $ \_ -> runWriter
-  nil = GInfDiff $ \_ -> nil
-  cons = GInfDiff $ \_ -> cons
-  listMatch = GInfDiff $ \_ -> listMatch
-  float2Double = GInfDiff $ \_ -> float2Double
-  double2Float = GInfDiff $ \_ -> double2Float
-  state = GInfDiff $ \_ -> state
-  runState = GInfDiff $ \_ -> runState
-  putStrLn = GInfDiff $ \_ -> putStrLn
-
-instance DLang r => DLang (GInfDiff r) where
diff --git a/DDF/IO.hs b/DDF/IO.hs
new file mode 100644
--- /dev/null
+++ b/DDF/IO.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE NoImplicitPrelude, FlexibleContexts #-}
+
+module DDF.IO (module DDF.IO, module DDF.List, module DDF.Char, module DDF.Unit) where
+
+import DDF.List
+import DDF.Char
+import DDF.Unit
+import qualified Prelude as M
+
+class (List r, Unit r, Char r, Monad r M.IO) => IO r where
+  putStrLn :: r h (String -> M.IO ())
diff --git a/DDF/ImpW.hs b/DDF/ImpW.hs
--- a/DDF/ImpW.hs
+++ b/DDF/ImpW.hs
@@ -5,13 +5,16 @@
   ScopedTypeVariables,
   ExistentialQuantification,
   TypeFamilies,
-  TypeApplications
+  TypeApplications,
+  FlexibleInstances,
+  MultiParamTypeClasses
 #-}
 
 module DDF.ImpW where
 
-import DDF.DLang
+import DDF.Lang
 import qualified DDF.Map as Map
+import qualified DDF.VectorTF as VTF
 
 runImpW :: forall r h x. Unit r => ImpW r h x -> RunImpW r h x
 runImpW (ImpW x) = RunImpW x
@@ -28,8 +31,6 @@
   app (NoImpW f) (ImpW x) = ImpW (lam $ \w -> app (conv f) (app (conv x) w))
   abs (ImpW f) = ImpW (flip1 $ abs f)
   abs (NoImpW x) = NoImpW (abs x)
-  liftEnv (NoImpW x) = NoImpW $ liftEnv x
-  liftEnv (ImpW x) = ImpW $ liftEnv x
 
 instance (Prod r, Bool r) => Bool (ImpW r) where
   bool = NoImpW . bool
@@ -50,6 +51,7 @@
   doubleMinus = NoImpW doubleMinus
   doubleMult = NoImpW doubleMult
   doubleDivide = NoImpW doubleDivide
+  doubleEq = NoImpW doubleEq
 
 instance (Prod r, Float r) => Float (ImpW r) where
   float = NoImpW . float
@@ -70,8 +72,19 @@
   lookup = NoImpW Map.lookup
   alter = NoImpW Map.alter
   mapMap = NoImpW Map.mapMap
+  unionWith = NoImpW Map.unionWith
 
 instance Bimap r => Bimap (ImpW r) where
+  size = NoImpW size
+  lookupL = NoImpW lookupL
+  lookupR = NoImpW lookupR
+  singleton = NoImpW singleton
+  empty = NoImpW empty
+  insert = NoImpW insert
+  toMapL = NoImpW toMapL
+  toMapR = NoImpW toMapR
+  updateL = NoImpW updateL
+  updateR = NoImpW updateR
 
 instance Dual r => Dual (ImpW r) where
   dual = NoImpW dual
@@ -80,24 +93,62 @@
 instance (Prod r, Unit r) => Unit (ImpW r) where
   unit = NoImpW unit
 
-instance Lang r => Lang (ImpW r) where
+instance (Prod r, Sum r) => Sum (ImpW r) where
+  left = NoImpW left
+  right = NoImpW right
+  sumMatch = NoImpW sumMatch
+
+instance (Prod r, Int r) => Int (ImpW r) where
+  int = NoImpW . int
+  pred = NoImpW pred
+  isZero = NoImpW isZero
+
+instance (Prod r, IO r) => IO (ImpW r) where
+  putStrLn = NoImpW putStrLn
+
+instance (Prod r, List r) => List (ImpW r) where
   nil = NoImpW nil
   cons = NoImpW cons
   listMatch = NoImpW listMatch
-  ioRet = NoImpW ioRet
-  ioMap = NoImpW ioMap
-  ioBind = NoImpW ioBind
-  exfalso = NoImpW exfalso
+
+instance (Prod r, Y r) => Y (ImpW r) where
+  y = NoImpW y
+
+instance (Prod r, Functor r x) => Functor (ImpW r) x where
+  map = NoImpW map
+
+instance (Prod r, Applicative r x) => Applicative (ImpW r) x where
+  ap = NoImpW ap
+  pure = NoImpW pure
+
+instance (Prod r, Monad r x) => Monad (ImpW r) x where
+  join = NoImpW join
+  bind = NoImpW bind
+
+instance (Prod r, VTF.VectorTF r) => VTF.VectorTF (ImpW r) where
+  zero = NoImpW VTF.zero
+  basis = NoImpW VTF.basis
+  plus = NoImpW VTF.plus
+  mult = NoImpW VTF.mult
+  vtfMatch = NoImpW VTF.vtfMatch
+
+instance (Prod r, DiffWrapper r) => DiffWrapper (ImpW r) where
+  diffWrapper = NoImpW diffWrapper
+  runDiffWrapper = NoImpW runDiffWrapper
+
+instance (Prod r, Fix r) => Fix (ImpW r) where
   fix = NoImpW fix
-  left = NoImpW left
-  right = NoImpW right
-  sumMatch = NoImpW sumMatch
+  runFix = NoImpW runFix
+
+instance (Prod r, FreeVector r) => FreeVector (ImpW r) where
+  freeVector = NoImpW freeVector
+  runFreeVector = NoImpW runFreeVector
+
+instance Lang r => Lang (ImpW r) where
+  exfalso = NoImpW exfalso
   writer = NoImpW writer
   runWriter = NoImpW runWriter
   float2Double = NoImpW float2Double
   double2Float = NoImpW double2Float
   state = NoImpW state
   runState = NoImpW runState
-  putStrLn = NoImpW putStrLn
-
-instance DLang r => DLang (ImpW r) where
diff --git a/DDF/ImportMeta.hs b/DDF/ImportMeta.hs
--- a/DDF/ImportMeta.hs
+++ b/DDF/ImportMeta.hs
@@ -2,7 +2,7 @@
 
 module DDF.ImportMeta (module Prelude, module Data.Void, module Control.Monad.Writer, module Control.Monad.State, module Data.Constraint, module Data.Constraint.Forall, module Data.Proxy, module DDF.Util) where
 
-import Prelude (($), show, (+), (-), (*), (/), (.), (++), (>>=), IO, Int, (<=), (<), (==), compare, print, Either, Maybe, String)
+import Prelude (($), show, (+), (-), (*), (/), (.), (++), (>>=), (<=), (<), (==), compare, print, Maybe, String)
 import Data.Void (Void, absurd)
 import Control.Monad.Writer (Writer)
 import Control.Monad.State (State)
diff --git a/DDF/InfDiff.hs b/DDF/InfDiff.hs
deleted file mode 100644
--- a/DDF/InfDiff.hs
+++ /dev/null
@@ -1,86 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude, FlexibleContexts, UndecidableInstances #-}
-
-module DDF.InfDiff where
-
-import DDF.DLang
-import qualified DDF.Map as Map
-import DDF.Combine ()
-import DDF.Diff ()
-
-instance DBI r => DBI (InfDiff r v) where
-  z = InfDiff z
-  s (InfDiff x) = InfDiff $ s x
-  abs (InfDiff x) = InfDiff $ abs x
-  app (InfDiff f) (InfDiff x) = InfDiff $ app f x
-  liftEnv (InfDiff x) = InfDiff $ liftEnv x
-
-instance Dual r => Dual (InfDiff r v) where
-  dual = InfDiff dual
-  runDual = InfDiff runDual
-
-instance Bimap r => Bimap (InfDiff r v) where
-
-instance (Vector (InfDiff r v) v, Lang r) => Float (InfDiff r v) where
-  float = InfDiff . float
-  floatPlus = InfDiff floatPlus
-  floatMinus = InfDiff floatMinus
-  floatMult = InfDiff floatMult
-  floatDivide = InfDiff floatDivide
-  floatExp = InfDiff floatExp
-
-instance (Vector (InfDiff r v) v, Dual r, Double r) => Double (InfDiff r v) where
-  double = InfDiff . double
-  doublePlus = InfDiff doublePlus
-  doubleMinus = InfDiff doubleMinus
-  doubleMult = InfDiff doubleMult
-  doubleDivide = InfDiff doubleDivide
-  doubleExp = InfDiff doubleExp
-
-instance Char r => Char (InfDiff r v) where
-  char = InfDiff . char
-
-instance Bool r => Bool (InfDiff r v) where
-  bool = InfDiff . bool
-  ite = InfDiff ite
-
-instance Prod r => Prod (InfDiff r v) where
-  mkProd = InfDiff mkProd
-  zro = InfDiff zro
-  fst = InfDiff fst
-
-instance Option r => Option (InfDiff r v) where
-  nothing = InfDiff nothing
-  just = InfDiff just
-  optionMatch = InfDiff optionMatch
-
-instance Map.Map r => Map.Map (InfDiff r v) where
-  empty = InfDiff Map.empty
-  singleton = InfDiff Map.singleton
-  lookup = InfDiff Map.lookup
-  alter = InfDiff Map.alter
-  mapMap = InfDiff Map.mapMap
-
-instance Unit r => Unit (InfDiff r v) where
-  unit = InfDiff unit
-
-instance (Vector (InfDiff r v) v, Lang r) => Lang (InfDiff r v) where
-  fix = InfDiff fix
-  left = InfDiff left
-  right = InfDiff right
-  sumMatch = InfDiff sumMatch
-  exfalso = InfDiff exfalso
-  ioRet = InfDiff ioRet
-  ioBind = InfDiff ioBind
-  ioMap = InfDiff ioMap
-  writer = InfDiff writer
-  runWriter = InfDiff runWriter
-  nil = InfDiff nil
-  cons = InfDiff cons
-  listMatch = InfDiff listMatch
-  float2Double = InfDiff float2Double
-  double2Float = InfDiff double2Float
-  state = InfDiff state
-  runState = InfDiff runState
-  putStrLn = InfDiff putStrLn
-
-instance (Vector (InfDiff r v) v, DLang r) => DLang (InfDiff r v) where
diff --git a/DDF/Int.hs b/DDF/Int.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Int.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE NoImplicitPrelude, NoMonomorphismRestriction #-}
+
+module DDF.Int (module DDF.Int, module DDF.Bool) where
+
+import DDF.Bool
+import qualified Prelude as M
+
+class Bool r => Int r where
+  int :: M.Int -> r h M.Int
+  pred :: r h (M.Int -> M.Int)
+  isZero :: r h (M.Int -> M.Bool)
+
+pred1 = app pred
+isZero1 = app isZero
diff --git a/DDF/Lang.hs b/DDF/Lang.hs
--- a/DDF/Lang.hs
+++ b/DDF/Lang.hs
@@ -2,7 +2,9 @@
   NoImplicitPrelude,
   NoMonomorphismRestriction,
   MultiParamTypeClasses,
-  FlexibleInstances
+  FlexibleInstances,
+  TypeFamilies,
+  ScopedTypeVariables
 #-}
 
 module DDF.Lang (
@@ -14,7 +16,13 @@
   module DDF.Bimap,
   module DDF.Dual,
   module DDF.Meta.Diff,
-  module DDF.Unit
+  module DDF.Unit,
+  module DDF.Sum,
+  module DDF.Int,
+  module DDF.IO,
+  module DDF.DiffWrapper,
+  module DDF.Fix,
+  module DDF.FreeVector
 ) where
 
 import DDF.Bool
@@ -26,37 +34,61 @@
 import DDF.Vector
 import DDF.Meta.Diff
 import DDF.Unit
+import DDF.Sum
+import DDF.Int
+import DDF.IO
+import DDF.DiffWrapper
+import DDF.Fix
+import DDF.FreeVector
 
+import qualified DDF.VectorTF as VTF
+import qualified DDF.Meta.VectorTF as M.VTF
 import qualified DDF.Meta.Dual as M
 import qualified Control.Monad.Writer as M (Writer)
 import qualified GHC.Float as M
 import qualified Prelude as M
 import qualified Data.Map as M
 import qualified DDF.Map as Map
+import qualified Data.Map as M.Map
+import qualified Data.Functor.Foldable as M
+import qualified Data.Bimap as M.Bimap
+import qualified DDF.Meta.FreeVector as M
 
-class (Bool r, Char r, Double r, Float r, Bimap r, Dual r, Unit r) => Lang r where
-  fix :: r h ((a -> a) -> a)
-  left :: r h (a -> M.Either a b)
-  right :: r h (b -> M.Either a b)
-  sumMatch :: r h ((a -> c) -> (b -> c) -> M.Either a b -> c)
+type FreeVectorBuilder b = M.Map.Map b M.Double
+type SVTFBuilder b = State (M.Bimap.Bimap (M.VTF.VectorTF b M.Int) M.Int) M.Int
+class (Bool r, Char r, Double r, Float r, Bimap r, Dual r, Unit r, Sum r, Int r, IO r, VTF.VectorTF r, DiffWrapper r, Fix r, FreeVector r) => Lang r where
   exfalso :: r h (Void -> a)
-  ioRet :: r h (a -> M.IO a)
-  ioBind :: r h (M.IO a -> (a -> M.IO b) -> M.IO b)
-  ioMap :: r h ((a -> b) -> M.IO a -> M.IO b)
-  nil :: r h [a]
-  cons :: r h (a -> [a] -> [a])
-  listMatch :: r h (b -> (a -> [a] -> b) -> [a] -> b)
-  listAppend :: r h ([a] -> [a] -> [a])
-  listAppend = lam2 $ \l r -> fix2 (lam $ \self -> listMatch2 r (lam2 $ \a as -> cons2 a (app self as))) l
   writer :: r h ((a, w) -> M.Writer w a)
   runWriter :: r h (M.Writer w a -> (a, w))
   float2Double :: r h (M.Float -> M.Double)
   double2Float :: r h (M.Double -> M.Float)
-  undefined :: r h a
-  undefined = fix1 id
   state :: r h ((x -> (y, x)) -> State x y)
   runState :: r h (State x y -> (x -> (y, x)))
-  putStrLn :: r h (String -> IO ())
+  iterate :: r h ((x -> x) -> x -> [x])
+  iterate = lam $ \f -> y1 $ lam2 $ \fi x -> cons2 x (app fi (app f x))
+  buildFreeVector :: Map.Ord b => r h (FreeVectorBuilder b -> M.FreeVector b M.Double)
+  buildFreeVector = lam $ \fb -> freeVector1 $ lam $ \b -> optionMatch3 (double 0) id (Map.lookup2 fb b)
+  toSVTFBuilder :: Map.Ord b => r h (M.VTF.VectorTF b M.Int -> SVTFBuilder b)
+  toSVTFBuilder = lam $ \x -> state1 $ lam $ \m ->
+    optionMatch3
+      (let_2 (size1 m) (lam $ \si -> mkProd2 si (insert2 (mkProd2 x si) m)))
+      (lam $ \xid -> mkProd2 xid m)
+      (lookupL2 m x)
+  get :: r h (Maybe a -> a)
+  get = optionMatch2 undefined id
+  getVar :: r h (State x x)
+  getVar = state1 (dup1 mkProd)
+  update :: r h ((x -> x) -> State x ())
+  update = lam $ \f -> state1 $ lam $ \x -> mkProd2 unit (app f x)
+  updateWengert :: r h (M.Int -> M.Double -> M.Map.Map M.Int M.Double -> M.Map M.Int M.Double)
+  updateWengert = lam2 $ \i d -> Map.alter2 (optionMatch2 (just1 d) (just `com2` (plus1 d))) i
+  vtfCata :: r h ((M.VTF.VectorTF a b -> b) -> M.Fix (M.VTF.VectorTF a) -> b)
+  vtfCata = lam $ \f -> y1 $ lam $ \fx ->
+    VTF.vtfMatch4
+      (app f VTF.zero)
+      (f `com2` VTF.basis)
+      (lam2 $ \l r -> app f (VTF.plus2 (app fx l) (app fx r)))
+      (lam2 $ \d v -> app f (VTF.mult2 d (app fx v))) `com2` runFix
 
 class Reify r x where
   reify :: x -> r h x
@@ -85,6 +117,8 @@
   minus = const1 $ const1 unit
 
 instance Lang r => Vector r () where
+  type Basis () = Void
+  toFreeVector = const1 $ freeVector1 exfalso
   mult = const1 $ const1 unit
   divide = const1 $ const1 unit
 
@@ -96,9 +130,14 @@
   minus = floatMinus
 
 instance Lang r => Vector r M.Float where
+  type Basis M.Float = ()
+  toFreeVector = freeVector `com2` const `com2` float2Double
   mult = com2 floatMult double2Float
   divide = com2 (flip2 com double2Float) floatDivide
 
+instance Lang r => Functor r (M.VTF.VectorTF b) where
+  map = lam $ \f -> VTF.vtfMatch4 VTF.zero VTF.basis (lam2 $ \l r -> app f l `VTF.plus2` app f r) (lam2 $ \d x -> d `VTF.mult2` app f x)
+
 instance (Prod repr, Monoid repr l, Monoid repr r) => Monoid repr (l, r) where
   zero = mkProd2 zero zero
   plus = lam2 $ \l r -> mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))
@@ -106,7 +145,10 @@
 instance (Prod repr, Group repr l, Group repr r) => Group repr (l, r) where
   invert = bimap2 invert invert
 
-instance (Prod repr, Double repr, Vector repr l, Vector repr r) => Vector repr (l, r) where
+instance (Prod repr, Double repr, Sum repr, FreeVector repr, Vector repr l, Vector repr r) => Vector repr (l, r) where
+  type Basis (l, r) = M.Either (Basis l) (Basis r)
+  toFreeVector = lam $ \p -> let_2 (toFreeVector1 $ zro1 p) $ lam $ \lfv -> let_2 (toFreeVector1 $ fst1 p) $ lam $ \rfv ->
+    freeVector1 $ sumMatch2 (runFreeVector1 lfv) (runFreeVector1 rfv)
   mult = lam $ \x -> bimap2 (mult1 x) (mult1 x)
 
 instance (Double r, Monoid r v) => Monoid r (M.Double -> v) where
@@ -117,16 +159,18 @@
   invert = lam2 $ \l x -> app l (invert1 x)
 
 instance (Lang r, Vector r v) => Vector r (M.Double -> v) where
+  type Basis (M.Double -> v) = Basis v
+  toFreeVector = lam $ \f -> toFreeVector1 $ app f (double 1)
   mult = lam3 $ \l r x -> app r (mult2 l x)
 
 instance Lang r => Monoid r [a] where
   zero = nil
   plus = listAppend
 
-instance Lang r => Functor r [] where
-  map = lam $ \f -> fix1 $ lam $ \self -> listMatch2 nil (lam2 $ \x xs -> cons2 (app f x) $ app self xs)
+instance {-# INCOHERENT #-} Lang r => Functor r [] where
+  map = lam $ \f -> y1 $ lam $ \self -> listMatch2 nil (lam2 $ \x xs -> cons2 (app f x) $ app self xs)
 
-instance Lang r => BiFunctor r Either where
+instance Lang r => BiFunctor r M.Either where
   bimap = lam2 $ \l r -> sumMatch2 (com2 left l) (com2 right r)
 
 instance Prod r => BiFunctor r (,) where
@@ -158,16 +202,6 @@
 instance Lang r => Monad r (State l) where
   join = lam $ \x -> state1 $ lam $ \st -> let_2 (runState2 x st) (uncurry1 runState)
 
-instance Lang r => Functor r M.IO where
-  map = ioMap
-
-instance Lang r => Applicative r M.IO where
-  pure = ioRet
-  ap = lam2 $ \f x -> ioBind2 f (flip2 ioMap x)
-
-instance Lang r => Monad r M.IO where
-  bind = ioBind
-
 instance Lang r => Functor r M.Maybe where
   map = lam $ \func -> optionMatch2 nothing (com2 just func)
 
@@ -178,20 +212,103 @@
 instance Lang r => Monad r M.Maybe where
   bind = lam2 $ \x func -> optionMatch3 nothing func x
 
-cons2 = app2 cons
-listMatch2 = app2 listMatch
-fix1 = app fix
-fix2 = app2 fix
+instance Lang r => Monoid r (M.FreeVector b M.Double) where
+  zero = freeVector1 $ const1 (double 0)
+  plus = lam2 $ \l r -> freeVector1 $ lam $ \x -> runFreeVector2 l x `plus2` runFreeVector2 r x
+
+instance Lang r => Group r (M.FreeVector b M.Double) where
+  invert = lam $ \f -> freeVector1 $ lam $ \x -> invert1 (runFreeVector2 f x)
+  minus = lam2 $ \l r -> freeVector1 $ lam $ \x -> runFreeVector2 l x `minus2` runFreeVector2 r x
+
+instance Lang r => Vector r (M.FreeVector b M.Double) where
+  type Basis (M.FreeVector b M.Double) = b
+  toFreeVector = id
+  mult = lam2 $ \d l -> freeVector1 $ lam $ \x -> d `mult2` runFreeVector2 l x
+  divide = lam2 $ \l d -> freeVector1 $ lam $ \x -> runFreeVector2 l x `divide2` d
+
+instance (Map.Ord b, Lang r) => Monoid r (FreeVectorBuilder b) where
+  zero = Map.empty
+  plus = Map.unionWith1 plus
+
+instance (Map.Ord b, Lang r) => Group r (FreeVectorBuilder b) where
+  invert = Map.mapMap1 invert
+
+instance (Map.Ord b, Lang r) => Vector r (FreeVectorBuilder b) where
+  type Basis (FreeVectorBuilder b) = b
+  toFreeVector = buildFreeVector
+  mult = Map.mapMap `com2` mult
+  divide = lam2 $ \m d -> Map.mapMap2 (lam $ \x -> divide2 x d) m
+
+instance Lang r => Monoid r (M.Fix (M.VTF.VectorTF b)) where
+  zero = fix1 VTF.zero
+  plus = lam2 $ \l r -> fix1 $ l `VTF.plus2` r
+
+instance (Map.Ord b, Lang r) => Group r (M.Fix (M.VTF.VectorTF b)) where
+  invert = mult1 (double (-1))
+
+instance (Map.Ord b, Lang r) => Vector r (M.Fix (M.VTF.VectorTF b)) where
+  type Basis (M.Fix (M.VTF.VectorTF b)) = b
+  toFreeVector = buildFreeVector `com2` vtfCata1 (VTF.vtfMatch4 zero (flip2 Map.singleton (double 1)) plus mult)
+  mult = lam $ \d -> fix `com2` VTF.mult1 d
+
+instance (Map.Ord b, Lang r) => Monoid r (SVTFBuilder b) where
+  zero = toSVTFBuilder1 VTF.zero
+  plus = lam2 $ \l r -> l `bind2` (lam $ \lid -> r `bind2` (lam $ \rid -> toSVTFBuilder1 (VTF.plus2 lid rid)))
+
+instance (Map.Ord b, Lang r) => Group r (SVTFBuilder b) where
+  invert = mult1 (double (-1))
+
+instance (Map.Ord b, Lang r) => Vector r (SVTFBuilder b) where
+  type Basis (SVTFBuilder b) = b
+  toFreeVector =
+    buildFreeVector `com2` flip2 id Map.empty `com2`
+    (lam $ \x -> zro `com2` (runState1 $ y2 (lam2 $ \fx i ->
+      map2 (lam $ \m -> mkProd2 (get1 $ Map.lookup2 (fst1 x) i) (get1 $ Map.lookup2 m i)) getVar `bind2`
+      (lam $ \p -> VTF.vtfMatch5
+        (return1 zero)
+        (lam $ \b -> return1 (Map.singleton2 b (fst1 p)))
+        (lam2 $ \lid rid -> map2 (const1 zero) (update1 (updateWengert2 lid (fst1 p) `com2` updateWengert2 rid (fst1 p))))
+        (lam2 $ \d xid -> map2 (const1 zero) (update1 (let_2 (d `mult2` (fst1 p)) (updateWengert1 xid))))
+        (zro1 p) `bind2` (lam $ \fvb -> ite3 (return1 fvb) (map2 (plus1 fvb) $ app fx (pred1 i)) (isZero1 i)))) (zro1 x))
+    `com2` Map.insert2 (zro1 x) (double 0)) `com2` bimap2 id toMapR `com2` flip2 runState empty
+  mult = lam2 $ \d x -> x `bind2` (lam $ \xid -> toSVTFBuilder1 (VTF.mult2 d xid))
+
+type instance DiffType v (M.VTF.VectorTF t f) = M.VTF.VectorTF (DiffType v t) (DiffType v f)
+instance (Map.Ord b, Map.Ord f) => Map.Ord (M.VTF.VectorTF b f) where
+  diffOrd (_ :: Proxy (v, M.VTF.VectorTF b f)) = withDict (Map.diffOrd (Proxy :: Proxy (v, b))) $ withDict (Map.diffOrd (Proxy :: Proxy (v, f))) Dict
+
+type instance DiffType v M.Int = M.Int
+instance Map.Ord M.Int where
+  diffOrd _ = Dict
+
+instance Double r => Monoid r M.Double where
+  zero = doubleZero
+  plus = doublePlus
+
+instance Double r => Group r M.Double where
+  minus = doubleMinus
+
+instance Lang r => Vector r M.Double where
+  type Basis M.Double = ()
+  toFreeVector = freeVector `com2` const
+  mult = doubleMult
+  divide = doubleDivide
+
 uncurry1 = app uncurry
 optionMatch2 = app2 optionMatch
 optionMatch3 = app3 optionMatch
 writer1 = app writer
 runWriter1 = app runWriter
-ioBind2 = app2 ioBind
 float2Double1 = app float2Double
-doubleExp1 = app doubleExp
 floatExp1 = app floatExp
-sumMatch2 = app2 sumMatch
 state1 = app state
 runState1 = app runState
 runState2 = app2 runState
+toSVTFBuilder1 = app toSVTFBuilder
+double2Float1 = app double2Float
+get1 = app get
+return1 = app return
+update1 = app update
+updateWengert1 = app updateWengert
+updateWengert2 = app2 updateWengert
+vtfCata1 = app vtfCata
diff --git a/DDF/List.hs b/DDF/List.hs
new file mode 100644
--- /dev/null
+++ b/DDF/List.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+module DDF.List (module DDF.List, module DDF.Y) where
+
+import DDF.Y
+
+class Y r => List r where
+  nil :: r h [a]
+  cons :: r h (a -> [a] -> [a])
+  listMatch :: r h (b -> (a -> [a] -> b) -> [a] -> b)
+  listAppend :: r h ([a] -> [a] -> [a])
+  listAppend = lam2 $ \l r -> y2 (lam $ \self -> listMatch2 r (lam2 $ \a as -> cons2 a (app self as))) l
+
+cons2 = app2 cons
+listMatch2 = app2 listMatch
diff --git a/DDF/Map.hs b/DDF/Map.hs
--- a/DDF/Map.hs
+++ b/DDF/Map.hs
@@ -2,7 +2,8 @@
   NoImplicitPrelude,
   ScopedTypeVariables,
   TypeApplications,
-  FlexibleInstances
+  FlexibleInstances,
+  NoMonomorphismRestriction
 #-}
 
 module DDF.Map (module DDF.Map, module DDF.Prod, module DDF.Option) where
@@ -12,35 +13,24 @@
 import qualified Data.Map as M
 import DDF.Option
 import DDF.Meta.Diff
-import qualified DDF.Meta.Dual as M
 
 class M.Ord x => Ord x where
   diffOrd :: Proxy (v, x) -> Dict (Ord (DiffType v x))
 
-instance Ord () where
-  diffOrd _ = Dict
-
-instance Ord a => Ord [a] where
-  diffOrd (_ :: Proxy (v, [a])) = withDict (diffOrd (Proxy :: Proxy (v, a))) Dict
-
-instance M.Eq l => M.Eq (M.Dual l r) where
-  M.Dual (l, _) == M.Dual (r, _) = l == r
-
-instance M.Ord l => M.Ord (M.Dual l r) where
-  M.Dual (l, _) `compare` M.Dual (r, _) = l `compare` r
-
-instance Ord l => Ord (M.Dual l r) where
-  diffOrd (_ :: Proxy (v, M.Dual l r)) = withDict (diffOrd (Proxy :: Proxy (v, l))) Dict
-
-instance Ord M.Double where
-  diffOrd _ = Dict
-
-instance Ord M.Float where
-  diffOrd _ = Dict
-
 class (Prod r, Option r) => Map r where
   empty :: r h (M.Map k a)
   singleton :: r h (k -> a -> M.Map k a)
-  lookup :: Ord k => r h (k -> M.Map k a -> Maybe a)
+  lookup :: Ord k => r h (M.Map k a -> k -> Maybe a)
   alter :: Ord k => r h ((Maybe a -> Maybe a) -> k -> M.Map k a -> M.Map k a)
   mapMap :: r h ((a -> b) -> M.Map k a -> M.Map k b)
+  unionWith :: Ord k => r h ((a -> a -> a) -> M.Map k a -> M.Map k a -> M.Map k a)
+  insert :: Ord k => r h (k -> a -> M.Map k a -> M.Map k a)
+  insert = lam2 $ \k a -> alter2 (const1 (just1 a)) k
+
+lookup2 = app2 lookup
+unionWith1 = app unionWith
+mapMap1 = app mapMap
+mapMap2 = app2 mapMap
+insert2 = app2 insert
+alter2 = app2 alter
+singleton2 = app2 singleton
diff --git a/DDF/Meta/Diff.hs b/DDF/Meta/Diff.hs
--- a/DDF/Meta/Diff.hs
+++ b/DDF/Meta/Diff.hs
@@ -1,4 +1,3 @@
-
 {-# LANGUAGE
   RankNTypes,
   ScopedTypeVariables,
@@ -17,33 +16,9 @@
 
 import DDF.Vector
 import DDF.Meta.Interpreter
-import DDF.Meta.Dual
-import Data.Map
 
 type family DiffType (v :: *) (x :: *)
-type instance DiffType v () = ()
-type instance DiffType v (l, r) = (DiffType v l, DiffType v r)
-type instance DiffType v (l -> r) = DiffType v l -> DiffType v r
-type instance DiffType v Void = Void
-type instance DiffType v Double = Dual Double v
-type instance DiffType v Float = Dual Float v
-type instance DiffType v (Writer l r) = Writer (DiffType v l) (DiffType v r)
-type instance DiffType v (IO l) = IO (DiffType v l)
-type instance DiffType v (Maybe l) = Maybe (DiffType v l)
-type instance DiffType v [l] = [DiffType v l]
-type instance DiffType v (Either l r) = Either (DiffType v l) (DiffType v r)
-type instance DiffType v (State l r) = State (DiffType v l) (DiffType v r)
-type instance DiffType v Bool = Bool
-type instance DiffType v Char = Char
-type instance DiffType v (Map k val) = Map (DiffType v k) (DiffType v val)
-type instance DiffType v (Dual l r) = Dual (DiffType v l) (DiffType v r)
 
 newtype GDiff r h x = GDiff {runGDiff :: forall v. Vector r v => Proxy v -> Diff r v h x}
-
-newtype RTInfDiff r h x = RTInfDiff {runRTInfDiff :: Combine r (GDiff (RTInfDiff r)) h x}
-
-newtype InfDiff r v h x = InfDiff {runInfDiff :: Combine r (Diff (InfDiff r v) v) h x}
-
-newtype GInfDiff r h x = GInfDiff {runGInfDiff :: forall v. (Vector r v, Vector (InfDiff r v) v) => Proxy v -> InfDiff r v h x}
 
 newtype Diff r v h x = Diff {runDiff :: r (DiffType v h) (DiffType v x)}
diff --git a/DDF/Meta/DiffWrapper.hs b/DDF/Meta/DiffWrapper.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Meta/DiffWrapper.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE KindSignatures, DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}
+
+module DDF.Meta.DiffWrapper (module DDF.Meta.DiffWrapper, module DDF.Meta.Diff) where
+
+import DDF.Meta.Diff
+
+type family FDiffType (a :: [*]) x
+type instance FDiffType '[] x = x
+type instance FDiffType (a ': as) x = DiffType a (FDiffType as x)
+
+newtype DiffWrapper (a :: [*]) x = DiffWrapper {runDiffWrapper :: FDiffType a x}
diff --git a/DDF/Meta/Dual.hs b/DDF/Meta/Dual.hs
--- a/DDF/Meta/Dual.hs
+++ b/DDF/Meta/Dual.hs
@@ -2,6 +2,12 @@
 
 newtype Dual l r = Dual {runDual :: (l, r)}
 
+instance Eq l => Eq (Dual l r) where
+  (Dual (l, _)) == (Dual (r, _)) = l == r
+
+instance Ord l => Ord (Dual l r) where
+  (Dual (l, _)) `compare` (Dual (r, _)) = l `compare` r
+
 dualOrig (Dual (l, _)) = l
 
 dualDiff (Dual (_, r)) = r
diff --git a/DDF/Meta/FreeVector.hs b/DDF/Meta/FreeVector.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Meta/FreeVector.hs
@@ -0,0 +1,3 @@
+module DDF.Meta.FreeVector where
+
+newtype FreeVector b d = FreeVector {runFreeVector :: b -> d}
diff --git a/DDF/Meta/VectorTF.hs b/DDF/Meta/VectorTF.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Meta/VectorTF.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE DeriveFunctor #-}
+
+module DDF.Meta.VectorTF where
+
+-- | F algebra of a Term Vector Spaces
+data VectorTF t f = Zero | Basis t | Plus f f | Mult Double f deriving (Eq, Ord, Functor)
diff --git a/DDF/Option.hs b/DDF/Option.hs
--- a/DDF/Option.hs
+++ b/DDF/Option.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
 module DDF.Option (module DDF.Option, module DDF.DBI) where
 
 import DDF.DBI
@@ -6,3 +8,5 @@
   nothing :: r h (Maybe a)
   just :: r h (a -> Maybe a)
   optionMatch :: r h (b -> (a -> b) -> Maybe a -> b)
+
+just1 = app just
diff --git a/DDF/PE.hs b/DDF/PE.hs
new file mode 100644
--- /dev/null
+++ b/DDF/PE.hs
@@ -0,0 +1,136 @@
+{-# LANGUAGE
+  RankNTypes,
+  NoImplicitPrelude,
+  GADTs,
+  ExplicitForAll,
+  ScopedTypeVariables,
+  NoMonomorphismRestriction,
+  IncoherentInstances,
+  InstanceSigs,
+  LambdaCase,
+  FlexibleContexts
+#-}
+
+module DDF.PE where
+
+import DDF.DBI
+import DDF.Double
+import qualified Prelude as M
+
+data P repr h a where
+  Unk :: repr h a -> P repr h a
+  Static :: a -> (forall h'. repr h' a) -> P repr h a
+  StaFun :: (forall hout. EnvT repr (a, h) hout -> P repr hout b) -> P repr h (a -> b)
+  Open   :: (forall hout. EnvT repr h hout -> P repr hout a) -> P repr h a
+
+data EnvT repr hin hout where
+  Dyn  :: EnvT repr hin hin
+  Arg  :: P repr hout a -> EnvT repr (a, hout) hout
+  Weak :: EnvT repr h (a, h)
+  Next :: EnvT repr hin hout -> EnvT repr (a, hin) (a, hout)
+
+dynamic:: DBI repr => P repr h a -> repr h a
+dynamic (Unk x)      = x
+dynamic (Static _ x) = x
+dynamic (StaFun f)   = abs $ dynamic (f Dyn)
+dynamic (Open f)     = dynamic (f Dyn)
+
+app_open :: DBI repr => P repr hin r -> EnvT repr hin hout -> P repr hout r
+app_open e Dyn            = Unk (dynamic e)
+app_open (Static es ed) _ = Static es ed
+app_open (Open fs) h      = fs h
+app_open (StaFun fs) h    = abs (fs (Next h))
+app_open (Unk env) h      = Unk (app_unk env h) where
+  app_unk :: DBI repr => repr hin a -> EnvT repr hin hout -> repr hout a
+  app_unk e Dyn      = e
+  app_unk e (Arg p)  = app (abs e) (dynamic p)
+  app_unk e (Next h') = app (s (app_unk (abs e) h')) z
+  app_unk e Weak     = s e
+
+instance DBI r => DBI (P r) where
+  z = Open f where
+    f :: EnvT r (a,h) hout -> P r hout a
+    f Dyn       = Unk z
+    f (Arg x)   = x
+    f (Next _)  = z
+    f Weak      = s z
+
+  s :: forall h a any. P r h a -> P r (any, h) a
+  s (Unk x) = Unk (s x)
+  s (Static a ar) = Static a ar
+  s (StaFun fs) = abs (fs (Next Weak))
+  s p = Open f where
+    f :: EnvT r (any, h) hout -> P r hout a
+    f Dyn              = Unk (s (dynamic p))
+    f (Arg _)          = p
+    f (Next h)         = s (app_open p h)
+    f Weak             = s (s p)
+
+  abs (Unk f) = Unk (abs f)
+  abs (Static k ks) = StaFun $ \_ -> Static k ks
+  abs body = StaFun (app_open body)
+  
+  app (Unk f) (Unk x) = Unk (app f x)
+  app (StaFun fs) p   = fs (Arg p)
+  app (Static _ fs) p = Unk (app fs (dynamic p))
+  app e1 e2           = Open (\h -> app (app_open e1 h) (app_open e2 h))
+
+instance Bool r => Bool (P r) where
+  bool x = Static x (bool x)
+  ite = lam3 (\l r b -> app2 (f b) l r)
+    where
+      f :: P r h M.Bool -> P r h (a -> a -> a)
+      f (Static M.True _) = const
+      f (Static M.False _) = const1 id
+      f (Unk x) = Unk (lam2 (\l r -> ite3 l r (s (s x))))
+      f x = Open (\h -> f (app_open x h))
+
+instance Double r => Double (P r) where
+  double x = Static x (double x)
+  doublePlus = abs (abs (f (s z) z))
+    where
+      f :: P r h M.Double -> P r h M.Double -> P r h M.Double
+      f (Static l _) (Static r _) = double (l + r)
+      f (Static 0 _) r = r
+      f l (Static 0 _) = l
+      f (Unk l) (Unk r) = Unk (doublePlus2 l r)
+      f l r = Open (\h -> f (app_open l h) (app_open r h))
+  doubleMult = abs (abs (f (s z) z))
+    where
+      f :: P r h M.Double -> P r h M.Double -> P r h M.Double
+      f (Static l _) (Static r _) = double (l * r)
+      f (Static 0 _) _ = double 0
+      f _ (Static 0 _) = double 0
+      f l (Static 1 _) = l
+      f (Static 1 _) r = r
+      f (Unk l) (Unk r) = Unk (doubleMult2 l r)
+      f l r = Open (\h -> f (app_open l h) (app_open r h))
+  doubleMinus = abs (abs (f (s z) z))
+    where
+      f :: P r h M.Double -> P r h M.Double -> P r h M.Double
+      f (Static l _) (Static r _) = double (l - r)
+      f l (Static 0 _) = l
+      f (Unk l) (Unk r) = Unk (doubleMinus2 l r)
+      f l r = Open (\h -> f (app_open l h) (app_open r h))
+  doubleDivide = abs (abs (f (s z) z))
+    where
+      f :: P r h M.Double -> P r h M.Double -> P r h M.Double
+      f (Static l _) (Static r _) = double (l / r)
+      f (Static 0 _) _ = double 0
+      f l (Static 1 _) = l
+      f (Unk l) (Unk r) = Unk (doubleDivide2 l r)
+      f l r = Open (\h -> f (app_open l h) (app_open r h))
+  doubleExp = abs (f z)
+    where
+      f :: P r h M.Double -> P r h M.Double
+      f (Static l _) = double (M.exp l) 
+      f (Unk l) = Unk (doubleExp1 l)
+      f l = Open (\h -> f (app_open l h))
+  doubleEq = abs (abs (f (s z) z)) where
+    f :: P r h M.Double -> P r h M.Double -> P r h M.Bool
+    f (Static l _) (Static r _) = bool (l == r)
+    f (Unk l) (Unk r) = Unk (doubleEq2 l r)
+    f l r = Open (\h -> f (app_open l h) (app_open r h))    
+
+pe :: Double repr => P repr () a -> repr () a
+pe = dynamic
diff --git a/DDF/Poly.lhs b/DDF/Poly.lhs
--- a/DDF/Poly.lhs
+++ b/DDF/Poly.lhs
@@ -102,7 +102,7 @@
 
 Now the main function:
 
-> main :: IO ()
+> main :: M.IO ()
 > main = do
 >   d <- solve print printSquare
 >   M.putStrLn $ "x is: " ++ (show d)
diff --git a/DDF/RTInfDiff.hs b/DDF/RTInfDiff.hs
deleted file mode 100644
--- a/DDF/RTInfDiff.hs
+++ /dev/null
@@ -1,90 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude, FlexibleContexts, ScopedTypeVariables, TypeApplications, TypeFamilies #-}
-
-module DDF.RTInfDiff where
-
-import DDF.Meta.Diff
-import DDF.DLang
-import DDF.Combine ()
-import DDF.GDiff ()
-import qualified DDF.Map as Map
-
-instance DBI r => DBI (RTInfDiff r) where
-  z = RTInfDiff z
-  s (RTInfDiff x) = RTInfDiff (s x)
-  abs (RTInfDiff x) = RTInfDiff (abs x)
-  app (RTInfDiff f) (RTInfDiff x) = RTInfDiff (app f x)
-  liftEnv (RTInfDiff x) = RTInfDiff (liftEnv x)
-
-instance Prod r => Prod (RTInfDiff r) where
-  zro = RTInfDiff zro
-  fst = RTInfDiff fst
-  mkProd = RTInfDiff mkProd
-
-instance Dual r => Dual (RTInfDiff r) where
-  dual = RTInfDiff dual
-  runDual = RTInfDiff runDual
-
-instance Option r => Option (RTInfDiff r) where
-  nothing = RTInfDiff nothing
-  just = RTInfDiff just
-  optionMatch = RTInfDiff optionMatch
-
-instance Bool r => Bool (RTInfDiff r) where
-  bool x = RTInfDiff (bool x)
-  ite = RTInfDiff ite
-
-instance Char r => Char (RTInfDiff r) where
-  char x = RTInfDiff (char x)
-
-instance (Dual r, Double r) => Double (RTInfDiff r) where
-  double x = RTInfDiff (double x)
-  doublePlus = RTInfDiff doublePlus
-  doubleMinus = RTInfDiff doubleMinus
-  doubleMult = RTInfDiff doubleMult
-  doubleDivide = RTInfDiff doubleDivide
-  doubleExp = RTInfDiff doubleExp
-
-instance Lang r => Float (RTInfDiff r) where
-  float x = RTInfDiff (float x)
-  floatPlus = RTInfDiff floatPlus
-  floatMinus = RTInfDiff floatMinus
-  floatMult = RTInfDiff floatMult
-  floatDivide = RTInfDiff floatDivide
-  floatExp = RTInfDiff floatExp
-
-instance Map.Map r => Map.Map (RTInfDiff r) where
-  empty = RTInfDiff Map.empty
-  singleton = RTInfDiff Map.singleton
-  alter = RTInfDiff Map.alter
-  mapMap = RTInfDiff Map.mapMap
-  lookup = RTInfDiff Map.lookup
-
-instance Bimap r => Bimap (RTInfDiff r) where
-
-instance Unit r => Unit (RTInfDiff r) where
-  unit = RTInfDiff unit
-
-instance Lang r => Lang (RTInfDiff r) where
-  fix = RTInfDiff fix
-  float2Double = RTInfDiff float2Double
-  double2Float = RTInfDiff double2Float
-  left = RTInfDiff left
-  right = RTInfDiff right
-  sumMatch = RTInfDiff sumMatch
-  exfalso = RTInfDiff exfalso
-  ioBind = RTInfDiff ioBind
-  ioMap = RTInfDiff ioMap
-  ioRet = RTInfDiff ioRet
-  nil = RTInfDiff nil
-  cons = RTInfDiff cons
-  listMatch = RTInfDiff listMatch
-  writer = RTInfDiff writer
-  runWriter = RTInfDiff runWriter
-  state = RTInfDiff state
-  runState = RTInfDiff runState
-  putStrLn = RTInfDiff putStrLn
-
-instance DLang r => DLang (RTInfDiff r) where
-
-diffInf :: (Vector (RTInfDiff r) v, DBI r) => Proxy v -> RTInfDiff r () x -> RTInfDiff r h (DiffType v x)
-diffInf p (RTInfDiff (Combine _ (GDiff f))) = liftEnv $ runDiff $ f p
diff --git a/DDF/Show.hs b/DDF/Show.hs
--- a/DDF/Show.hs
+++ b/DDF/Show.hs
@@ -1,10 +1,11 @@
-{-# LANGUAGE NoImplicitPrelude, TypeFamilies #-}
+{-# LANGUAGE NoImplicitPrelude, TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}
 
-module DDF.Show (module DDF.Show) where
+module DDF.Show where
 
-import DDF.DLang
+import DDF.Lang
 import qualified Prelude as M
 import qualified DDF.Map as Map
+import qualified DDF.VectorTF as VTF
 
 data AST = Leaf M.String | App M.String AST [AST] | Lam M.String [M.String] AST
 
@@ -30,7 +31,6 @@
   app (Show f) (Show x) = Show $ \va h -> appAST (f va h) (x va h)
   hoas f = Show $ \(v:va) h ->
     lamAST v (runShow (f $ Show $ M.const $ M.const $ Leaf v) va (h + 1))
-  liftEnv (Show x) = Show x
 
 instance Bool Show where
   bool = name . show
@@ -51,6 +51,7 @@
   doubleMult = name "mult"
   doubleDivide = name "divide"
   doubleExp = name "exp"
+  doubleEq = name "eq"
 
 instance Float Show where
   float = name . show
@@ -66,13 +67,24 @@
   optionMatch = name "optionMatch"
 
 instance Map.Map Show where
-  empty = name "empty"
-  singleton = name "singleton"
-  lookup = name "lookup"
-  alter = name "alter"
-  mapMap = name "mapMap"
+  empty = name "Map.empty"
+  singleton = name "Map.singleton"
+  lookup = name "Map.lookup"
+  alter = name "Map.alter"
+  mapMap = name "Map.mapMap"
+  unionWith = name "Map.unionWith"
 
 instance Bimap Show where
+  size = name "size"
+  lookupL = name "lookupL"
+  lookupR = name "lookupR"
+  toMapL = name "toMapL"
+  toMapR = name "toMapR"
+  updateL = name "updateL"
+  updateR = name "updateR"
+  empty = name "empty"
+  singleton = name "singleton"
+  insert = name "insert"
 
 instance Dual Show where
   dual = name "dual"
@@ -81,24 +93,62 @@
 instance Unit Show where
   unit = name "unit"
 
-instance Lang Show where
-  fix = name "fix"
+instance Sum Show where
   left = name "left"
   right = name "right"
   sumMatch = name "sumMatch"
-  exfalso = name "exfalso"
-  ioRet = name "ioRet"
-  ioBind = name "ioBind"
+
+instance Int Show where
+  int = name . show
+  pred = name "pred"
+  isZero = name "isZero"
+
+instance List Show where
   nil = name "nil"
   cons = name "cons"
   listMatch = name "listMatch"
-  ioMap = name "ioMap"
+
+instance Y Show where
+  y = name "Y"
+
+instance IO Show where
+  putStrLn = name "putStrLn"
+
+instance Functor Show x where
+  map = name "map"
+
+instance Applicative Show x where
+  pure = name "pure"
+  ap = name "ap"
+
+instance Monad Show x where
+  join = name "join"
+  bind = name "bind"
+
+instance VTF.VectorTF Show where
+  zero = name "VTF.zero"
+  basis = name "VTF.basis"
+  plus = name "VTF.plus"
+  mult = name "VTF.mult"
+  vtfMatch = name "VTF.vtfMatch"
+
+instance DiffWrapper Show where
+  diffWrapper = name "diffWrapper"
+  runDiffWrapper = name "runDiffWrapper"
+
+instance Fix Show where
+  fix = name "fix"
+  runFix = name "runFix"
+
+instance FreeVector Show where
+  freeVector = name "freeVector"
+  runFreeVector = name "runFreeVector"
+
+instance Lang Show where
+  exfalso = name "exfalso"
   writer = name "writer"
   runWriter = name "runWriter"
   float2Double = name "float2Double"
   double2Float = name "double2Float"
   state = name "state"
   runState = name "runState"
-  putStrLn = name "putStrLn"
-
-instance DLang Show where
diff --git a/DDF/Size.hs b/DDF/Size.hs
--- a/DDF/Size.hs
+++ b/DDF/Size.hs
@@ -1,20 +1,21 @@
-{-# LANGUAGE NoImplicitPrelude, TypeFamilies #-}
+{-# LANGUAGE NoImplicitPrelude, TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}
 
 module DDF.Size where
 
-import DDF.DLang
+import DDF.Lang
+import qualified Prelude as M
 import qualified DDF.Map as Map
+import qualified DDF.VectorTF as VTF
 
-newtype Size h x = Size {runSize :: Int}
+newtype Size h x = Size {runSize :: M.Int}
 
 one = Size 1
 
 instance DBI Size where
   z = one
-  s (Size x) = (Size x)
+  s (Size x) = Size x
   app (Size l) (Size r) = Size (l + r)
-  abs (Size l) = Size (1 + l)
-  liftEnv (Size l) = Size l
+  abs (Size x) = Size x
 
 instance Bool Size where
   bool _ = one
@@ -35,6 +36,7 @@
   doubleMult = one
   doubleDivide = one
   doubleExp = one
+  doubleEq = one
 
 instance Float Size where
   float _ = one
@@ -50,6 +52,7 @@
   empty = one
   singleton = one
   lookup = one
+  unionWith = one
 
 instance Prod Size where
   mkProd = one
@@ -61,28 +64,76 @@
   runDual = one
 
 instance Bimap Size where
+  updateL = one
+  updateR = one
+  singleton = one
+  empty = one
+  insert = one
+  lookupL = one
+  lookupR = one
+  size = one
+  toMapL = one
+  toMapR = one
 
 instance Unit Size where
   unit = one
 
-instance Lang Size where
-  fix = one
+instance Sum Size where
   left = one
   right = one
   sumMatch = one
-  exfalso = one
-  ioRet = one
-  ioBind = one
-  ioMap = one
+
+instance Int Size where
+  int _ = one
+  pred = one
+  isZero = one
+
+instance IO Size where
+  putStrLn = one
+
+instance Y Size where
+  y = one
+
+instance List Size where
   nil = one
   cons = one
   listMatch = one
+
+instance Functor Size x where
+  map = one
+
+instance Applicative Size x where
+  pure = one
+  ap = one
+
+instance Monad Size x where
+  bind = one
+  join = one
+
+instance VTF.VectorTF Size where
+  zero = one
+  basis = one
+  plus = one
+  mult = one
+  vtfMatch = one
+
+instance DiffWrapper Size where
+  diffWrapper = one
+  runDiffWrapper = one
+
+instance Fix Size where
+  fix = one
+  runFix = one
+
+instance FreeVector Size where
+  freeVector = one
+  runFreeVector = one
+
+instance Lang Size where
+  exfalso = one
   writer = one
   runWriter = one
   float2Double = one
   double2Float = one
   state = one
   runState = one
-  putStrLn = one
-
-instance DLang Size where
diff --git a/DDF/Sum.hs b/DDF/Sum.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Sum.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+module DDF.Sum (module DDF.Sum, module DDF.DBI) where
+
+import DDF.DBI
+
+class DBI r => Sum r where
+  left :: r h (a -> Either a b)
+  right :: r h (b -> Either a b)
+  sumMatch :: r h ((a -> c) -> (b -> c) -> Either a b -> c)
+
+sumMatch2 = app2 sumMatch
+left1 = app left
+right1 = app right
diff --git a/DDF/UInt.hs b/DDF/UInt.hs
--- a/DDF/UInt.hs
+++ b/DDF/UInt.hs
@@ -1,9 +1,10 @@
-{-# LANGUAGE NoImplicitPrelude, TypeFamilies #-}
+{-# LANGUAGE NoImplicitPrelude, TypeFamilies, MultiParamTypeClasses, PartialTypeSignatures, FlexibleInstances #-}
 
 module DDF.UInt where
 
-import DDF.DLang
+import DDF.Lang
 import qualified DDF.Map as Map
+import qualified DDF.VectorTF as VTF
 
 data UInt h x = UInt
 
@@ -12,7 +13,6 @@
   s _ = UInt
   abs _ = UInt
   app _ _ = UInt
-  liftEnv _ = UInt
 
 instance Bool UInt where
   bool _ = UInt
@@ -28,6 +28,7 @@
   doubleMult = UInt
   doubleDivide = UInt
   doubleExp = UInt
+  doubleEq = UInt
 
 instance Float UInt where
   float _ = UInt
@@ -38,6 +39,16 @@
   floatExp = UInt
 
 instance Bimap UInt where
+  size = UInt
+  empty = UInt
+  singleton = UInt
+  lookupL = UInt
+  lookupR = UInt
+  toMapL = UInt
+  toMapR = UInt
+  insert = UInt
+  updateL = UInt
+  updateR = UInt
 
 instance Dual UInt where
   dual = UInt
@@ -49,6 +60,7 @@
   lookup = UInt
   alter = UInt
   mapMap = UInt
+  unionWith = UInt
 
 instance Prod UInt where
   mkProd = UInt
@@ -63,24 +75,62 @@
 instance Unit UInt where
   unit = UInt
 
-instance Lang UInt where
-  fix = UInt
+instance Sum UInt where
   left = UInt
   right = UInt
   sumMatch = UInt
-  exfalso = UInt
-  ioRet = UInt
-  ioBind = UInt
-  ioMap = UInt
+
+instance Int UInt where
+  int _ = UInt
+  pred = UInt
+  isZero = UInt
+
+instance Y UInt where
+  y = UInt
+
+instance Functor UInt x where
+  map = UInt
+
+instance Applicative UInt x where
+  ap = UInt
+  pure = UInt
+
+instance Monad UInt x where
+  join = UInt
+  bind = UInt
+
+instance IO UInt where
+  putStrLn = UInt
+
+instance List UInt where
   nil = UInt
   cons = UInt
   listMatch = UInt
+
+instance VTF.VectorTF UInt where
+  zero = UInt
+  basis = UInt
+  plus = UInt
+  mult = UInt
+  vtfMatch = UInt
+
+instance DiffWrapper UInt where
+  diffWrapper = UInt
+  runDiffWrapper = UInt
+
+instance Fix UInt where
+  fix = UInt
+  runFix = UInt
+
+instance FreeVector UInt where
+  freeVector = UInt
+  runFreeVector = UInt
+
+instance Lang UInt where
+  exfalso = UInt
   runWriter = UInt
   writer = UInt
   double2Float = UInt
   float2Double = UInt
   state = UInt
   runState = UInt
-  putStrLn = UInt
-
-instance DLang UInt where
diff --git a/DDF/UnHOAS.hs b/DDF/UnHOAS.hs
--- a/DDF/UnHOAS.hs
+++ b/DDF/UnHOAS.hs
@@ -1,16 +1,23 @@
-{-# LANGUAGE NoImplicitPrelude, TypeFamilies, TypeApplications, ScopedTypeVariables #-}
+{-# LANGUAGE
+  NoImplicitPrelude,
+  TypeFamilies,
+  TypeApplications,
+  ScopedTypeVariables,
+  FlexibleInstances,
+  MultiParamTypeClasses
+#-}
 
 module DDF.UnHOAS where
 
-import DDF.DLang
+import DDF.Lang
 import qualified DDF.Map as Map
+import qualified DDF.VectorTF as VTF
 
 instance DBI repr => DBI (UnHOAS repr) where
   z = UnHOAS z
   s (UnHOAS x) = UnHOAS $ s x
   abs (UnHOAS x) = UnHOAS $ abs x
   app (UnHOAS f) (UnHOAS x) = UnHOAS $ app f x
-  liftEnv (UnHOAS x) = UnHOAS $ liftEnv x
 
 instance Bool r => Bool (UnHOAS r) where
   bool = UnHOAS . bool
@@ -31,6 +38,7 @@
   doubleMult = UnHOAS doubleMult
   doubleDivide = UnHOAS doubleDivide
   doubleExp = UnHOAS doubleExp
+  doubleEq = UnHOAS doubleEq
 
 instance Float r => Float (UnHOAS r) where
   float = UnHOAS . float
@@ -51,8 +59,19 @@
   alter = UnHOAS Map.alter
   lookup = UnHOAS Map.lookup
   mapMap = UnHOAS Map.mapMap
+  unionWith = UnHOAS Map.unionWith
 
 instance Bimap r => Bimap (UnHOAS r) where
+  size = UnHOAS size
+  insert = UnHOAS insert
+  lookupL = UnHOAS lookupL
+  toMapL = UnHOAS toMapL
+  lookupR = UnHOAS lookupR
+  toMapR = UnHOAS toMapR
+  empty = UnHOAS empty
+  singleton = UnHOAS singleton
+  updateL = UnHOAS updateL
+  updateR = UnHOAS updateR
 
 instance Dual r => Dual (UnHOAS r) where
   dual = UnHOAS dual
@@ -61,24 +80,62 @@
 instance Unit r => Unit (UnHOAS r) where
   unit = UnHOAS unit
 
-instance Lang r => Lang (UnHOAS r) where
-  float2Double = UnHOAS float2Double
-  fix = UnHOAS fix
+instance Sum r => Sum (UnHOAS r) where
   left = UnHOAS left
   right = UnHOAS right
   sumMatch = UnHOAS sumMatch
-  exfalso = UnHOAS exfalso
-  ioRet = UnHOAS ioRet
-  ioBind = UnHOAS ioBind
+
+instance Int r => Int (UnHOAS r) where
+  int = UnHOAS . int
+  pred = UnHOAS pred
+  isZero = UnHOAS isZero
+
+instance Y r => Y (UnHOAS r) where
+  y = UnHOAS y
+
+instance Functor r x => Functor (UnHOAS r) x where
+  map = UnHOAS map
+
+instance Applicative r x => Applicative (UnHOAS r) x where
+  pure = UnHOAS pure
+  ap = UnHOAS ap
+
+instance Monad r x => Monad (UnHOAS r) x where
+  join = UnHOAS join
+  bind = UnHOAS bind
+
+instance IO r => IO (UnHOAS r) where
+  putStrLn = UnHOAS putStrLn
+
+instance List r => List (UnHOAS r) where
   nil = UnHOAS nil
   cons = UnHOAS cons
   listMatch = UnHOAS listMatch
-  ioMap = UnHOAS ioMap
+
+instance VTF.VectorTF r => VTF.VectorTF (UnHOAS r) where
+  zero = UnHOAS VTF.zero
+  basis = UnHOAS VTF.basis
+  plus = UnHOAS VTF.plus
+  mult = UnHOAS VTF.mult
+  vtfMatch = UnHOAS VTF.vtfMatch
+
+instance DiffWrapper r => DiffWrapper (UnHOAS r) where
+  diffWrapper = UnHOAS diffWrapper
+  runDiffWrapper = UnHOAS runDiffWrapper
+
+instance Fix r => Fix (UnHOAS r) where
+  fix = UnHOAS fix
+  runFix = UnHOAS runFix
+
+instance FreeVector r => FreeVector (UnHOAS r) where
+  freeVector = UnHOAS freeVector
+  runFreeVector = UnHOAS runFreeVector
+
+instance Lang r => Lang (UnHOAS r) where
+  float2Double = UnHOAS float2Double
+  exfalso = UnHOAS exfalso
   writer = UnHOAS writer
   runWriter = UnHOAS runWriter
   double2Float = UnHOAS double2Float
   state = UnHOAS state
   runState = UnHOAS runState
-  putStrLn = UnHOAS putStrLn
-
-instance DLang r => DLang (UnHOAS r) where
diff --git a/DDF/UnLiftEnv.hs b/DDF/UnLiftEnv.hs
--- a/DDF/UnLiftEnv.hs
+++ b/DDF/UnLiftEnv.hs
@@ -1,27 +1,31 @@
-
-{-# LANGUAGE NoImplicitPrelude, NoMonomorphismRestriction #-}
+{-# LANGUAGE
+  NoImplicitPrelude,
+  NoMonomorphismRestriction,
+  FlexibleInstances,
+  MultiParamTypeClasses
+#-}
 
 module DDF.UnLiftEnv where
 
-import DDF.DLang
+import DDF.Lang
 import qualified DDF.Map as Map
+import qualified DDF.VectorTF as VTF
 
 newtype UnLiftEnv r h x = UnLiftEnv {runUnLiftEnv :: r () (h -> x)}
 
 unLiftEnv = UnLiftEnv . const1
 
-instance (Prod r, Unit r) => DBI (UnLiftEnv r) where
+instance Prod r => DBI (UnLiftEnv r) where
   z = UnLiftEnv zro
   s (UnLiftEnv x) = UnLiftEnv $ x `com2` fst
   abs (UnLiftEnv x) = UnLiftEnv $ curry1 $ x `com2` swap
   app (UnLiftEnv f) (UnLiftEnv x) = UnLiftEnv $ scomb2 f x
-  liftEnv (UnLiftEnv x) = UnLiftEnv $ x `com2` (const1 unit)
 
-instance (Dual r, Unit r) => Dual (UnLiftEnv r) where
+instance Dual r => Dual (UnLiftEnv r) where
   dual = unLiftEnv dual
   runDual = unLiftEnv runDual
 
-instance (Prod r, Unit r, Float r) => Float (UnLiftEnv r) where
+instance (Prod r, Float r) => Float (UnLiftEnv r) where
   float = unLiftEnv . float
   floatPlus = unLiftEnv floatPlus
   floatMinus = unLiftEnv floatMinus
@@ -29,22 +33,23 @@
   floatDivide = unLiftEnv floatDivide
   floatExp = unLiftEnv floatExp
 
-instance (Prod r, Unit r, Double r) => Double (UnLiftEnv r) where
+instance (Prod r, Double r) => Double (UnLiftEnv r) where
   double = unLiftEnv . double
   doublePlus = unLiftEnv doublePlus
   doubleMinus = unLiftEnv doubleMinus
   doubleMult = unLiftEnv doubleMult
   doubleDivide = unLiftEnv doubleDivide
   doubleExp = unLiftEnv doubleExp
+  doubleEq = unLiftEnv doubleEq
 
-instance (Prod r, Unit r, Char r) => Char (UnLiftEnv r) where
+instance (Prod r, Char r) => Char (UnLiftEnv r) where
   char = unLiftEnv . char
 
-instance (Prod r, Unit r, Bool r) => Bool (UnLiftEnv r) where
+instance (Prod r, Bool r) => Bool (UnLiftEnv r) where
   bool = unLiftEnv . bool
   ite = unLiftEnv ite
 
-instance (Prod r, Unit r) => Prod (UnLiftEnv r) where
+instance Prod r => Prod (UnLiftEnv r) where
   mkProd = unLiftEnv mkProd
   zro = unLiftEnv zro
   fst = unLiftEnv fst
@@ -52,38 +57,87 @@
 instance (Prod r, Unit r) => Unit (UnLiftEnv r) where
   unit = unLiftEnv unit
 
-instance (Prod r, Unit r, Option r) => Option (UnLiftEnv r) where
+instance (Prod r, Option r) => Option (UnLiftEnv r) where
   nothing = unLiftEnv nothing
   just = unLiftEnv just
   optionMatch = unLiftEnv optionMatch
 
-instance (Unit r, Map.Map r) => Map.Map (UnLiftEnv r) where
+instance Map.Map r => Map.Map (UnLiftEnv r) where
   empty = unLiftEnv Map.empty
   singleton = unLiftEnv Map.singleton
   lookup = unLiftEnv Map.lookup
   alter = unLiftEnv Map.alter
   mapMap = unLiftEnv Map.mapMap
+  unionWith = unLiftEnv Map.unionWith
 
-instance (Unit r, Bimap r) => Bimap (UnLiftEnv r) where
+instance Bimap r => Bimap (UnLiftEnv r) where
+  size = unLiftEnv size
+  insert = unLiftEnv insert
+  lookupL = unLiftEnv lookupL
+  lookupR = unLiftEnv lookupR
+  empty = unLiftEnv empty
+  singleton = unLiftEnv singleton
+  toMapL = unLiftEnv toMapL
+  toMapR = unLiftEnv toMapR
+  updateL = unLiftEnv updateL
+  updateR = unLiftEnv updateR
 
-instance Lang r => Lang (UnLiftEnv r) where
-  fix = unLiftEnv fix
+instance (Prod r, Sum r) => Sum (UnLiftEnv r) where
   left = unLiftEnv left
   right = unLiftEnv right
   sumMatch = unLiftEnv sumMatch
-  exfalso = unLiftEnv exfalso
-  ioRet = unLiftEnv ioRet
-  ioBind = unLiftEnv ioBind
-  ioMap = unLiftEnv ioMap
+
+instance (Prod r, Int r) => Int (UnLiftEnv r) where
+  int = unLiftEnv . int
+  isZero = unLiftEnv isZero
+  pred = unLiftEnv pred
+
+instance (Prod r, Y r) => Y (UnLiftEnv r) where
+  y = unLiftEnv y
+
+instance (Prod r, IO r) => IO (UnLiftEnv r) where
+  putStrLn = unLiftEnv putStrLn
+
+instance (Unit r, Prod r, List r) => List (UnLiftEnv r) where
   nil = unLiftEnv nil
   cons = unLiftEnv cons
   listMatch = unLiftEnv listMatch
+
+instance (Prod r, Functor r m) => Functor (UnLiftEnv r) m where
+  map = unLiftEnv map
+
+instance (Prod r, Applicative r m) => Applicative (UnLiftEnv r) m where
+  pure = unLiftEnv pure
+  ap = unLiftEnv ap
+
+instance (Prod r, Monad r m) => Monad (UnLiftEnv r) m where
+  bind = unLiftEnv bind
+  join = unLiftEnv join
+
+instance (Prod r, VTF.VectorTF r) => VTF.VectorTF (UnLiftEnv r) where
+  zero = unLiftEnv VTF.zero
+  basis = unLiftEnv VTF.basis
+  plus = unLiftEnv VTF.plus
+  mult = unLiftEnv VTF.mult
+  vtfMatch = unLiftEnv VTF.vtfMatch
+
+instance (Prod r, DiffWrapper r) => DiffWrapper (UnLiftEnv r) where
+  diffWrapper = unLiftEnv diffWrapper
+  runDiffWrapper = unLiftEnv runDiffWrapper
+
+instance (Prod r, Fix r) => Fix (UnLiftEnv r) where
+  fix = unLiftEnv fix
+  runFix = unLiftEnv runFix
+
+instance (Prod r, FreeVector r) => FreeVector (UnLiftEnv r) where
+  freeVector = unLiftEnv freeVector
+  runFreeVector = unLiftEnv runFreeVector
+
+instance Lang r => Lang (UnLiftEnv r) where
+  exfalso = unLiftEnv exfalso
   writer = unLiftEnv writer
   runWriter = unLiftEnv runWriter
   state = unLiftEnv state
   runState = unLiftEnv runState
   float2Double = unLiftEnv float2Double
   double2Float = unLiftEnv double2Float
-  putStrLn = unLiftEnv putStrLn
-
-instance DLang r => DLang (UnLiftEnv r) where
diff --git a/DDF/Unit.hs b/DDF/Unit.hs
--- a/DDF/Unit.hs
+++ b/DDF/Unit.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
 module DDF.Unit (module DDF.DBI, module DDF.Unit) where
 
 import DDF.DBI
diff --git a/DDF/Vector.hs b/DDF/Vector.hs
--- a/DDF/Vector.hs
+++ b/DDF/Vector.hs
@@ -4,12 +4,14 @@
   MultiParamTypeClasses,
   NoMonomorphismRestriction,
   FlexibleContexts,
-  FlexibleInstances
+  FlexibleInstances,
+  TypeFamilies
 #-}
 
 module DDF.Vector where
 import DDF.Double
 import qualified Prelude as M
+import DDF.Meta.FreeVector
 
 class Monoid r g => Group r g where
   invert :: r h (g -> g)
@@ -21,13 +23,15 @@
   {-# MINIMAL (invert | minus) #-}
 
 class Group r v => Vector r v where
+  type Basis v :: *
   mult :: r h (M.Double -> v -> v)
   divide :: r h (v -> M.Double -> v)
   default mult :: Double r => r h (M.Double -> v -> v)
-  mult = lam2 $ \x y -> divide2 y (recip1 x)
+  mult = lam2 $ \x y -> divide2 y (app2 doubleDivide doubleOne x)
   default divide :: Double r => r h (v -> M.Double -> v)
-  divide = lam2 $ \x y -> mult2 (recip1 y) x
-  {-# MINIMAL (mult | divide) #-}
+  divide = lam2 $ \x y -> mult2 (app2 doubleDivide doubleOne y) x
+  toFreeVector :: r h (v -> FreeVector (Basis v) M.Double)
+  {-# MINIMAL (mult | divide), toFreeVector #-}
 
 minus2 = app2 minus
 mult1 = app mult
@@ -38,14 +42,4 @@
 divide1 = app divide
 recip = divide1 doubleOne
 recip1 = app recip
-
-instance Double r => Monoid r M.Double where
-  zero = doubleZero
-  plus = doublePlus
-
-instance Double r => Group r M.Double where
-  minus = doubleMinus
-
-instance Double r => Vector r M.Double where
-  mult = doubleMult
-  divide = doubleDivide
+toFreeVector1 = app toFreeVector
diff --git a/DDF/VectorTF.hs b/DDF/VectorTF.hs
new file mode 100644
--- /dev/null
+++ b/DDF/VectorTF.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE NoImplicitPrelude, NoMonomorphismRestriction #-}
+
+module DDF.VectorTF where
+
+import qualified DDF.Double as Double
+import qualified DDF.Meta.VectorTF as M
+import qualified Prelude as M
+
+class Double.Double r => VectorTF r where
+  zero :: r h (M.VectorTF t f)
+  basis :: r h (t -> M.VectorTF t f)
+  plus :: r h (f -> f -> M.VectorTF t f)
+  mult :: r h (M.Double -> f -> M.VectorTF t f)
+  vtfMatch :: r h (a -> (t -> a) -> (f -> f -> a) -> (M.Double -> f -> a) -> M.VectorTF t f -> a)
+
+vtfMatch4 = Double.app4 vtfMatch
+vtfMatch5 = Double.app5 vtfMatch
+plus2 = Double.app2 plus
+mult1 = Double.app mult
+mult2 = Double.app2 mult
diff --git a/DDF/WithDiff.hs b/DDF/WithDiff.hs
--- a/DDF/WithDiff.hs
+++ b/DDF/WithDiff.hs
@@ -6,9 +6,9 @@
 #-}
 
 module DDF.WithDiff where
-
-import DDF.DLang
+import DDF.Lang
 import qualified Prelude as M
+import DDF.Diff ()
 
 class Monoid r w => WithDiff r w where
   withDiff :: r h ((w -> x) -> w -> DiffType x w)
@@ -17,16 +17,16 @@
 selfWithDiff :: (DBI r, WithDiff r w) => r h (w -> DiffType w w)
 selfWithDiff = withDiff1 id
 
-instance DLang repr => ProdCon (WithDiff repr) l r where prodCon = Sub Dict
+instance Lang repr => ProdCon (WithDiff repr) l r where prodCon = Sub Dict
 
-instance DLang r => WithDiff r () where
+instance Lang r => WithDiff r () where
   withDiff = const1 id
 
-instance DLang r => WithDiff r M.Double where
+instance Lang r => WithDiff r M.Double where
   withDiff = lam2 $ \con d -> dual1 $ mkProd2 d (app con doubleOne)
 
-instance DLang r => WithDiff r M.Float where
+instance Lang r => WithDiff r M.Float where
   withDiff = lam2 $ \con d -> dual1 $ mkProd2 d (app con floatOne)
 
-instance (DLang repr, WithDiff repr l, WithDiff repr r) => WithDiff repr (l, r) where
+instance (Lang repr, WithDiff repr l, WithDiff repr r) => WithDiff repr (l, r) where
   withDiff = lam $ \con -> bimap2 (withDiff1 (lam $ \l -> app con (mkProd2 l zero))) (withDiff1 (lam $ \r -> app con (mkProd2 zero r)))
diff --git a/DDF/Xor.lhs b/DDF/Xor.lhs
--- a/DDF/Xor.lhs
+++ b/DDF/Xor.lhs
@@ -1,5 +1,4 @@
-
-> {-# LANGUAGE ScopedTypeVariables, NoMonomorphismRestriction, TypeApplications, RankNTypes #-}
+> {-# LANGUAGE ScopedTypeVariables, NoMonomorphismRestriction, TypeApplications, RankNTypes, NoImplicitPrelude #-}
 
 This is the classical example of using sigmoid NN to approximate Xor.
 You should already read DDF.Poly before this.
@@ -89,11 +88,11 @@
 However, unlike Poly, there are more than one datapoint, so we need to use a list, and map xor onto it.
 
 > loss :: Lang repr => repr h (XOR -> M.Double)
-> loss = lam $ \xor -> fix2 (lam $ \self -> listMatch2 doubleZero (lam2 $ \x xs -> plus2 x (app self xs))) (map2 (app eval xor) dataset)
+> loss = lam $ \xor -> y2 (lam $ \self -> listMatch2 doubleZero (lam2 $ \x xs -> plus2 x (app self xs))) (map2 (app eval xor) dataset)
 
 Now we are good to implement the train function!
 
-> findXor :: forall g m. (RandomGen g, M.Monad m) => g -> (AST -> m ()) -> (Int -> M.Double -> M.String -> m ()) -> m XOR
+> findXor :: forall g m. (RandomGen g, M.Monad m) => g -> (AST -> m ()) -> (M.Int -> M.Double -> M.String -> m ()) -> m XOR
 > findXor rand doAST doIter = case runImpW $ noEnv xorNet of
 >   RunImpW ((Combine (Show xorS) (Combine (Eval xorEv) xorE)) :: Weight w => Combine Show (Combine Eval (GDiff Eval)) () (w -> XOR)) -> do
 >     doAST $ xorS vars 0
@@ -109,22 +108,22 @@
 >     where
 >       diff :: GDiff Eval () x -> DiffType w x
 >       diff x = ((runEval (runDiff (runGDiff x (Proxy :: Proxy w))) ()) \\ weightCon @w @(Vector Eval))
->       go :: M.Show w => (DiffType w (w -> XOR)) -> w -> (w -> DiffType w w) -> (DiffType w (XOR -> M.Double)) -> (M.Double -> w -> w -> w) -> Int -> (w -> XOR) -> m XOR
->       go xor weight reifyE lossE update i orig | i <= 2500 = do
+>       go :: M.Show w => (DiffType w (w -> XOR)) -> w -> (w -> DiffType w w) -> (DiffType w (XOR -> M.Double)) -> (M.Double -> w -> w -> w) -> M.Int -> (w -> XOR) -> m XOR
+>       go xor weight reifyE lossE updateW i orig | i <= 2500 = do
 >         doIter i lossVal (M.show weight)
->         go xor (update 0.3 weight lossDiff) reifyE lossE update (1 + i) orig
+>         go xor (updateW 0.3 weight lossDiff) reifyE lossE updateW (1 + i) orig
 >           where
 >             M.Dual (lossVal, lossDiff) = lossE $ xor (reifyE weight)
 >       go _ weight _ _ _ _ orig = M.return $ orig weight
 
-> main :: IO ()
+> main :: M.IO ()
 > main = do
 >   g <- getStdGen
 >   xorTrained <- findXor g print (\i d w -> when (isSquare i) $ do
 >     print d
 >     M.putStrLn w
 >     M.putStrLn "")
->   let doXor :: M.Double -> M.Double -> IO ()
+>   let doXor :: M.Double -> M.Double -> M.IO ()
 >       doXor l r = M.putStrLn $ M.show l ++ " xor " ++ M.show r ++ " is " ++ (M.show $ xorTrained (l, r))
 >   doXor 0 0
 >   doXor 0 1
diff --git a/DDF/Y.hs b/DDF/Y.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Y.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE NoImplicitPrelude, NoMonomorphismRestriction #-}
+
+module DDF.Y (module DDF.Y, module DDF.DBI) where
+
+import DDF.DBI
+
+class DBI r => Y r where
+  y :: r h ((a -> a) -> a)
+  undefined :: r h a
+  undefined = y1 id
+
+y1 = app y
+y2 = app2 y
diff --git a/DeepDarkFantasy.cabal b/DeepDarkFantasy.cabal
--- a/DeepDarkFantasy.cabal
+++ b/DeepDarkFantasy.cabal
@@ -1,5 +1,5 @@
 name: DeepDarkFantasy
-version: 0.2017.4.19
+version: 0.2017.8.4
 cabal-version: 1.12
 build-type: Simple
 license: Apache
@@ -10,6 +10,11 @@
 synopsis: A DSL for creating neural network.
 license-file: LICENSE
 
+Flag WError
+  Description: make warning error
+  Manual: True
+  Default: False
+
 source-repository head
   type: git
   location: https://github.com/ThoughtWorksInc/DeepDarkFantasy
@@ -22,43 +27,55 @@
     DDF.Combine
     DDF.DBI
     DDF.Diff
-    DDF.DLang
+    DDF.DiffWrapper
     DDF.Double
     DDF.Dual
     DDF.Eval
+    DDF.Fix
     DDF.Float
+    DDF.FreeVector
     DDF.GDiff
-    DDF.GInfDiff
     DDF.ImportMeta
     DDF.ImpW
-    DDF.InfDiff
+    DDF.Int
+    DDF.IO
     DDF.Lang
+    DDF.List
     DDF.Map
     DDF.Meta.Interpreter
     DDF.Meta.Diff
+    DDF.Meta.DiffWrapper
     DDF.Meta.Dual
+    DDF.Meta.FreeVector
+    DDF.Meta.VectorTF
     DDF.Option
     DDF.Poly
     DDF.Prod
-    DDF.RTInfDiff
     DDF.Show
     DDF.Size
+    DDF.Sum
     DDF.UInt
     DDF.UnHOAS
     DDF.Unit
     DDF.UnLiftEnv
     DDF.Util
     DDF.Vector
+    DDF.VectorTF
     DDF.WithDiff
     DDF.Xor
+    DDF.Y
+    DDF.PE
   build-depends:
     base >= 4.9.0.0 && <= 4.9.1.0,
     mtl -any,
     random -any,
     constraints -any,
     containers -any,
-    bimap -any
+    bimap -any,
+    recursion-schemes -any
   ghc-options: -Wall -Wno-type-defaults -Wno-missing-signatures -Wno-orphans -fwarn-tabs -ferror-spans
+  if flag(WError)
+    ghc-options: -Werror
   default-language: Haskell2010
 
 Test-Suite TestPoly
@@ -83,4 +100,17 @@
     mtl -any,
     random -any,
     constraints -any,
+    DeepDarkFantasy
+
+Test-Suite TestPE
+  type: exitcode-stdio-1.0
+  default-language: Haskell2010
+  hs-source-dirs: test
+  main-is: TestPE.hs
+  build-depends:
+    base >= 4.9.0.0 && <= 4.9.1.0,
+    mtl -any,
+    random -any,
+    constraints -any,
+    QuickCheck,
     DeepDarkFantasy
diff --git a/test/TestPE.hs b/test/TestPE.hs
new file mode 100644
--- /dev/null
+++ b/test/TestPE.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE
+  NoImplicitPrelude,
+  NoMonomorphismRestriction,
+  RankNTypes,
+  FlexibleInstances
+#-}
+
+module Main where
+
+import DDF.PE
+import DDF.Double
+import DDF.Size
+import qualified Prelude as M
+import Prelude ((>), (>=))
+import System.Exit (exitFailure)
+import Control.Monad
+import DDF.Meta.Interpreter
+import Test.QuickCheck
+import DDF.Eval
+import DDF.Combine
+
+class TestEqual x where
+  testEqual :: x -> x -> M.IO ()
+
+instance TestEqual M.Double where
+  testEqual l r = quickCheck (l == r)
+
+instance TestEqual (M.Double -> M.Double) where
+  testEqual l r = quickCheck (\x -> l x == r x)
+
+instance TestEqual (M.Double -> M.Double -> M.Double) where
+  testEqual l r = quickCheck (\x y -> l x y == r x y)
+
+test :: TestEqual x => (forall r. Double r => r () x) -> (M.Int -> M.Int -> M.Bool) -> M.IO ()
+test x c = do
+  quickCheck (c (runSize x) (runSize (pe x)))
+  testEqual (runEval x ()) (runEval (pe x) ())
+
+optimized x y = quickCheck (runSize x > runSize y)
+
+main :: M.IO ()
+main = do
+  test (doublePlus2 (double 1.0) (double 1.0)) (>)
+  test (doublePlus1 (double 1.0)) n
+  test (abs (doublePlus2 z (double 1.0))) n
+  test (doublePlus1 (double 1.0)) n
+  test (abs (doublePlus2 z (double 0.0))) (>)
+  test (doubleExp1 (double 1.0)) (>)
+  test (abs (doubleExp1 z)) n
+  test (abs $ abs $ (app2 (s doublePlus) z (s z))) n
+  where
+    n _ _ = M.True