diff --git a/DDF/Char.hs b/DDF/Char.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Char.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+module DDF.Char (module DDF.Char, module DDF.DBI) where
+
+import DDF.DBI
+import qualified Prelude as M
+
+class DBI r => Char r where
+  char :: M.Char -> r h M.Char
diff --git a/DDF/Combine.hs b/DDF/Combine.hs
--- a/DDF/Combine.hs
+++ b/DDF/Combine.hs
@@ -3,7 +3,6 @@
 module DDF.Combine where
 
 import DDF.Lang
-import DDF.ImportMeta
 
 data Combine l r h x = Combine (l h x) (r h x)
 
@@ -12,37 +11,59 @@
   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 r -> l) (hoas $ \x -> case f (Combine z x) of Combine l r -> 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)
 
 instance (Bool l, Bool r) => Bool (Combine l r) where
   bool x = Combine (bool x) (bool x)
   ite = Combine ite ite
 
-instance (Lang l, Lang r) => Lang (Combine l r) where
+instance (Char l, Char r) => Char (Combine l r) where
+  char x = Combine (char x) (char x)
+
+instance (Prod l, Prod r) => Prod (Combine l r) where
   mkProd = Combine mkProd mkProd
   zro = Combine zro zro
   fst = Combine fst fst
+
+instance (Double l, Double r) => Double (Combine l r) where
   double x = Combine (double x) (double x)
   doublePlus = Combine doublePlus doublePlus
   doubleMinus = Combine doubleMinus doubleMinus
   doubleMult = Combine doubleMult doubleMult
   doubleDivide = Combine doubleDivide doubleDivide
   doubleExp = Combine doubleExp doubleExp
+
+instance (Float l, Float r) => Float (Combine l r) where
   float x = Combine (float x) (float x)
   floatPlus = Combine floatPlus floatPlus
   floatMinus = Combine floatMinus floatMinus
   floatMult = Combine floatMult floatMult
   floatDivide = Combine floatDivide floatDivide
   floatExp = Combine floatExp floatExp
+
+instance (Option l, Option r) => Option (Combine l r) where
+  nothing = Combine nothing nothing
+  just = Combine just just
+  optionMatch = Combine optionMatch optionMatch
+
+instance (Map l, Map r) => Map (Combine l r) where
+  empty = Combine empty empty
+  lookup = Combine lookup lookup
+  singleton = Combine singleton singleton
+  alter = Combine alter alter
+  mapMap = Combine mapMap mapMap
+
+instance (Dual l, Dual r) => Dual (Combine l r) where
+  dual = Combine dual dual
+  runDual = Combine runDual runDual
+
+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
-  nothing = Combine nothing nothing
-  just = Combine just just
-  optionMatch = Combine optionMatch optionMatch
   ioRet = Combine ioRet ioRet
   ioBind = Combine ioBind ioBind
   ioMap = Combine ioMap ioMap
@@ -55,3 +76,4 @@
   float2Double = Combine float2Double float2Double
   state = Combine state state
   runState = Combine runState runState
