diff --git a/DDF/Float.hs b/DDF/Float.hs
--- a/DDF/Float.hs
+++ b/DDF/Float.hs
@@ -1,3 +1,5 @@
+{-# Language NoMonomorphismRestriction #-}
+
 module DDF.Float (module DDF.Float, module DDF.DBI) where
 
 import DDF.DBI
@@ -14,3 +16,13 @@
   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)
+
+floatPlus1 = app1 floatPlus
+floatPlus2 = app2 floatPlus
+floatMinus1 = app1 floatMinus
+floatMinus2 = app2 floatMinus
+floatMult1 = app1 floatMult
+floatMult2 = app2 floatMult
+floatDivide1 = app1 floatDivide
+floatDivide2 = app2 floatDivide
+floatExp1 = app1 floatExp
diff --git a/DDF/Lang.hs b/DDF/Lang.hs
--- a/DDF/Lang.hs
+++ b/DDF/Lang.hs
@@ -294,7 +294,6 @@
 writer1 = app writer
 runWriter1 = app runWriter
 float2Double1 = app float2Double
-floatExp1 = app floatExp
 state1 = app state
 runState1 = app runState
 runState2 = app2 runState
diff --git a/DDF/PE.hs b/DDF/PE.hs
--- a/DDF/PE.hs
+++ b/DDF/PE.hs
@@ -10,7 +10,8 @@
   LambdaCase,
   FlexibleContexts,
   KindSignatures,
-  TypeFamilies
+  TypeFamilies,
+  TypeApplications
 #-}
 
 module DDF.PE where
@@ -29,10 +30,21 @@
     (forall hh ht. (hh, ht) ~ h => P repr ht (hh -> a)) ->
     P repr h a
 
+know :: DBI repr =>
+  K repr h a ->
+  repr h a ->
+  (forall hout. EnvT repr h hout -> P repr hout a) ->
+  (forall any. P repr (any, h) a) ->
+  P repr h a
+know a b c d = Known a b c d (mkFun c)
+
+static :: forall repr h a. DBI repr => (forall h'. (K repr h' a, repr h' a)) -> P repr h a
+static x = know (M.fst $ x @h) (M.snd x) (\_ -> static x) (static x)
+
 isOpen (Open _) = M.True
 isOpen _ = M.False
 
-type family   K (repr :: * -> * -> *) h a
+type family K (repr :: * -> * -> *) h a
 
 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))
@@ -86,9 +98,8 @@
   app f x                            = Unk (app (dynamic f) (dynamic x))
 
 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))
+  bool x = static (x, 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)
@@ -98,9 +109,8 @@
       f x@(Open _) = Open (\h -> f (app_open x h))
 
 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))
+  double x = static (x, 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
@@ -146,17 +156,58 @@
     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)
+type instance K repr h M.Float = M.Float
+instance Float r => Float (P r) where
+  float x = static (x, float x)
+  floatPlus = abs (abs (f (s z) z))
+    where
+      f :: P r h M.Float -> P r h M.Float -> P r h M.Float
+      f (Known l _ _ _ _) (Known r _ _ _ _) = float (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 (floatPlus2 (dynamic l) (dynamic r))
+  floatMult = abs (abs (f (s z) z))
+    where
+      f :: P r h M.Float -> P r h M.Float -> P r h M.Float
+      f (Known l _ _ _ _) (Known r _ _ _ _) = float (l * r)
+      f (Known 0 _ _ _ _) _ = float 0
+      f _ (Known 0 _ _ _ _) = float 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 (floatMult2 (dynamic l) (dynamic r))
+  floatMinus = abs (abs (f (s z) z))
+    where
+      f :: P r h M.Float -> P r h M.Float -> P r h M.Float
+      f (Known l _ _ _ _) (Known r _ _ _ _) = float (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 (floatMinus2 (dynamic l) (dynamic r))
+  floatDivide = abs (abs (f (s z) z))
+    where
+      f :: P r h M.Float -> P r h M.Float -> P r h M.Float
+      f (Known l _ _ _ _) (Known r _ _ _ _) = float (l / r)
+      f (Known 0 _ _ _ _) _ = float 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 (floatDivide2 (dynamic l) (dynamic r))
+  floatExp = abs (f z)
+    where
+      f :: P r h M.Float -> P r h M.Float
+      f (Known l _ _ _ _) = float (M.exp l) 
+      f (Unk l) = Unk (floatExp1 l)
+      f l@(Open _) = Open (\h -> f (app_open l h))
 
+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
       f :: P r h a -> P r h b -> P r h (a, b)
-      f l r = Known (l, r)
+      f l r = know (l, r)
                 (mkProd2 (dynamic l) (dynamic r))
                 (\h -> mkProd2 (app_open l h) (app_open r h))
                 (s (mkProd2 l r))
-                (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
@@ -175,19 +226,17 @@
   left = abs (f z)
     where
       f :: P r h a -> P r h (M.Either a b)
-      f x = Known (Left x)
+      f x = know (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)
+      f x = know (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
@@ -201,15 +250,14 @@
 
 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)
+  nil = static (Nothing, 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))
+      f h t = know (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
@@ -225,6 +273,24 @@
       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))
+
+type instance K repr h (Maybe a) = Maybe (P repr h a)
+instance Option repr => Option (P repr) where
+  nothing = static (Nothing, nothing)
+  just = abs (f z)
+    where
+      f :: P repr h a -> P repr h (Maybe a)
+      f x = know (Just x)
+              (just1 $ dynamic x)
+              (\h -> just1 $ app_open x h)
+              (just1 $ s x)
+  optionMatch = abs $ abs $ abs (f (s (s z)) (s z) z)
+    where
+      f :: P repr h b -> P repr h (a -> b) -> P repr h (Maybe a) -> P repr h b
+      f l _ (Known Nothing _ _ _ _) = l
+      f _ r (Known (Just x) _ _ _ _) = app r x
+      f l r (Unk x) = Unk $ optionMatch3 (dynamic l) (dynamic r) x
+      f l r (Open x) = Open $ \h -> f (app_open l h) (app_open r h) (x h)
 
 pe :: DBI 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.15
+version: 0.2017.8.16
 cabal-version: 1.12
 build-type: Simple
 license: Apache