diff --git a/DeepDarkFantasy.cabal b/DeepDarkFantasy.cabal
--- a/DeepDarkFantasy.cabal
+++ b/DeepDarkFantasy.cabal
@@ -1,5 +1,5 @@
 name: DeepDarkFantasy
-version: 0.0.1.1
+version: 0.2017.3.28
 cabal-version: 1.12
 build-type: Simple
 license: Apache
@@ -16,17 +16,16 @@
 
 library
   exposed-modules:
-    Comb
     DBI
-    HOAS
-    Main
     Poly
     Xor
     Util
+    Lang
   build-depends:
     base >= 4.9.0.0 && <= 4.9.1.0,
     mtl -any,
-    random -any
+    random -any,
+    constraints -any
   default-language: Haskell2010
   hs-source-dirs: src
-  ghc-options: -ferror-spans
+  ghc-options: -ferror-spans 
diff --git a/src/Comb.hs b/src/Comb.hs
deleted file mode 100644
--- a/src/Comb.hs
+++ /dev/null
@@ -1,47 +0,0 @@
-{-# LANGUAGE
-    MultiParamTypeClasses,
-    RankNTypes,
-    ScopedTypeVariables,
-    FlexibleInstances,
-    FlexibleContexts,
-    UndecidableInstances,
-    IncoherentInstances,
-    PolyKinds,
-    LambdaCase,
-    MonomorphismRestriction #-}
-
-module Comb where
-
-class Comb repr where
-  app :: repr (a -> b) -> repr a -> repr b
-  s :: repr ((a -> b -> c) -> (a -> b) -> (a -> c))
-  k :: repr (a -> b -> a)
-  i :: repr (a -> a)
-  b :: repr ((b -> c) -> (a -> b) -> (a -> c))
-  c :: repr ((a -> b -> c) -> (b -> a -> c))
-  w :: repr ((a -> a -> b) -> (a -> b))
-
-newtype Eval x = Eval {unEval :: x}
-
-instance Comb Eval where
-  app (Eval f) (Eval x) = Eval (f x)
-  s = Eval (\f x arg -> f arg $ x arg)
-  k = Eval const
-  i = Eval id
-  b = Eval (.)
-  c = Eval flip
-  w = Eval (\f x -> f x x)
-
-newtype SShow x = SShow {unSShow :: String}
-
-instance Comb SShow where
-  app (SShow f) (SShow x) = SShow $ "(" ++ f ++ " " ++ x ++ ")"
-  s = SShow "s"
-  k = SShow "k"
-  i = SShow "i"
-  b = SShow "b"
-  c = SShow "c"
-  w = SShow "w"
-
-main :: IO ()
-main = return ()
diff --git a/src/DBI.hs b/src/DBI.hs
--- a/src/DBI.hs
+++ b/src/DBI.hs
@@ -10,26 +10,39 @@
     NoMonomorphismRestriction,
     TypeFamilies,
     LiberalTypeSynonyms,
-    EmptyCase,
     FunctionalDependencies,
     ExistentialQuantification,
     InstanceSigs,
-    AllowAmbiguousTypes,
     TupleSections,
-    ConstraintKinds #-}
+    ConstraintKinds,
+    DefaultSignatures,
+    UndecidableSuperClasses,
+    TypeOperators,
+    TypeApplications,
+    PartialTypeSignatures #-}
 
 module DBI where
 import qualified Prelude as P
 import Prelude (($), (.), (+), (-), (++), show, (>>=), (*), (/), undefined)
 import Util
-import Data.Void
 import Control.Monad (when)
-import qualified Control.Monad.Writer as P
-import qualified Data.Functor.Identity as P
-import qualified Data.Tuple as P
 import System.Random
 import Data.Proxy
+import Data.Constraint
+import Data.Constraint.Forall
 
+class Monoid r m where
+  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)
+
+withDiff1 = app withDiff
+
+selfWithDiff :: (DBI repr, WithDiff repr w) => repr h (w -> Diff w w)
+selfWithDiff = withDiff1 id
+
 instance Random () where
   random = ((),)
   randomR _ = random
@@ -44,227 +57,56 @@
       (l, g1) = randomR (llo, lhi) g0
       (r, g2) = randomR (rlo, rhi) g1
 
-class Reify repr x where
-  reify :: x -> repr h x
-
-instance DBI repr => Reify repr () where
-  reify _ = unit
-
-instance DBI repr => Reify repr P.Double where
-  reify = lit
-
-instance (DBI repr, Reify repr l, Reify repr r) => Reify repr (l, r) where
-  reify (l, r) = mkProd2 (reify l) (reify r)
-
 class DBI repr where
   z :: repr (a, h) a
   s :: repr h b -> repr (a, h) b
-  lam :: repr (a, h) b -> repr h (a -> b)
+  abs :: repr (a, h) b -> repr h (a -> b)
   app :: repr h (a -> b) -> repr h a -> repr h b
-  mkProd :: repr h (a -> b -> (a, b))
-  zro :: repr h ((a, b) -> a)
-  fst :: repr h ((a, b) -> b)
-  lit :: P.Double -> repr h P.Double
-  litZero :: repr h P.Double
-  litZero = lit 0
-  litOne :: repr h P.Double
-  litOne = lit 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)
   hoas :: (repr (a, h) a -> repr (a, h) b) -> repr h (a -> b)
-  hoas f = lam $ f z
-  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)
+  hoas f = abs $ f z
   com :: repr h ((b -> c) -> (a -> b) -> (a -> c))