+  putStrLn = Combine putStrLn putStrLn
diff --git a/DDF/DBI.hs b/DDF/DBI.hs
--- a/DDF/DBI.hs
+++ b/DDF/DBI.hs
@@ -1,30 +1,29 @@
 {-# LANGUAGE
-    MultiParamTypeClasses,
-    RankNTypes,
-    ScopedTypeVariables,
-    FlexibleInstances,
-    FlexibleContexts,
-    UndecidableInstances,
-    PolyKinds,
-    LambdaCase,
-    NoMonomorphismRestriction,
-    TypeFamilies,
-    LiberalTypeSynonyms,
-    FunctionalDependencies,
-    ExistentialQuantification,
-    InstanceSigs,
-    ConstraintKinds,
-    DefaultSignatures,
-    TypeOperators,
-    TypeApplications,
-    PartialTypeSignatures #-}
+  MultiParamTypeClasses,
+  RankNTypes,
+  ScopedTypeVariables,
+  FlexibleInstances,
+  FlexibleContexts,
+  UndecidableInstances,
+  PolyKinds,
+  LambdaCase,
+  NoMonomorphismRestriction,
+  TypeFamilies,
+  LiberalTypeSynonyms,
+  FunctionalDependencies,
+  ExistentialQuantification,
+  InstanceSigs,
+  ConstraintKinds,
+  DefaultSignatures,
+  TypeOperators,
+  TypeApplications,
+  PartialTypeSignatures
+#-}
 
 module DDF.DBI (module DDF.DBI, module DDF.ImportMeta) where
 import qualified Prelude as P
 import DDF.Util
-import Control.Monad (when)
 import System.Random
-import Data.Proxy
 import Data.Constraint
 import Data.Constraint.Forall
 import DDF.ImportMeta
@@ -33,26 +32,6 @@
   zero :: r h m
   plus :: r h (m -> m -> m)
 
-class Monoid repr w => WithDiff repr w where
-  withDiff :: repr h ((w -> x) -> w -> Diff x w)
-
-class DBI repr => ConvDiff repr w where
-  toDiff :: forall h x. Monoid repr x => Proxy x -> repr h (w -> Diff x w)
-  toDiff _ = toDiffBy1 @repr @w @x zero
-  toDiffBy :: forall h x. repr h (x -> w -> Diff x w)
-  fromDiff :: forall h x. Monoid repr x => Proxy x -> repr h (Diff x w -> w)
-  fromDiff _ = fromDiffBy1 @repr @w @x zero
-  fromDiffBy :: repr h (x -> Diff x w -> w)
-
-withDiff1 = app withDiff
-toDiffBy1 :: forall repr w x h. ConvDiff repr w => repr h x -> repr h (w -> Diff x w)
-toDiffBy1 = app toDiffBy
-fromDiffBy1 :: forall repr w x h. ConvDiff repr w => repr h x -> repr h (Diff x w -> w)
-fromDiffBy1 = app fromDiffBy
-
-selfWithDiff :: (DBI repr, WithDiff repr w) => repr h (w -> Diff w w)
-selfWithDiff = withDiff1 id
-
 class DBI (repr :: * -> * -> *) where
   z :: repr (a, h) a
   s :: repr h b -> repr (a, h) b
@@ -88,7 +67,7 @@
 let_2 = app2 let_
 
 class Functor r f where
-  map :: r h ((a -> b) -> (f a -> f b))
+  map ::  r h ((a -> b) -> (f a -> f b))
 
 class Functor r a => Applicative r a where
   pure :: r h (x -> a x)
@@ -104,7 +83,7 @@
 class BiFunctor r p where
   bimap :: r h ((a -> b) -> (c -> d) -> p a c -> p b d)
 
-app3 f x y z = app (app2 f x y) z
+app3 f a b c = app (app2 f a b) c
 com2 = app2 com
 
 class NT repr l r where
@@ -130,26 +109,12 @@
   ((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 $ \x y -> lam $ \z -> f x y z
-
-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
-
-newtype WDiff repr v h x = WDiff {runWDiff :: repr (Diff v h) (Diff v x)}
+lam3 f = lam2 $ \a b -> lam $ \c -> f a b c
 
 app2 f a = app (app f a)
 
 plus2 = app2 plus
 
-instance DBI repr => DBI (WDiff repr 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 (runWDiff . f . WDiff)
-
 noEnv :: repr () x -> repr () x
 noEnv = P.id
 
@@ -171,15 +136,4 @@
 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
-
-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
+  weightCon :: (con (), con P.Float, con P.Double, ForallV (ProdCon con)) :- con w
diff --git a/DDF/Diff.hs b/DDF/Diff.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Diff.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE
+  NoImplicitPrelude,
+  RankNTypes,
+  ScopedTypeVariables,
+  TypeApplications,
+  TypeFamilies,
+  KindSignatures,
+  MultiParamTypeClasses,
+  FlexibleInstances,
+  NoMonomorphismRestriction
+#-}
+
+module DDF.Diff where
+
+import DDF.ImportMeta
+import DDF.Meta.Dual
+import Prelude
+import Data.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)
diff --git a/DDF/Double.hs b/DDF/Double.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Double.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module DDF.Double (module DDF.Double, module DDF.DBI) where
+
+import DDF.DBI
+import qualified Prelude as M
+
+class DBI r => Double r where
+  double :: M.Double -> r h M.Double
+  doubleZero :: r h M.Double
+  doubleZero = double 0
+  doubleOne :: r h M.Double
+  doubleOne = double 1
+  doublePlus :: r h (M.Double -> M.Double -> M.Double)
+  doubleMinus :: r h (M.Double -> M.Double -> M.Double)
+  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)
diff --git a/DDF/Dual.hs b/DDF/Dual.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Dual.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE
+  NoImplicitPrelude,
+  NoMonomorphismRestriction
+#-}
+
+module DDF.Dual (module DDF.Dual, module DDF.Prod) where
+
+import DDF.Prod
+import qualified DDF.Meta.Dual as M
+
+class Prod r => Dual r where
+  dual :: r h ((x, y) -> M.Dual x y)
+  runDual :: r h (M.Dual x y -> (x, y))
+  mkDual :: r h (x -> y -> M.Dual x y)
+  mkDual = curry1 dual
+  dualOrig :: r h (M.Dual x y -> x)
+  dualOrig = zro `com2` runDual
+  dualDiff :: r h (M.Dual x y -> y)
+  dualDiff = fst `com2` runDual
+
+dual1 = app dual
+mkDual2 = app2 mkDual
+dualOrig1 = app dualOrig
+dualDiff1 = app dualDiff
diff --git a/DDF/Eval.hs b/DDF/Eval.hs
--- a/DDF/Eval.hs
+++ b/DDF/Eval.hs
@@ -1,3 +1,4 @@
+
 {-# LANGUAGE NoImplicitPrelude,
   LambdaCase #-}
 
@@ -6,11 +7,13 @@
 import DDF.ImportMeta
 import DDF.Lang
 import qualified Prelude as M
-import qualified Control.Monad.Writer as M
+import qualified Control.Monad.Writer as M (WriterT(WriterT), runWriter)
 import qualified Control.Monad.State as M
 import qualified GHC.Float as M
 import qualified Data.Functor.Identity as M
 import qualified Data.Bool as M
+import qualified Data.Map as M.Map
+import qualified DDF.Meta.Dual as M
 
 newtype Eval h x = Eval {runEval :: h -> x}
 
@@ -26,15 +29,49 @@
   bool = comb
   ite = comb M.bool
 
-instance Lang Eval where
+instance Char Eval where
+  char = comb
+
+instance Prod Eval where
+  mkProd = comb (,)
   zro = comb M.fst
   fst = comb M.snd
-  mkProd = comb (,)
+
+instance Double Eval where
   double = comb
   doublePlus = comb (+)
   doubleMinus = comb (-)
   doubleMult = comb (*)
   doubleDivide = comb (/)
+  doubleExp = comb M.exp
+
+instance Float Eval where
+  float = comb
+  floatPlus = comb (+)
+  floatMinus = comb (-)
+  floatMult = comb (*)
+  floatDivide = comb (/)
+  floatExp = comb M.exp
+
+instance Option Eval where
+  nothing = comb M.Nothing
+  just = comb M.Just
+  optionMatch = comb $ \l r -> \case
+                              M.Nothing -> l
+                              M.Just x -> r x
+
+instance Map Eval where
+  empty = comb M.Map.empty
+  singleton = comb M.Map.singleton
+  lookup = comb M.Map.lookup
+  alter = comb M.Map.alter
+  mapMap = comb M.fmap
+
+instance Dual Eval where
+  dual = comb M.Dual
+  runDual = comb M.runDual
+
+instance Lang Eval where
   fix = comb loop
     where loop x = x $ loop x
   left = comb M.Left
@@ -44,8 +81,6 @@
                              M.Right x -> r x
   unit = comb ()
   exfalso = comb absurd
-  nothing = comb M.Nothing
-  just = comb M.Just
   ioRet = comb M.return
   ioBind = comb (>>=)
   nil = comb []
@@ -53,20 +88,11 @@
   listMatch = comb $ \l r -> \case
                             [] -> l
                             x:xs -> r x xs
-  optionMatch = comb $ \l r -> \case
-                              M.Nothing -> l
-                              M.Just x -> r x
   ioMap = comb M.fmap
   writer = comb (M.WriterT . M.Identity)
   runWriter = comb M.runWriter
-  doubleExp = comb M.exp
-  float = comb
-  floatPlus = comb (+)
-  floatMinus = comb (-)
-  floatMult = comb (*)
-  floatDivide = comb (/)
-  floatExp = comb M.exp
   float2Double = comb M.float2Double
   double2Float = comb M.double2Float
   state = comb M.state
   runState = comb M.runState
+  putStrLn = comb M.putStrLn
diff --git a/DDF/Float.hs b/DDF/Float.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Float.hs
@@ -0,0 +1,16 @@
+module DDF.Float (module DDF.Float, module DDF.DBI) where
+
+import DDF.DBI
+import qualified GHC.Float as M
+
+class DBI r => Float r where
+  float :: M.Float -> r h M.Float
+  floatZero :: r h M.Float
+  floatZero = float 0
+  floatOne :: r h M.Float
+  floatOne = float 1
+  floatPlus :: r h (M.Float -> M.Float -> M.Float)
+  floatMinus :: r h (M.Float -> M.Float -> M.Float)
+  floatMult :: r h (M.Float -> M.Float -> M.Float)
+  floatDivide :: r h (M.Float -> M.Float -> M.Float)
+  floatExp :: r h (M.Float -> M.Float)
diff --git a/DDF/GWDiff.hs b/DDF/GWDiff.hs
--- a/DDF/GWDiff.hs
+++ b/DDF/GWDiff.hs
@@ -1,13 +1,19 @@
-{-# LANGUAGE NoImplicitPrelude, RankNTypes #-}
+{-# LANGUAGE
+  NoImplicitPrelude,
+  RankNTypes,
+  InstanceSigs,
+  ScopedTypeVariables
+#-}
 
-module DDF.GWDiff where
+module DDF.GWDiff (module DDF.GWDiff, module DDF.Diff) where
 import DDF.Lang
 import qualified Prelude as M
-import Data.Proxy
+import DDF.Diff
+import qualified Data.Map as M
 
-newtype GWDiff repr h x = GWDiff {runGWDiff :: forall v. Vector repr v => Proxy v -> repr (Diff v h) (Diff v x)}
+newtype GWDiff r h x = GWDiff {runGWDiff :: forall v. Vector r v => Proxy v -> r (Diff v h) (Diff v x)}
 
-instance DBI repr => DBI (GWDiff repr) where
+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))
@@ -17,54 +23,79 @@
   bool x = GWDiff $ M.const $ bool x
   ite = GWDiff $ M.const ite
 
-instance Lang repr => Lang (GWDiff repr) where
+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
-  double x = GWDiff $ M.const $ mkProd2 (double x) zero
+
+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 ->
-    mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))
+    mkDual2 (plus2 (dualOrig1 l) (dualOrig1 r)) (plus2 (dualDiff1 l) (dualDiff1 r))
   doubleMinus = GWDiff $ M.const $ lam2 $ \l r ->
-    mkProd2 (minus2 (zro1 l) (zro1 r)) (minus2 (fst1 l) (fst1 r))
+    mkDual2 (minus2 (dualOrig1 l) (dualOrig1 r)) (minus2 (dualDiff1 l) (dualDiff1 r))
   doubleMult = GWDiff $ M.const $ lam2 $ \l r ->
-    mkProd2 (mult2 (zro1 l) (zro1 r))
-      (plus2 (mult2 (zro1 l) (fst1 r)) (mult2 (zro1 r) (fst1 l)))
+    mkDual2 (mult2 (dualOrig1 l) (dualOrig1 r))
+      (plus2 (mult2 (dualOrig1 l) (dualDiff1 r)) (mult2 (dualOrig1 r) (dualDiff1 l)))
   doubleDivide = GWDiff $ M.const $ lam2 $ \l r ->
-    mkProd2 (divide2 (zro1 l) (zro1 r))
-      (divide2 (minus2 (mult2 (zro1 r) (fst1 l)) (mult2 (zro1 l) (fst1 r)))
-        (mult2 (zro1 r) (zro1 r)))
-  doubleExp = GWDiff $ M.const $ lam $ \x -> mkProd2 (doubleExp1 (zro1 x)) (mult2 (doubleExp1 (zro1 x)) (fst1 x))
+    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 r => Map (GWDiff r) where
+  empty = GWDiff $ M.const empty
+  singleton = GWDiff $ M.const singleton
+  lookup :: forall h k a. Ord k => GWDiff r h (k -> M.Map k a -> Maybe a)
+  lookup = GWDiff $ \(_ :: Proxy v) -> withDict (diffOrd (Proxy :: Proxy (v, k))) lookup
+  alter :: forall h k a. Ord k => GWDiff r h ((Maybe a -> Maybe a) -> k -> M.Map k a -> M.Map k a)
+  alter = GWDiff $ \(_ :: Proxy v) -> withDict (diffOrd (Proxy :: Proxy (v, k))) alter
+  mapMap = GWDiff $ M.const mapMap
+
+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
-  nothing = GWDiff $ M.const nothing
-  just = GWDiff $ M.const just
   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
-  optionMatch = GWDiff $ M.const optionMatch
   ioMap = GWDiff $ M.const ioMap
   writer = GWDiff $ M.const writer
   runWriter = GWDiff $ M.const runWriter
-  float x = GWDiff $ M.const $ mkProd2 (float x) zero
-  floatPlus = GWDiff $ M.const $ lam2 $ \l r ->
-    mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))
-  floatMinus = GWDiff $ M.const $ lam2 $ \l r ->
-    mkProd2 (minus2 (zro1 l) (zro1 r)) (minus2 (fst1 l) (fst1 r))
-  floatMult = GWDiff $ M.const $ lam2 $ \l r ->
-    mkProd2 (mult2 (float2Double1 (zro1 l)) (zro1 r))
-      (plus2 (mult2 (float2Double1 (zro1 l)) (fst1 r)) (mult2 (float2Double1 (zro1 r)) (fst1 l)))
-  floatDivide = GWDiff $ M.const $ lam2 $ \l r ->
-    mkProd2 (divide2 (zro1 l) (float2Double1 (zro1 r)))
-      (divide2 (minus2 (mult2 (float2Double1 (zro1 r)) (fst1 l)) (mult2 (float2Double1 (zro1 l)) (fst1 r)))
-        (float2Double1 (mult2 (float2Double1 (zro1 r)) (zro1 r))))
-  floatExp = GWDiff $ M.const $ lam $ \x -> mkProd2 (floatExp1 (zro1 x)) (mult2 (float2Double1 (floatExp1 (zro1 x))) (fst1 x))
   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
