diff --git a/DDF/Combine.hs b/DDF/Combine.hs
--- a/DDF/Combine.hs
+++ b/DDF/Combine.hs
@@ -1,18 +1,18 @@
-{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE NoImplicitPrelude, TypeFamilies, TypeApplications, ScopedTypeVariables, NoMonomorphismRestriction #-}
 
 module DDF.Combine where
 
-import DDF.Lang
+import DDF.Meta.Interpreter
+import DDF.DLang
 import qualified DDF.Map as Map
 
-data Combine l r h x = Combine (l h x) (r h x)
-
 instance (DBI l, DBI r) => DBI (Combine l r) where
   z = Combine z z
   s (Combine l r) = Combine (s l) (s r)
   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)
@@ -60,12 +60,14 @@
   dual = Combine dual dual
   runDual = Combine runDual runDual
 
+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
   left = Combine left left
   right = Combine right right
   sumMatch = Combine sumMatch sumMatch
-  unit = Combine unit unit
   exfalso = Combine exfalso exfalso
   ioRet = Combine ioRet ioRet
   ioBind = Combine ioBind ioBind
@@ -80,3 +82,5 @@
   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
@@ -22,39 +22,36 @@
 
 module DDF.DBI (module DDF.DBI, module DDF.ImportMeta) where
 import qualified Prelude as P
-import DDF.Util
-import System.Random
-import Data.Constraint
-import Data.Constraint.Forall
 import DDF.ImportMeta
 
 class Monoid r m where
   zero :: r h m
   plus :: r h (m -> m -> m)
 
-class DBI (repr :: * -> * -> *) where
-  z :: repr (a, h) a
-  s :: repr h b -> repr (a, h) b
-  abs :: repr (a, h) b -> repr h (a -> b)
-  app :: repr h (a -> b) -> repr h a -> repr h b
+class DBI (r :: * -> * -> *) where
+  z :: r (a, h) a
+  s :: r h b -> r (a, h) b
+  abs :: r (a, h) b -> r h (a -> b)
+  app :: r h (a -> b) -> r h a -> r h b
   -- | We use a variant of HOAS so it can be compile to DBI, which is more compositional (No Negative Occurence).
   -- It require explicit lifting of variables.
   -- Use lam to do automatic lifting of variables.
-  hoas :: (repr (a, h) a -> repr (a, h) b) -> repr h (a -> b)
+  hoas :: (r (a, h) a -> r (a, h) b) -> r h (a -> b)
   hoas f = abs $ f z
-  com :: repr h ((b -> c) -> (a -> b) -> (a -> c))
+  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 :: repr h ((a -> b -> c) -> (b -> a -> c))
+  flip :: r h ((a -> b -> c) -> (b -> a -> c))
   flip = lam3 $ \f b a -> app2 f a b
-  id :: repr h (a -> a)
+  id :: r h (a -> a)
   id = lam $ \x -> x
-  const :: repr h (a -> b -> a)
+  const :: r h (a -> b -> a)
   const = lam2 $ \x _ -> x
-  scomb :: repr h ((a -> b -> c) -> (a -> b) -> (a -> c))
+  scomb :: r h ((a -> b -> c) -> (a -> b) -> (a -> c))
   scomb = lam3 $ \f x arg -> app2 f arg (app x arg)
-  dup :: repr h ((a -> a -> b) -> (a -> b))
+  dup :: r h ((a -> a -> b) -> (a -> b))
   dup = lam2 $ \f x -> app2 f x x
-  let_ :: repr h (a -> (a -> b) -> b)
+  let_ :: r h (a -> (a -> b) -> b)
   let_ = flip1 id
 
 const1 = app const
@@ -121,22 +118,4 @@
 noEnv :: repr () x -> repr () x
 noEnv = P.id
 