-  com = hlam3 $ \f g x -> app f (app g x)
-  listAppend :: repr h ([a] -> [a] -> [a])
-  listAppend = hlam2 $ \l r -> fix2 (hlam $ \self -> listMatch2 r (hlam2 $ \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 = hlam $ \p -> mkProd2 (fst1 p) (zro1 p)
+  com = lam3 $ \f g x -> app f (app g x)
   flip :: repr h ((a -> b -> c) -> (b -> a -> c))
-  flip = hlam3 $ \f b a -> app2 f a b
+  flip = lam3 $ \f b a -> app2 f a b
   id :: repr h (a -> a)
-  id = hlam $ \x -> x
+  id = lam $ \x -> x
   const :: repr h (a -> b -> a)
-  const = hlam2 $ \x _ -> x
+  const = lam2 $ \x _ -> x
   scomb :: repr h ((a -> b -> c) -> (a -> b) -> (a -> c))
-  scomb = hlam3 $ \f x arg -> app (app f arg) (app x arg)
-  exp :: repr h (P.Double -> P.Double)
-  curry :: repr h (((a, b) -> c) -> (a -> b -> c))
-  uncurry :: repr h ((a -> b -> c) -> ((a, b) -> c))
-  curry = hlam3 $ \f a b -> app f (mkProd2 a b)
-  uncurry = hlam2 $ \f p -> app2 f (zro1 p) (fst1 p)
+  scomb = lam3 $ \f x arg -> app2 f arg (app x arg)
+  dup :: repr h ((a -> a -> b) -> (a -> b))
+  dup = lam2 $ \f x -> app2 f x x
 
 const1 = app const
-cons2 = app2 cons
-listMatch2 = app2 listMatch
-fix1 = app fix
-fix2 = app2 fix
-uncurry1 = app uncurry
-
-class Monoid r m where
-  zero :: r h m
-  plus :: r h (m -> m -> m)
-
-class (DBI r, Monoid r g) => Group r g where
-  invert :: r h (g -> g)
-  minus :: r h (g -> g -> g)
-  invert = minus1 zero
-  minus = hlam2 $ \x y -> plus2 x (invert1 y)
-  {-# MINIMAL (invert | minus) #-}
-
-minus1 = app minus
-divide1 = app divide
-
-recip = divide1 litOne
-recip1 = app recip
-
-class Group r v => Vector r v where
-  mult :: r h (P.Double -> v -> v)
-  divide :: r h (v -> P.Double -> v)
-  mult = hlam2 $ \x y -> divide2 y (recip1 x)
-  divide = hlam2 $ \x y -> mult2 (recip1 y) x
-  {-# MINIMAL (mult | divide) #-}
-
-instance DBI r => Monoid r () where
-  zero = unit
-  plus = const1 $ const1 unit
-
-instance DBI r => Group r () where
-  invert = const1 unit
-  minus = const1 $ const1 unit
-
-instance DBI r => Vector r () where
-  mult = const1 $ const1 unit
-  divide = const1 $ const1 unit
-
-instance DBI r => Monoid r P.Double where
-  zero = litZero
-  plus = doublePlus
-
-instance DBI r => Group r P.Double where
-  minus = doubleMinus
-
-instance DBI r => Vector r P.Double where
-  mult = doubleMult
-  divide = doubleDivide
-
-instance (DBI repr, Monoid repr l, Monoid repr r) => Monoid repr (l, r) where
-  zero = mkProd2 zero zero
-  plus = hlam2 $ \l r -> mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))
-
-instance (DBI repr, Group repr l, Group repr r) => Group repr (l, r) where
-  invert = bimap2 invert invert
-
-instance (DBI repr, Vector repr l, Vector repr r) => Vector repr (l, r) where
-  mult = hlam $ \x -> bimap2 (mult1 x) (mult1 x)
-
-instance (DBI repr, Monoid repr l, Monoid repr r) => Monoid repr (l -> r) where
-  zero = const1 zero
-  plus = hlam3 $ \l r x -> plus2 (app l x) (app r x)
-
-instance (DBI repr, Group repr l, Group repr r) => Group repr (l -> r) where
-  invert = hlam2 $ \l x -> app l (invert1 x)
-
-instance (DBI repr, Vector repr l, Vector repr r) => Vector repr (l -> r) where
-  mult = hlam3 $ \l r x -> app r (mult2 l x)
-
-instance DBI r => Monoid r [a] where
-  zero = nil
-  plus = listAppend
+map2 = app2 map
+return = pure
+bind2 = app2 bind
+map1 = app map
+join1 = app join
+bimap2 = app2 bimap
+flip1 = app flip
+flip2 = app2 flip
 
 class Functor r f where
   map :: r h ((a -> b) -> (f a -> f b))
 
-instance DBI r => Functor r [] where
-  map = hlam $ \f -> fix1 $ hlam $ \self -> listMatch2 nil (hlam2 $ \x xs -> cons2 (app f x) $ app self xs)
-
-map2 = app2 map
-
 class Functor r a => Applicative r a where
   pure :: r h (x -> a x)
   ap :: r h (a (x -> y) -> a x -> a y)
 
-return = pure
-
 class (DBI r, Applicative r m) => Monad r m where
   bind :: r h (m a -> (a -> m b) -> m b)
   join :: r h (m (m a) -> m a)
-  join = hlam $ \m -> bind2 m id
-  bind = hlam2 $ \m f -> join1 (app2 map f m)
+  join = lam $ \m -> bind2 m id
+  bind = lam2 $ \m f -> join1 (app2 map f m)
   {-# MINIMAL (join | bind) #-}
 
-bind2 = app2 bind
-map1 = app map
-join1 = app join
-bimap2 = app2 bimap
-flip1 = app flip
-flip2 = app2 flip
-
-class DBI r => BiFunctor r p where
+class BiFunctor r p where
   bimap :: r h ((a -> b) -> (c -> d) -> p a c -> p b d)
 
-instance DBI r => BiFunctor r (,) where
-  bimap = hlam3 $ \l r p -> mkProd2 (app l (zro1 p)) (app r (fst1 p))
-
-instance DBI r => Functor r (P.Writer w) where
-  map = hlam $ \f -> com2 writer (com2 (bimap2 f id) runWriter)
-
-writer1 = app writer
-runWriter1 = app runWriter
-
-instance (DBI r, Monoid r w) => Applicative r (P.Writer w) where
-  pure = com2 writer (flip2 mkProd zero)
-  ap = hlam2 $ \f x -> writer1 (mkProd2 (app (zro1 (runWriter1 f)) (zro1 (runWriter1 x))) (plus2 (fst1 (runWriter1 f)) (fst1 (runWriter1 x))))
-
-instance (DBI r, Monoid r w) => Monad r (P.Writer w) where
-  join = hlam $ \x -> writer1 $ mkProd2 (zro1 $ runWriter1 $ zro1 $ runWriter1 x) (plus2 (fst1 $ runWriter1 $ zro1 $ runWriter1 x) (fst1 $ runWriter1 x))
-
-instance DBI r => Functor r P.IO where
-  map = ioMap
-
-ioBind2 = app2 ioBind
-
-instance DBI r => Applicative r P.IO where
-  pure = ioRet
-  ap = hlam2 $ \f x -> ioBind2 f (flip2 ioMap x)
-
-instance DBI r => Monad r P.IO where
-  bind = ioBind
-
 app3 f x y z = app (app2 f x y) z
-
-optionMatch2 = app2 optionMatch
-optionMatch3 = app3 optionMatch
 com2 = app2 com
 
-instance DBI r => Functor r P.Maybe where
-  map = hlam $ \func -> optionMatch2 nothing (com2 just func)
-
-instance DBI r => Applicative r P.Maybe where
-  pure = just
-  ap = optionMatch2 (const1 nothing) map
-
-instance DBI r => Monad r P.Maybe where
-  bind = hlam2 $ \x func -> optionMatch3 nothing func x
-
 newtype Eval h x = Eval {runEval :: h -> x}
 
 comb = Eval . P.const
@@ -272,41 +114,8 @@
 instance DBI Eval where
   z = Eval P.fst
   s (Eval a) = Eval $ a . P.snd
-  lam (Eval f) = Eval $ \a h -> f (h, a)
+  abs (Eval f) = Eval $ \a h -> f (h, a)
   app (Eval f) (Eval x) = Eval $ \h -> f h $ x h
-  zro = comb P.fst
-  fst = comb P.snd
-  mkProd = comb (,)
-  lit = comb
-  doublePlus = comb (+)
-  doubleMinus = comb (-)
-  doubleMult = comb (*)
-  doubleDivide = comb (/)
-  fix = comb loop
-    where loop x = x $ loop x
-  left = comb P.Left
-  right = comb P.Right
-  sumMatch = comb $ \l r -> \case
-                             P.Left x -> l x
-                             P.Right x -> r x
-  unit = comb ()
-  exfalso = comb absurd
-  nothing = comb P.Nothing
-  just = comb P.Just
-  ioRet = comb P.return
-  ioBind = comb (>>=)
-  nil = comb []
-  cons = comb (:)
-  listMatch = comb $ \l r -> \case
-                            [] -> l
-                            x:xs -> r x xs
-  optionMatch = comb $ \l r -> \case
-                              P.Nothing -> l
-                              P.Just x -> r x
-  ioMap = comb P.fmap
-  writer = comb (P.WriterT . P.Identity)
-  runWriter = comb P.runWriter
-  exp = comb P.exp
 
 data AST = Leaf P.String | App P.String AST [AST] | Lam P.String [P.String] AST
 
@@ -321,139 +130,64 @@
   show (Leaf f) = f
   show (App f x l) = "(" ++ f ++ " " ++ show x ++ P.concatMap ((" " ++) . show) l ++ ")"
   show (Lam s l t) = "(\\" ++ s ++ P.concatMap (" " ++) l ++ " -> " ++ show t ++ ")"
+
 newtype Show h a = Show {runShow :: [P.String] -> P.Int -> AST}
 name = Show . P.const . P.const . Leaf
 
 instance DBI Show where
   z = Show $ P.const $ Leaf . show . P.flip (-) 1
   s (Show v) = Show $ \vars -> v vars . P.flip (-) 1
-  lam (Show f) = Show $ \vars x -> lamAST (show x) (f vars (x + 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 $ P.const $ P.const $ Leaf v) vars (h + 1))
-  mkProd = name "mkProd"
-  zro = name "zro"
-  fst = name "fst"
-  lit = name . show
-  doublePlus = name "plus"
-  doubleMinus = name "minus"
-  doubleMult = name "mult"
-  doubleDivide = name "divide"
-  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"
-  exp = name "exp"
 
 class NT repr l r where
     conv :: repr l t -> repr r t
 
-instance {-# INCOHERENT #-} (DBI repr, NT repr l r) => NT repr l (a, r) where
-    conv = s . conv
+class NTS repr l r where
+    convS :: repr l t -> repr r t
 
-instance NT repr x x where
+instance (DBI repr, NT repr l r) => NTS repr l (a, r) where
+    convS = s . conv
+
+instance {-# OVERLAPPABLE #-} NTS repr l r => NT repr l r where
+    conv = convS
+
+instance {-# OVERLAPPING #-} NT repr x x where
     conv = P.id
 
-hlam :: forall repr a b h. DBI repr =>
+lam :: forall repr a b h. DBI repr =>
   ((forall k. NT repr (a, h) k => repr k a) -> (repr (a, h)) b) -> repr h (a -> b)
-hlam f = hoas (\x -> f $ conv x)
+lam f = hoas (\x -> f $ conv x)
 
-hlam2 :: forall repr a b c h. DBI repr =>
+lam2 :: forall repr a b c h. DBI repr =>
   ((forall k. NT repr (a, h) k => repr k a) -> (forall k. NT repr (b, (a, h)) k => repr k b) -> (repr (b, (a, h))) c) -> repr h (a -> b -> c)
-hlam2 f = hlam $ \x -> hlam $ \y -> f x y
+lam2 f = lam $ \x -> lam $ \y -> f x y
 
-hlam3 f = hlam2 $ \x y -> hlam $ \z -> f x y z
+lam3 f = lam2 $ \x y -> lam $ \z -> f x y z
 
 type family Diff v x
-type instance Diff v P.Double = (P.Double, v)
 type instance Diff v () = ()
-type instance Diff v (a, b) = (Diff v a, Diff v b)
 type instance Diff v (a -> b) = Diff v a -> Diff v b
-type instance Diff v (P.Either a b) = P.Either (Diff v a) (Diff v b)
-type instance Diff v Void = Void
-type instance Diff v (P.Maybe a) = P.Maybe (Diff v a)
-type instance Diff v (P.IO a) = P.IO (Diff v a)
-type instance Diff v [a] = [Diff v a]
-type instance Diff v (P.Writer w a) = P.Writer (Diff v w) (Diff v a)
+type instance Diff v (a, b) = (Diff v a, Diff v b)
 
 newtype WDiff repr v h x = WDiff {runWDiff :: repr (Diff v h) (Diff v x)}
 
 app2 f a = app (app f a)
 
-mkProd1 = app mkProd
-mkProd2 = app2 mkProd
 plus2 = app2 plus
-zro1 = app zro
-fst1 = app fst
-minus2 = app2 minus
-mult1 = app mult
-mult2 = app2 mult
-divide2 = app2 divide
-invert1 = app invert
 
-instance (Vector repr v, DBI repr) => DBI (WDiff repr v) where
+instance DBI repr => DBI (WDiff repr v) where
   z = WDiff z
   s (WDiff x) = WDiff $ s x
-  lam (WDiff f) = WDiff $ lam f
+  abs (WDiff f) = WDiff $ abs f
   app (WDiff f) (WDiff x) = WDiff $ app f x
-  mkProd = WDiff mkProd
-  zro = WDiff zro
-  fst = WDiff fst
-  lit x = WDiff $ mkProd2 (lit x) zero
-  doublePlus = WDiff $ hlam2 $ \l r ->
-    mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))
-  doubleMinus = WDiff $ hlam2 $ \l r ->
-    mkProd2 (minus2 (zro1 l) (zro1 r)) (minus2 (fst1 l) (fst1 r))
-  doubleMult = WDiff $ hlam2 $ \l r ->
-    mkProd2 (mult2 (zro1 l) (zro1 r))
-      (plus2 (mult2 (zro1 l) (fst1 r)) (mult2 (zro1 r) (fst1 l)))
-  doubleDivide = WDiff $ hlam2 $ \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)))
   hoas f = WDiff $ hoas (runWDiff . f . WDiff)
-  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
-  exp = WDiff $ hlam $ \x -> mkProd2 (exp1 (zro1 x)) (mult2 (exp1 (zro1 x)) (fst1 x))
 
-exp1 = app exp
-
 noEnv :: repr () x -> repr () x
 noEnv = P.id
 
-selfWithDiff :: (DBI repr, Weight repr w) => repr h (w -> Diff w w)
-selfWithDiff = withDiff1 id
-
-withDiff1 = app withDiff
-
 class RandRange w where
   randRange :: (P.Double, P.Double) -> (w, w)
 
@@ -469,100 +203,34 @@
       (llo, lhi) = randRange (lo, hi)
       (rlo, rhi) = randRange (lo, hi)
 
-instance DBI repr => Weight repr () where
-  withDiff = const1 id
-  fromDiff _ = id
+instance Weight () where weightCon = Sub Dict
 
-instance DBI repr => Weight repr P.Double where
-  withDiff = hlam2 $ \conv d -> mkProd2 d (app conv litOne)
-  fromDiff _ = zro
+instance Weight P.Double where weightCon = Sub Dict
 
-instance (DBI repr, Weight repr l, Weight repr r) => Weight repr (l, r) where
-  withDiff = hlam $ \conv -> bimap2 (withDiff1 (hlam $ \l -> app conv (mkProd2 l zero))) (withDiff1 (hlam $ \r -> app conv (mkProd2 zero r)))
-  fromDiff p = bimap2 (fromDiff p) (fromDiff p)
+instance (Weight l, Weight r) => Weight (l, r) where
+  weightCon :: forall con. (con (), 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 (Random w, RandRange w, Reify repr w, P.Show w, Vector repr w) => Weight repr w where
-  withDiff :: repr h ((w -> x) -> w -> Diff x w)
-  fromDiff :: Proxy x -> repr h (Diff x w -> w)
+class ProdCon con l r where
+  prodCon :: (con l, con r) :- con (l, r)
 
-data RunImpW repr h x = forall w. Weight repr w => RunImpW (repr h (w -> x))
-data ImpW repr h x = NoImpW (repr h x) | forall w. Weight repr w => ImpW (repr h (w -> x))
+instance ProdCon Random l r where prodCon = Sub Dict
 
-runImpW :: forall repr h x. DBI repr => ImpW repr h x -> RunImpW repr h x
-runImpW (ImpW x) = RunImpW x
-runImpW (NoImpW x) = RunImpW (const1 x :: repr h (() -> x))
+instance ProdCon RandRange l r where prodCon = Sub Dict
 
-data Term con h x = Term (forall r. con r => r h x)
+instance ProdCon P.Show l r where prodCon = Sub Dict
 
-instance DBI repr => DBI (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
-  doublePlus = NoImpW doublePlus
-  doubleMinus = NoImpW doubleMinus
-  doubleMult = NoImpW doubleMult
-  doubleDivide = NoImpW doubleDivide
-  fix = NoImpW fix
-  left = NoImpW left
-  right = NoImpW right
-  sumMatch = NoImpW sumMatch
-  lit = NoImpW . lit
-  writer = NoImpW writer
-  runWriter = NoImpW runWriter
-  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 repr 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 (hlam $ \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 (hlam $ \w -> app2 (conv f) w (conv x))
-  app (NoImpW f) (ImpW x) = ImpW (hlam $ \w -> app (conv f) (app (conv x) w))
-  lam (ImpW f) = ImpW (flip1 $ lam f)
-  lam (NoImpW x) = NoImpW (lam x)
-  exp = NoImpW exp
+class Weight w where
+  weightCon :: (con (), con P.Double, ForallV (ProdCon con)) :- con w
 
-instance DBI (Term DBI) where
-  z = Term z
-  s (Term x) = Term (s x)
-  lam (Term x) = Term (lam x)
-  app (Term f) (Term x) = Term $ app f x
-  mkProd = Term mkProd
-  zro = Term zro
-  fst = Term fst
-  lit x = Term $ lit x
-  doublePlus = Term doublePlus
-  doubleMinus = Term doubleMinus
-  doubleMult = Term doubleMult
-  doubleDivide = Term doubleDivide
-  fix = Term fix
-  left = Term left
-  right = Term right
-  sumMatch = Term sumMatch
-  unit = Term unit
-  exfalso = Term exfalso
-  nothing = Term nothing
-  just = Term just
-  optionMatch = Term optionMatch
-  exp = Term exp
-  ioRet = Term ioRet
-  ioMap = Term ioMap
-  ioBind = Term ioBind
-  nil = Term nil
-  cons = Term cons
-  listMatch = Term listMatch
-  writer = Term writer
-  runWriter = Term runWriter
+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))
+
+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 r -> l) (hoas $ \x -> case f (Combine z x) of Combine l r -> r)
diff --git a/src/HOAS.hs b/src/HOAS.hs
deleted file mode 100644
--- a/src/HOAS.hs
+++ /dev/null
@@ -1,35 +0,0 @@
-{-# LANGUAGE
-    MultiParamTypeClasses,
-    RankNTypes,
-    ScopedTypeVariables,
-    FlexibleInstances,
-    FlexibleContexts,
-    UndecidableInstances,
-    IncoherentInstances,
-    PolyKinds,
-    LambdaCase,
-    MonomorphismRestriction #-}
-
-module HOAS where
-import Util
-
-class HOAS repr where
-  app :: repr (a -> b) -> repr a -> repr b
-  lam :: (repr a -> repr b) -> repr (a -> b)
-
-newtype Eval x = Eval {unEval :: x}
-
-instance HOAS Eval where
-  app (Eval f) (Eval x) = Eval (f x)
-  lam f = Eval (unEval . f . Eval)
-
-newtype HShow x = HShow {unHShow :: [String] -> String}
-
-instance HOAS HShow where
-  app (HShow f) (HShow x) = HShow (\vars -> "(" ++ f vars ++ " " ++ x vars ++ ")")
-  lam f = HShow (\(v:vars) -> "(\\" ++ v ++ " -> " ++ (unHShow $ f $ HShow $ const v) vars ++ ")")
-
-s = lam (\f -> lam (\x -> lam (\arg -> app (app f arg) (app x arg))))
-
-main :: IO ()
-main = putStrLn ((unHShow s) $ vars)
diff --git a/src/Lang.hs b/src/Lang.hs
new file mode 100644
--- /dev/null
+++ b/src/Lang.hs
@@ -0,0 +1,543 @@
+{-# LANGUAGE
+    MultiParamTypeClasses,
+    RankNTypes,
+    ScopedTypeVariables,
+    FlexibleInstances,
+    FlexibleContexts,
+    UndecidableInstances,
+    PolyKinds,
+    LambdaCase,
+    NoMonomorphismRestriction,
+    TypeFamilies,
+    LiberalTypeSynonyms,
+    FunctionalDependencies,
+    ExistentialQuantification,
+    InstanceSigs,
+    TupleSections,
+    ConstraintKinds,
+    DefaultSignatures,
+    UndecidableSuperClasses,
+    TypeOperators,
+    TypeApplications,
+    PartialTypeSignatures #-}
+
+module Lang where
+import DBI
+import qualified Prelude as P
+import Prelude (($), (.), (+), (-), (++), show, (>>=), (*), (/), undefined)
+import qualified Control.Monad.Writer as P
+import qualified Data.Functor.Identity as P
+import qualified GHC.Float as P
+import qualified Data.Tuple as P
+import Data.Void
+import Data.Proxy
+import Data.Proxy
+import Data.Constraint
+import Data.Constraint.Forall
+
+type instance Diff v (P.Writer w a) = P.Writer (Diff v w) (Diff v a)
+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 (P.Either a b) = P.Either (Diff v a) (Diff v b)
+type instance Diff v (P.Maybe a) = P.Maybe (Diff v a)
+type instance Diff v (P.IO a) = P.IO (Diff v a)
+type instance Diff v [a] = [Diff v a]
+
+class DBI 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])
+  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)
+
+class Reify repr x where
+  reify :: x -> repr h x
+
+instance Lang repr => Reify repr () where
+  reify _ = unit
+
+instance Lang repr => Reify repr P.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 Lang Eval where
+  zro = comb P.fst
+  fst = comb P.snd
+  mkProd = comb (,)
+  double = comb
+  doublePlus = comb (+)
+  doubleMinus = comb (-)
+  doubleMult = comb (*)
+  doubleDivide = comb (/)
+  fix = comb loop
+    where loop x = x $ loop x
+  left = comb P.Left
+  right = comb P.Right
+  sumMatch = comb $ \l r -> \case
+                             P.Left x -> l x
+                             P.Right x -> r x
+  unit = comb ()
+  exfalso = comb absurd
+  nothing = comb P.Nothing
+  just = comb P.Just
+  ioRet = comb P.return
+  ioBind = comb (>>=)
+  nil = comb []
+  cons = comb (:)
+  listMatch = comb $ \l r -> \case
+                            [] -> l
+                            x:xs -> r x xs
+  optionMatch = comb $ \l r -> \case
+                              P.Nothing -> l
+                              P.Just x -> r x
+  ioMap = comb P.fmap
+  writer = comb (P.WriterT . P.Identity)
+  runWriter = comb P.runWriter
+  doubleExp = comb P.exp
+  float = comb
+  floatPlus = comb (+)
+  floatMinus = comb (-)
+  floatMult = comb (*)
+  floatDivide = comb (/)
+  floatExp = comb P.exp
+  float2Double = comb P.float2Double
+  double2Float = comb P.double2Float
+
+instance Lang Show where
+  mkProd = name "mkProd"
+  zro = name "zro"
+  fst = name "fst"
+  double = name . show
+  doublePlus = name "plus"
+  doubleMinus = name "minus"
+  doubleMult = name "mult"
+  doubleDivide = name "divide"
+  doubleExp = name "exp"
+  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"
+
+instance Lang repr => Lang (GWDiff repr) where
+  mkProd = GWDiff (P.const mkProd)
+  zro = GWDiff $ P.const $ zro
+  fst = GWDiff $ P.const $ fst
+  double x = GWDiff $ P.const $ mkProd2 (double x) zero
+  doublePlus = GWDiff $ P.const $ lam2 $ \l r ->
+    mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))
+  doubleMinus = GWDiff $ P.const $ lam2 $ \l r ->
+    mkProd2 (minus2 (zro1 l) (zro1 r)) (minus2 (fst1 l) (fst1 r))
+  doubleMult = GWDiff $ P.const $ lam2 $ \l r ->
+    mkProd2 (mult2 (zro1 l) (zro1 r))
+      (plus2 (mult2 (zro1 l) (fst1 r)) (mult2 (zro1 r) (fst1 l)))
+  doubleDivide = GWDiff $ P.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 $ P.const $ lam $ \x -> mkProd2 (doubleExp1 (zro1 x)) (mult2 (doubleExp1 (zro1 x)) (fst1 x))
+  fix = GWDiff $ P.const fix
+  left = GWDiff $ P.const left
+  right = GWDiff $ P.const right
+  sumMatch = GWDiff $ P.const sumMatch
+  unit = GWDiff $ P.const unit
+  exfalso = GWDiff $ P.const exfalso
+  nothing = GWDiff $ P.const nothing
+  just = GWDiff $ P.const just
+  ioRet = GWDiff $ P.const ioRet
+  ioBind = GWDiff $ P.const ioBind
+  nil = GWDiff $ P.const nil
+  cons = GWDiff $ P.const cons
+  listMatch = GWDiff $ P.const listMatch
+  optionMatch = GWDiff $ P.const optionMatch
+  ioMap = GWDiff $ P.const ioMap
+  writer = GWDiff $ P.const writer
+  runWriter = GWDiff $ P.const runWriter
+  float x = GWDiff $ P.const $ mkProd2 (float x) zero
+  floatPlus = GWDiff $ P.const $ lam2 $ \l r ->
+    mkProd2 (plus2 (zro1 l) (zro1 r)) (plus2 (fst1 l) (fst1 r))
+  floatMinus = GWDiff $ P.const $ lam2 $ \l r ->
+    mkProd2 (minus2 (zro1 l) (zro1 r)) (minus2 (fst1 l) (fst1 r))
+  floatMult = GWDiff $ P.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 $ P.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 $ P.const $ lam $ \x -> mkProd2 (floatExp1 (zro1 x)) (mult2 (float2Double1 (floatExp1 (zro1 x))) (fst1 x))
+  float2Double = GWDiff $ P.const $ bimap2 float2Double id
+  double2Float = GWDiff $ P.const $ bimap2 double2Float id
+
+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
+
+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
+
+instance (Lang l, Lang r) => Lang (Combine l r) where
+  mkProd = Combine mkProd mkProd
+  zro = Combine zro zro
+  fst = Combine fst fst
+  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
+  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
+  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
+  nil = Combine nil nil
+  cons = Combine cons cons
+  listMatch = Combine listMatch listMatch
+  runWriter = Combine runWriter runWriter
+  writer = Combine writer writer
+  double2Float = Combine double2Float double2Float
+  float2Double = Combine float2Double float2Double
+
+instance Lang repr => WithDiff repr () where
+  withDiff = const1 id
+
+instance Lang repr => WithDiff repr P.Double where
+  withDiff = lam2 $ \conv d -> mkProd2 d (app conv doubleOne)
+
+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)
+  invert = minus1 zero
+  default minus :: Lang 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 (P.Double -> v -> v)
+  divide :: r h (v -> P.Double -> v)
+  default mult :: Lang r => r h (P.Double -> v -> v)
+  mult = lam2 $ \x y -> divide2 y (recip1 x)
+  default divide :: Lang r => r h (v -> P.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
+
+instance Lang r => Group r () where
+  invert = const1 unit
+  minus = const1 $ const1 unit
+
+instance Lang r => Vector r () where
+  mult = const1 $ const1 unit
+  divide = const1 $ const1 unit
+
+instance Lang r => Monoid r P.Double where
+  zero = doubleZero
+  plus = doublePlus
+
+instance Lang r => Group r P.Double where
+  minus = doubleMinus
+
+instance Lang r => Vector r P.Double where
+  mult = doubleMult
+  divide = doubleDivide
+
+instance Lang r => Monoid r P.Float where
+  zero = floatZero
+  plus = floatPlus
+
+instance Lang r => Group r P.Float where
+  minus = floatMinus
+
+instance Lang r => Vector r P.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
+  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
+  invert = bimap2 invert invert
+
+instance (Lang 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 l, Monoid repr r) => Monoid repr (l -> r) where
+  zero = const1 zero
+  plus = lam3 $ \l r x -> plus2 (app l x) (app r x)
+
+instance (Lang repr, Group repr l, Group repr r) => Group repr (l -> r) where
+  invert = lam2 $ \l x -> app l (invert1 x)
+
+instance (Lang repr, Vector repr l, Vector repr r) => Vector repr (l -> r) where
+  mult = lam3 $ \l r x -> app r (mult2 l x)
+
+instance Lang r => Monoid r [a] where
+  zero = nil
+  plus = listAppend
+
+instance Lang r => Functor r [] where
+  map = lam $ \f -> fix1 $ lam $ \self -> listMatch2 nil (lam2 $ \x xs -> cons2 (app f x) $ app self xs)
+
+instance Lang r => BiFunctor r (,) where
+  bimap = lam3 $ \l r p -> mkProd2 (app l (zro1 p)) (app r (fst1 p))
+
+instance Lang r => Functor r (P.Writer w) where
+  map = lam $ \f -> com2 writer (com2 (bimap2 f id) runWriter)
+
+instance (Lang r, Monoid r w) => Applicative r (P.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))))
+
+instance (Lang r, Monoid r w) => Monad r (P.Writer w) where
+  join = lam $ \x -> writer1 $ mkProd2 (zro1 $ runWriter1 $ zro1 $ runWriter1 x) (plus2 (fst1 $ runWriter1 $ zro1 $ runWriter1 x) (fst1 $ runWriter1 x))
+
+instance Lang r => Functor r P.IO where
+  map = ioMap
+
+instance Lang r => Applicative r P.IO where
+  pure = ioRet
+  ap = lam2 $ \f x -> ioBind2 f (flip2 ioMap x)
+
+instance Lang r => Monad r P.IO where
+  bind = ioBind
+
+instance Lang r => Functor r P.Maybe where
+  map = lam $ \func -> optionMatch2 nothing (com2 just func)
+
+instance Lang r => Applicative r P.Maybe where
+  pure = just
+  ap = optionMatch2 (const1 nothing) map
+
+instance Lang r => Monad r P.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))
+
+newtype GWDiff repr h x = GWDiff {runGWDiff :: forall v. Vector repr v => Proxy v -> repr (Diff v h) (Diff v x)}
+
+instance DBI repr => DBI (GWDiff repr) where
+  z = GWDiff (P.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)
+
+cons2 = app2 cons
+listMatch2 = app2 listMatch
+fix1 = app fix
+fix2 = app2 fix
+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
+recip1 = app recip
+writer1 = app writer
+runWriter1 = app runWriter
+ioBind2 = app2 ioBind
+minus2 = app2 minus
+float2Double1 = app float2Double
+doubleExp1 = app doubleExp
+floatExp1 = app floatExp
+
+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)
diff --git a/src/Main.hs b/src/Main.hs
deleted file mode 100644
--- a/src/Main.hs
+++ /dev/null
@@ -1,19 +0,0 @@
-{-# LANGUAGE
-    MultiParamTypeClasses,
-    RankNTypes,
-    ScopedTypeVariables,
-    FlexibleInstances,
-    FlexibleContexts,
-    UndecidableInstances,
-    IncoherentInstances,
-    PolyKinds,
-    LambdaCase,
-    NoMonomorphismRestriction #-}
-
-module Main (main) where
-import qualified HOAS
-import qualified Comb
-import qualified DBI
-import qualified Poly
-
-main = Poly.main
diff --git a/src/Poly.lhs b/src/Poly.lhs
--- a/src/Poly.lhs
+++ b/src/Poly.lhs
@@ -16,18 +16,19 @@
 > module Poly where
 > import Control.Monad (when)
 > import Util
-> import DBI hiding (main, return)
+> import DBI hiding (return)
+> import Lang
 
 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. DBI repr => repr h (Double -> Double)
-> poly = hlam $ \x -> plus2 (mult2 x x) (plus2 (mult2 (lit 2.0) x) (lit 3.0))
+> poly :: forall repr h. Lang repr => repr h (Double -> Double)
+> poly = lam $ \x -> plus2 (mult2 x x) (plus2 (mult2 (double 2.0) x) (double 3.0))
 
 poly x = x * x + (2 * x + 3)
 
-> l2 = hlam $ \x -> mult2 (minus2 x (lit 27)) (minus2 x (lit 27))
+> l2 = lam $ \x -> mult2 (minus2 x (double 27)) (minus2 x (double 27))
 
 l2 x = (x - 27) * (x - 27)
 l2 measure how far is the input from 27
diff --git a/src/Xor.lhs b/src/Xor.lhs
--- a/src/Xor.lhs
+++ b/src/Xor.lhs
@@ -1,22 +1,4 @@
-> {-# LANGUAGE
->     MultiParamTypeClasses,
->     RankNTypes,
->     ScopedTypeVariables,
->     FlexibleInstances,
->     FlexibleContexts,
->     UndecidableInstances,
->     PolyKinds,
->     LambdaCase,
->     NoMonomorphismRestriction,
->     TypeFamilies,
->     LiberalTypeSynonyms,
->     EmptyCase,
->     FunctionalDependencies,
->     ExistentialQuantification,
->     InstanceSigs,
->     TupleSections,
->     ConstraintKinds,
->     AllowAmbiguousTypes #-}
+> {-# LANGUAGE ScopedTypeVariables, NoMonomorphismRestriction, TypeApplications #-}
 
 This is the classical example of using sigmoid NN to approximate Xor.
 
@@ -28,6 +10,9 @@
 > import Util
 > import System.Random
 > import Control.Monad (when)
+> import Data.Proxy
+> import Data.Constraint
+> import Lang
 
 Recall in poly, we constructed a function Double -> Double,
 with argument being the weight, and do gradient descend to found a solution.
@@ -45,7 +30,7 @@
 
 Let's start by constructing a weight.
 
-> weight :: DBI repr => ImpW repr h Double
+> weight :: Lang repr => ImpW repr h Double
 > weight = ImpW id
 
 Note that we are just manipulating AST.
@@ -55,72 +40,72 @@
 
 We have the weight, now we need the activation function, sigmoid.
 
-> sigmoid = hlam $ \x -> recip1 (plus2 litOne (exp1 (invert1 x)))
+> 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.
 We then add the two scaled input, with the bias, and pass them into sigmoid.
 
-> scaleAdd :: DBI repr => ImpW repr h ((Double, Double) -> Double)
-> scaleAdd = ImpW $ hlam2 $ \w p -> plus2 (mult2 (zro1 w) (zro1 p)) (plus2 (fst1 w) (fst1 p))
+> scaleAdd :: Lang repr => ImpW repr h ((Double, Double) -> Double)
+> scaleAdd = ImpW $ lam2 $ \w p -> plus2 (mult2 (zro1 w) (zro1 p)) (plus2 (fst1 w) (fst1 p))
 
-> withBias :: DBI repr => ImpW repr h (Double -> Double)
+> withBias :: Lang repr => ImpW repr h (Double -> Double)
 > withBias = ImpW $ plus
 
-> neuron :: DBI repr => ImpW repr h ((Double, Double) -> Double)
+> neuron :: Lang repr => ImpW repr h ((Double, Double) -> Double)
 > neuron = com2 (com2 sigmoid withBias) scaleAdd
 > neuron1 = app neuron
 
 Now, the hidden layer of type (Double, Double) -> ((Double, Double), (Double, Double))
 
-> hidden = hlam $ \p -> mkProd2 (mkProd2 (neuron1 p) (neuron1 p)) (mkProd2 (neuron1 p) (neuron1 p))
+> 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 :: DBI repr => ImpW repr h XOR
+> xor :: Lang repr => ImpW repr h XOR
 > xor = neuron `com2` (bimap2 scaleAdd scaleAdd) `com2` hidden
 
 But before we can train it, we need to define the dataset and the loss function.
 
-> l2 :: DBI repr => repr h (Double -> Double -> Double)
-> l2 = hlam2 $ \l r -> (mult2 (minus2 l r) (minus2 l r))
+> l2 :: Lang repr => repr h (Double -> Double -> Double)
+> l2 = lam2 $ \l r -> (mult2 (minus2 l r) (minus2 l r))
 > l22 = app2 l2
 
-> eval :: DBI repr => repr h (XOR -> ((Double, Double), Double) -> Double)
-> eval = hlam2 $ \xor p -> l22 (app xor (zro1 p)) (fst1 p)
+> eval :: Lang repr => repr h (XOR -> ((Double, Double), Double) -> Double)
+> eval = lam2 $ \xor p -> l22 (app xor (zro1 p)) (fst1 p)
 
-> dataset :: DBI repr => repr h [((Double, Double), Double)]
+> dataset :: Lang repr => repr h [((Double, Double), 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 (lit l) (lit r)) (lit ret)
+>   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 :: DBI repr => repr h (XOR -> Double)
-> loss = hlam $ \xor -> fix2 (hlam $ \self -> listMatch2 litZero (hlam2 $ \x xs -> plus2 x (app self xs))) (map2 (app eval xor) dataset)
+> loss :: Lang repr => repr h (XOR -> Double)
+> loss = lam $ \xor -> fix2 (lam $ \self -> listMatch2 doubleZero (lam2 $ \x xs -> plus2 x (app self xs))) (map2 (app eval xor) dataset)
 
 Let's try to print the thing.
 
 > main :: IO ()
 > main = case runImpW $ noEnv xor of RunImpW xor -> inner xor
 >   where
->     inner :: forall w. Weight (Term DBI) w => Term DBI () (w -> (Double, Double) -> Double) -> IO ()
->     inner (Term xor) = do
->       print $ runShow xor vars 0
+>     inner :: forall w. Weight w => Combine Show (GWDiff Eval) () (w -> (Double, Double) -> Double) -> IO ()
+>     inner (Combine xorS xorE) = do
+>       print $ runShow xorS vars 0
 
 now you will see a list of gibberish
 
->       initWeight :: w <- randomRIO (randRange (-0.01, 0.01))
+>       initWeight :: w <- ((randomRIO (randRange (-0.01, 0.01)) \\ weightCon @w @Random) \\ weightCon @w @RandRange)
 
 Getting random weights...
 
->       diffAST (runWDiff xor :: Term DBI () (Diff w (w -> XOR))) initWeight
->         (selfWithDiff :: Term DBI () (w -> Diff w w)) (runWDiff $ noEnv loss :: Term DBI () (Diff w (XOR -> Double)))
->         ((hlam3 $ \d o n -> minus2 o (mult2 d n)) :: Term DBI () (Double -> w -> w -> w))
->     diffAST (Term xor) weight (Term wdiff) (Term loss) (Term update) =
->       go (runEval xor ()) weight (runEval wdiff ()) (runEval loss ()) (runEval update ()) 0
->     go :: forall w. P.Show w => (Diff w (w -> XOR)) -> w -> (w -> Diff w w) -> (Diff w (XOR -> Double)) -> (Double -> w -> w -> w) -> Int -> IO ()
+>       (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) \\ weightCon @w @P.Show
+>         where
+>           diff :: GWDiff Eval () x -> Diff w x
+>           diff x = (runEval (runGWDiff x (Proxy :: Proxy w)) ()) \\ weightCon @w @(Vector Eval)
+>     go :: P.Show w => (Diff w (w -> XOR)) -> w -> (w -> Diff w w) -> (Diff w (XOR -> Double)) -> (Double -> w -> w -> w) -> Int -> IO ()
 >     go xor weight reify loss update i | i <= 2500 = do
 >       when (isSquare i) $ do
 >         print weight