new file mode 100644
--- /dev/null
+++ b/DDF/ImpW.hs
@@ -0,0 +1,97 @@
+{-# LANGUAGE NoImplicitPrelude, RankNTypes, InstanceSigs, ScopedTypeVariables, ExistentialQuantification #-}
+
+module DDF.ImpW where
+
+import DDF.Lang
+
+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 (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
+
+instance Prod r => DBI (ImpW r) where
+  z = NoImpW z
+  s :: forall a h b. ImpW r h b -> ImpW r (a, h) b
+  s (ImpW w) = ImpW (s w)
+  s (NoImpW x) = NoImpW (s x)
+  app (ImpW f) (ImpW x) = ImpW (lam $ \p -> app (app (conv f) (zro1 p)) (app (conv x) (fst1 p)))
+  app (NoImpW f) (NoImpW x) = NoImpW (app f x)
+  app (ImpW f) (NoImpW x) = ImpW (lam $ \w -> app2 (conv f) w (conv x))
+  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)
+
+instance (Prod r, Bool r) => Bool (ImpW r) where
+  bool = NoImpW . bool
+  ite = NoImpW ite
+
+instance (Prod r, Char r) => Char (ImpW r) where
+  char = NoImpW . char
+
+instance Prod r => Prod (ImpW r) where
+  mkProd = NoImpW mkProd
+  zro = NoImpW zro
+  fst = NoImpW fst
+  
+instance (Prod r, Double r) => Double (ImpW r) where
+  double = NoImpW . double
+  doubleExp = NoImpW doubleExp
+  doublePlus = NoImpW doublePlus
+  doubleMinus = NoImpW doubleMinus
+  doubleMult = NoImpW doubleMult
+  doubleDivide = NoImpW doubleDivide
+
+instance (Prod r, Float r) => Float (ImpW r) where
+  float = NoImpW . float
+  floatExp = NoImpW floatExp
+  floatPlus = NoImpW floatPlus
+  floatMinus = NoImpW floatMinus
+  floatMult = NoImpW floatMult
+  floatDivide = NoImpW floatDivide
+
+instance (Prod r, Option r) => Option (ImpW r) where
+  nothing = NoImpW nothing
+  just = NoImpW just
+  optionMatch = NoImpW optionMatch
+
+instance Map r => Map (ImpW r) where
+  empty = NoImpW empty
+  singleton = NoImpW singleton
+  lookup = NoImpW lookup
+  alter = NoImpW alter
+  mapMap = NoImpW mapMap
+
+instance Dual r => Dual (ImpW r) where
+  dual = NoImpW dual
+  runDual = NoImpW runDual
+
+instance Lang r => Lang (ImpW r) where
+  nil = NoImpW nil
+  cons = NoImpW cons
+  listMatch = NoImpW listMatch
+  ioRet = NoImpW ioRet
+  ioMap = NoImpW ioMap
+  ioBind = NoImpW ioBind
+  unit = NoImpW unit
+  exfalso = NoImpW exfalso
+  fix = NoImpW fix
+  left = NoImpW left
+  right = NoImpW right
+  sumMatch = NoImpW sumMatch
+  writer = NoImpW writer
+  runWriter = NoImpW runWriter
+  float2Double = NoImpW float2Double
+  double2Float = NoImpW double2Float
+  state = NoImpW state
+  runState = NoImpW runState
+  putStrLn = NoImpW putStrLn
diff --git a/DDF/ImportMeta.hs b/DDF/ImportMeta.hs
--- a/DDF/ImportMeta.hs
+++ b/DDF/ImportMeta.hs
@@ -1,6 +1,10 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module DDF.ImportMeta (module Prelude, module Data.Void) where
+module DDF.ImportMeta (module Prelude, module Data.Void, module Control.Monad.Writer, module Control.Monad.State, module Data.Constraint, module Data.Proxy) where
 
-import Prelude (($), show, (+), (-), (*), (/), (.), (++), (>>=), Double, IO, Int, (<=), print)
-import Data.Void (absurd)
+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.Proxy
diff --git a/DDF/Lang.hs b/DDF/Lang.hs
--- a/DDF/Lang.hs
+++ b/DDF/Lang.hs
@@ -18,267 +18,81 @@
     DefaultSignatures,
     TypeOperators,
     TypeApplications,
-    PartialTypeSignatures #-}
+    PartialTypeSignatures,
+    NoImplicitPrelude #-}
 
-module DDF.Lang (module DDF.Lang, module DDF.Bool) where
-import DDF.DBI
-import qualified Prelude as P
-import Prelude (($), (.), (+), (-), (++), show, (>>=), (*), (/), Double, Either, IO, Maybe)
-import qualified Control.Monad.Writer as P
-import Control.Monad.Writer (Writer, WriterT)
-import qualified Control.Monad.State as P
-import Control.Monad.State (State)
-import qualified GHC.Float as P
-import GHC.Float (Float)
-import qualified Data.Tuple as P
-import Data.Void
-import Data.Proxy
-import Data.Proxy
-import Data.Constraint
-import Data.Constraint.Forall
-import qualified Data.Bool as P
+module DDF.Lang (module DDF.Lang, module DDF.Bool, module DDF.Char, module DDF.Double, module DDF.Float, module DDF.Map, module DDF.Dual) where
 import DDF.Bool
+import DDF.Char
+import DDF.Double
+import DDF.Float
+import DDF.Map
+import DDF.Dual
 
-type instance Diff v Void = Void
-type instance Diff v P.Double = (P.Double, v)
-type instance Diff v P.Float = (P.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 P.Bool = P.Bool
+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
 
-class Bool repr => Lang repr where
-  mkProd :: repr h (a -> b -> (a, b))
-  zro :: repr h ((a, b) -> a)
-  fst :: repr h ((a, b) -> b)
-  double :: P.Double -> repr h P.Double
-  doubleZero :: repr h P.Double
-  doubleZero = double 0
-  doubleOne :: repr h P.Double
-  doubleOne = double 1
-  doublePlus :: repr h (P.Double -> P.Double -> P.Double)
-  doubleMinus :: repr h (P.Double -> P.Double -> P.Double)
-  doubleMult :: repr h (P.Double -> P.Double -> P.Double)
-  doubleDivide :: repr h (P.Double -> P.Double -> P.Double)
-  doubleExp :: repr h (P.Double -> P.Double)
-  float :: P.Float -> repr h P.Float
-  floatZero :: repr h P.Float
-  floatZero = float 0
-  floatOne :: repr h P.Float
-  floatOne = float 1
-  floatPlus :: repr h (P.Float -> P.Float -> P.Float)
-  floatMinus :: repr h (P.Float -> P.Float -> P.Float)
-  floatMult :: repr h (P.Float -> P.Float -> P.Float)
-  floatDivide :: repr h (P.Float -> P.Float -> P.Float)
-  floatExp :: repr h (P.Float -> P.Float)
-  fix :: repr h ((a -> a) -> a)
-  left :: repr h (a -> P.Either a b)
-  right :: repr h (b -> P.Either a b)
-  sumMatch :: repr h ((a -> c) -> (b -> c) -> P.Either a b -> c)
-  unit :: repr h ()
-  exfalso :: repr h (Void -> a)
-  nothing :: repr h (P.Maybe a)
-  just :: repr h (a -> P.Maybe a)
-  optionMatch :: repr h (b -> (a -> b) -> P.Maybe a -> b)
-  ioRet :: repr h (a -> P.IO a)
-  ioBind :: repr h (P.IO a -> (a -> P.IO b) -> P.IO b)
-  ioMap :: repr h ((a -> b) -> P.IO a -> P.IO b)
-  nil :: repr h [a]
-  cons :: repr h (a -> [a] -> [a])
-  listMatch :: repr h (b -> (a -> [a] -> b) -> [a] -> b)
-  listAppend :: repr h ([a] -> [a] -> [a])
+class (Bool r, Char r, Double r, Float r, Map r, Dual 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)
+  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 :: repr h ((a, w) -> P.Writer w a)
-  runWriter :: repr h (P.Writer w a -> (a, w))
-  swap :: repr h ((l, r) -> (r, l))
-  swap = lam $ \p -> mkProd2 (fst1 p) (zro1 p)
-  curry :: repr h (((a, b) -> c) -> (a -> b -> c))
-  uncurry :: repr h ((a -> b -> c) -> ((a, b) -> c))
-  curry = lam3 $ \f a b -> app f (mkProd2 a b)
-  uncurry = lam2 $ \f p -> app2 f (zro1 p) (fst1 p)
-  float2Double :: repr h (P.Float -> P.Double)
-  double2Float :: repr h (P.Double -> P.Float)
-  undefined :: repr h a
+  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 :: repr h ((l -> (r, l)) -> State l r)
-  runState :: repr h (State l r -> (l -> (r, l)))
-
-instance Lang repr => ConvDiff repr () where
-  toDiffBy = const1 id
-  fromDiffBy = const1 id
-
-instance Lang repr => ConvDiff repr Double where
-  toDiffBy = flip1 mkProd
-  fromDiffBy = const1 zro
-
-instance Lang repr => ConvDiff repr Float where
-  toDiffBy = flip1 mkProd
-  fromDiffBy = const1 zro
-
-instance (Lang repr, ConvDiff repr l, ConvDiff repr r) => ConvDiff repr (l, r) where
-  toDiffBy = lam $ \x -> bimap2 (toDiffBy1 x) (toDiffBy1 x)
-  fromDiffBy = lam $ \x -> bimap2 (fromDiffBy1 x) (fromDiffBy1 x)
-
-instance (Lang repr, ConvDiff repr l, ConvDiff repr r) => ConvDiff repr (Either l r) where
-  toDiffBy = lam $ \x -> bimap2 (toDiffBy1 x) (toDiffBy1 x)
-  fromDiffBy = lam $ \x -> bimap2 (fromDiffBy1 x) (fromDiffBy1 x)
-
-instance (Lang repr, ConvDiff repr l, ConvDiff repr r) => ConvDiff repr (l -> r) where
-  toDiffBy = lam2 $ \x f -> (toDiffBy1 x) `com2` f `com2` (fromDiffBy1 x)
-  fromDiffBy = lam2 $ \x f -> (fromDiffBy1 x) `com2` f `com2` (toDiffBy1 x)
-
-instance (Lang repr, ConvDiff repr l) => ConvDiff repr [l] where
-  toDiffBy = lam $ \x -> map1 (toDiffBy1 x)
-  fromDiffBy = lam $ \x -> map1 (fromDiffBy1 x)
+  state :: r h ((x -> (y, x)) -> State x y)
+  runState :: r h (State x y -> (x -> (y, x)))
+  putStrLn :: r h (String -> IO ())
 
-class Reify repr x where
-  reify :: x -> repr h x
+class Reify r x where
+  reify :: x -> r h x
 
-instance Lang repr => Reify repr () where
+instance Lang r => Reify r () where
   reify _ = unit
 
-instance Lang repr => Reify repr Double where
+instance Lang r => Reify r M.Double where
   reify = double
 
 instance (Lang repr, Reify repr l, Reify repr r) => Reify repr (l, r) where
   reify (l, r) = mkProd2 (reify l) (reify r)
 
-instance (Bool r, Vector r v) => Bool (WDiff r v) where
-  bool = WDiff . bool
-  ite = WDiff ite
-
-instance (Vector repr v, Lang repr) => Lang (WDiff repr v) where
-  mkProd = WDiff mkProd
-  zro = WDiff zro
-  fst = WDiff fst
-  double x = WDiff $ mkProd2 (double x) zero
-  doublePlus = WDiff $ lam2 $ \l r ->
-    mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))
-  doubleMinus = WDiff $ lam2 $ \l r ->
-    mkProd2 (minus2 (zro1 l) (zro1 r)) (minus2 (fst1 l) (fst1 r))
-  doubleMult = WDiff $ lam2 $ \l r ->
-    mkProd2 (mult2 (zro1 l) (zro1 r))
-      (plus2 (mult2 (zro1 l) (fst1 r)) (mult2 (zro1 r) (fst1 l)))
-  doubleDivide = WDiff $ lam2 $ \l r ->
-    mkProd2 (divide2 (zro1 l) (zro1 r))
-      (divide2 (minus2 (mult2 (zro1 r) (fst1 l)) (mult2 (zro1 l) (fst1 r)))
-        (mult2 (zro1 r) (zro1 r)))
-  doubleExp = WDiff $ lam $ \x -> mkProd2 (doubleExp1 (zro1 x)) (mult2 (doubleExp1 (zro1 x)) (fst1 x))
-  fix = WDiff fix
-  left = WDiff left
-  right = WDiff right
-  sumMatch = WDiff sumMatch
-  unit = WDiff unit
-  exfalso = WDiff exfalso
-  nothing = WDiff nothing
-  just = WDiff just
-  ioRet = WDiff ioRet
-  ioBind = WDiff ioBind
-  nil = WDiff nil
-  cons = WDiff cons
-  listMatch = WDiff listMatch
-  optionMatch = WDiff optionMatch
-  ioMap = WDiff ioMap
-  writer = WDiff writer
-  runWriter = WDiff runWriter
-  float x = WDiff $ mkProd2 (float x) zero
-  floatPlus = WDiff $ lam2 $ \l r ->
-    mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))
-  floatMinus = WDiff $ lam2 $ \l r ->
-    mkProd2 (minus2 (zro1 l) (zro1 r)) (minus2 (fst1 l) (fst1 r))
-  floatMult = WDiff $ lam2 $ \l r ->
-    mkProd2 (mult2 (float2Double1 (zro1 l)) (zro1 r))
-      (plus2 (mult2 (float2Double1 (zro1 l)) (fst1 r)) (mult2 (float2Double1 (zro1 r)) (fst1 l)))
-  floatDivide = WDiff $ lam2 $ \l r ->
-    mkProd2 (divide2 (zro1 l) (float2Double1 (zro1 r)))
-      (divide2 (minus2 (mult2 (float2Double1 (zro1 r)) (fst1 l)) (mult2 (float2Double1 (zro1 l)) (fst1 r)))
-        (float2Double1 (mult2 (float2Double1 (zro1 r)) (zro1 r))))
-  floatExp = WDiff $ lam $ \x -> mkProd2 (floatExp1 (zro1 x)) (mult2 (float2Double1 (floatExp1 (zro1 x))) (fst1 x))
-  float2Double = WDiff $ bimap2 float2Double id
-  double2Float = WDiff $ bimap2 double2Float id
-  state = WDiff state
-  runState = WDiff runState
-
 instance Lang repr => ProdCon (Monoid repr) l r where prodCon = Sub Dict
 
-instance Lang repr => ProdCon (WithDiff repr) l r where prodCon = Sub Dict
-
 instance Lang repr => ProdCon (Reify repr) l r where prodCon = Sub Dict
 
 instance Lang repr => ProdCon (Vector repr) l r where prodCon = Sub Dict
 
-instance Lang repr => Lang (ImpW repr) where
-  nil = NoImpW nil
-  cons = NoImpW cons
-  listMatch = NoImpW listMatch
-  zro = NoImpW zro
-  fst = NoImpW fst
-  mkProd = NoImpW mkProd
-  ioRet = NoImpW ioRet
-  ioMap = NoImpW ioMap
-  ioBind = NoImpW ioBind
-  unit = NoImpW unit
-  nothing = NoImpW nothing
-  just = NoImpW just
-  optionMatch = NoImpW optionMatch
-  exfalso = NoImpW exfalso
-  fix = NoImpW fix
-  left = NoImpW left
-  right = NoImpW right
-  sumMatch = NoImpW sumMatch
-  writer = NoImpW writer
-  runWriter = NoImpW runWriter
-  double = NoImpW . double
-  doubleExp = NoImpW doubleExp
-  doublePlus = NoImpW doublePlus
-  doubleMinus = NoImpW doubleMinus
-  doubleMult = NoImpW doubleMult
-  doubleDivide = NoImpW doubleDivide
-  float = NoImpW . float
-  floatExp = NoImpW floatExp
-  floatPlus = NoImpW floatPlus
-  floatMinus = NoImpW floatMinus
-  floatMult = NoImpW floatMult
-  floatDivide = NoImpW floatDivide
-  float2Double = NoImpW float2Double
-  double2Float = NoImpW double2Float
-  state = NoImpW state
-  runState = NoImpW runState
-
-instance Lang r => Bool (ImpW r) where
-  bool = NoImpW . bool
-  ite = NoImpW ite
-
-instance Lang repr => WithDiff repr () where
-  withDiff = const1 id
-
-instance Lang repr => WithDiff repr Double where
-  withDiff = lam2 $ \conv d -> mkProd2 d (app conv doubleOne)
-
-instance Lang repr => WithDiff repr P.Float where
-  withDiff = lam2 $ \conv d -> mkProd2 d (app conv floatOne)
-
-instance (Lang repr, WithDiff repr l, WithDiff repr r) => WithDiff repr (l, r) where
-  withDiff = lam $ \conv -> bimap2 (withDiff1 (lam $ \l -> app conv (mkProd2 l zero))) (withDiff1 (lam $ \r -> app conv (mkProd2 zero r)))
-
 class Monoid r g => Group r g where
   invert :: r h (g -> g)
   minus :: r h (g -> g -> g)
-  default invert :: Lang r => r h (g -> g)
+  default invert :: DBI r => r h (g -> g)
   invert = minus1 zero
-  default minus :: Lang r => r h (g -> g -> g)
+  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 (Double -> v -> v)
-  divide :: r h (v -> Double -> v)
-  default mult :: Lang r => r h (Double -> v -> 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)
-  default divide :: Lang r => r h (v -> Double -> v)
+  default divide :: Double r => r h (v -> M.Double -> v)
   divide = lam2 $ \x y -> mult2 (recip1 y) x
   {-# MINIMAL (mult | divide) #-}
 
@@ -294,46 +108,46 @@
   mult = const1 $ const1 unit
   divide = const1 $ const1 unit
 
-instance Lang r => Monoid r Double where
+instance Double r => Monoid r M.Double where
   zero = doubleZero
   plus = doublePlus
 
-instance Lang r => Group r Double where
+instance Double r => Group r M.Double where
   minus = doubleMinus
 
-instance Lang r => Vector r Double where
+instance Double r => Vector r M.Double where
   mult = doubleMult
   divide = doubleDivide
 
-instance Lang r => Monoid r P.Float where
+instance Float r => Monoid r M.Float where
   zero = floatZero
   plus = floatPlus
 
-instance Lang r => Group r P.Float where
+instance Float r => Group r M.Float where
   minus = floatMinus
 
-instance Lang r => Vector r P.Float where
+instance Lang r => Vector r M.Float where
   mult = com2 floatMult double2Float
   divide = com2 (flip2 com double2Float) floatDivide
 
-instance (Lang repr, Monoid repr l, Monoid repr r) => Monoid repr (l, r) where
+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))
 
-instance (Lang repr, Group repr l, Group repr r) => Group repr (l, r) where
+instance (Prod repr, Group repr l, Group repr r) => Group repr (l, r) where
   invert = bimap2 invert invert
 
-instance (Lang repr, Vector repr l, Vector repr r) => Vector repr (l, r) where
+instance (Prod repr, Double repr, Vector repr l, Vector repr r) => Vector repr (l, r) where
   mult = lam $ \x -> bimap2 (mult1 x) (mult1 x)
 
-instance (Lang repr, Monoid repr v) => Monoid repr (Double -> v) where
+instance (Double r, Monoid r v) => Monoid r (M.Double -> v) where
   zero = const1 zero
   plus = lam3 $ \l r x -> plus2 (app l x) (app r x)
 
-instance (Lang repr, Group repr v) => Group repr (Double -> v) where
+instance (Lang r, Group r v) => Group r (M.Double -> v) where
   invert = lam2 $ \l x -> app l (invert1 x)
 
-instance (Lang repr, Vector repr v) => Vector repr (Double -> v) where
+instance (Lang r, Vector r v) => Vector r (M.Double -> v) where
   mult = lam3 $ \l r x -> app r (mult2 l x)
 
 instance Lang r => Monoid r [a] where
@@ -346,12 +160,18 @@
 instance Lang r => BiFunctor r Either where
   bimap = lam2 $ \l r -> sumMatch2 (com2 left l) (com2 right r)
 
-instance Lang r => BiFunctor r (,) where
+instance Prod r => BiFunctor r (,) where
   bimap = lam3 $ \l r p -> mkProd2 (app l (zro1 p)) (app r (fst1 p))
 
+instance Dual r => BiFunctor r M.Dual where
+  bimap = lam2 $ \l r -> dual `com2` bimap2 l r `com2` runDual
+
 instance Lang r => Functor r (Writer w) where
   map = lam $ \f -> com2 writer (com2 (bimap2 f id) runWriter)
 
+instance Lang r => Functor r (M.Map k) where
+  map = mapMap
+
 instance (Lang r, Monoid r w) => Applicative r (Writer w) where
   pure = com2 writer (flip2 mkProd zero)
   ap = lam2 $ \f x -> writer1 (mkProd2 (app (zro1 (runWriter1 f)) (zro1 (runWriter1 x))) (plus2 (fst1 (runWriter1 f)) (fst1 (runWriter1 x))))
@@ -360,56 +180,35 @@
   join = lam $ \x -> writer1 $ mkProd2 (zro1 $ runWriter1 $ zro1 $ runWriter1 x) (plus2 (fst1 $ runWriter1 $ zro1 $ runWriter1 x) (fst1 $ runWriter1 x))
 
 instance Lang r => Functor r (State l) where
-  map = lam2 $ \f s -> state1 (com2 (bimap2 f id) (runState1 s))
+  map = lam2 $ \f st -> state1 (com2 (bimap2 f id) (runState1 st))
 
 instance Lang r => Applicative r (State l) where
   pure = lam $ \x -> state1 (mkProd1 x)
-  ap = lam2 $ \f x -> state1 $ lam $ \s -> let_2 (runState2 f s) (lam $ \p -> bimap3 (zro1 p) id (runState2 x (fst1 p)))
+  ap = lam2 $ \f x -> state1 $ lam $ \st -> let_2 (runState2 f st) (lam $ \p -> bimap3 (zro1 p) id (runState2 x (fst1 p)))
 
 instance Lang r => Monad r (State l) where
-  join = lam $ \x -> state1 $ lam $ \s -> let_2 (runState2 x s) (uncurry1 runState)
+  join = lam $ \x -> state1 $ lam $ \st -> let_2 (runState2 x st) (uncurry1 runState)
 
-instance Lang r => Functor r P.IO where
+instance Lang r => Functor r M.IO where
   map = ioMap
 
-instance Lang r => Applicative r P.IO where
+instance Lang r => Applicative r M.IO where
   pure = ioRet
   ap = lam2 $ \f x -> ioBind2 f (flip2 ioMap x)
 
-instance Lang r => Monad r P.IO where
+instance Lang r => Monad r M.IO where
   bind = ioBind
 
-instance Lang r => Functor r P.Maybe where
+instance Lang r => Functor r M.Maybe where
   map = lam $ \func -> optionMatch2 nothing (com2 just func)
 
-instance Lang r => Applicative r P.Maybe where
+instance Lang r => Applicative r M.Maybe where
   pure = just
   ap = optionMatch2 (const1 nothing) map
 
-instance Lang r => Monad r P.Maybe where
+instance Lang r => Monad r M.Maybe where
   bind = lam2 $ \x func -> optionMatch3 nothing func x
 
