diff --git a/DDF/ImportMeta.hs b/DDF/ImportMeta.hs
--- a/DDF/ImportMeta.hs
+++ b/DDF/ImportMeta.hs
@@ -2,7 +2,7 @@
 
 module DDF.ImportMeta (module Prelude, module Data.Void, module Control.Monad.Writer, module Control.Monad.State, module Data.Constraint, module Data.Constraint.Forall, module Data.Proxy, module DDF.Util) where
 
-import Prelude (($), show, (+), (-), (*), (/), (.), (++), (>>=), (<=), (<), (==), compare, print, Maybe, String)
+import Prelude (($), show, (+), (-), (*), (/), (.), (++), (>>=), (<=), (<), (==), compare, print, Maybe, String, (||))
 import Data.Void (Void, absurd)
 import Control.Monad.Writer (Writer)
 import Control.Monad.State (State)
diff --git a/DDF/PE.hs b/DDF/PE.hs
--- a/DDF/PE.hs
+++ b/DDF/PE.hs
@@ -8,58 +8,70 @@
   IncoherentInstances,
   InstanceSigs,
   LambdaCase,
-  FlexibleContexts
+  FlexibleContexts,
+  KindSignatures,
+  TypeFamilies
 #-}
 
 module DDF.PE where
 
-import DDF.DBI
-import DDF.Double
+import DDF.Lang
 import qualified Prelude as M
 
 data P repr h a where
-  Unk :: repr h a -> P repr h a
-  Static :: a -> (forall h'. repr h' a) -> P repr h a
-  StaFun :: (forall hout. EnvT repr (a, h) hout -> P repr hout b) -> P repr h (a -> b)
   Open   :: (forall hout. EnvT repr h hout -> P repr hout a) -> P repr h a
+  Unk    :: repr h a -> P repr h a
+  Known  ::
+    K repr h a ->
+    repr h a ->
+    (forall hout. EnvT repr h hout -> P repr hout a) ->
+    (forall any. P repr (any, h) a) ->
+    (forall hh ht. (hh, ht) ~ h => P repr ht (hh -> a)) ->
+    P repr h a
 
+isOpen (Open _) = M.True
+isOpen _ = M.False
+type family   K (repr :: * -> * -> *) h a
+type instance K repr h (a, b)   = (P repr h a, P repr h b)
+type instance K repr h M.Bool   = M.Bool
+type instance K repr h M.Double = M.Double
+type instance K repr h (a -> b) = Fun repr h a b
+newtype Fun repr h a b = Fun {runFun :: forall hout. EnvT repr (a, h) hout -> P repr hout b}
+
+mkFun :: Prod repr => (forall hout. EnvT repr (a, h) hout -> P repr hout b) -> P repr h (a -> b)
+mkFun f = Known (Fun f) (abs $ dynamic (f Dyn)) (\h -> abs $ f $ Next h) (abs $ f $ Next Weak) (mkFun $ app_open (mkFun f))
+
 data EnvT repr hin hout where
   Dyn  :: EnvT repr hin hin
   Arg  :: P repr hout a -> EnvT repr (a, hout) hout
   Weak :: EnvT repr h (a, h)
   Next :: EnvT repr hin hout -> EnvT repr (a, hin) (a, hout)
 
-dynamic:: DBI repr => P repr h a -> repr h a
+dynamic:: Prod repr => P repr h a -> repr h a
 dynamic (Unk x)      = x
-dynamic (Static _ x) = x
-dynamic (StaFun f)   = abs $ dynamic (f Dyn)
 dynamic (Open f)     = dynamic (f Dyn)
+dynamic (Known _ d _ _ _)  = d
 
-app_open :: DBI repr => P repr hin r -> EnvT repr hin hout -> P repr hout r
-app_open e Dyn            = Unk (dynamic e)
-app_open (Static es ed) _ = Static es ed
-app_open (Open fs) h      = fs h
-app_open (StaFun fs) h    = abs (fs (Next h))
-app_open (Unk env) h      = Unk (app_unk env h) where
-  app_unk :: DBI repr => repr hin a -> EnvT repr hin hout -> repr hout a
-  app_unk e Dyn      = e
-  app_unk e (Arg p)  = app (abs e) (dynamic p)
-  app_unk e (Next h') = app (s (app_unk (abs e) h')) z
-  app_unk e Weak     = s e
+app_open :: Prod repr => P repr hin r -> EnvT repr hin hout -> P repr hout r
+app_open (Open fs) h       = fs h
+app_open (Unk e) Dyn       = Unk e
+app_open (Unk e) (Arg p)   = Unk (app (abs e) (dynamic p))
+app_open (Unk e) (Next h)  = app (s (app_open (Unk (abs e)) h)) z
+app_open (Unk e) Weak      = Unk (s e)
+app_open (Known _ _ x _ _) h = x h
 
