diff --git a/Makefile b/Makefile
deleted file mode 100644
--- a/Makefile
+++ /dev/null
@@ -1,1 +0,0 @@
-include ../cho-home-cabal-make.inc
diff --git a/README b/README
deleted file mode 100644
--- a/README
+++ /dev/null
@@ -1,11 +0,0 @@
-project-foo [1] is a template for a package, to make it easy to copy &
-modify.  It uses cabal-make [2] for convenience.  It's even equipped with
-a darcs repo.  Copy the directory ("cp -rp"), "darcs mv" and edit the
-.cabal file, edit README and wikipage.tw, and "rm _darcs/prefs/*repo*".
-Then add new content with "make check-add" and "make add-new".  "darcs
-record" the changes.  When ready, do a "darcs put" or "make repo".
-
-References:
-
-[1] http://haskell.org/haskellwiki/project-foo
-
diff --git a/functor-combo.cabal b/functor-combo.cabal
--- a/functor-combo.cabal
+++ b/functor-combo.cabal
@@ -1,5 +1,5 @@
 Name:                functor-combo
-Version:             0.0.7
+Version:             0.0.8
 Cabal-Version:       >= 1.2
 Synopsis:            Functor combinators with tries & zippers
 Category:            Data
@@ -29,8 +29,9 @@
   Extensions:
   Build-Depends:       base<5, TypeCompose >= 0.8, containers, data-inttrie, lub
   Exposed-Modules:     
+                       FunctorCombo.Strict
                        FunctorCombo.Functor
-                       FunctorCombo.Lub
+                       FunctorCombo.LubF
                        FunctorCombo.Derivative
                        FunctorCombo.Holey
                        FunctorCombo.DHoley
diff --git a/src/FunctorCombo/DHoley.hs b/src/FunctorCombo/DHoley.hs
--- a/src/FunctorCombo/DHoley.hs
+++ b/src/FunctorCombo/DHoley.hs
@@ -132,11 +132,11 @@
 
 -- At first it was a bit disappointing that extract is so complicated for
 -- functor composition, but I played a bit with the code and tweak2 can be