-runImpW :: forall repr h x. Lang repr => ImpW repr h x -> RunImpW repr h x
-runImpW (ImpW x) = RunImpW x
-runImpW (NoImpW x) = RunImpW (const1 x :: repr h (() -> x))
-
-instance Lang repr => DBI (ImpW repr) where
-  z = NoImpW z
-  s :: forall a h b. ImpW repr h b -> ImpW repr (a, h) b
-  s (ImpW x) = work x
-    where
-      work :: Weight w => repr h (w -> b) -> ImpW repr (a, h) b
-      work x = ImpW (s x)
-  s (NoImpW x) = NoImpW (s x)
-  app (ImpW f) (ImpW x) = ImpW (lam $ \p -> app (app (conv f) (zro1 p)) (app (conv x) (fst1 p)))
-  app (NoImpW f) (NoImpW x) = NoImpW (app f x)
-  app (ImpW f) (NoImpW x) = ImpW (lam $ \w -> app2 (conv f) w (conv x))
-  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)
-
-
-
 cons2 = app2 cons
 listMatch2 = app2 listMatch
 fix1 = app fix
@@ -417,14 +216,10 @@
 uncurry1 = app uncurry
 optionMatch2 = app2 optionMatch
 optionMatch3 = app3 optionMatch
-zro1 = app zro
-fst1 = app fst
 mult1 = app mult
 mult2 = app2 mult
 divide2 = app2 divide
 invert1 = app invert
-mkProd1 = app mkProd
-mkProd2 = app2 mkProd
 minus1 = app minus
 divide1 = app divide
 recip = divide1 doubleOne