-instance DBI r => DBI (P r) where
+instance Prod r => DBI (P r) where
   z = Open f where
     f :: EnvT r (a,h) hout -> P r hout a
-    f Dyn       = Unk z
-    f (Arg x)   = x
-    f (Next _)  = z
-    f Weak      = s z
+    f Dyn      = Unk z
+    f (Arg x)  = x
+    f (Next _) = z
+    f Weak     = s z
 
   s :: forall h a any. P r h a -> P r (any, h) a
   s (Unk x) = Unk (s x)
-  s (Static a ar) = Static a ar
-  s (StaFun fs) = abs (fs (Next Weak))
-  s p = Open f where
+  s (Known _ _ _ x _) = x
+  s p@(Open _) = Open f where
     f :: EnvT r (any, h) hout -> P r hout a
     f Dyn              = Unk (s (dynamic p))
     f (Arg _)          = p
@@ -67,70 +79,91 @@
     f Weak             = s (s p)
 
   abs (Unk f) = Unk (abs f)
-  abs (Static k ks) = StaFun $ \_ -> Static k ks
-  abs body = StaFun (app_open body)
-  
-  app (Unk f) (Unk x) = Unk (app f x)
-  app (StaFun fs) p   = fs (Arg p)
-  app (Static _ fs) p = Unk (app fs (dynamic p))
-  app e1 e2           = Open (\h -> app (app_open e1 h) (app_open e2 h))
+  abs o@(Open _) = mkFun (app_open o)
+  abs (Known _ _ _ _ x) = x
 
-instance Bool r => Bool (P r) where
-  bool x = Static x (bool x)
+  app (Known (Fun fs) _ _ _ _) p     = fs (Arg p)
+  app e1 e2 | isOpen e1 || isOpen e2 = Open (\h -> app (app_open e1 h) (app_open e2 h))
+  app f x                            = Unk (app (dynamic f) (dynamic x))
+
+instance (Prod r, Bool r) => Bool (P r) where
+  bool x = Known x (bool x) (\_ -> bool x) (bool x) (mkFun (\_ -> bool x))
   ite = lam3 (\l r b -> app2 (f b) l r)
     where
       f :: P r h M.Bool -> P r h (a -> a -> a)
-      f (Static M.True _) = const
-      f (Static M.False _) = const1 id
+      f (Known M.True _ _ _ _) = const
+      f (Known M.False _ _ _ _) = const1 id
       f (Unk x) = Unk (lam2 (\l r -> ite3 l r (s (s x))))
-      f x = Open (\h -> f (app_open x h))
+      f x@(Open _) = Open (\h -> f (app_open x h))
 
-instance Double r => Double (P r) where
-  double x = Static x (double x)
+instance (Prod r, Double r) => Double (P r) where
+  double x = Known x (double x) (\_ -> double x) (double x) (mkFun (\_ -> double x))
   doublePlus = abs (abs (f (s z) z))
     where
       f :: P r h M.Double -> P r h M.Double -> P r h M.Double
-      f (Static l _) (Static r _) = double (l + r)
-      f (Static 0 _) r = r
-      f l (Static 0 _) = l
-      f (Unk l) (Unk r) = Unk (doublePlus2 l r)
-      f l r = Open (\h -> f (app_open l h) (app_open r h))
+      f (Known l _ _ _ _) (Known r _ _ _ _) = double (l + r)
+      f (Known 0 _ _ _ _) r = r
+      f l (Known 0 _ _ _ _) = l
+      f l r | isOpen l || isOpen r = Open (\h -> f (app_open l h) (app_open r h))
+      f l r = Unk (doublePlus2 (dynamic l) (dynamic r))
   doubleMult = abs (abs (f (s z) z))
     where
       f :: P r h M.Double -> P r h M.Double -> P r h M.Double
-      f (Static l _) (Static r _) = double (l * r)
-      f (Static 0 _) _ = double 0
-      f _ (Static 0 _) = double 0
-      f l (Static 1 _) = l
-      f (Static 1 _) r = r
-      f (Unk l) (Unk r) = Unk (doubleMult2 l r)
-      f l r = Open (\h -> f (app_open l h) (app_open r h))
+      f (Known l _ _ _ _) (Known r _ _ _ _) = double (l * r)
+      f (Known 0 _ _ _ _) _ = double 0
+      f _ (Known 0 _ _ _ _) = double 0
+      f l (Known 1 _ _ _ _) = l
+      f (Known 1 _ _ _ _) r = r
+      f l r | isOpen l || isOpen r = Open (\h -> f (app_open l h) (app_open r h))
+      f l r = Unk (doubleMult2 (dynamic l) (dynamic r))
   doubleMinus = abs (abs (f (s z) z))
     where
       f :: P r h M.Double -> P r h M.Double -> P r h M.Double
-      f (Static l _) (Static r _) = double (l - r)
-      f l (Static 0 _) = l
-      f (Unk l) (Unk r) = Unk (doubleMinus2 l r)
-      f l r = Open (\h -> f (app_open l h) (app_open r h))
+      f (Known l _ _ _ _) (Known r _ _ _ _) = double (l - r)
+      f l (Known 0 _ _ _ _) = l 
+      f l r | isOpen l || isOpen r = Open (\h -> f (app_open l h) (app_open r h))
+      f l r = Unk (doubleMinus2 (dynamic l) (dynamic r))
   doubleDivide = abs (abs (f (s z) z))
     where
       f :: P r h M.Double -> P r h M.Double -> P r h M.Double
-      f (Static l _) (Static r _) = double (l / r)
-      f (Static 0 _) _ = double 0
-      f l (Static 1 _) = l
-      f (Unk l) (Unk r) = Unk (doubleDivide2 l r)
-      f l r = Open (\h -> f (app_open l h) (app_open r h))
+      f (Known l _ _ _ _) (Known r _ _ _ _) = double (l / r)
+      f (Known 0 _ _ _ _) _ = double 0
+      f l (Known 1 _ _ _ _) = l 
+      f l r | isOpen l || isOpen r = Open (\h -> f (app_open l h) (app_open r h))
+      f l r = Unk (doubleDivide2 (dynamic l) (dynamic r))
   doubleExp = abs (f z)
     where
       f :: P r h M.Double -> P r h M.Double
-      f (Static l _) = double (M.exp l) 
+      f (Known l _ _ _ _) = double (M.exp l) 
       f (Unk l) = Unk (doubleExp1 l)
-      f l = Open (\h -> f (app_open l h))
+      f l@(Open _) = Open (\h -> f (app_open l h))
   doubleEq = abs (abs (f (s z) z)) where
     f :: P r h M.Double -> P r h M.Double -> P r h M.Bool
-    f (Static l _) (Static r _) = bool (l == r)
-    f (Unk l) (Unk r) = Unk (doubleEq2 l r)
-    f l r = Open (\h -> f (app_open l h) (app_open r h))    
+    f (Known l _ _ _ _) (Known r _ _ _ _) = bool (l == r)
+    f l r | isOpen l || isOpen r = Open (\h -> f (app_open l h) (app_open r h))
+    f l r = Unk (doubleEq2 (dynamic l) (dynamic r))
 
-pe :: Double repr => P repr () a -> repr () a
+instance Prod r => Prod (P r) where
+  mkProd = abs (abs (f (s z) z))
+    where
+      f :: P r h a -> P r h b -> P r h (a, b)
+      f l r = Known (l, r)
+                (mkProd2 (dynamic l) (dynamic r))
+                (\h -> mkProd2 (app_open l h) (app_open r h))
+                (s (mkProd2 l r))
+                (mkFun $ \x -> mkProd2 (app_open l x) (app_open r x))
+  zro = abs (f z)
+    where
+      f :: P r h (a, b) -> P r h a
+      f (Known (l, _) _ _ _ _) = l
+      f (Unk p) = Unk (zro1 p)
+      f p = Open (\h -> f (app_open p h))
+  fst = abs (f z)
+    where
+      f :: P r h (a, b) -> P r h b
+      f (Known (_, r) _ _ _ _) = r
+      f (Unk p) = Unk (fst1 p)
+      f p = Open (\h -> f (app_open p h))
+
+pe :: Prod repr => P repr () a -> repr () a
 pe = dynamic
diff --git a/DeepDarkFantasy.cabal b/DeepDarkFantasy.cabal
--- a/DeepDarkFantasy.cabal
+++ b/DeepDarkFantasy.cabal
@@ -1,5 +1,5 @@
 name: DeepDarkFantasy
-version: 0.2017.8.13
+version: 0.2017.8.14
 cabal-version: 1.12
 build-type: Simple
 license: Apache
@@ -63,7 +63,7 @@
                    DDF.VectorTF
                    DDF.WithDiff
                    DDF.Y
-  build-depends: base >= 4.9.0.0 && <= 4.10.0.0,
+  build-depends: base >= 4.9.0.0 && < 5,
                  mtl -any,
                  random -any,
                  constraints -any,