-instance Weight () where weightCon = Sub Dict
-
-instance Weight P.Double where weightCon = Sub Dict
-
-instance (Weight l, Weight r) => Weight (l, r) where
-  weightCon :: forall con. (con (), con P.Float, con P.Double, ForallV (ProdCon con)) :- con (l, r)
-  weightCon = Sub (mapDict (prodCon \\ (instV :: (ForallV (ProdCon con) :- ProdCon con l r))) (Dict \\ weightCon @l @con \\ weightCon @r @con))
-
-class ProdCon con l r where
-  prodCon :: (con l, con r) :- con (l, r)
-
-instance ProdCon Random l r where prodCon = Sub Dict
-
-instance ProdCon RandRange l r where prodCon = Sub Dict
-
-instance ProdCon P.Show l r where prodCon = Sub Dict
-
-class Weight w where
-  weightCon :: (con (), con P.Float, con P.Double, ForallV (ProdCon con)) :- con w
+scomb2 = app2 scomb
diff --git a/DDF/DLang.hs b/DDF/DLang.hs
new file mode 100644
--- /dev/null
+++ b/DDF/DLang.hs
@@ -0,0 +1,12 @@
+{-# 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
@@ -1,37 +1,111 @@
 {-# LANGUAGE
   NoImplicitPrelude,
-  RankNTypes,
+  ExplicitForAll,
+  InstanceSigs,
   ScopedTypeVariables,
   TypeApplications,
-  TypeFamilies,
-  KindSignatures,
-  MultiParamTypeClasses,
-  FlexibleInstances,
-  NoMonomorphismRestriction
+  FlexibleContexts,
+  UndecidableInstances,
+  TypeFamilies
 #-}
 
 module DDF.Diff where
 
-import DDF.ImportMeta
-import DDF.Meta.Dual
-import Prelude
-import Data.Map
+import DDF.DLang
+import qualified Data.Map as M
+import qualified DDF.Map as Map
 
-type family Diff (v :: *) (x :: *)
-type instance Diff v () = ()
-type instance Diff v (l, r) = (Diff v l, Diff v r)
-type instance Diff v (l -> r) = Diff v l -> Diff v r
-type instance Diff v Void = Void
-type instance Diff v Double = Dual Double v
-type instance Diff v Float = Dual Float v
-type instance Diff v (Writer l r) = Writer (Diff v l) (Diff v r)
-type instance Diff v (IO l) = IO (Diff v l)
-type instance Diff v (Maybe l) = Maybe (Diff v l)
-type instance Diff v [l] = [Diff v l]
-type instance Diff v (Either l r) = Either (Diff v l) (Diff v r)
-type instance Diff v (State l r) = State (Diff v l) (Diff v r)
-type instance Diff v Bool = Bool
-type instance Diff v Char = Char
-type instance Diff v Ordering = Ordering
-type instance Diff v (Map k val) = Map (Diff v k) (Diff v val)
-type instance Diff v (Dual l r) = Dual (Diff v l) (Diff 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
+
+instance Bool r => Bool (Diff r v) where
+  bool x = Diff $ bool x
+  ite = Diff ite
+
+instance Char r => Char (Diff r v) where
+  char = Diff . char
+
+instance Prod r => Prod (Diff r v) where
+  mkProd = Diff mkProd
+  zro = Diff zro
+  fst = Diff fst
+
+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
+  double x = Diff $ mkDual2 (double x) zero
+  doublePlus = Diff $ lam2 $ \l r ->
+    mkDual2 (plus2 (dualOrig1 l) (dualOrig1 r)) (plus2 (dualDiff1 l) (dualDiff1 r))
+  doubleMinus = Diff $ lam2 $ \l r ->
+    mkDual2 (minus2 (dualOrig1 l) (dualOrig1 r)) (minus2 (dualDiff1 l) (dualDiff1 r))
+  doubleMult = Diff $ lam2 $ \l r ->
+    mkDual2 (mult2 (dualOrig1 l) (dualOrig1 r))
+      (plus2 (mult2 (dualOrig1 l) (dualDiff1 r)) (mult2 (dualOrig1 r) (dualDiff1 l)))
+  doubleDivide = Diff $ lam2 $ \l r ->
+    mkDual2 (divide2 (dualOrig1 l) (dualOrig1 r))
+      (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)))
+
+instance (Vector r v, Lang r) => Float (Diff r v) where
+  float x = Diff $ mkDual2 (float x) zero
+  floatPlus = Diff $ lam2 $ \l r ->
+    mkDual2 (plus2 (dualOrig1 l) (dualOrig1 r)) (plus2 (dualDiff1 l) (dualDiff1 r))
+  floatMinus = Diff $ lam2 $ \l r ->
+    mkDual2 (minus2 (dualOrig1 l) (dualOrig1 r)) (minus2 (dualDiff1 l) (dualDiff1 r))
+  floatMult = Diff $ lam2 $ \l r ->
+    mkDual2 (mult2 (float2Double1 (dualOrig1 l)) (dualOrig1 r))
+      (plus2 (mult2 (float2Double1 (dualOrig1 l)) (dualDiff1 r)) (mult2 (float2Double1 (dualOrig1 r)) (dualDiff1 l)))
+  floatDivide = Diff $ lam2 $ \l r ->
+    mkDual2 (divide2 (dualOrig1 l) (float2Double1 (dualOrig1 r)))
+      (divide2 (minus2 (mult2 (float2Double1 (dualOrig1 r)) (dualDiff1 l)) (mult2 (float2Double1 (dualOrig1 l)) (dualDiff1 r)))
+        (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))))
+
+instance Option r => Option (Diff r v) where
+  nothing = Diff nothing
+  just = Diff just
+  optionMatch = Diff optionMatch
+
+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 = 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
+
+instance Bimap r => Bimap (Diff r v) where
+
+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
+  left = Diff left
+  right = Diff right
+  sumMatch = Diff sumMatch
+  exfalso = Diff exfalso
+  ioRet = Diff ioRet
+  ioBind = Diff ioBind
+  nil = Diff nil
+  cons = Diff cons
+  listMatch = Diff listMatch
+  ioMap = Diff ioMap
+  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
diff --git a/DDF/Eval.hs b/DDF/Eval.hs
--- a/DDF/Eval.hs
+++ b/DDF/Eval.hs
@@ -1,12 +1,13 @@
 {-# LANGUAGE
   NoImplicitPrelude,
-  LambdaCase
+  LambdaCase,
+  TypeFamilies,
+  FlexibleContexts
 #-}
 
 module DDF.Eval where
 
 import DDF.ImportMeta
-import DDF.Lang
 import qualified Prelude as M
 import qualified Control.Monad.Writer as M (WriterT(WriterT), runWriter)
 import qualified Control.Monad.State as M
@@ -16,16 +17,16 @@
 import qualified Data.Map as M.Map
 import qualified DDF.Meta.Dual as M
 import qualified DDF.Map as Map
-
-newtype Eval h x = Eval {runEval :: h -> x}
+import DDF.DLang
 
 comb = Eval . M.const
 
 instance DBI Eval where
   z = Eval M.fst
   s (Eval a) = Eval $ a . M.snd
-  abs (Eval f) = Eval $ \a h -> f (h, a)
+  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
@@ -75,6 +76,9 @@
   dual = comb M.Dual
   runDual = comb M.runDual
 
+instance Unit Eval where
+  unit = comb ()
+
 instance Lang Eval where
   fix = comb loop
     where loop x = x $ loop x
@@ -83,7 +87,6 @@
   sumMatch = comb $ \l r -> \case
                              M.Left x -> l x
                              M.Right x -> r x
-  unit = comb ()
   exfalso = comb absurd
   ioRet = comb M.return
   ioBind = comb (>>=)
@@ -100,3 +103,5 @@
   state = comb M.state
   runState = comb M.runState
   putStrLn = comb M.putStrLn
+
+instance DLang Eval where
diff --git a/DDF/GDiff.hs b/DDF/GDiff.hs
new file mode 100644
--- /dev/null
+++ b/DDF/GDiff.hs
@@ -0,0 +1,96 @@
+{-# LANGUAGE
+  NoImplicitPrelude,
+  RankNTypes,
+  InstanceSigs,
+  ScopedTypeVariables,
+  TypeFamilies,
+  TypeApplications
+#-}
+
+module DDF.GDiff (module DDF.Meta.Diff) where
+import DDF.DLang
+import qualified Prelude as M
+import DDF.Meta.Diff
+import DDF.Diff ()
+import qualified Data.Map as M
+import qualified DDF.Map as Map
+
+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
+  ite = GDiff $ M.const ite
+
+instance Char r => Char (GDiff r) where
+  char x = GDiff $ M.const $ char x
+
+instance Prod r => Prod (GDiff r) where
+  mkProd = GDiff (M.const mkProd)
+  zro = GDiff $ M.const zro
+  fst = GDiff $ M.const fst
+
+instance Dual r => Dual (GDiff r) where
+  dual = GDiff $ M.const $ dual
+  runDual = GDiff $ M.const $ runDual
+
+instance (Double r, Dual 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
+
+instance Lang r => Float (GDiff r) where
+  float x = GDiff $ M.const $ float x
+  floatPlus = GDiff $ M.const $ floatPlus
+  floatMinus = GDiff $ M.const $ floatMinus
+  floatMult = GDiff $ M.const $ floatMult
+  floatDivide = GDiff $ M.const $ floatDivide
+  floatExp = GDiff $ M.const $ floatExp
+
+instance Option r => Option (GDiff r) where
+  nothing = GDiff $ M.const nothing
+  just = GDiff $ M.const just
+  optionMatch = GDiff $ M.const optionMatch
+
+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
+  mapMap = GDiff $ M.const Map.mapMap
+
+instance Bimap r => Bimap (GDiff r) where
+
+instance Unit r => Unit (GDiff r) where
+  unit = GDiff $ M.const unit
+
+instance Lang r => Lang (GDiff r) where
+  fix = GDiff $ M.const fix
+  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
+  nil = GDiff $ M.const nil
+  cons = GDiff $ M.const cons
+  listMatch = GDiff $ M.const listMatch
+  ioMap = GDiff $ M.const ioMap
+  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
new file mode 100644
--- /dev/null
+++ b/DDF/GInfDiff.hs
@@ -0,0 +1,85 @@
+{-# 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/GWDiff.hs b/DDF/GWDiff.hs
deleted file mode 100644
--- a/DDF/GWDiff.hs
+++ /dev/null
@@ -1,104 +0,0 @@
-{-# LANGUAGE
-  NoImplicitPrelude,
-  RankNTypes,
-  InstanceSigs,
-  ScopedTypeVariables
-#-}
-
-module DDF.GWDiff (module DDF.GWDiff, module DDF.Diff) where
-import DDF.Lang
-import qualified Prelude as M
-import DDF.Diff
-import qualified Data.Map as M
-import qualified DDF.Map as Map
-
-newtype GWDiff r h x = GWDiff {runGWDiff :: forall v. Vector r v => Proxy v -> r (Diff v h) (Diff v x)}
-
-instance DBI r => DBI (GWDiff r) where
-  z = GWDiff (M.const z)
-  s (GWDiff x) = GWDiff (\p -> s $ x p)
-  app (GWDiff f) (GWDiff x) = GWDiff (\p -> app (f p) (x p))
-  abs (GWDiff x) = GWDiff (\p -> abs $ x p)
-
-instance Bool r => Bool (GWDiff r) where
-  bool x = GWDiff $ M.const $ bool x
-  ite = GWDiff $ M.const ite
-
-instance Char r => Char (GWDiff r) where
-  char x = GWDiff $ M.const $ char x
-
-instance Prod r => Prod (GWDiff r) where
-  mkProd = GWDiff (M.const mkProd)
-  zro = GWDiff $ M.const zro
-  fst = GWDiff $ M.const fst
-
-instance Dual r => Dual (GWDiff r) where
-  dual = GWDiff $ M.const $ dual
-  runDual = GWDiff $ M.const $ runDual
-
-instance (Double r, Dual r) => Double (GWDiff r) where
-  double x = GWDiff $ M.const $ mkDual2 (double x) zero
-  doublePlus = GWDiff $ M.const $ lam2 $ \l r ->
-    mkDual2 (plus2 (dualOrig1 l) (dualOrig1 r)) (plus2 (dualDiff1 l) (dualDiff1 r))
-  doubleMinus = GWDiff $ M.const $ lam2 $ \l r ->
-    mkDual2 (minus2 (dualOrig1 l) (dualOrig1 r)) (minus2 (dualDiff1 l) (dualDiff1 r))
-  doubleMult = GWDiff $ M.const $ lam2 $ \l r ->
-    mkDual2 (mult2 (dualOrig1 l) (dualOrig1 r))
-      (plus2 (mult2 (dualOrig1 l) (dualDiff1 r)) (mult2 (dualOrig1 r) (dualDiff1 l)))
-  doubleDivide = GWDiff $ M.const $ lam2 $ \l r ->
-    mkDual2 (divide2 (dualOrig1 l) (dualOrig1 r))
-      (divide2 (minus2 (mult2 (dualOrig1 r) (dualDiff1 l)) (mult2 (dualOrig1 l) (dualDiff1 r)))
-        (mult2 (dualOrig1 r) (dualOrig1 r)))
-  doubleExp = GWDiff $ M.const $ lam $ \x -> let_2 (doubleExp1 (dualOrig1 x)) $ lam $ \e -> mkDual2 e (mult2 e (dualDiff1 x))
-
-instance Lang r => Float (GWDiff r) where
-  float x = GWDiff $ M.const $ mkDual2 (float x) zero
-  floatPlus = GWDiff $ M.const $ lam2 $ \l r ->
-    mkDual2 (plus2 (dualOrig1 l) (dualOrig1 r)) (plus2 (dualDiff1 l) (dualDiff1 r))
-  floatMinus = GWDiff $ M.const $ lam2 $ \l r ->
-    mkDual2 (minus2 (dualOrig1 l) (dualOrig1 r)) (minus2 (dualDiff1 l) (dualDiff1 r))
-  floatMult = GWDiff $ M.const $ lam2 $ \l r ->
-    mkDual2 (mult2 (float2Double1 (dualOrig1 l)) (dualOrig1 r))
-      (plus2 (mult2 (float2Double1 (dualOrig1 l)) (dualDiff1 r)) (mult2 (float2Double1 (dualOrig1 r)) (dualDiff1 l)))
-  floatDivide = GWDiff $ M.const $ lam2 $ \l r ->
-    mkDual2 (divide2 (dualOrig1 l) (float2Double1 (dualOrig1 r)))
-      (divide2 (minus2 (mult2 (float2Double1 (dualOrig1 r)) (dualDiff1 l)) (mult2 (float2Double1 (dualOrig1 l)) (dualDiff1 r)))
-        (float2Double1 (mult2 (float2Double1 (dualOrig1 r)) (dualOrig1 r))))
-  floatExp = GWDiff $ M.const $ lam $ \x -> let_2 (floatExp1 (dualOrig1 x)) $ lam $ \e -> mkDual2 e (mult2 (float2Double1 e) (dualDiff1 x))
-
-instance Option r => Option (GWDiff r) where
-  nothing = GWDiff $ M.const nothing
-  just = GWDiff $ M.const just
-  optionMatch = GWDiff $ M.const optionMatch
-
-instance Map.Map r => Map.Map (GWDiff r) where
-  empty = GWDiff $ M.const Map.empty
-  singleton = GWDiff $ M.const Map.singleton
-  lookup :: forall h k a. Map.Ord k => GWDiff r h (k -> M.Map k a -> Maybe a)
-  lookup = GWDiff $ \(_ :: Proxy v) -> withDict (Map.diffOrd (Proxy :: Proxy (v, k))) Map.lookup
-  alter :: forall h k a. Map.Ord k => GWDiff r h ((Maybe a -> Maybe a) -> k -> M.Map k a -> M.Map k a)
-  alter = GWDiff $ \(_ :: Proxy v) -> withDict (Map.diffOrd (Proxy :: Proxy (v, k))) Map.alter
-  mapMap = GWDiff $ M.const Map.mapMap
-
-instance Bimap r => Bimap (GWDiff r) where
-
-instance Lang r => Lang (GWDiff r) where
-  fix = GWDiff $ M.const fix
-  left = GWDiff $ M.const left
-  right = GWDiff $ M.const right
-  sumMatch = GWDiff $ M.const sumMatch
-  unit = GWDiff $ M.const unit
-  exfalso = GWDiff $ M.const exfalso
-  ioRet = GWDiff $ M.const ioRet
-  ioBind = GWDiff $ M.const ioBind
-  nil = GWDiff $ M.const nil
-  cons = GWDiff $ M.const cons
-  listMatch = GWDiff $ M.const listMatch
-  ioMap = GWDiff $ M.const ioMap
-  writer = GWDiff $ M.const writer
-  runWriter = GWDiff $ M.const runWriter
-  float2Double = GWDiff $ M.const $ bimap2 float2Double id
-  double2Float = GWDiff $ M.const $ bimap2 double2Float id
-  state = GWDiff $ M.const state
-  runState = GWDiff $ M.const runState
-  putStrLn = GWDiff $ M.const putStrLn
diff --git a/DDF/ImpW.hs b/DDF/ImpW.hs
--- a/DDF/ImpW.hs
+++ b/DDF/ImpW.hs
@@ -1,24 +1,21 @@
-{-# LANGUAGE NoImplicitPrelude, RankNTypes, InstanceSigs, ScopedTypeVariables, ExistentialQuantification #-}
+{-# LANGUAGE
+  NoImplicitPrelude,
+  RankNTypes,
+  InstanceSigs,
+  ScopedTypeVariables,
+  ExistentialQuantification,
+  TypeFamilies,
+  TypeApplications
+#-}
 
 module DDF.ImpW where
 
-import DDF.Lang
+import DDF.DLang
 import qualified DDF.Map as Map
 
-data RunImpW repr h x = forall w. Weight w => RunImpW (repr h (w -> x))
-data ImpW repr h x = NoImpW (repr h x) | forall w. Weight w => ImpW (repr h (w -> x))
-
-runImpW :: forall repr h x. Lang repr => ImpW repr h x -> RunImpW repr h x
+runImpW :: forall r h x. Unit r => ImpW r h x -> RunImpW r h x
 runImpW (ImpW x) = RunImpW x
-runImpW (NoImpW x) = RunImpW (const1 x :: repr h (() -> x))
-
-type RunImpWR repr h x = forall r. (forall w. Weight w => repr h (w -> x) -> r) -> r
-
-runImpW2RunImpWR :: RunImpW repr h x -> RunImpWR repr h x
-runImpW2RunImpWR (RunImpW x) = \f -> f x
-
-runImpWR2RunImpW :: RunImpWR repr h x -> RunImpW repr h x
-runImpWR2RunImpW f = f RunImpW
+runImpW (NoImpW x) = RunImpW (const1 x :: r h (() -> x))
 
 instance Prod r => DBI (ImpW r) where
   z = NoImpW z
@@ -31,6 +28,8 @@
   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
@@ -78,6 +77,9 @@
   dual = NoImpW dual
   runDual = NoImpW runDual
 
+instance (Prod r, Unit r) => Unit (ImpW r) where
+  unit = NoImpW unit
+
 instance Lang r => Lang (ImpW r) where
   nil = NoImpW nil
   cons = NoImpW cons
@@ -85,7 +87,6 @@
   ioRet = NoImpW ioRet
   ioMap = NoImpW ioMap
   ioBind = NoImpW ioBind
-  unit = NoImpW unit
   exfalso = NoImpW exfalso
   fix = NoImpW fix
   left = NoImpW left
@@ -98,3 +99,5 @@
   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
@@ -1,10 +1,12 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module DDF.ImportMeta (module Prelude, module Data.Void, module Control.Monad.Writer, module Control.Monad.State, module Data.Constraint, module Data.Proxy) where
+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 Data.Void (Void, absurd)
 import Control.Monad.Writer (Writer)
 import Control.Monad.State (State)
 import Data.Constraint
+import Data.Constraint.Forall
 import Data.Proxy
+import DDF.Util
diff --git a/DDF/InfDiff.hs b/DDF/InfDiff.hs
new file mode 100644
--- /dev/null
+++ b/DDF/InfDiff.hs
@@ -0,0 +1,86 @@
+{-# 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/Lang.hs b/DDF/Lang.hs
--- a/DDF/Lang.hs
+++ b/DDF/Lang.hs
@@ -1,33 +1,31 @@
 {-# LANGUAGE
-    MultiParamTypeClasses,
-    RankNTypes,
-    ScopedTypeVariables,
-    FlexibleInstances,
-    FlexibleContexts,
-    UndecidableInstances,
-    PolyKinds,
-    LambdaCase,
-    NoMonomorphismRestriction,
-    TypeFamilies,
-    LiberalTypeSynonyms,
-    FunctionalDependencies,
-    ExistentialQuantification,
-    InstanceSigs,
-    TupleSections,
-    ConstraintKinds,
-    DefaultSignatures,
-    TypeOperators,
-    TypeApplications,
-    PartialTypeSignatures,
-    NoImplicitPrelude #-}
+  NoImplicitPrelude,
+  NoMonomorphismRestriction,
+  MultiParamTypeClasses,
+  FlexibleInstances
+#-}
 
-module DDF.Lang (module DDF.Lang, module DDF.Bool, module DDF.Char, module DDF.Double, module DDF.Float, module DDF.Bimap, module DDF.Dual) where
+module DDF.Lang (
+  module DDF.Lang,
+  module DDF.Bool,
+  module DDF.Char,
+  module DDF.Double,
+  module DDF.Float,
+  module DDF.Bimap,
+  module DDF.Dual,
+  module DDF.Meta.Diff,
+  module DDF.Unit
+) where
+
 import DDF.Bool
 import DDF.Char
 import DDF.Double
 import DDF.Float
 import DDF.Bimap
 import DDF.Dual
+import DDF.Vector
+import DDF.Meta.Diff
+import DDF.Unit
 
 import qualified DDF.Meta.Dual as M
 import qualified Control.Monad.Writer as M (Writer)
@@ -36,12 +34,11 @@
 import qualified Data.Map as M
 import qualified DDF.Map as Map
 
-class (Bool r, Char r, Double r, Float r, Bimap r, Dual r) => Lang r where
+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)
-  unit :: r h ()
   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)
@@ -79,24 +76,6 @@
 
 instance Lang repr => ProdCon (Vector repr) l r where prodCon = Sub Dict
 
-class Monoid r g => Group r g where
-  invert :: r h (g -> g)
-  minus :: r h (g -> g -> g)
-  default invert :: DBI r => r h (g -> g)
-  invert = minus1 zero
-  default minus :: DBI r => r h (g -> g -> g)
-  minus = lam2 $ \x y -> plus2 x (invert1 y)
-  {-# MINIMAL (invert | minus) #-}
-
-class Group r v => Vector r v where
-  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)
-  default divide :: Double r => r h (v -> M.Double -> v)
-  divide = lam2 $ \x y -> mult2 (recip1 y) x
-  {-# MINIMAL (mult | divide) #-}
-
 instance Lang r => Monoid r () where
   zero = unit
   plus = const1 $ const1 unit
@@ -109,17 +88,6 @@
   mult = const1 $ const1 unit
   divide = const1 $ const1 unit
 
-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
-
 instance Float r => Monoid r M.Float where
   zero = floatZero
   plus = floatPlus
@@ -217,18 +185,9 @@
 uncurry1 = app uncurry
 optionMatch2 = app2 optionMatch
 optionMatch3 = app3 optionMatch
-mult1 = app mult
-mult2 = app2 mult
-divide2 = app2 divide
-invert1 = app invert
-minus1 = app minus
-divide1 = app divide
-recip = divide1 doubleOne
-recip1 = app recip
 writer1 = app writer
 runWriter1 = app runWriter
 ioBind2 = app2 ioBind
-minus2 = app2 minus
 float2Double1 = app float2Double
 doubleExp1 = app doubleExp
 floatExp1 = app floatExp
diff --git a/DDF/Map.hs b/DDF/Map.hs
--- a/DDF/Map.hs
+++ b/DDF/Map.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE
   NoImplicitPrelude,
-  ScopedTypeVariables
+  ScopedTypeVariables,
+  TypeApplications,
+  FlexibleInstances
 #-}
 
 module DDF.Map (module DDF.Map, module DDF.Prod, module DDF.Option) where
@@ -9,11 +11,11 @@
 import qualified Prelude as M
 import qualified Data.Map as M
 import DDF.Option
-import DDF.Diff
+import DDF.Meta.Diff
 import qualified DDF.Meta.Dual as M
 
 class M.Ord x => Ord x where
-  diffOrd :: Proxy (v, x) -> Dict (Ord (Diff v x))
+  diffOrd :: Proxy (v, x) -> Dict (Ord (DiffType v x))
 
 instance Ord () where
   diffOrd _ = Dict
diff --git a/DDF/Meta/Diff.hs b/DDF/Meta/Diff.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Meta/Diff.hs
@@ -0,0 +1,49 @@
+
+{-# LANGUAGE
+  RankNTypes,
+  ScopedTypeVariables,
+  TypeApplications,
+  TypeFamilies,
+  KindSignatures,
+  MultiParamTypeClasses,
+  FlexibleInstances,
+  NoMonomorphismRestriction,
+  ConstraintKinds,
+  DataKinds,
+  FlexibleContexts
+#-}
+
+module DDF.Meta.Diff (module DDF.Meta.Diff, module DDF.Meta.Interpreter, module DDF.Vector) where
+
+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/Interpreter.hs b/DDF/Meta/Interpreter.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Meta/Interpreter.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE
+  RankNTypes,
+  TypeApplications,
+  TypeOperators,
+  ScopedTypeVariables,
+  MultiParamTypeClasses,
+  ExistentialQuantification,
+  FlexibleInstances,
+  InstanceSigs
+#-}
+
+module DDF.Meta.Interpreter (module DDF.Meta.Interpreter, module DDF.ImportMeta) where
+
+import DDF.ImportMeta
+
+newtype Eval h x = Eval {runEval :: h -> x}
+
+data Combine l r h x = Combine (l h x) (r h x)
+
+combineLeft (Combine l _) = l
+combineRight (Combine _ r) = r
+
+newtype UnHOAS repr h x = UnHOAS {runUnHOAS :: repr h x}
+
+class ProdCon con l r where
+  prodCon :: (con l, con r) :- con (l, r)
+
+instance ProdCon Random l r where prodCon = Sub Dict
+
+instance ProdCon RandRange l r where prodCon = Sub Dict
+
+instance ProdCon Show l r where prodCon = Sub Dict
+
+class Weight w where
+  weightCon :: (con (), con Float, con Double, ForallV (ProdCon con)) :- con w
+
+instance Weight () where weightCon = Sub Dict
+
+instance Weight Double where weightCon = Sub Dict
+
+instance Weight Float where weightCon = Sub Dict
+
+instance (Weight l, Weight r) => Weight (l, r) where
+  weightCon :: forall con. (con (), con Float, con Double, ForallV (ProdCon con)) :- con (l, r)
+  weightCon = Sub (mapDict (prodCon \\ (instV :: (ForallV (ProdCon con) :- ProdCon con l r))) (Dict \\ weightCon @l @con \\ weightCon @r @con))
+
+data RunImpW repr h x = forall w. Weight w => RunImpW (repr h (w -> x))
+data ImpW repr h x = NoImpW (repr h x) | forall w. Weight w => ImpW (repr h (w -> x))
+type RunImpWR repr h x = forall r. (forall w. Weight w => repr h (w -> x) -> r) -> r
+
+runImpW2RunImpWR :: RunImpW repr h x -> RunImpWR repr h x
+runImpW2RunImpWR (RunImpW x) = \f -> f x
+
+runImpWR2RunImpW :: RunImpWR repr h x -> RunImpW repr h x
+runImpWR2RunImpW f = f RunImpW
diff --git a/DDF/Poly.lhs b/DDF/Poly.lhs
--- a/DDF/Poly.lhs
+++ b/DDF/Poly.lhs
@@ -20,12 +20,12 @@
 > import DDF.Util
 > import DDF.Lang
 > import DDF.Show
-> import DDF.Eval
-> import DDF.WDiff
+> import DDF.Diff ()
 > import qualified Control.Monad as M
 > import Prelude (Integer)
 > import qualified Prelude as M
 > import qualified DDF.Meta.Dual as M
+> import DDF.Eval ()
 
 Importing files and opening language extension...
 So, our goal is to find x, where x * x + 2 * x + 3 = 27.
@@ -64,7 +64,7 @@
 >     go :: Integer -> M.Double -> m M.Double
 >     go i w | i < 200 = do
 >       doIter i w
->       go (1 + i) $ w - 0.001 * M.dualDiff (runEval (runWDiff $ noEnv comp) () $ M.Dual (w, 1))
+>       go (1 + i) $ w - 0.001 * M.dualDiff (runEval (runDiff $ noEnv comp) () $ M.Dual (w, 1))
 
 noEnv comp assume the term (which is a De Brujin Index term) need no environment (is free)
 and it is a finally tagless term, with WDiff interpreter being implicitly applied,
diff --git a/DDF/RTInfDiff.hs b/DDF/RTInfDiff.hs
new file mode 100644
--- /dev/null
+++ b/DDF/RTInfDiff.hs
@@ -0,0 +1,90 @@
+{-# 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,8 +1,8 @@
-{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE NoImplicitPrelude, TypeFamilies #-}
 
 module DDF.Show (module DDF.Show) where
 
-import DDF.Lang
+import DDF.DLang
 import qualified Prelude as M
 import qualified DDF.Map as Map
 
@@ -25,11 +25,12 @@
 
 instance DBI Show where
   z = Show $ M.const $ Leaf . show . M.flip (-) 1
-  s (Show v) = Show $ \vars -> v vars . M.flip (-) 1
-  abs (Show f) = Show $ \vars x -> lamAST (show x) (f vars (x + 1))
-  app (Show f) (Show x) = Show $ \vars h -> appAST (f vars h) (x vars h)
-  hoas f = Show $ \(v:vars) h ->
-    lamAST v (runShow (f $ Show $ M.const $ M.const $ Leaf v) vars (h + 1))
+  s (Show v) = Show $ \va -> v va . M.flip (-) 1
+  abs (Show f) = Show $ \va x -> lamAST (show x) (f va (x + 1))
+  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
@@ -77,12 +78,14 @@
   dual = name "dual"
   runDual = name "runDual"
 
+instance Unit Show where
+  unit = name "unit"
+
 instance Lang Show where
   fix = name "fix"
   left = name "left"
   right = name "right"
   sumMatch = name "sumMatch"
-  unit = name "unit"
   exfalso = name "exfalso"
   ioRet = name "ioRet"
   ioBind = name "ioBind"
@@ -97,3 +100,5 @@
   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,8 +1,8 @@
-{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE NoImplicitPrelude, TypeFamilies #-}
 
 module DDF.Size where
 
-import DDF.Lang
+import DDF.DLang
 import qualified DDF.Map as Map
 
 newtype Size h x = Size {runSize :: Int}
@@ -14,6 +14,7 @@
   s (Size x) = (Size x)
   app (Size l) (Size r) = Size (l + r)
   abs (Size l) = Size (1 + l)
+  liftEnv (Size l) = Size l
 
 instance Bool Size where
   bool _ = one
@@ -61,12 +62,14 @@
 
 instance Bimap Size where
 
+instance Unit Size where
+  unit = one
+
 instance Lang Size where
   fix = one
   left = one
   right = one
   sumMatch = one
-  unit = one
   exfalso = one
   ioRet = one
   ioBind = one
@@ -81,3 +84,5 @@
   state = one
   runState = one
   putStrLn = one
+
+instance DLang Size where
diff --git a/DDF/UInt.hs b/DDF/UInt.hs
new file mode 100644
--- /dev/null
+++ b/DDF/UInt.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE NoImplicitPrelude, TypeFamilies #-}
+
+module DDF.UInt where
+
+import DDF.DLang
+import qualified DDF.Map as Map
+
+data UInt h x = UInt
+
+instance DBI UInt where
+  z = UInt
+  s _ = UInt
+  abs _ = UInt
+  app _ _ = UInt
+  liftEnv _ = UInt
+
+instance Bool UInt where
+  bool _ = UInt
+  ite = UInt
+
+instance Char UInt where
+  char _ = UInt
+
+instance Double UInt where
+  double _ = UInt
+  doublePlus = UInt
+  doubleMinus = UInt
+  doubleMult = UInt
+  doubleDivide = UInt
+  doubleExp = UInt
+
+instance Float UInt where
+  float _ = UInt
+  floatPlus = UInt
+  floatMinus = UInt
+  floatMult = UInt
+  floatDivide = UInt
+  floatExp = UInt
+
+instance Bimap UInt where
+
+instance Dual UInt where
+  dual = UInt
+  runDual = UInt
+
+instance Map.Map UInt where
+  empty = UInt
+  singleton = UInt
+  lookup = UInt
+  alter = UInt
+  mapMap = UInt
+
+instance Prod UInt where
+  mkProd = UInt
+  zro = UInt
+  fst = UInt
+
+instance Option UInt where
+  nothing = UInt
+  just = UInt
+  optionMatch = UInt
+
+instance Unit UInt where
+  unit = UInt
+
+instance Lang UInt where
+  fix = UInt
+  left = UInt
+  right = UInt
+  sumMatch = UInt
+  exfalso = UInt
+  ioRet = UInt
+  ioBind = UInt
+  ioMap = UInt
+  nil = UInt
+  cons = UInt
+  listMatch = 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,17 +1,16 @@
-{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE NoImplicitPrelude, TypeFamilies, TypeApplications, ScopedTypeVariables #-}
 
 module DDF.UnHOAS where
 
-import DDF.Lang
+import DDF.DLang
 import qualified DDF.Map as Map
 
-newtype UnHOAS repr h x = UnHOAS {runUnHOAS :: repr h x}
-
 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
@@ -59,13 +58,15 @@
   dual = UnHOAS dual
   runDual = UnHOAS runDual
 
+instance Unit r => Unit (UnHOAS r) where
+  unit = UnHOAS unit
+
 instance Lang r => Lang (UnHOAS r) where
   float2Double = UnHOAS float2Double
   fix = UnHOAS fix
   left = UnHOAS left
   right = UnHOAS right
   sumMatch = UnHOAS sumMatch
-  unit = UnHOAS unit
   exfalso = UnHOAS exfalso
   ioRet = UnHOAS ioRet
   ioBind = UnHOAS ioBind
@@ -79,3 +80,5 @@
   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
new file mode 100644
--- /dev/null
+++ b/DDF/UnLiftEnv.hs
@@ -0,0 +1,89 @@
+
+{-# LANGUAGE NoImplicitPrelude, NoMonomorphismRestriction #-}
+
+module DDF.UnLiftEnv where
+
+import DDF.DLang
+import qualified DDF.Map as Map
+
+newtype UnLiftEnv r h x = UnLiftEnv {runUnLiftEnv :: r () (h -> x)}
+
+unLiftEnv = UnLiftEnv . const1
+
+instance (Prod r, Unit 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
+  dual = unLiftEnv dual
+  runDual = unLiftEnv runDual
+
+instance (Prod r, Unit r, Float r) => Float (UnLiftEnv r) where
+  float = unLiftEnv . float
+  floatPlus = unLiftEnv floatPlus
+  floatMinus = unLiftEnv floatMinus
+  floatMult = unLiftEnv floatMult
+  floatDivide = unLiftEnv floatDivide
+  floatExp = unLiftEnv floatExp
+
+instance (Prod r, Unit 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
+
+instance (Prod r, Unit r, Char r) => Char (UnLiftEnv r) where
+  char = unLiftEnv . char
+
+instance (Prod r, Unit r, Bool r) => Bool (UnLiftEnv r) where
+  bool = unLiftEnv . bool
+  ite = unLiftEnv ite
+
+instance (Prod r, Unit r) => Prod (UnLiftEnv r) where
+  mkProd = unLiftEnv mkProd
+  zro = unLiftEnv zro
+  fst = unLiftEnv fst
+
+instance (Prod r, Unit r) => Unit (UnLiftEnv r) where
+  unit = unLiftEnv unit
+
+instance (Prod r, Unit 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
+  empty = unLiftEnv Map.empty
+  singleton = unLiftEnv Map.singleton
+  lookup = unLiftEnv Map.lookup
+  alter = unLiftEnv Map.alter
+  mapMap = unLiftEnv Map.mapMap
+
+instance (Unit r, Bimap r) => Bimap (UnLiftEnv r) where
+
+instance Lang r => Lang (UnLiftEnv r) where
+  fix = unLiftEnv fix
+  left = unLiftEnv left
+  right = unLiftEnv right
+  sumMatch = unLiftEnv sumMatch
+  exfalso = unLiftEnv exfalso
+  ioRet = unLiftEnv ioRet
+  ioBind = unLiftEnv ioBind
+  ioMap = unLiftEnv ioMap
+  nil = unLiftEnv nil
+  cons = unLiftEnv cons
+  listMatch = unLiftEnv listMatch
+  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
new file mode 100644
--- /dev/null
+++ b/DDF/Unit.hs
@@ -0,0 +1,6 @@
+module DDF.Unit (module DDF.DBI, module DDF.Unit) where
+
+import DDF.DBI
+
+class DBI r => Unit r where
+  unit :: r h ()
diff --git a/DDF/Util.hs b/DDF/Util.hs
--- a/DDF/Util.hs
+++ b/DDF/Util.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE TupleSections #-}
 
-module DDF.Util where
+module DDF.Util (module DDF.Util, module System.Random) where
 
 import System.Random
 import GHC.Float
diff --git a/DDF/Vector.hs b/DDF/Vector.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Vector.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE
+  NoImplicitPrelude,
+  DefaultSignatures,
+  MultiParamTypeClasses,
+  NoMonomorphismRestriction,
+  FlexibleContexts,
+  FlexibleInstances
+#-}
+
+module DDF.Vector where
+import DDF.Double
+import qualified Prelude as M
+
+class Monoid r g => Group r g where
+  invert :: r h (g -> g)
+  minus :: r h (g -> g -> g)
+  default invert :: DBI r => r h (g -> g)
+  invert = minus1 zero
+  default minus :: DBI r => r h (g -> g -> g)
+  minus = lam2 $ \x y -> plus2 x (invert1 y)
+  {-# MINIMAL (invert | minus) #-}
+
+class Group r v => Vector r v where
+  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)
+  default divide :: Double r => r h (v -> M.Double -> v)
+  divide = lam2 $ \x y -> mult2 (recip1 y) x
+  {-# MINIMAL (mult | divide) #-}
+
+minus2 = app2 minus
+mult1 = app mult
+mult2 = app2 mult
+divide2 = app2 divide
+invert1 = app invert
+minus1 = app minus
+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
diff --git a/DDF/WDiff.hs b/DDF/WDiff.hs
deleted file mode 100644
--- a/DDF/WDiff.hs
+++ /dev/null
@@ -1,105 +0,0 @@
-{-# LANGUAGE
-  NoImplicitPrelude,
-  ExplicitForAll,
-  InstanceSigs,
-  ScopedTypeVariables
-#-}
-
-module DDF.WDiff where
-
-import DDF.Lang
-import DDF.Diff
-import qualified Data.Map as M
-import qualified DDF.Map as Map
-
-newtype WDiff r v h x = WDiff {runWDiff :: r (Diff v h) (Diff v x)}
-
-instance DBI r => DBI (WDiff r v) where
-  z = WDiff z
-  s (WDiff x) = WDiff $ s x
-  abs (WDiff f) = WDiff $ abs f
-  app (WDiff f) (WDiff x) = WDiff $ app f x
-  hoas f = WDiff $ hoas (\x -> runWDiff $ f $ WDiff x)
-
-instance Bool r => Bool (WDiff r v) where
-  bool x = WDiff $ bool x
-  ite = WDiff ite
-
-instance Char r => Char (WDiff r v) where
-  char = WDiff . char
-
-instance Prod r => Prod (WDiff r v) where
-  mkProd = WDiff mkProd
-  zro = WDiff zro
-  fst = WDiff fst
-
-instance Dual r => Dual (WDiff r v) where
-  dual = WDiff $ dual
-  runDual = WDiff $ runDual
-
-instance (Vector r v, Double r, Dual r) => Double (WDiff r v) where
-  double x = WDiff $ mkDual2 (double x) zero
-  doublePlus = WDiff $ lam2 $ \l r ->
-    mkDual2 (plus2 (dualOrig1 l) (dualOrig1 r)) (plus2 (dualDiff1 l) (dualDiff1 r))
-  doubleMinus = WDiff $ lam2 $ \l r ->
-    mkDual2 (minus2 (dualOrig1 l) (dualOrig1 r)) (minus2 (dualDiff1 l) (dualDiff1 r))
-  doubleMult = WDiff $ lam2 $ \l r ->
-    mkDual2 (mult2 (dualOrig1 l) (dualOrig1 r))
-      (plus2 (mult2 (dualOrig1 l) (dualDiff1 r)) (mult2 (dualOrig1 r) (dualDiff1 l)))
-  doubleDivide = WDiff $ lam2 $ \l r ->
-    mkDual2 (divide2 (dualOrig1 l) (dualOrig1 r))
-      (divide2 (minus2 (mult2 (dualOrig1 r) (dualDiff1 l)) (mult2 (dualOrig1 l) (dualDiff1 r)))
-        (mult2 (dualOrig1 r) (dualOrig1 r)))
-  doubleExp = WDiff $ lam $ \x -> let_2 (doubleExp1 (dualOrig1 x)) (lam $ \e -> mkDual2 e (mult2 e (dualDiff1 x)))
-
-instance (Vector r v, Lang r) => Float (WDiff r v) where
-  float x = WDiff $ mkDual2 (float x) zero
-  floatPlus = WDiff $ lam2 $ \l r ->
-    mkDual2 (plus2 (dualOrig1 l) (dualOrig1 r)) (plus2 (dualDiff1 l) (dualDiff1 r))
-  floatMinus = WDiff $ lam2 $ \l r ->
-    mkDual2 (minus2 (dualOrig1 l) (dualOrig1 r)) (minus2 (dualDiff1 l) (dualDiff1 r))
-  floatMult = WDiff $ lam2 $ \l r ->
-    mkDual2 (mult2 (float2Double1 (dualOrig1 l)) (dualOrig1 r))
-      (plus2 (mult2 (float2Double1 (dualOrig1 l)) (dualDiff1 r)) (mult2 (float2Double1 (dualOrig1 r)) (dualDiff1 l)))
-  floatDivide = WDiff $ lam2 $ \l r ->
-    mkDual2 (divide2 (dualOrig1 l) (float2Double1 (dualOrig1 r)))
-      (divide2 (minus2 (mult2 (float2Double1 (dualOrig1 r)) (dualDiff1 l)) (mult2 (float2Double1 (dualOrig1 l)) (dualDiff1 r)))
-        (float2Double1 (mult2 (float2Double1 (dualOrig1 r)) (dualOrig1 r))))
-  floatExp = WDiff (lam $ \x -> let_2 (floatExp1 (dualOrig1 x)) (lam $ \e -> mkDual2 e (mult2 (float2Double1 e) (dualDiff1 x))))
-
-instance Option r => Option (WDiff r v) where
-  nothing = WDiff nothing
-  just = WDiff just
-  optionMatch = WDiff optionMatch
-
-instance Map.Map r => Map.Map (WDiff r v) where
-  empty = WDiff Map.empty
-  singleton = WDiff Map.singleton
-  lookup :: forall h k a. Map.Ord k => WDiff r v h (k -> M.Map k a -> Maybe a)
-  lookup = withDict (Map.diffOrd (Proxy :: Proxy (v, k))) (WDiff Map.lookup)
-  alter :: forall h k a. Map.Ord k => WDiff r v h ((Maybe a -> Maybe a) -> k -> M.Map k a -> M.Map k a)
-  alter = withDict (Map.diffOrd (Proxy :: Proxy (v, k))) (WDiff Map.alter)
-  mapMap = WDiff Map.mapMap
-
-instance Bimap r => Bimap (WDiff r v) where
-
-instance (Vector r v, Lang r) => Lang (WDiff r v) where
-  fix = WDiff fix
-  left = WDiff left
-  right = WDiff right
-  sumMatch = WDiff sumMatch
-  unit = WDiff unit
-  exfalso = WDiff exfalso
-  ioRet = WDiff ioRet
-  ioBind = WDiff ioBind
-  nil = WDiff nil
-  cons = WDiff cons
-  listMatch = WDiff listMatch
-  ioMap = WDiff ioMap
-  writer = WDiff writer
-  runWriter = WDiff runWriter
-  float2Double = WDiff $ bimap2 float2Double id
-  double2Float = WDiff $ bimap2 double2Float id
-  state = WDiff state
-  runState = WDiff runState
-  putStrLn = WDiff putStrLn
diff --git a/DDF/WithDiff.hs b/DDF/WithDiff.hs
--- a/DDF/WithDiff.hs
+++ b/DDF/WithDiff.hs
@@ -7,27 +7,26 @@
 
 module DDF.WithDiff where
 
-import DDF.Lang
-import DDF.Diff
+import DDF.DLang
 import qualified Prelude as M
 
 class Monoid r w => WithDiff r w where
-  withDiff :: r h ((w -> x) -> w -> Diff x w)
+  withDiff :: r h ((w -> x) -> w -> DiffType x w)
 
 withDiff1 = app withDiff
-selfWithDiff :: (DBI r, WithDiff r w) => r h (w -> Diff w w)
+selfWithDiff :: (DBI r, WithDiff r w) => r h (w -> DiffType w w)
 selfWithDiff = withDiff1 id
 
-instance Lang repr => ProdCon (WithDiff repr) l r where prodCon = Sub Dict
+instance DLang repr => ProdCon (WithDiff repr) l r where prodCon = Sub Dict
 
-instance Lang r => WithDiff r () where
+instance DLang r => WithDiff r () where
   withDiff = const1 id
 
-instance Lang r => WithDiff r M.Double where
+instance DLang r => WithDiff r M.Double where
   withDiff = lam2 $ \con d -> dual1 $ mkProd2 d (app con doubleOne)
 
-instance Lang r => WithDiff r M.Float where
+instance DLang r => WithDiff r M.Float where
   withDiff = lam2 $ \con d -> dual1 $ mkProd2 d (app con floatOne)
 
-instance (Lang repr, WithDiff repr l, WithDiff repr r) => WithDiff repr (l, r) where
+instance (DLang 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,3 +1,4 @@
+
 > {-# LANGUAGE ScopedTypeVariables, NoMonomorphismRestriction, TypeApplications, RankNTypes #-}
 
 This is the classical example of using sigmoid NN to approximate Xor.
@@ -12,9 +13,9 @@
 > import DDF.Util
 > import DDF.Lang
 > import DDF.Show
-> import DDF.Combine
-> import DDF.Eval
-> import DDF.GWDiff
+> import DDF.Combine ()
+> import DDF.Eval ()
+> import DDF.GDiff ()
 > import DDF.ImpW
 > import DDF.WithDiff
 > import qualified DDF.Meta.Dual as M
@@ -94,7 +95,7 @@
 
 > findXor :: forall g m. (RandomGen g, M.Monad m) => g -> (AST -> 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 (GWDiff Eval)) () (w -> XOR)) -> do
+>   RunImpW ((Combine (Show xorS) (Combine (Eval xorEv) xorE)) :: Weight w => Combine Show (Combine Eval (GDiff Eval)) () (w -> XOR)) -> do
 >     doAST $ xorS vars 0
 
 printing weights. now you will see a list of gibberish
@@ -106,9 +107,9 @@
 >     (go (diff xorE) initWeight (runEval selfWithDiff () \\ weightCon @w @(WithDiff Eval)) (diff loss)
 >         ((runEval (lam3 $ \d o n -> minus2 o (mult2 d n)) ()) \\ weightCon @w @(Vector Eval)) 0 (xorEv ())) \\ weightCon @w @M.Show
 >     where
->       diff :: GWDiff Eval () x -> Diff w x
->       diff x = (runEval (runGWDiff x (Proxy :: Proxy w)) ()) \\ weightCon @w @(Vector Eval)
->       go :: M.Show w => (Diff w (w -> XOR)) -> w -> (w -> Diff w w) -> (Diff w (XOR -> M.Double)) -> (M.Double -> w -> w -> w) -> Int -> (w -> XOR) -> m XOR
+>       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
 >         doIter i lossVal (M.show weight)
 >         go xor (update 0.3 weight lossDiff) reifyE lossE update (1 + i) orig
diff --git a/DeepDarkFantasy.cabal b/DeepDarkFantasy.cabal
--- a/DeepDarkFantasy.cabal
+++ b/DeepDarkFantasy.cabal
@@ -1,5 +1,5 @@
 name: DeepDarkFantasy
-version: 0.2017.4.9
+version: 0.2017.4.19
 cabal-version: 1.12
 build-type: Simple
 license: Apache
@@ -22,24 +22,33 @@
     DDF.Combine
     DDF.DBI
     DDF.Diff
+    DDF.DLang
     DDF.Double
     DDF.Dual
     DDF.Eval
     DDF.Float
-    DDF.GWDiff
+    DDF.GDiff
+    DDF.GInfDiff
     DDF.ImportMeta
     DDF.ImpW
+    DDF.InfDiff
     DDF.Lang
     DDF.Map
+    DDF.Meta.Interpreter
+    DDF.Meta.Diff
     DDF.Meta.Dual
     DDF.Option
     DDF.Poly
     DDF.Prod
+    DDF.RTInfDiff
     DDF.Show
     DDF.Size
+    DDF.UInt
     DDF.UnHOAS
+    DDF.Unit
+    DDF.UnLiftEnv
     DDF.Util
-    DDF.WDiff
+    DDF.Vector
     DDF.WithDiff
     DDF.Xor
   build-depends: