diff --git a/DDF/DBI.hs b/DDF/DBI.hs
--- a/DDF/DBI.hs
+++ b/DDF/DBI.hs
@@ -118,7 +118,9 @@
 
 lam4 f = lam3 $ \a b c -> lam $ \d -> f a b c d
 
-app2 f a = app (app f a)
+app1 = app 
+
+app2 f a = app (app1 f a)
 
 app3 f a b = app (app2 f a b)
 
diff --git a/DDF/ImportMeta.hs b/DDF/ImportMeta.hs
--- a/DDF/ImportMeta.hs
+++ b/DDF/ImportMeta.hs
@@ -1,8 +1,16 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-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
+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(Just, Nothing), String, (||), Either(Left, Right))
 import Data.Void (Void, absurd)
 import Control.Monad.Writer (Writer)
 import Control.Monad.State (State)
diff --git a/DDF/List.hs b/DDF/List.hs
--- a/DDF/List.hs
+++ b/DDF/List.hs
@@ -13,4 +13,5 @@
 
 cons2 = app2 cons
 listMatch2 = app2 listMatch
+listMatch3 = app3 listMatch
 listAppend2 = app2 listAppend
diff --git a/DDF/PE.hs b/DDF/PE.hs
--- a/DDF/PE.hs
+++ b/DDF/PE.hs
@@ -31,14 +31,10 @@
 
 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 :: DBI 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
@@ -47,12 +43,12 @@
   Weak :: EnvT repr h (a, h)
   Next :: EnvT repr hin hout -> EnvT repr (a, hin) (a, hout)
 
-dynamic:: Prod repr => P repr h a -> repr h a
+dynamic:: DBI repr => P repr h a -> repr h a
 dynamic (Unk x)      = x
 dynamic (Open f)     = dynamic (f Dyn)
 dynamic (Known _ d _ _ _)  = d
 
-app_open :: Prod repr => P repr hin r -> EnvT repr hin hout -> P repr hout r
+app_open :: DBI 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))
@@ -60,7 +56,10 @@
 app_open (Unk e) Weak      = Unk (s e)
 app_open (Known _ _ x _ _) h = x h
 
-instance Prod r => DBI (P r) where
+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}
+
+instance DBI r => DBI (P r) where
   z = Open f where
     f :: EnvT r (a,h) hout -> P r hout a
     f Dyn      = Unk z
@@ -86,7 +85,9 @@
   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
+type instance K repr h M.Bool = M.Bool
+
+instance 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
@@ -96,7 +97,9 @@
       f (Unk x) = Unk (lam2 (\l r -> ite3 l r (s (s x))))
       f x@(Open _) = Open (\h -> f (app_open x h))
 
-instance (Prod r, Double r) => Double (P r) where
+type instance K repr h M.Double = M.Double
+
+instance 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
@@ -143,6 +146,8 @@
     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))
 
+type instance K repr h (a, b) = (P repr h a, P repr h b)
+
 instance Prod r => Prod (P r) where
   mkProd = abs (abs (f (s z) z))
     where
@@ -151,7 +156,7 @@
                 (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))
+                (mkFun $ \h -> mkProd2 (app_open l h) (app_open r h))
   zro = abs (f z)
     where
       f :: P r h (a, b) -> P r h a
@@ -165,5 +170,61 @@
       f (Unk p) = Unk (fst1 p)
       f p = Open (\h -> f (app_open p h))
 
-pe :: Prod repr => P repr () a -> repr () a
+type instance K repr h (M.Either a b) = M.Either (P repr h a) (P repr h b)
+instance Sum r => Sum (P r) where
+  left = abs (f z)
+    where
+      f :: P r h a -> P r h (M.Either a b)
+      f x = Known (Left x)
+              (left1 $ dynamic x)
+              (\h -> left1 $ app_open x h)
+              (s $ left1 x)
+              (mkFun $ \h -> left1 (app_open x h))
+  right = abs (f z)
+    where
+      f :: P r h b -> P r h (M.Either a b)
+      f x = Known (Right x)
+              (right1 $ dynamic x)
+              (\h -> right1 $ app_open x h)
+              (s $ right1 x)
+              (mkFun $ \h -> right1 $ app_open x h)
+  sumMatch = abs $ abs $ abs (f (s (s z)) (s z) z)
+    where
+      f :: P r h (a -> c) -> P r h (b -> c) -> P r h (M.Either a b) -> P r h c
+      f l _ (Known (M.Left x) _ _ _ _) = app l x
+      f _ r (Known (M.Right x) _ _ _ _) = app r x
+      f l r (Unk x) = Unk $ sumMatch3 (dynamic l) (dynamic r) x
+      f l r (Open x) = Open $ \h -> f (app_open l h) (app_open r h) (x h)
+
+instance Y r => Y (P r) where
+  y = Unk y -- naive strategy to avoid infinite loop in PE. Later might do infinite PE thx to laziness.
+
+type instance K repr h [a] = Maybe (P repr h a, P repr h [a])
+instance List repr => List (P repr) where
+  nil = Known Nothing nil (\_ -> nil) nil (mkFun $ \_ -> nil)
+  cons = abs $ abs (f (s z) z)
+    where
+      f :: P repr h a -> P repr h [a] -> P repr h [a]
+      f h t = Known (Just (h, t))
+                (cons2 (dynamic h) (dynamic t))
+                (\env -> cons2 (app_open h env) (app_open t env))
+                (s $ cons2 h t)
+                (mkFun $ \env -> cons2 (app_open h env) (app_open t env))
+  listMatch = abs $ abs $ abs (f (s $ s z) (s z) z)
+    where
+      f :: P repr h b -> P repr h (a -> [a] -> b) -> P repr h [a] -> P repr h b
+      f l _ (Known Nothing _ _ _ _) = l -- You know nothing, Jon Snow.
+      f _ r (Known (Just (h, t)) _ _ _ _) = app2 r h t
+      f l r (Unk x) = Unk $ listMatch3 (dynamic l) (dynamic r) x
+      f l r (Open x) = Open $ \h -> f (app_open l h) (app_open r h) (x h)
+  listAppend = abs $ abs (f (s z) z)
+    where
+      f :: P repr h [a] -> P repr h [a] -> P repr h [a]
+      f (Known Nothing _ _ _ _) r = r
+      f (Known (Just (h, t)) _ _ _ _) r = cons2 h (listAppend2 t r)
+      f l (Known Nothing _ _ _ _) = l
+      f l r | isOpen l || isOpen r = Open $ \h -> f (app_open l h) (app_open r h)
+      f l r = Unk (listAppend2 (dynamic l) (dynamic r))
+
+pe :: DBI repr => P repr () a -> repr () a
 pe = dynamic
diff --git a/DDF/Sum.hs b/DDF/Sum.hs
--- a/DDF/Sum.hs
+++ b/DDF/Sum.hs
@@ -9,6 +9,8 @@
   right :: r h (b -> Either a b)
   sumMatch :: r h ((a -> c) -> (b -> c) -> Either a b -> c)
 
+sumMatch1 = app1 sumMatch
 sumMatch2 = app2 sumMatch
+sumMatch3 = app3 sumMatch
 left1 = app left
 right1 = app right
diff --git a/DeepDarkFantasy.cabal b/DeepDarkFantasy.cabal
--- a/DeepDarkFantasy.cabal
+++ b/DeepDarkFantasy.cabal
@@ -1,5 +1,5 @@
 name: DeepDarkFantasy
-version: 0.2017.8.14
+version: 0.2017.8.15
 cabal-version: 1.12
 build-type: Simple
 license: Apache