--- simplified (if I didn’t make a mistake) to:
+-- simplified (if I didn't make a mistake) to:
 
 -- tweak2 (dgfa, fl) = (fmap.first) (O dgfa :*:) fl
 
--- It’s interesting that (tweak2 . second extract) is very much like down!
+-- It's interesting that (tweak2 . second extract) is very much like down!
 -- Probably because Fix f is like repeated functor composition of f.
 
 tweak2 :: Functor f => (dg (f a), f (df a, a)) -> f (((dg :. f) :*: df) a, a)
diff --git a/src/FunctorCombo/Functor.hs b/src/FunctorCombo/Functor.hs
--- a/src/FunctorCombo/Functor.hs
+++ b/src/FunctorCombo/Functor.hs
@@ -16,6 +16,7 @@
   (
     Const(..),Void,voidF,Unit,unit,Id(..),unId,inId,inId2,(:+:)(..),eitherF
   , (:*:)(..),(:.)(..),unO,inO,inO2,(~>)
+  , Lift(..), (:*:!)(..), (:+:!)(..), eitherF'
   , pairF, unPairF, inProd, inProd2
   ) where
 
@@ -53,10 +54,10 @@
 --   newtype Id a = Id a
 
 -- | Product on unary type constructors
-data (f :*: g) a = f a :*: g a deriving (Show)
+data (f :*: g) a = f a :*: g a deriving (Show,Functor)
 
 -- | Sum on unary type constructors
-data (f :+: g) a = InL (f a) | InR (g a) deriving (Show)
+data (f :+: g) a = InL (f a) | InR (g a) deriving (Show,Functor)
 
 eitherF :: (f a -> b) -> (g a -> b) -> (f :+: g) a -> b
 eitherF p _ (InL fa) = p fa
@@ -87,7 +88,6 @@
 -- TODO: replace explicit definition with deriving, when the compiler fix
 -- has been around for a while.
 
-
 -- instance Functor Id where
 --   fmap h (Id a) = Id (h a)
 
@@ -102,13 +102,13 @@
 --     fmap h . InL  ==  InL . fmap h
 --     fmap h . InR  ==  InR . fmap h
 
-deriving instance (Functor f, Functor g) => Functor (f :+: g)
+-- deriving instance (Functor f, Functor g) => Functor (f :+: g)
 
 -- instance (Functor f, Functor g) => Functor (f :*: g) where
 --   fmap h (fa :*: ga) = fmap h fa :*: fmap h ga
 
 -- Or:
-deriving instance (Functor f, Functor g) => Functor (f :*: g)
+-- deriving instance (Functor f, Functor g) => Functor (f :*: g)
 
 -- TODO: Verify that the deriving instances are equivalent to the explicit versions.
 
@@ -127,6 +127,12 @@
   pure a = pure a :*: pure a
   (f :*: g) <*> (a :*: b) = (f <*> a) :*: (g <*> b)
 
+-- instance (Applicative f, Applicative g) => Applicative (f :+: g) where
+--   -- pure = ?? -- could use either 'InL . pure' or 'InR . pure'
+--   InL f <*> InL a = InL (f <*> a)
+--   InR g <*> InR b = InR (g <*> b)
+--   _ <*> _ = error "(<*>) on f :+: g: structural mismatch"
+
 -- instance (Functor g, Functor f) => Functor (g :. f) where
 --   fmap = inO.fmap.fmap
 
@@ -156,3 +162,43 @@
 inProd2 :: ((f a , g a) -> (h b , i b) -> (j c , k c))
         -> ((f :*: g) a -> (h :*: i) b -> (j :*: k) c)
 inProd2 = unPairF ~> inProd
+
+
+{--------------------------------------------------------------------
+    Explicit non-strictness
+--------------------------------------------------------------------}
+
+-- Idea: make all non-strictness explicit via unlifted product & sums,
+-- and explicit lifting.  Note that Id and Const are already strict.
+
+-- | Add a bottom to a type
+data Lift a = Lift { unLift :: a } deriving Functor
+
+infixl 6 :+:!
+infixl 7 :*:!
+
+-- | Strict product functor
+
+-- data (f :*:! g) a = (:*:!) { pfst :: !(f a), psnd :: !(g a) } deriving Functor
+
+data (f :*:! g) a = !(f a) :*:! !(g a) deriving Functor
+
+-- pfst :: (f :*:! g) a -> f a
+-- pfst (fa :*:! _) = fa
+
+-- psnd :: (f :*:! g) a -> g a
+-- psnd (_ :*:! ga) = ga
+
+-- t1 :: Id Int
+-- t1 = psnd (undefined :*:! Id 3)   -- *** Id Exception: Prelude.undefined
+
+-- t1 :: Id Int
+-- t1 = x where x :*:! _ = undefined :*:! Id 3   -- *** Id Exception: Prelude.undefined
+
+-- | Strict sum functor
+data (f :+:! g) a = InL' !(f a) | InR' !(g a) deriving Functor
+
+-- | Case analysis on strict sum functor
+eitherF' :: (f a -> c) -> (g a -> c) -> ((f :+:! g) a -> c)
+eitherF' p _ (InL' fa) = p fa
+eitherF' _ q (InR' ga) = q ga
diff --git a/src/FunctorCombo/Lub.hs b/src/FunctorCombo/Lub.hs
deleted file mode 100644
--- a/src/FunctorCombo/Lub.hs
+++ /dev/null
@@ -1,64 +0,0 @@
-{-# LANGUAGE StandaloneDeriving, TypeOperators, FlexibleContexts #-}
-{-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
-----------------------------------------------------------------------
--- |
--- Module      :  FunctorCombo.Lub
--- Copyright   :  (c) Conal Elliott 2010
--- License     :  GPL-3
--- 
--- Maintainer  :  conal@conal.net
--- Stability   :  experimental
--- 
--- Least upper bounds for functor combinators
-----------------------------------------------------------------------
-
-module FunctorCombo.Lub (HasLubF) where
-
-import Data.Lub
-
-import FunctorCombo.Functor
-
--- deriving instance HasLub a => HasLub (Id a)
-
--- Kills ghc: genDerivBinds: bad derived class lub-0.0.6:Data.Lub.HasLub{tc r3S}
-
--- ghc: panic! (the 'impossible' happened)
---   (GHC version 6.12.1 for i386-apple-darwin):
--- 	genDerivBinds: bad derived class lub-0.0.6:Data.Lub.HasLub{tc r3S}
-
-{-
-
-instance HasLub a => HasLub (Id a) where
-  lub = inId2 lub
-
-instance (HasLub a, HasLub (f a), HasLub (g a))
-  => HasLub ((f :*: g) a) where
-    lub = inProd2 lub
-
--}
-
-{--------------------------------------------------------------------
-    Functor-level lubs
---------------------------------------------------------------------}
-
-class HasLubF f where
-  lubF :: HasLub v => f v -> f v -> f v
-
--- instance HasLubF Id where lubF = lub
-
--- instance (HasLubF f, HasLubF g) => HasLubF (f :*: g) where lubF = lub
-
--- Could not deduce (HasLub (f v), HasLub (g v)) from the context (HasLub v)
-
-
-instance HasLubF Id where lubF = inId2 lub
-
--- instance (HasLubF f, HasLubF g) => HasLubF (f :*: g) where lubF = inProd2 lub
-
--- Same error.
-
-
-instance (HasLubF f, HasLubF g) => HasLubF (f :*: g) where
-  (p :*: q) `lubF` (r :*: s) = (p `lubF` r) :*: (q `lubF` s)
-
--- TODO: Fix to match lub on pairs.  Sublety with strictness.
diff --git a/src/FunctorCombo/LubF.hs b/src/FunctorCombo/LubF.hs
new file mode 100644
--- /dev/null
+++ b/src/FunctorCombo/LubF.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE StandaloneDeriving, TypeOperators, FlexibleContexts #-}
+{-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
+----------------------------------------------------------------------
+-- |
+-- Module      :  FunctorCombo.LubF
+-- Copyright   :  (c) Conal Elliott 2010
+-- License     :  GPL-3
+-- 
+-- Maintainer  :  conal@conal.net
+-- Stability   :  experimental
+-- 
+-- Least upper bounds for functor combinators
+----------------------------------------------------------------------
+
+module FunctorCombo.LubF (HasLubF) where
+
+import Data.Lub
+
+import FunctorCombo.Functor
+
+-- deriving instance HasLub a => HasLub (Id a)
+
+-- Kills ghc: genDerivBinds: bad derived class lub-0.0.6:Data.Lub.HasLub{tc r3S}
+
+-- ghc: panic! (the 'impossible' happened)
+--   (GHC version 6.12.1 for i386-apple-darwin):
+-- 	genDerivBinds: bad derived class lub-0.0.6:Data.Lub.HasLub{tc r3S}
+
+{-
+
+instance HasLub a => HasLub (Id a) where
+  lub = inId2 lub
+
+instance (HasLub a, HasLub (f a), HasLub (g a))
+  => HasLub ((f :*: g) a) where
+    lub = inProd2 lub
+
+-}
+
+{--------------------------------------------------------------------
+    Functor-level lubs
+--------------------------------------------------------------------}
+
+class HasLubF f where
+  lubF :: HasLub v => f v -> f v -> f v
+
+-- instance HasLubF Id where lubF = lub
+
+-- instance (HasLubF f, HasLubF g) => HasLubF (f :*: g) where lubF = lub
+
+-- Could not deduce (HasLub (f v), HasLub (g v)) from the context (HasLub v)
+
+
+instance HasLubF Id where lubF = inId2 lub
+
+-- instance (HasLubF f, HasLubF g) => HasLubF (f :*: g) where lubF = inProd2 lub
+
+-- Same error.
+
+
+instance (HasLubF f, HasLubF g) => HasLubF (f :*: g) where
+  (p :*: q) `lubF` (r :*: s) = (p `lubF` r) :*: (q `lubF` s)
+
+-- TODO: Fix to match lub on pairs.  Sublety with strictness.
diff --git a/src/FunctorCombo/MemoTrie.hs b/src/FunctorCombo/MemoTrie.hs
deleted file mode 100644
--- a/src/FunctorCombo/MemoTrie.hs
+++ /dev/null
@@ -1,407 +0,0 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, UndecidableInstances, CPP
- #-}
-{-# OPTIONS_GHC -Wall #-}
-{-# OPTIONS_GHC -fno-warn-unused-binds -fno-warn-unused-imports #-}  -- temporary while testing
-----------------------------------------------------------------------
--- |
--- Module      :  FunctorCombo.MemoTrie
--- Copyright   :  (c) Conal Elliott 2010
--- License     :  BSD3
--- 
--- Maintainer  :  conal@conal.net
--- Stability   :  experimental
--- 
--- Functor-based memo tries
--- 
-----------------------------------------------------------------------
-
-module FunctorCombo.MemoTrie
-  (
-    HasTrie(..),memo,memo2,memo3
-  ) where
-
-#define NonstrictMemo
-
-import Control.Arrow (first)
-import Control.Applicative ((<$>))
-
-import qualified Data.IntTrie as IT  -- data-inttrie
-import Data.Tree
-
-import Control.Compose (result)  -- TypeCompose
-
-#ifdef NonstrictMemo
-import Data.Lub
-#endif
-
-import FunctorCombo.Functor
-import FunctorCombo.Regular
-
-
-{--------------------------------------------------------------------
-    Misc
---------------------------------------------------------------------}
-
-type Unop a = a -> a
-
-bool :: a -> a -> Bool -> a
-bool t e b = if b then t else e
-
-
-{--------------------------------------------------------------------
-    Class
---------------------------------------------------------------------}
-
-infixr 0 :->:
-
-#ifdef NonstrictMemo
-data Trie k v = Trie v (STrie k v)
-
-type k :->: v = Trie k v
-
--- Bottom
-bottom :: a
-bottom = error "MemoTrie: evaluated bottom.  Oops!"
-
--- | Create the trie for the entire domain of a function
-trie   :: HasLub(v) => HasTrie k => (k  ->  v) -> (k :->: v)
-trie f = Trie (f bottom) (sTrie f)
-
--- | Convert k trie to k function, i.e., access k field of the trie
-untrie :: HasLub(v) => HasTrie k => (k :->: v) -> (k  ->  v)
-untrie (Trie b t) = const b `lub` sUntrie t
-
-#else
-type Trie k = STrie k
-
-type k :->: v = k :-> v
-
--- Bogus HasLub constraint
-#define HasLub(v) ()
-
-trie   :: HasTrie k => (k  ->  v) -> (k :->: v)
-trie = sTrie
-
-untrie :: HasTrie k => (k :->: v) -> (k  ->  v)
-untrie = sUntrie
-
-#endif
-
--- | Memo trie from k to v
-type k :-> v = STrie k v
-
--- | Domain types with associated memo tries
-class HasTrie k where
-    -- | Representation of trie with domain type @a@
-    type STrie k :: * -> *
-    -- | Create the trie for the entire domain of a function
-    sTrie   :: HasLub(v) => (k  ->  v) -> (k :-> v)
-    -- | Convert k trie to k function, i.e., access k field of the trie
-    sUntrie :: HasLub(v) => (k :-> v) -> (k  ->  v)
-
---     -- | List the trie elements.  Order of keys (@:: k@) is always the same.
---     enumerate :: HasLub(v) => (k :-> v) -> [(k,v)]
-
--- -- | Domain elements of a trie
--- domain :: HasTrie a => [a]
--- domain = map fst (enumerate (trie (const oops)))
---  where
---    oops = error "Data.MemoTrie.domain: range element evaluated."
-
-
--- TODO: what about enumerate and strict/nonstrict?
-
-
-{--------------------------------------------------------------------
-    Memo functions
---------------------------------------------------------------------}
-
--- | Trie-based function memoizer
-memo :: HasLub(v) => HasTrie k => Unop (k -> v)
-memo = untrie . trie
-
--- | Memoize a binary function, on its first argument and then on its
--- second.  Take care to exploit any partial evaluation.
-memo2 :: HasLub(a) => (HasTrie s,HasTrie t) => Unop (s -> t -> a)
-
--- | Memoize a ternary function on successive arguments.  Take care to
--- exploit any partial evaluation.
-memo3 :: HasLub(a) => (HasTrie r,HasTrie s,HasTrie t) => Unop (r -> s -> t -> a)
-
--- | Lift a memoizer to work with one more argument.
-mup :: HasLub(c) => HasTrie t => (b -> c) -> (t -> b) -> (t -> c)
-mup mem f = memo (mem . f)
-
-memo2 = mup memo
-memo3 = mup memo2
-
-{--------------------------------------------------------------------
-    Instances
---------------------------------------------------------------------}
-
-instance HasTrie () where
-  type STrie ()  = Id
-  sTrie   f      = Id (f ())
-  sUntrie (Id v) = const v
---   enumerate (Id a) = [((),a)]
-
-instance (HasTrie a, HasTrie b) => HasTrie (Either a b) where
-  type STrie (Either a b) = Trie a :*: Trie b
-  sTrie   f           = trie (f . Left) :*: trie (f . Right)
-  sUntrie (ta :*: tb) = untrie ta `either` untrie tb
---   enumerate (ta :*: tb) = enum' Left ta `weave` enum' Right tb
-
--- enum' :: HasLub(b) => HasTrie a => (a -> a') -> (a :->: b) -> [(a', b)]
--- enum' f = (fmap.first) f . enumerate
-
--- weave :: [a] -> [a] -> [a]
--- [] `weave` as = as
--- as `weave` [] = as
--- (a:as) `weave` bs = a : (bs `weave` as)
-
--- To do: rethink enumerate and come back to it.  How might enumeration
--- work in the presence of nonstrict memo tries?  Maybe lub the
--- approximation into each of the values enumerated from the strict memo tries.
--- Would it help any??
-
-instance (HasTrie a, HasTrie b) => HasTrie (a , b) where
-  type STrie (a , b) = Trie a :. Trie b
-  sTrie   f = O (trie (trie . curry f))
-  sUntrie (O tt) = uncurry (untrie . untrie tt)
---   enumerate (O tt) =
---     [ ((a,b),x) | (a,t) <- enumerate tt , (b,x) <- enumerate t ]
-
--- Oops:
--- 
---     Could not deduce (HasLub (Trie b v)) from the context (HasLub v)
---       arising from a use of `trie'
--- 
---     Could not deduce (HasLub (Trie b v)) from the context (HasLub v)
---       arising from a use of `untrie'
-
--- Eep.  How to fix this one?
-
-{-
-
-
-#define HasTrieIsomorph(Context,Type,IsoType,toIso,fromIso) \
-instance Context => HasTrie (Type) where { \
-  type STrie (Type) = Trie (IsoType); \
-  sTrie f = sTrie (f . (fromIso)); \
-  sUntrie t = sUntrie t . (toIso); \
-  enumerate = (result.fmap.first) (fromIso) enumerate; \
-}
-
-
-HasTrieIsomorph( (), Bool, Either () ()
-               , bool (Left ()) (Right ())
-               , either (\ () -> True) (\ () -> False))
-
-HasTrieIsomorph((HasTrie a, HasTrie b, HasTrie c), (a,b,c), ((a,b),c)
-               , \ (a,b,c) -> ((a,b),c), \ ((a,b),c) -> (a,b,c))
-
-HasTrieIsomorph((HasTrie a, HasTrie b, HasTrie c, HasTrie d)
-               , (a,b,c,d), ((a,b,c),d)
-               , \ (a,b,c,d) -> ((a,b,c),d), \ ((a,b,c),d) -> (a,b,c,d))
-
-
--- As well as the functor combinators themselves
-
-HasTrieIsomorph( HasTrie x, Const x a, x, getConst, Const )
-
-HasTrieIsomorph( HasTrie a, Id a, a, unId, Id )
-
-HasTrieIsomorph( (HasTrie (f a), HasTrie (g a))
-               , (f :*: g) a, (f a,g a)
-               , \ (fa :*: ga) -> (fa,ga), \ (fa,ga) -> (fa :*: ga) )
-
-HasTrieIsomorph( (HasTrie (f a), HasTrie (g a))
-               , (f :+: g) a, Either (f a) (g a)
-               , eitherF Left Right, either InL InR )
-
-HasTrieIsomorph( HasTrie (g (f a))
-               , (g :. f) a, g (f a) , unO, O )
-
-
--- newtype ListTrie a v = ListTrie (PF [a] [a] :-> v)
--- instance HasTrie a => HasTrie [a] where
---   type STrie [a] = ListTrie a
---   sTrie f = ListTrie (trie (f . wrap))
---   sUntrie (ListTrie t) = sUntrie t . unwrap
---   enumerate (ListTrie t) = (result.fmap.first) wrap enumerate $ t
--- HasTrieIsomorph( HasTrie (PF ([a]) ([a]) :->: v)
---                , ListTrie a v, PF ([a]) ([a]) :->: v
---                , \ (ListTrie w) -> w, ListTrie )
-
-
--- Works.  Now abstract into a macro
-
-#define HasTrieRegular(Context,Type,TrieType,TrieCon) \
-newtype TrieType v = TrieCon (PF (Type) (Type) :->: v); \
-instance Context => HasTrie (Type) where { \
-  type STrie (Type) = TrieType; \
-  sTrie f = TrieCon (sTrie (f . wrap)); \
-  sUntrie (TrieCon t) = sUntrie t . unwrap; \
-  enumerate (TrieCon t) = (result.fmap.first) wrap enumerate t; \
-}; \
-HasTrieIsomorph( HasTrie (PF (Type) (Type) :->: v) \
-               , TrieType v, PF (Type) (Type) :->: v \
-               , \ (TrieCon w) -> w, TrieCon )
-
--- For instance,
-
--- HasTrieRegular(HasTrie a, [a]   , ListTrie a, ListTrie)
--- HasTrieRegular(HasTrie a, Tree a, TreeTrie a, TreeTrie)
-
--- Simplify a bit with a macro for unary regular types.
--- Make similar defs for binary etc as needed.
-
-#define HasTrieRegular1(TypeCon,TrieCon) \
-HasTrieRegular(HasTrie a, TypeCon a, TrieCon a, TrieCon)
-
-HasTrieRegular1([]  , ListTrie)
-HasTrieRegular1(Tree, TreeTrie)
-
-
--- HasTrieIsomorph(Context,Type,IsoType,toIso,fromIso)
-
--- HasTrieIsomorph( HasTrie (PF [a] [a] :->: v)
---                , ListTrie a v, PF [a] [a] :->: v
---                , \ (ListTrie w) -> w, ListTrie )
-
-
-enumerateEnum :: (Enum k, Num k, HasTrie k) => (k :->: v) -> [(k,v)]
-enumerateEnum t = [(k, f k) | k <- [0 ..] `weave` [-1, -2 ..]]
- where
-   f = untrie t
-
-#define HasTrieIntegral(Type) \
-instance HasTrie Type where { \
-  type STrie Type = IT.IntTrie; \
-  sTrie   = (<$> IT.identity); \
-  sUntrie = IT.apply; \
-  enumerate = enumerateEnum; \
-}
-
-HasTrieIntegral(Int)
-HasTrieIntegral(Integer)
-
-
--- Memoizing higher-order functions
-
-HasTrieIsomorph((HasTrie a, HasTrie (a :->: b)), a -> b, a :->: b, trie, untrie)
-
-
-{-
-
-{--------------------------------------------------------------------
-    Testing
---------------------------------------------------------------------}
-
-fib :: Integer -> Integer
-fib m = mfib m
- where
-   mfib = memo fib'
-   fib' 0 = 0
-   fib' 1 = 1
-   fib' n = mfib (n-1) + mfib (n-2)
-
--- The eta-redex in fib is important to prevent a CAF.
-
-
--}
-
-ft1 :: (Bool -> a) -> [a]
-ft1 f = [f False, f True]
-
-f1 :: Bool -> Int
-f1 False = 0
-f1 True  = 1
-
-trie1a :: HasTrie a => (Bool -> a) :->: [a]
-trie1a = trie ft1
-
-trie1b :: HasTrie a => (Bool :->: a) :->: [a]
-trie1b = trie1a
-
-trie1c :: HasTrie a => (Either () () :->: a) :->: [a]
-trie1c = trie1a
-
-trie1d :: HasTrie a => ((Trie () :*: Trie ()) a) :->: [a]
-trie1d = trie1a
-
-trie1e :: HasTrie a => (Trie () a, Trie () a) :->: [a]
-trie1e = trie1a
-
-trie1f :: HasTrie a => (() :->: a, () :->: a) :->: [a]
-trie1f = trie1a
-
-trie1g :: HasTrie a => (a, a) :->: [a]
-trie1g = trie1a
-
-trie1h :: HasTrie a => (Trie a :. Trie a) [a]
-trie1h = trie1a
-
-trie1i :: HasTrie a => a :->: a :->: [a]
-trie1i = unO trie1a
-
-
-ft2 :: ([Bool] -> Int) -> Int
-ft2 f = f (alts 15)
-
-alts :: Int -> [Bool]
-alts n = take n (cycle [True,False])
-
-f2 :: [Bool] -> Int
-f2 = length . filter id
-
--- Memoization fails:
-
--- *FunctorCombo.MemoTrie> ft2 f2
--- 8
--- *FunctorCombo.MemoTrie> memo ft2 f2
--- ... (hang forever) ...
-
--- Would nonstrict memoization work?  <http://conal.net/blog/posts/nonstrict-memoization/>
-
-f3 :: Bool -> Integer
-f3 = const 3
-
--- *FunctorCombo.MemoTrie> f3 undefined
--- 3
--- *FunctorCombo.MemoTrie> memo f3 undefined
--- *** Exception: Prelude.undefined
-
-f4 :: () -> Integer
-f4 = const 4
-
--- *FunctorCombo.MemoTrie> f4 undefined
--- 4
--- *FunctorCombo.MemoTrie> memo f4 undefined
--- 4
-
-f5 :: ((),()) -> Integer
-f5 = const 5
-
--- *FunctorCombo.MemoTrie> f5 undefined
--- 5
--- *FunctorCombo.MemoTrie> memo f5 undefined
--- 5
-
-f6 :: Either () () -> Integer
-f6 = const 6
-
--- *FunctorCombo.MemoTrie> f6 undefined
--- 6
--- *FunctorCombo.MemoTrie> memo f6 undefined
--- *** Exception: Prelude.undefined
-
--- Aha!
-
-t6 :: Either () () :-> Integer
-t6 = trie f6
-
--- *FunctorCombo.MemoTrie> t6
--- Id 6 :*: Id 6
-
--}
diff --git a/src/FunctorCombo/NonstrictMemo.hs b/src/FunctorCombo/NonstrictMemo.hs
--- a/src/FunctorCombo/NonstrictMemo.hs
+++ b/src/FunctorCombo/NonstrictMemo.hs
@@ -2,8 +2,8 @@
            , DeriveFunctor, StandaloneDeriving
            , FlexibleContexts
  #-}
-{-# OPTIONS_GHC -Wall #-}
-{-# OPTIONS_GHC -fno-warn-unused-binds -fno-warn-unused-imports #-}  -- temporary while testing
+{-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
+{-# OPTIONS_GHC -fno-warn-unused-binds -fno-warn-unused-imports #-}  -- TEMP
 ----------------------------------------------------------------------
 -- |
 -- Module      :  FunctorCombo.NonstrictMemo
@@ -13,13 +13,13 @@
 -- Maintainer  :  conal@conal.net
 -- Stability   :  experimental
 -- 
--- Functor-based memo tries
--- 
+-- Functor-based memo tries.  See
+-- <http://conal.net/blog/posts/details-for-nonstrict-memoization-part-1/>
 ----------------------------------------------------------------------
 
 module FunctorCombo.NonstrictMemo
   (
-    HasTrie(..),memo,memo2,memo3
+    HasTrie(..),(:->:),memo,memo2,memo3
   ) where
 
 #define NonstrictMemo
@@ -36,6 +36,7 @@
 import Data.Lub
 #endif
 
+import FunctorCombo.Strict
 import FunctorCombo.Functor
 import FunctorCombo.Regular
 
@@ -60,7 +61,7 @@
 
 #ifdef FunctorSuperClass
 
-#define HasTrieContext(Ty) Functor (STrie(Ty))
+#define HasTrieContext(Ty) Functor (STrie (Ty))
 #define HF(Ty) HasTrie (Ty)
 
 #else
@@ -206,6 +207,31 @@
 -- 
 -- Solution: switch from inner-then-outer to outer-then-inner.
 
+
+-- Experiment: strict sums & pairs.
+-- TODO: re-work non-strict versions in terms of strict ones and Lift
+
+instance (HasTrie a, HasTrie b) => HasTrie (a :+! b) where
+  type STrie (a :+! b) = STrie a :*: STrie b
+  sTrie   f           = sTrie (f . Left') :*: sTrie (f . Right')
+  sUntrie (ta :*: tb) = sUntrie ta `either'` sUntrie tb
+--   enumerate (ta :*: tb) = enum' Left' ta `weave` enum' Right' tb
+
+instance (HF(a), HasTrie b) => HasTrie (a :*! b) where
+  type STrie (a :*! b) = STrie a :. STrie b
+--   sTrie   f = O (trie (trie . curry f))
+--   sUntrie (O tt) = uncurry (untrie . untrie tt)
+  sTrie   f      = O (fmap sTrie (sTrie (curry' f)))
+  sUntrie (O tt) = uncurry' (sUntrie (fmap sUntrie tt))
+
+-- Lift a has an additional bottom.  A strict function or trie is
+-- only strict in the lower (outer) one.
+instance (HF(a)) => HasTrie (Lift a) where
+  type STrie (Lift a) = Trie a
+  sTrie   f = trie (f . Lift)
+  sUntrie t = untrie t . unLift
+
+
 #define HasTrieIsomorph(Context,Type,IsoType,toIso,fromIso) \
 instance Context => HasTrie (Type) where { \
   type STrie (Type) = STrie (IsoType); \
@@ -228,7 +254,9 @@
                , (a,b,c,d), ((a,b,c),d)
                , \ (a,b,c,d) -> ((a,b,c),d), \ ((a,b,c),d) -> (a,b,c,d))
 
+-- OOPS! Fix the isomorphs above
 
+
 -- As well as the functor combinators themselves
 
 HasTrieIsomorph( HasTrie x, Const x a, x, getConst, Const )
@@ -246,7 +274,23 @@
 HasTrieIsomorph( HasTrie (g (f a))
                , (g :. f) a, g (f a) , unO, O )
 
+-- Strict variants
 
+HasTrieIsomorph( ( HF(f a), HasTrie (g a) )
+               , (f :*:! g) a, (f a :*! g a)
+               , \ (fa :*:! ga) -> (fa :*! ga), \ (fa :*! ga) -> (fa :*:! ga) )
+
+HasTrieIsomorph( (HasTrie (f a), HasTrie (g a))
+               , (f :+:! g) a, (f a :+! g a)
+               , fToSum, sumToF)
+
+-- Factored out to avoid clash between primes and GHC's use of classic CPP
+sumToF :: (f a :+! g a) -> (f :+:! g) a
+sumToF = either' InL' InR'
+
+fToSum :: (f :+:! g) a -> (f a :+! g a)
+fToSum = eitherF' Left' Right'
+
 newtype ListSTrie a v = ListSTrie (PF [a] [a] :-> v)
  
 deriving instance Functor (STrie a) => Functor (ListSTrie a)
@@ -257,11 +301,12 @@
   sUntrie (ListSTrie t) = sUntrie t . unwrap
   -- enumerate (ListSTrie t) = (result.fmap.first) wrap enumerate $ t
 
--- Compiles fine, but has many points of undefinedness than a list does.
+-- Compiles fine, but has many points of undefinedness than a list does.  See
+-- <http://conal.net/blog/posts/details-for-nonstrict-memoization-part-1/>
+-- 
 -- Experiment with some alternatives.
 
 
-
 -- Now a trie for ListSTrie a v.  Use the isomorphism with PF [a] [a] :-> v
 
 -- HasTrieIsomorph( HasTrie (PF ([a]) ([a]) :->: v)
@@ -353,10 +398,6 @@
 
 -}
 
-
-
-{-
-
 -- Now abstract into a macro
 
 #define HasTrieRegular(Context,Type,TrieType,TrieCon) \
@@ -396,28 +437,59 @@
 --                , \ (ListSTrie w) -> w, ListSTrie )
 
 
-enumerateEnum :: (Enum k, Num k, HasTrie k) => (k :->: v) -> [(k,v)]
-enumerateEnum t = [(k, f k) | k <- [0 ..] `weave` [-1, -2 ..]]
- where
-   f = untrie t
+-- enumerateEnum :: (Enum k, Num k, HasTrie k) => (k :->: v) -> [(k,v)]
+-- enumerateEnum t = [(k, f k) | k <- [0 ..] `weave` [-1, -2 ..]]
+--  where
+--    f = untrie t
 
 #define HasTrieIntegral(Type) \
 instance HasTrie Type where { \
   type STrie Type = IT.IntTrie; \
   sTrie   = (<$> IT.identity); \
   sUntrie = IT.apply; \
-  enumerate = enumerateEnum; \
 }
+  -- enumerate = enumerateEnum;
 
 HasTrieIntegral(Int)
 HasTrieIntegral(Integer)
 
-
 -- Memoizing higher-order functions
 
-HasTrieIsomorph((HasTrie a, HasTrie (a :->: b)), a -> b, a :->: b, trie, untrie)
+HasTrieIsomorph((HasTrie a, HasTrie (a :->: b), HasLub b)
+               ,a -> b, a :->: b, trie, untrie)
 
 
+{--------------------------------------------------------------------
+    Regular instances.
+--------------------------------------------------------------------}
+
+-- Re-think where to put these instances.  I want different versions for
+-- list, depending on whether I'm taking care with bottoms.
+
+instance Regular [a] where
+  type PF [a] = Unit :+:! Const (Lift a) :*:! Lift
+  unwrap []     = InL' (Const ())
+  unwrap (a:as) = InR' (Const (Lift a) :*:! Lift as)
+  wrap (InL' (Const ()))            = []
+  wrap (InR' (Const (Lift a) :*:! Lift as)) = a:as
+
+-- Rose tree (from Data.Tree)
+-- 
+--   data Tree  a = Node a [Tree a]
+
+-- instance Functor Tree where
+--   fmap f (Node a ts) = Node (f a) (fmap f ts)
+
+instance Regular (Tree a) where
+  type PF (Tree a) = Const a :*: []
+  unwrap (Node a ts) = Const a :*: ts
+  wrap (Const a :*: ts) = Node a ts
+
+-- Note that we're using the non-strict pairing functor.
+-- Does PF (Tree a) have the right strictness?
+-- I think so, since a tree can be either _|_ or Node applied to a
+-- possibly-_|_ value and a possibly-_|_ list.
+
 {-
 
 {--------------------------------------------------------------------
@@ -436,6 +508,8 @@
 
 
 -}
+
+{-
 
 ft1 :: (Bool -> a) -> [a]
 ft1 f = [f False, f True]
diff --git a/src/FunctorCombo/Regular.hs b/src/FunctorCombo/Regular.hs
--- a/src/FunctorCombo/Regular.hs
+++ b/src/FunctorCombo/Regular.hs
@@ -14,9 +14,9 @@
 
 module FunctorCombo.Regular (Regular(..)) where
 
-import Data.Tree
+-- import Data.Tree
 
-import FunctorCombo.Functor
+-- import FunctorCombo.Functor
 
 
 -- Pattern functors, similar to PolyC and the Regular class from
@@ -27,15 +27,28 @@
   wrap   :: PF t t -> t
   unwrap :: t -> PF t t
 
+{-
 
+-- For now, move these instances to StrictMemo and NonstrictMemo, since I
+-- want different instances, depending on how careful I'm taking care with
+-- bottoms.
+
 -- Some Regular instances:
 
+-- instance Regular [a] where
+--   type PF [a] = Unit :+: Const a :*: Id
+--   unwrap []     = InL (Const ())
+--   unwrap (a:as) = InR (Const a :*: Id as)
+--   wrap (InL (Const ()))          = []
+--   wrap (InR (Const a :*: Id as)) = a:as
+
+
 instance Regular [a] where
-  type PF [a] = Unit :+: Const a :*: Id
-  unwrap []     = InL (Const ())
-  unwrap (a:as) = InR (Const a :*: Id as)
-  wrap (InL (Const ()))          = []
-  wrap (InR (Const a :*: Id as)) = a:as
+  type PF [a] = Unit :+:! Const (Lift a) :*:! Lift
+  unwrap []     = InL' (Const ())
+  unwrap (a:as) = InR' (Const (Lift a) :*:! Lift as)
+  wrap (InL' (Const ()))            = []
+  wrap (InR' (Const (Lift a) :*:! Lift as)) = a:as
 
 
 -- Rose tree (from Data.Tree)
@@ -49,3 +62,10 @@
   type PF (Tree a) = Const a :*: []
   unwrap (Node a ts) = Const a :*: ts
   wrap (Const a :*: ts) = Node a ts
+
+-- Note that we're using the non-strict pairing functor.
+-- Does PF (Tree a) have the right strictness?
+-- I think so, since a tree can be either _|_ or Node applied to a
+-- possibly-_|_ value and a possibly-_|_ list.
+
+-}
diff --git a/src/FunctorCombo/Strict.hs b/src/FunctorCombo/Strict.hs
new file mode 100644
--- /dev/null
+++ b/src/FunctorCombo/Strict.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -Wall #-}
+----------------------------------------------------------------------
+-- |
+-- Module      :  FunctorCombo.Strict
+-- Copyright   :  (c) Conal Elliott 2010
+-- License     :  BSD3
+-- 
+-- Maintainer  :  conal@conal.net
+-- Stability   :  experimental
+-- 
+-- Strict products and sums.Strict
+----------------------------------------------------------------------
+
+module FunctorCombo.Strict
+  ( (:*!)(..),curry',uncurry', (:+!)(..),either'
+  ) where
+
+infixl 7 :*!
+infixl 6 :+!
+
+{--------------------------------------------------------------------
+    Products
+--------------------------------------------------------------------}
+
+-- | Strict pair
+data a :*! b = !a :*! !b
+
+-- | Curry on strict pairs
+curry' :: (a :*! b -> c) -> (a -> b -> c)
+curry' f a b = f (a :*! b)
+
+-- | Uncurry on strict pairs
+uncurry' :: (a -> b -> c) -> ((a :*! b) -> c)
+uncurry' f (a :*! b) = f a b
+
+
+{--------------------------------------------------------------------
+    Sums
+--------------------------------------------------------------------}
+
+-- | Strict sum
+data a :+! b = Left' !a | Right' !b
+
+-- | Case analysis for strict sums.  Like 'either'.
+either' :: (a -> c) -> (b -> c) -> (a :+! b -> c)
+either' f _ (Left'  a) = f a
+either' _ g (Right' b) = g b
diff --git a/src/FunctorCombo/StrictMemo.hs b/src/FunctorCombo/StrictMemo.hs
--- a/src/FunctorCombo/StrictMemo.hs
+++ b/src/FunctorCombo/StrictMemo.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE TypeOperators, TypeFamilies, UndecidableInstances, CPP
            , FlexibleContexts, DeriveFunctor, StandaloneDeriving
  #-}
-{-# OPTIONS_GHC -Wall #-}
+{-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
 {-# OPTIONS_GHC -fno-warn-unused-binds -fno-warn-unused-imports #-}  -- temporary while testing
 ----------------------------------------------------------------------
 -- |
@@ -18,17 +18,20 @@
 
 module FunctorCombo.StrictMemo
   (
-    HasTrie(..),memo,memo2,memo3
+    HasTrie(..),(:->:),memo,memo2,memo3
   ) where
 
 import Control.Arrow (first)
 import Control.Applicative ((<$>))
 
+import Data.Tree
+
 import qualified Data.IntTrie as IT  -- data-inttrie
 import Data.Tree
 
 import Control.Compose (result)  -- TypeCompose
 
+-- import FunctorCombo.Strict
 import FunctorCombo.Functor
 import FunctorCombo.Regular
 
@@ -133,6 +136,8 @@
   enumerate (O tt) =
     [ ((a,b),x) | (a,t) <- enumerate tt , (b,x) <- enumerate t ]
 
+
+
 #define HasTrieIsomorph(Context,Type,IsoType,toIso,fromIso) \
 instance Context => HasTrie (Type) where {\
   type Trie (Type) = Trie (IsoType); \
@@ -142,8 +147,8 @@
 }
 
 HasTrieIsomorph( (), Bool, Either () ()
-               , bool (Left ()) (Right ())
-               , either (\ () -> True) (\ () -> False))
+               , bool (Right ()) (Left ())
+               , either (\ () -> False) (\ () -> True))
 
 HasTrieIsomorph( (HF(a),HF(b), HasTrie c)
                , (a,b,c), ((a,b),c)
@@ -154,6 +159,7 @@
                , \ (a,b,c,d) -> ((a,b,c),d), \ ((a,b,c),d) -> (a,b,c,d))
 
 
+
 -- As well as the functor combinators themselves
 
 HasTrieIsomorph( HasTrie x, Const x a, x, getConst, Const )
@@ -172,6 +178,7 @@
                , (g :. f) a, g (f a) , unO, O )
 
 
+
 -- newtype ListTrie a v = ListTrie (PF [a] [a] :->: v)
  
 -- instance (HF(a)) => HasTrie [a] where
@@ -390,3 +397,28 @@
 
 -- Would nonstrict memoization work?  <http://conal.net/blog/posts/nonstrict-memoization/>
 
+{--------------------------------------------------------------------
+    Regular instances.
+--------------------------------------------------------------------}
+
+-- Re-think where to put these instances.  I want different versions for
+-- list, depending on whether I'm taking care with bottoms.
+
+instance Regular [a] where
+  type PF [a] = Unit :+: Const a :*: Id
+  unwrap []     = InL (Const ())
+  unwrap (a:as) = InR (Const a :*: Id as)
+  wrap (InL (Const ()))          = []
+  wrap (InR (Const a :*: Id as)) = a:as
+
+-- Rose tree (from Data.Tree)
+-- 
+--   data Tree  a = Node a [Tree a]
+
+-- instance Functor Tree where
+--   fmap f (Node a ts) = Node (f a) (fmap f ts)
+
+instance Regular (Tree a) where
+  type PF (Tree a) = Const a :*: []
+  unwrap (Node a ts) = Const a :*: ts
+  wrap (Const a :*: ts) = Node a ts