diff --git a/DDF/Map.hs b/DDF/Map.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Map.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE
+  NoImplicitPrelude,
+  ScopedTypeVariables
+#-}
+
+module DDF.Map (module DDF.Map, module DDF.Prod, module DDF.Option) where
+
+import DDF.Prod
+import qualified Prelude as M
+import qualified Data.Map as M
+import DDF.Option
+import DDF.Diff
+import qualified DDF.Meta.Dual as M
+
+class M.Ord x => Ord x where
+  diffOrd :: Proxy (v, x) -> Dict (Ord (Diff 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)
+  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)
diff --git a/DDF/Meta/Dual.hs b/DDF/Meta/Dual.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Meta/Dual.hs
@@ -0,0 +1,9 @@
+module DDF.Meta.Dual where
+
+newtype Dual l r = Dual {runDual :: (l, r)}
+
+dualOrig (Dual (l, _)) = l
+
+dualDiff (Dual (_, r)) = r
+
+mkDual l r = Dual (l, r)
diff --git a/DDF/Option.hs b/DDF/Option.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Option.hs
@@ -0,0 +1,8 @@
+module DDF.Option (module DDF.Option, module DDF.DBI) where
+
+import DDF.DBI
+
+class DBI r => Option r where
+  nothing :: r h (Maybe a)
+  just :: r h (a -> Maybe a)
+  optionMatch :: r h (b -> (a -> b) -> Maybe a -> b)
diff --git a/DDF/Poly.lhs b/DDF/Poly.lhs
--- a/DDF/Poly.lhs
+++ b/DDF/Poly.lhs
@@ -1,17 +1,19 @@
 > {-# LANGUAGE
->     MultiParamTypeClasses,
->     RankNTypes,
->     ScopedTypeVariables,
->     FlexibleInstances,
->     FlexibleContexts,
->     UndecidableInstances,
->     IncoherentInstances,
->     PolyKinds,
->     LambdaCase,
->     NoMonomorphismRestriction,
->     TypeFamilies,
->     LiberalTypeSynonyms,
->     EmptyCase #-}
+>   NoImplicitPrelude,
+>   MultiParamTypeClasses,
+>   RankNTypes,
+>   ScopedTypeVariables,
+>   FlexibleInstances,
+>   FlexibleContexts,
+>   UndecidableInstances,
+>   IncoherentInstances,
+>   PolyKinds,
+>   LambdaCase,
+>   NoMonomorphismRestriction,
+>   TypeFamilies,
+>   LiberalTypeSynonyms,
+>   EmptyCase
+> #-}
 
 > module DDF.Poly where
 > import Control.Monad (when)
@@ -19,13 +21,17 @@
 > import DDF.Lang
 > import DDF.Show
 > import DDF.Eval
+> import DDF.WDiff
 > import qualified Control.Monad as M
+> import Prelude (Integer)
+> import qualified Prelude as M
+> import qualified DDF.Meta.Dual as M
 
 Importing files and opening language extension...
 So, our goal is to find x, where x * x + 2 * x + 3 = 27.
 To do so, we try to minimize their difference squared (l2 norm).
 
-> poly :: forall repr h. Lang repr => repr h (Double -> Double)
+> poly :: forall repr h. Lang repr => repr h (M.Double -> M.Double)
 > poly = lam $ \x -> plus2 (mult2 x x) (plus2 (mult2 (double 2.0) x) (double 3.0))
 
 poly x = x * x + (2 * x + 3)
@@ -42,7 +48,7 @@
 
 Now write a generic function that calculate x and return it.
 
-> solve :: forall m. M.Monad m => (AST -> m ()) -> (Integer -> Double -> m ()) -> m Double
+> solve :: forall m. M.Monad m => (AST -> m ()) -> (Integer -> M.Double -> m ()) -> m M.Double
 > solve doAST doIter = do
 
 Let's begin by trying to print poly
@@ -55,10 +61,10 @@
 We start by assuming x = 0 is the solution,
 and minimize (comp x) by taking derivative of x, and decrease it whenever it is positive (and vice versa).
 
->     go :: Integer -> Double -> m Double
+>     go :: Integer -> M.Double -> m M.Double
 >     go i w | i < 200 = do
 >       doIter i w
->       go (1 + i) $ w - 0.001 * snd (runEval (runWDiff $ noEnv comp) () (w, 1))
+>       go (1 + i) $ w - 0.001 * M.dualDiff (runEval (runWDiff $ 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,
@@ -70,7 +76,7 @@
 the whole computation return a pair of (x * x + (2 * x + 3) - 27)^2, and it's derivative.
 we modify w using the derivative.
 
->     go i w = M.return w
+>     go _ w = M.return w
 
 By running the program, you shall see
 (\a -> (plus (mult a a) (plus (mult 2.0 a) 3.0)))
@@ -99,7 +105,7 @@
 > main :: IO ()
 > main = do
 >   d <- solve print printSquare
->   putStrLn $ "x is: " ++ (show d)
+>   M.putStrLn $ "x is: " ++ (show d)
 >   M.return ()
 >   where
 >     printSquare i x = when (isSquare i) (print x)
diff --git a/DDF/Prod.hs b/DDF/Prod.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Prod.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE NoImplicitPrelude, NoMonomorphismRestriction #-}
+
+module DDF.Prod (module DDF.Prod, module DDF.DBI) where
+
+import DDF.DBI
+
+class DBI r => Prod r where
+  mkProd :: r h (a -> b -> (a, b))
+  zro :: r h ((a, b) -> a)
+  fst :: r h ((a, b) -> b)
+  swap :: r h ((x, y) -> (y, x))
+  swap = lam $ \p -> mkProd2 (fst1 p) (zro1 p)
+  curry :: r h (((a, b) -> c) -> (a -> b -> c))
+  curry = lam3 $ \f a b -> app f (mkProd2 a b)
+  uncurry :: r h ((a -> b -> c) -> ((a, b) -> c))
+  uncurry = lam2 $ \f p -> app2 f (zro1 p) (fst1 p)
+
+zro1 = app zro
+fst1 = app fst
+mkProd1 = app mkProd
+mkProd2 = app2 mkProd
+curry1 = app curry
diff --git a/DDF/Show.hs b/DDF/Show.hs
--- a/DDF/Show.hs
+++ b/DDF/Show.hs
@@ -4,21 +4,20 @@
 
 import DDF.Lang
 import qualified Prelude as M
-import DDF.ImportMeta
 
 data AST = Leaf M.String | App M.String AST [AST] | Lam M.String [M.String] AST
 
 appAST (Leaf f) x = App f x []
 appAST (App f x l) r = App f x (l ++ [r])
-appAST lam r = appAST (Leaf $ show lam) r
+appAST l r = appAST (Leaf $ show l) r
 
-lamAST str (Lam s l t) = Lam str (s:l) t
+lamAST str (Lam st l t) = Lam str (st:l) t
 lamAST str r = Lam str [] r
 
 instance M.Show AST where
   show (Leaf f) = f
   show (App f x l) = "(" ++ f ++ " " ++ show x ++ M.concatMap ((" " ++) . show) l ++ ")"
-  show (Lam s l t) = "(\\" ++ s ++ M.concatMap (" " ++) l ++ " -> " ++ show t ++ ")"
+  show (Lam str l t) = "(\\" ++ str ++ M.concatMap (" " ++) l ++ " -> " ++ show t ++ ")"
 
 newtype Show h a = Show {runShow :: [M.String] -> M.Int -> AST}
 name = Show . M.const . M.const . Leaf
@@ -35,40 +34,63 @@
   bool = name . show
   ite = name "ite"
 
-instance Lang Show where
+instance Char Show where
+  char = name . show
+
+instance Prod Show where
   mkProd = name "mkProd"
   zro = name "zro"
   fst = name "fst"
+
+instance Double Show where
   double = name . show
   doublePlus = name "plus"
   doubleMinus = name "minus"
   doubleMult = name "mult"
   doubleDivide = name "divide"
   doubleExp = name "exp"
+
+instance Float Show where
+  float = name . show
+  floatPlus = name "plus"
+  floatMinus = name "minus"
+  floatMult = name "mult"
+  floatDivide = name "divide"
+  floatExp = name "exp"
+
+instance Option Show where
+  nothing = name "nothing"
+  just = name "just"
+  optionMatch = name "optionMatch"
+
+instance Map Show where
+  empty = name "empty"
+  singleton = name "singleton"
+  lookup = name "lookup"
+  alter = name "alter"
+  mapMap = name "mapMap"
+
+instance Dual Show where
+  dual = name "dual"
+  runDual = name "runDual"
+
+instance Lang Show where
   fix = name "fix"
   left = name "left"
   right = name "right"
   sumMatch = name "sumMatch"
   unit = name "unit"
   exfalso = name "exfalso"
-  nothing = name "nothing"
-  just = name "just"
   ioRet = name "ioRet"
   ioBind = name "ioBind"
   nil = name "nil"
   cons = name "cons"
   listMatch = name "listMatch"
-  optionMatch = name "optionMatch"
   ioMap = name "ioMap"
   writer = name "writer"
   runWriter = name "runWriter"
-  float = name . show
-  floatPlus = name "plus"
-  floatMinus = name "minus"
-  floatMult = name "mult"
-  floatDivide = name "divide"
-  floatExp = name "exp"
   float2Double = name "float2Double"
   double2Float = name "double2Float"
   state = name "state"
   runState = name "runState"
+  putStrLn = name "putStrLn"
diff --git a/DDF/Size.hs b/DDF/Size.hs
new file mode 100644
--- /dev/null
+++ b/DDF/Size.hs
@@ -0,0 +1,80 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module DDF.Size where
+
+import DDF.Lang
+
+newtype Size h x = Size {runSize :: Int}
+
+one = Size 1
+
+instance DBI Size where
+  z = one
+  s (Size x) = (Size x)
+  app (Size l) (Size r) = Size (l + r)
+  abs (Size l) = Size (1 + l)
+
+instance Bool Size where
+  bool _ = one
+  ite = one
+
+instance Char Size where
+  char _ = one
+
+instance Option Size where
+  nothing = one
+  just = one
+  optionMatch = one
+
+instance Double Size where
+  double _ = one
+  doublePlus = one
+  doubleMinus = one
+  doubleMult = one
+  doubleDivide = one
+  doubleExp = one
+
+instance Float Size where
+  float _ = one
+  floatPlus = one
+  floatMinus = one
+  floatMult = one
+  floatDivide = one
+  floatExp = one
+
+instance Map Size where
+  mapMap = one
+  alter = one
+  empty = one
+  singleton = one
+  lookup = one
+
+instance Prod Size where
+  mkProd = one
+  zro = one
+  fst = one
+
+instance Dual Size where
+  dual = one
+  runDual = one
+
+instance Lang Size where
+  fix = one
+  left = one
+  right = one
+  sumMatch = one
+  unit = one
+  exfalso = one
+  ioRet = one
+  ioBind = one
+  ioMap = one
+  nil = one
+  cons = one
+  listMatch = one
+  writer = one
+  runWriter = one
+  float2Double = one
+  double2Float = one
+  state = one
+  runState = one
+  putStrLn = one
diff --git a/DDF/UnHOAS.hs b/DDF/UnHOAS.hs
--- a/DDF/UnHOAS.hs
+++ b/DDF/UnHOAS.hs
@@ -16,40 +16,63 @@
   bool = UnHOAS . bool
   ite = UnHOAS ite
 
-instance Lang repr => Lang (UnHOAS repr) where
+instance Char r => Char (UnHOAS r) where
+  char = UnHOAS . char
+
+instance Prod r => Prod (UnHOAS r) where
   mkProd = UnHOAS mkProd
   zro = UnHOAS zro
   fst = UnHOAS fst
+
+instance Double r => Double (UnHOAS r) where
   double = UnHOAS . double
   doublePlus = UnHOAS doublePlus
   doubleMinus = UnHOAS doubleMinus
   doubleMult = UnHOAS doubleMult
   doubleDivide = UnHOAS doubleDivide
   doubleExp = UnHOAS doubleExp
+
+instance Float r => Float (UnHOAS r) where
+  float = UnHOAS . float
+  floatPlus = UnHOAS floatPlus
+  floatMinus = UnHOAS floatMinus
+  floatMult = UnHOAS floatMult
+  floatDivide = UnHOAS floatDivide
+  floatExp = UnHOAS floatExp
+
+instance Option r => Option (UnHOAS r) where
+  nothing = UnHOAS nothing
+  just = UnHOAS just
+  optionMatch = UnHOAS optionMatch
+
+instance Map r => Map (UnHOAS r) where
+  empty = UnHOAS empty
+  singleton = UnHOAS singleton
+  alter = UnHOAS alter
+  lookup = UnHOAS lookup
+  mapMap = UnHOAS mapMap
+
+instance Dual r => Dual (UnHOAS r) where
+  dual = UnHOAS dual
+  runDual = UnHOAS runDual
+
+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
-  nothing = UnHOAS nothing
-  just = UnHOAS just
   ioRet = UnHOAS ioRet
   ioBind = UnHOAS ioBind
   nil = UnHOAS nil
   cons = UnHOAS cons
   listMatch = UnHOAS listMatch
-  optionMatch = UnHOAS optionMatch
   ioMap = UnHOAS ioMap
   writer = UnHOAS writer
   runWriter = UnHOAS runWriter
-  float = UnHOAS . float
-  floatPlus = UnHOAS floatPlus
-  floatMinus = UnHOAS floatMinus
-  floatMult = UnHOAS floatMult
-  floatDivide = UnHOAS floatDivide
-  floatExp = UnHOAS floatExp
-  float2Double = UnHOAS float2Double
   double2Float = UnHOAS double2Float
   state = UnHOAS state
   runState = UnHOAS runState
+  putStrLn = UnHOAS putStrLn
diff --git a/DDF/WDiff.hs b/DDF/WDiff.hs
new file mode 100644
--- /dev/null
+++ b/DDF/WDiff.hs
@@ -0,0 +1,102 @@
+{-# LANGUAGE
+  NoImplicitPrelude,
+  ExplicitForAll,
+  InstanceSigs,
+  ScopedTypeVariables
+#-}
+
+module DDF.WDiff where
+
+import DDF.Lang
+import DDF.Diff
+import qualified Data.Map as M
+
+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 r => Map (WDiff r v) where
+  empty = WDiff empty
+  singleton = WDiff singleton
+  lookup :: forall h k a. Ord k => WDiff r v h (k -> M.Map k a -> Maybe a)
+  lookup = withDict (diffOrd (Proxy :: Proxy (v, k))) (WDiff lookup)
+  alter :: forall h k a. Ord k => WDiff r v h ((Maybe a -> Maybe a) -> k -> M.Map k a -> M.Map k a)
+  alter = withDict (diffOrd (Proxy :: Proxy (v, k))) (WDiff alter)
+  mapMap = WDiff mapMap
+
+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
new file mode 100644
--- /dev/null
+++ b/DDF/WithDiff.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE
+  NoImplicitPrelude,
+  MultiParamTypeClasses,
+  FlexibleInstances,
+  NoMonomorphismRestriction
+#-}
+
+module DDF.WithDiff where
+
+import DDF.Lang
+import DDF.Diff
+import qualified Prelude as M
+
+class Monoid r w => WithDiff r w where
+  withDiff :: r h ((w -> x) -> w -> Diff x w)
+
+withDiff1 = app withDiff
+selfWithDiff :: (DBI r, WithDiff r w) => r h (w -> Diff w w)
+selfWithDiff = withDiff1 id
+
+instance Lang repr => ProdCon (WithDiff repr) l r where prodCon = Sub Dict
+
+instance Lang r => WithDiff r () where
+  withDiff = const1 id
+
+instance Lang r => WithDiff r M.Double where
+  withDiff = lam2 $ \con d -> dual1 $ mkProd2 d (app con doubleOne)
+
+instance Lang 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
+  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,9 +1,9 @@
 > {-# LANGUAGE ScopedTypeVariables, NoMonomorphismRestriction, TypeApplications, RankNTypes #-}
 
 This is the classical example of using sigmoid NN to approximate Xor.
+You should already read DDF.Poly before this.
 
 > module DDF.Xor where
-> import qualified DDF.Poly as YouShouldAlreadyReadThis
 > import qualified Prelude as M
 > import System.Random
 > import Control.Monad (when)
@@ -15,6 +15,9 @@
 > import DDF.Combine
 > import DDF.Eval
 > import DDF.GWDiff
+> import DDF.ImpW
+> import DDF.WithDiff
+> import qualified DDF.Meta.Dual as M
 
 Recall in poly, we constructed a function Double -> Double,
 with argument being the weight, and do gradient descend to found a solution.
@@ -32,8 +35,8 @@
 
 Let's start by constructing a weight.
 
-> weight :: Lang repr => ImpW repr h Double
-> weight = ImpW id
+> doubleWeight :: Lang repr => ImpW repr h M.Double
+> doubleWeight = ImpW id
 
 Note that we are just manipulating AST.
 If you wanna do weight sharing, you need to use let(in DDF) yourself.
@@ -45,52 +48,52 @@
 > sigmoid = lam $ \x -> recip1 (plus2 doubleOne (doubleExp1 (invert1 x)))
 > sigmoid1 = app sigmoid
 
-With weight and sigmoid we can construct a neuron of type ((Double, Double) -> Double)
-The weight should be a pair of Double, each as a scale on the actual input, with a bias.
+With weight and sigmoid we can construct a neuron of type ((M.Double, M.Double) -> M.Double)
+The weight should be a pair of M.Double, each as a scale on the actual input, with a bias.
 We then add the two scaled input, with the bias, and pass them into sigmoid.
 
-> scaleAdd :: Lang repr => ImpW repr h ((Double, Double) -> Double)
+> scaleAdd :: Lang repr => ImpW repr h ((M.Double, M.Double) -> M.Double)
 > scaleAdd = ImpW $ lam2 $ \w p -> plus2 (mult2 (zro1 w) (zro1 p)) (plus2 (fst1 w) (fst1 p))
 
-> withBias :: Lang repr => ImpW repr h (Double -> Double)
+> withBias :: Lang repr => ImpW repr h (M.Double -> M.Double)
 > withBias = ImpW $ plus
 
-> neuron :: Lang repr => ImpW repr h ((Double, Double) -> Double)
+> neuron :: Lang repr => ImpW repr h ((M.Double, M.Double) -> M.Double)
 > neuron = com2 (com2 sigmoid withBias) scaleAdd
 > neuron1 = app neuron
 
-Now, the hidden layer of type (Double, Double) -> ((Double, Double), (Double, Double))
+Now, the hidden layer of type (M.Double, M.Double) -> ((M.Double, M.Double), (M.Double, M.Double))
 
 > hidden = lam $ \p -> mkProd2 (mkProd2 (neuron1 p) (neuron1 p)) (mkProd2 (neuron1 p) (neuron1 p))
 
 And finally, the whole NN:
 
-> type XOR = (Double, Double) -> Double
-> xor :: Lang repr => ImpW repr h XOR
-> xor = neuron `com2` (bimap2 scaleAdd scaleAdd) `com2` hidden
+> type XOR = (M.Double, M.Double) -> M.Double
+> xorNet :: Lang repr => ImpW repr h XOR
+> xorNet = neuron `com2` (bimap2 scaleAdd scaleAdd) `com2` hidden
 
 But before we can train it, we need to define the dataset and the loss function.
 
-> l2 :: Lang repr => repr h (Double -> Double -> Double)
+> l2 :: Lang repr => repr h (M.Double -> M.Double -> M.Double)
 > l2 = lam2 $ \l r -> (mult2 (minus2 l r) (minus2 l r))
 > l22 = app2 l2
 
-> eval :: Lang repr => repr h (XOR -> ((Double, Double), Double) -> Double)
+> eval :: Lang repr => repr h (XOR -> ((M.Double, M.Double), M.Double) -> M.Double)
 > eval = lam2 $ \xor p -> l22 (app xor (zro1 p)) (fst1 p)
 
-> dataset :: Lang repr => repr h [((Double, Double), Double)]
+> dataset :: Lang repr => repr h [((M.Double, M.Double), M.Double)]
 > dataset = cons2 (build 0 0 0) (cons2 (build 0 1 1) (cons2 (build 1 0 1) (cons2 (build 1 1 0) nil)))
 >   where build l r ret = mkProd2 (mkProd2 (double l) (double r)) (double ret)
 
 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 -> Double)
+> 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)
 
 Now we are good to implement the train function!
 
-> findXor :: forall g m. (RandomGen g, M.Monad m) => g -> (AST -> m ()) -> (Int -> Double -> M.String -> m ()) -> m XOR
-> findXor rand doAST doIter = case runImpW $ noEnv xor of
+> 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
 >     doAST $ xorS vars 0
 
@@ -105,23 +108,23 @@
 >     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 -> Double)) -> (Double -> w -> w -> w) -> Int -> (w -> XOR) -> m XOR
->       go xor weight reify loss update i orig | i <= 2500 = do
+>       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
+>       go xor weight reifyE lossE update i orig | i <= 2500 = do
 >         doIter i lossVal (M.show weight)
->         go xor (update 0.3 weight lossDiff) reify loss update (1 + i) orig
+>         go xor (update 0.3 weight lossDiff) reifyE lossE update (1 + i) orig
 >           where
->             (lossVal, lossDiff) = loss $ xor (reify weight)
->       go xor weight _ _ _ _ orig = M.return $ orig weight
+>             M.Dual (lossVal, lossDiff) = lossE $ xor (reifyE weight)
+>       go _ weight _ _ _ _ orig = M.return $ orig weight
 
 > main :: IO ()
 > main = do
 >   g <- getStdGen
->   xor <- findXor g print (\i d w -> when (isSquare i) $ do
+>   xorTrained <- findXor g print (\i d w -> when (isSquare i) $ do
 >     print d
 >     M.putStrLn w
 >     M.putStrLn "")
->   let doXor :: Double -> Double -> IO ()
->       doXor l r = M.putStrLn $ M.show l ++ " xor " ++ M.show r ++ " is " ++ (M.show $ xor (l, r))
+>   let doXor :: M.Double -> M.Double -> 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
 >   doXor 1 0
diff --git a/DeepDarkFantasy.cabal b/DeepDarkFantasy.cabal
--- a/DeepDarkFantasy.cabal
+++ b/DeepDarkFantasy.cabal
@@ -1,5 +1,5 @@
 name: DeepDarkFantasy
-version: 0.2017.4.1
+version: 0.2017.4.5
 cabal-version: 1.12
 build-type: Simple
 license: Apache
@@ -17,23 +17,37 @@
 library
   exposed-modules:
     DDF.Bool
+    DDF.Char
     DDF.Combine
     DDF.DBI
+    DDF.Diff
+    DDF.Double
+    DDF.Dual
     DDF.Eval
+    DDF.Float
     DDF.GWDiff
     DDF.ImportMeta
+    DDF.ImpW
     DDF.Lang
+    DDF.Map
+    DDF.Meta.Dual
+    DDF.Option
     DDF.Poly
+    DDF.Prod
     DDF.Show
+    DDF.Size
     DDF.UnHOAS
     DDF.Util
+    DDF.WDiff
+    DDF.WithDiff
     DDF.Xor
   build-depends:
     base >= 4.9.0.0 && <= 4.9.1.0,
     mtl -any,
     random -any,
-    constraints -any 
-  ghc-options: -ferror-spans 
+    constraints -any,
+    containers -any
+  ghc-options: -Wall -Wno-type-defaults -Wno-missing-signatures -Wno-orphans -fwarn-tabs -ferror-spans
   default-language: Haskell2010
 
 Test-Suite TestPoly