diff --git a/Algebra.hs b/Algebra.hs
deleted file mode 100644
--- a/Algebra.hs
+++ /dev/null
@@ -1,28 +0,0 @@
-{-# LANGUAGE ImplicitParams #-}
-module Algebra (
-  module Algebra.Core,
-  module Algebra.Arrow,
-  module Algebra.Traversable,
-  module Algebra.Lens,
-  trace,trace2,mtrace,debug,
-
-  cli
-  ) where
-
-import Algebra.Arrow
-import Algebra.Core hiding (flip)
-import Algebra.Lens
-import Algebra.Traversable
-import System.Environment (getArgs)
-
-trace :: String -> a -> a
-trace s x = (putStrLn s^.thunk)`seq`x
-trace2 :: String -> String -> a -> a
-trace2 b a x = trace b (x`seq`trace a x)
-mtrace :: Unit f => String -> f ()
-mtrace str = trace str (pure ())
-debug :: Show a => a -> a
-debug x = trace (show x) x
-
-cli :: (( ?cliargs :: [String] ) => IO a) -> IO a
-cli main = getArgs >>= \a -> let ?cliargs = a in main
diff --git a/Algebra/Applicative.hs b/Algebra/Applicative.hs
--- a/Algebra/Applicative.hs
+++ b/Algebra/Applicative.hs
@@ -1,24 +1,25 @@
 -- |A module describing applicative functors
+{-# LANGUAGE UndecidableInstances #-}
 module Algebra.Applicative(
   module Algebra.Functor,
 
   Applicative(..),
-  ZipList(..),ZipTree(..),Backwards(..),
+  Zip(..),Backwards(..),
+  c'zip,c'backwards,
 
-  (*>),(<*),(<**>),ap,sequence_,traverse_,for_,forever,
+  (*>),(<*),(<**>),ap,
 
   between,
   
-  liftA,liftA2,liftA3,liftA4,
+  liftA,liftA2,liftA3,liftA4,forever,
 
   plusA,zeroA
   ) where
 
 import Algebra.Functor
 import Algebra.Classes
-import Algebra.Core
+import Algebra.Core hiding (flip)
 import Data.Tree
-import Algebra.Foldable
 
 instance Applicative (Either a)
 instance Monad (Either a) where join (Right a) = a
@@ -32,10 +33,6 @@
 instance Monoid w => Applicative ((,) w)
 instance Monoid w => Monad ((,) w) where
   join ~(w,~(w',a)) = (w+w',a)
-instance Applicative []
-instance Monad [] where join = fold
-instance Applicative Maybe
-instance Monad Maybe where join = fold
 
 instance (Unit f,Unit g) => Unit (f:**:g) where pure a = pure a:**:pure a
 instance (Applicative f,Applicative g) => Applicative (f:**:g) where
@@ -44,44 +41,43 @@
 instance Applicative Tree
 instance Monad Tree where
   join (Node (Node a subs) subs') = Node a (subs + map join subs')
-deriving instance Unit Interleave
-instance Applicative Interleave
-instance Monad Interleave where join = fold
 
 instance (Applicative f,Applicative g) => Applicative (f:.:g) where
   Compose fs <*> Compose xs = Compose ((<*>)<$>fs<*>xs)
 
 {-|
 A wrapper type for lists with zipping Applicative instances, such that
-@ZipList [f1,...,fn] '<*>' ZipList [x1,...,xn] == ZipList [f1 x1,...,fn xn]@
+@Zip [f1,...,fn] '<*>' Zip [x1,...,xn] == Zip [f1 x1,...,fn xn]@
 -}
-newtype ZipList a = ZipList { getZipList :: [a] }
-instance Semigroup a => Semigroup (ZipList a) where (+) = plusA
-instance Monoid a => Monoid (ZipList a) where zero = zeroA
+newtype Zip f a = Zip { deZip :: f a }
+c'zip :: Constraint (f a) -> Constraint (Zip f a)
+c'zip _ = id
 
-instance Functor ZipList where
-  map f (ZipList l) = ZipList (map f l)
-instance Unit ZipList where
-  pure a = ZipList (repeat a)
-instance Applicative ZipList where
-  ZipList zf <*> ZipList zx = ZipList (zip_ zf zx)
+instance (Applicative (Zip f),Semigroup a) => Semigroup (Zip f a) where (+) = plusA
+instance (Applicative (Zip f),Monoid a) => Monoid (Zip f a) where zero = zeroA
+
+instance Functor f => Functor (Zip f) where
+  map f (Zip l) = Zip (map f l)
+deriving instance Foldable f => Foldable (Zip f)
+
+instance Unit (Zip []) where
+  pure a = Zip (repeat a)
+instance Applicative (Zip []) where
+  Zip zf <*> Zip zx = Zip (zip_ zf zx)
     where zip_ (f:fs) (x:xs) = f x:zip_ fs xs
           zip_ _ _ = []
-deriving instance Foldable ZipList
 
--- |The Tree equivalent to ZipList
-newtype ZipTree a = ZipTree (Tree a)
-instance Functor ZipTree where
-  map f (ZipTree t) = ZipTree (map f t)
-instance Unit ZipTree where
-  pure a = ZipTree (Node a (getZipList (pure (pure a))))
-instance Applicative ZipTree where
-  ZipTree (Node f fs) <*> ZipTree (Node x xs) =
-    ZipTree (Node (f x) (getZipList ((<*>)<$>ZipList fs<*>ZipList xs)))
-deriving instance Foldable ZipTree
+instance Unit (Zip Tree) where
+  pure a = Zip (Node a (deZip (pure (pure a))))
+instance Applicative (Zip Tree) where
+  Zip (Node f fs) <*> Zip (Node x xs) =
+    Zip (Node (f x) (deZip ((<*>)<$>Zip fs<*>Zip xs)))
 
 -- |A wrapper for applicative functors with actions executed in the reverse order
 newtype Backwards f a = Backwards { forwards :: f a }
+c'backwards :: Constraint (f a) -> Constraint (Backwards f a)
+c'backwards _ = id
+
 deriving instance Semigroup (f a) => Semigroup (Backwards f a)
 deriving instance Monoid (f a) => Monoid (Backwards f a)
 deriving instance Semiring (f a) => Semiring (Backwards f a)
@@ -91,7 +87,6 @@
 instance Applicative f => Applicative (Backwards f) where
   Backwards fs <*> Backwards xs = Backwards (fs<**>xs)
 
-
 ap :: Applicative f => f (a -> b) -> f a -> f b
 
 plusA :: (Applicative f,Semigroup a) => f a -> f a -> f a
@@ -109,13 +104,6 @@
 (*>) = liftA2 (flip const)
 (<*) = liftA2 const
 f <**> x = liftA2 (&) x f
-
-sequence_ = foldr (*>) (pure ())
-sequence_ :: (Applicative f,Foldable t) => t (f a) -> f ()
-traverse_ f = sequence_ . map f
-traverse_ :: (Applicative f,Foldable t) => (a -> f b) -> t a -> f ()
-for_ = flip traverse_
-for_ :: (Applicative f,Foldable t) => t a -> (a -> f b) -> f ()
 
 forever :: Applicative f => f a -> f b
 forever m = fix (m *>)
diff --git a/Algebra/Classes.hs b/Algebra/Classes.hs
--- a/Algebra/Classes.hs
+++ b/Algebra/Classes.hs
@@ -3,6 +3,7 @@
 
 import Algebra.Core
 
+
 class Functor f where
   map :: (a -> b) -> f a -> f b
 class (Unit f, Functor f) => Applicative f where
@@ -17,6 +18,11 @@
   (>>=) :: m a -> (a -> m b) -> m b
   ma >>= k = join (map k ma)
 
+class Functor f => Foldable f where
+  fold :: Monoid m => f m -> m
+class Functor t => Traversable t where
+  sequence :: Applicative f => t (f a) -> f (t a)
+
 -- |The class of all monads that have a fixpoint
 class Monad m => MonadFix m where
   mfix :: (a -> m a) -> m a
@@ -40,6 +46,8 @@
   censor :: m (a,w -> w) -> m a
 class (SubSemi acc w,MonadWriter w m) => MonadWriterAcc w acc m where
   getAcc :: m acc
+class Monad m => MonadIO m where
+  liftIO :: IO a -> m a
 
 class Monad m => MonadList m where
   fork :: [a] -> m a
@@ -48,3 +56,6 @@
 class Monad m => MonadError e m | m -> e where
   throw :: e -> m a
   catch :: (e -> m a) -> m a -> m a
+
+class MonadFuture m t | t -> m where
+  future :: m a -> t a
diff --git a/Algebra/Core.hs b/Algebra/Core.hs
--- a/Algebra/Core.hs
+++ b/Algebra/Core.hs
@@ -4,6 +4,7 @@
   Handle,
   Bytes,readBytes,writeBytes,contentBytes,
   Chunk,readChunk,writeChunk,contentChunk,
+  readString,writeString,contentString,
   
   -- * Basic union and product types
   Void,(:*:),(:+:),
@@ -31,12 +32,15 @@
   -- ** Splitting and Choosing
   Choice(..),Split(..),
   
-  -- * Misc functions
+  -- * Expression-level type constraints
+  Constraint,c'listOf,c'list,c'int,c'float,
+  
+  -- * Miscellaneous functions
   const,(&),($^),is,fix,
 
   first,second,
 
-  ifThenElse,bool,guard,fail,unit,when,unless,
+  ifThenElse,bool,extreme,guard,fail,unit,when,unless,
 
   tailSafe,headDef,fromMaybe,
 
@@ -46,6 +50,9 @@
   Orderable(..),
   comparing,insertOrd,invertOrd,
   
+  -- ** Ranges
+  Range(..),
+  
   -- * The rest is imported from the Prelude
   module Prelude
   ) where
@@ -60,16 +67,26 @@
   map,(++),foldl,foldr,foldr1,concat,filter,length,sum,lookup,
   (+),(*),(.),id,const,(-),
 
-  or,any,and,all,elem,
+  or,any,and,all,elem,span,break,splitAt,take,drop,takeWhile,dropWhile,
 
   until,negate)
 import qualified Prelude as P
 import Data.Tree
 import qualified Data.ByteString.Lazy as BSL
 import qualified Data.ByteString as BSS
-import GHC.IO.Handle (Handle)
+import GHC.IO.Handle (Handle,hGetContents)
 import Data.Ord (comparing)
 
+type Constraint a = a -> a
+c'listOf :: Constraint a -> Constraint [a]
+c'listOf _ = id
+c'list :: Constraint [a]
+c'list = id
+c'int :: Constraint Int
+c'int = id
+c'float :: Constraint Float
+c'float = id
+
 type Chunk = BSS.ByteString
 type Bytes = BSL.ByteString
 
@@ -77,14 +94,20 @@
 readBytes = BSL.readFile
 readChunk :: String -> IO Chunk
 readChunk = BSS.readFile
+readString :: String -> IO String
+readString = P.readFile
 writeBytes :: String -> Bytes -> IO ()
 writeBytes = BSL.writeFile
 writeChunk :: String -> Chunk -> IO ()
 writeChunk = BSS.writeFile
+writeString :: String -> String -> IO ()
+writeString = P.writeFile
 contentBytes :: Handle -> IO Bytes
 contentBytes = BSL.hGetContents
 contentChunk :: Handle -> IO Chunk
 contentChunk = BSS.hGetContents
+contentString :: Handle -> IO String
+contentString = hGetContents
 
 data Void
 type a:*:b = (a,b)
@@ -251,7 +274,8 @@
 
 -- |The Identity Functor
 newtype Id a = Id { getId :: a }
-             deriving Show
+instance Show a => Show (Id a) where
+  show (Id a) = "Id "+show a
 instance Unit Id where pure = Id
 
 {-| The Max monoid, where @(+) =~ max@ -}
@@ -294,6 +318,36 @@
 insertOrd e (x:xs) = a:y:ys
   where (a,_,z) = inOrder e x
         ~(y:ys) = if z then x:xs else insertOrd e xs
+
+{- | A range of shape (min,max) of ordered values.
+
+Such ranges may be multiplied to create n-dimensional ranges for which
+equivalence means sharing an n-dimensional subrange.  They may be very
+useful in creating Maps that partition an n-dimensional space in which
+we may query for subrange membership with logarithmic complexity for
+any point P (a point is a subrange of volume 0, or `(pure x0,...,pure
+xn) where (x0,..,xn) = p`).
+
+Indeed, a point is equivalent to a range iff it belongs to that range.
+
+-}
+newtype Range a = Range (a,a)
+
+instance Unit Range where pure a = Range (a,a)
+-- | @r < r'@ iff all values of @r@ are below any value of @r'@
+instance Ord a => Ord (Range a) where
+  compare (Range (a,b)) (Range (a',b'))
+    | b<a' = LT
+    | b'<a = GT 
+    | otherwise = EQ
+-- | Range equivalence. Two ranges are equivalent iff they share a
+-- common subrange (equivalence in this case is not transitive, so
+-- beware of unintended consequences)
+instance Ord a => Eq (Range a) where
+  a == b = compare a b == EQ
+
+extreme :: Bounded a => Bool -> a
+extreme b = if b then maxBound else minBound
 
 newtype Interleave a = Interleave { interleave :: [a] }
 instance Semigroup (Interleave a) where
diff --git a/Algebra/Foldable.hs b/Algebra/Foldable.hs
--- a/Algebra/Foldable.hs
+++ b/Algebra/Foldable.hs
@@ -1,13 +1,11 @@
 {-# LANGUAGE TupleSections, MultiParamTypeClasses #-}
 module Algebra.Foldable where
 
-import Algebra.Core
+import Algebra.Core hiding (flip)
 import Algebra.Classes
 import Algebra.Functor
 import Data.Tree
 
-class Functor t => Foldable t where
-  fold :: Monoid m => t m -> m
 instance Foldable Id where fold = getId
 instance Foldable (Either a) where
   fold = pure zero <|> id
@@ -15,8 +13,12 @@
   fold (Just w) = w ; fold Nothing = zero
 instance Foldable ((,) a) where fold = snd
 instance Foldable [] where
-  fold [] = zero
+  -- | For performance reasons, we want to avoid computing (f+zero)
+  -- needlessly. This cannot be inferred by the compiler, since
+  -- `f+zero == f` is an implicit assumption of Monoid instances.
+  fold [a] = a 
   fold (x:t) = x+fold t
+  fold [] = zero
 instance Foldable Tree where fold (Node m subs) = m + fold (map fold subs)
 deriving instance Foldable Interleave
 deriving instance Foldable OrdList
@@ -32,6 +34,14 @@
   fold (Sum (Left f)) = fold f
   fold (Sum (Right g)) = fold g
 
+instance Applicative []
+instance Monad [] where join = fold
+instance Applicative Maybe
+instance Monad Maybe where join = fold
+deriving instance Unit Interleave
+instance Applicative Interleave
+instance Monad Interleave where join = fold
+
 foldMap :: (Monoid m, Foldable t) => (a -> m) -> t a -> m
 foldMap f = fold . map f
 convert :: (Unit f, Monoid (f a), Foldable t) => t a -> f a
@@ -45,6 +55,13 @@
 length :: [a] -> Int
 length = size
 
+sequence_ :: (Applicative f,Foldable t) => t (f a) -> f ()
+sequence_ = foldr ((<*>) . map (flip const)) (pure ())
+traverse_ :: (Applicative f,Foldable t) => (a -> f b) -> t a -> f ()
+traverse_ f = sequence_ . map f
+for_ :: (Applicative f,Foldable t) => t a -> (a -> f b) -> f ()
+for_ = flip traverse_
+
 split :: (Foldable t,Monoid b,Monoid c) => t (b:+:c) -> (b,c)
 split = foldMap ((,zero)<|>(zero,))
 partitionEithers :: (Foldable t,Unit t,Monoid (t a),Monoid (t b))
@@ -61,6 +78,8 @@
 
 compose :: (Category k, Foldable t) => t (k a a) -> k a a
 compose = runEndo . foldMap Endo
+iter :: (Contravariant (k a),Category k,Foldable t) => k a (t (k a a) -> a)
+iter = flip compose
 
 foldr :: Foldable t => (b -> a -> a) -> a -> t b -> a
 foldr f e t = (runEndo . getDual) (foldMap (\b -> Dual (Endo (f b))) t) e
diff --git a/Algebra/Functor.hs b/Algebra/Functor.hs
--- a/Algebra/Functor.hs
+++ b/Algebra/Functor.hs
@@ -1,10 +1,11 @@
 {-# LANGUAGE MultiParamTypeClasses, RankNTypes, DefaultSignatures #-}
 -- |A module for functors
 module Algebra.Functor(
-  Functor(..),Cofunctor(..),Bifunctor(..),Commutative(..),
+  Functor(..),Cofunctor(..),Bifunctor(..),Commutative(..),Contravariant(..),
   
-  Id(..),Const(..),Flip(..),(:.:)(..),(:**:)(..),(:++:)(..),
+  Strict(..),Id(..),Const(..),Flip(..),(:.:)(..),(:**:)(..),(:++:)(..),
 
+  flip,project,
   (<$>),(|||),(<$),(<&>),void,left,right,
   promap,map2,map3
   ) where
@@ -12,7 +13,7 @@
 import qualified Prelude as P
 
 import Algebra.Classes
-import Algebra.Core
+import Algebra.Core hiding (flip)
 import Data.Tree
 
 class Cofunctor f where
@@ -23,6 +24,16 @@
   comap f (Flip g) = Flip (g . f)
 instance Bifunctor (->)
 
+class Functor t => Contravariant t where
+  collect :: Functor f => f (t a) -> t (f a)
+instance Contravariant Id where collect f = Id (map getId f)
+instance Contravariant ((->) a) where collect f = \a -> map ($a) f
+flip :: (Contravariant c,Functor f) => f (c a) -> c (f a)
+flip = collect
+-- | The Contravariant version of 'traverse'
+project :: (Contravariant c,Functor f) => (a -> c b) -> f a -> c (f b)
+project f x = collect (map f x)
+
 class Bifunctor p where
   dimap :: (c -> a) -> (b -> d) -> p a b -> p c d
   default dimap :: (Functor (p a),Cofunctor (Flip p d)) => (c -> a) -> (b -> d) -> p a b -> p c d
@@ -40,6 +51,14 @@
 instance Functor Id where map f (Id a) = Id (f a)
 instance Applicative Id
 instance Monad Id where join (Id a) = a
+
+newtype Strict a = Strict { lazy :: a }
+instance Unit Strict where pure = Strict
+instance Functor Strict where map f (Strict a) = Strict (f a)
+instance Applicative Strict where
+  Strict f <*> Strict x = Strict (f$!x)
+instance Monad Strict where
+  join (Strict x) = x
 
 -- |The Constant Functor
 newtype Const a b = Const { getConst :: a }
diff --git a/Algebra/Lens.hs b/Algebra/Lens.hs
--- a/Algebra/Lens.hs
+++ b/Algebra/Lens.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE Rank2Types, MultiParamTypeClasses, FunctionalDependencies, ViewPatterns, TupleSections #-}
+{-# LANGUAGE Rank2Types, MultiParamTypeClasses, FunctionalDependencies, ViewPatterns, TupleSections, LiberalTypeSynonyms #-}
 {-|
 A module providing simple Lens functionality.
 
@@ -16,12 +16,12 @@
 module Algebra.Lens(
   -- * The lens types
   Iso,Iso',(:<->:),
-  LensLike,LensLike',
+  LensLike,
   Fold,Fold',
   Getter,Getter',
   Lens,Lens',
   Traversal,Traversal',
-
+  
   -- * Constructing lenses
   iso,from,lens,getter,prism,sat,simple,(.+),forl,forl_,
 
@@ -33,27 +33,27 @@
   Lens1(..),Lens2(..),Lens3(..),Lens4(..),
   Trav1(..),Trav2(..),
   Compound(..),
-  _list,_head,_tail,
+  i'list,i'pair,t'head,t'tail,
   
   -- * Isomorphisms
   Isomorphic(..),
 
   -- ** Miscellaneous
-  thunk,chunk,
+  thunk,chunk,curried,
 
   -- ** Type wrappers
-  _Id,_OrdList,_Const,_Dual,_Endo,_Flip,_maybe,_Max,_Compose,_Backwards,
+  i'Id,i'OrdList,i'Const,i'Dual,i'Endo,i'Flip,i'maybe,i'Max,i'Compose,i'Backwards,i'Accum,
 
   -- ** Algebraic isomorphisms
   negated,commuted,adding,
-
+  
   -- ** Higher-order isomorphisms
   warp2,mapping,mapping',promapping,
 
   IsoFunctor(..),(<.>),IsoFunctor2(..)
   ) where
 
-import Algebra.Core
+import Algebra.Core hiding (flip)
 import Algebra.Functor
 import Algebra.Applicative
 import System.IO.Unsafe (unsafePerformIO)
@@ -61,18 +61,18 @@
 import Data.ByteString.Lazy (toStrict,fromStrict)
 
 type LensLike f s t a b = (s -> f t) -> (a -> f b)
-type LensLike' f a b = LensLike f b b a a
+type Simple f a b = f b b a a
 
 type Lens s t a b = forall f.Functor f => LensLike f s t a b
-type Lens' a b = Lens b b a a
+type Lens' a b = Simple Lens a b
 type Getter s t a b = LensLike (Const s) s t a b
-type Getter' a b = Getter b b a a
+type Getter' a b = Simple Getter a b
 type Traversal s t a b = forall f. Applicative f => LensLike f s t a b
-type Traversal' a b = Traversal b b a a
+type Traversal' a b = Simple Traversal a b
 type Fold s t a b = forall f. (Semigroup (f b),Applicative f) => LensLike f s t a b
-type Fold' a b = Fold b b a a 
+type Fold' a b = Simple Fold a b
 type Iso s t a b = forall p f. (Functor f,Bifunctor p) => p s (f t) -> p a (f b)
-type Iso' a b = Iso b b a a
+type Iso' a b = Simple Iso a b
 type a :<->: b = Iso' a b
 
 data IsoT a b s t = IsoT (s -> a) (b -> t)
@@ -114,7 +114,7 @@
 prism :: (a -> (b:+:s)) -> (a -> t -> b) -> Traversal s t a b 
 prism f g = \k a -> (pure <|> map (g a) . k) (f a)
 
-simple :: Traversal a b a b -> Traversal a b a b
+simple :: LensLike f a b a b -> LensLike f a b a b
 simple l = l
 
 sat :: (a -> Bool) -> Traversal' a a
@@ -131,11 +131,11 @@
 (^..) :: a -> Iso a a b b -> b
 (^..) = flip yb
 -- |
-(%~) :: Traversal s t a b -> (s -> t) -> (a -> b)
+(%~) :: LensLike Id s t a b -> (s -> t) -> (a -> b)
 (%~) = warp
 (%%~) :: Iso s t a b -> (b -> a) -> (t -> s)
 (%%~) i = warp (from i)
-(%-) :: Traversal s t a b -> t -> (a -> b)
+(%-) :: LensLike Id s t a b -> t -> (a -> b)
 (%-) = set
 (%%-) :: Iso s t a b -> a -> (t -> s)
 (%%-) i = set (from i)
@@ -153,9 +153,9 @@
 by l = getConst . l Const
 yb :: Iso s t a b -> t -> b
 yb i = by (from i)
-warp :: Traversal s t a b -> (s -> t) -> (a -> b)
+warp :: LensLike Id s t a b -> (s -> t) -> (a -> b)
 warp l = map getId . l . map Id
-set :: Traversal s t a b -> t -> (a -> b)
+set :: LensLike Id s t a b -> t -> (a -> b)
 set l = warp l . const 
 
 forl :: LensLike f a b c d -> c -> (a -> f b) -> f d
@@ -164,49 +164,51 @@
 forl_ l c f = void $ l (\a -> a<$f a) c
 
 class Lens1 s t a b | a -> s, a t -> b where
-  _1 :: Lens s t a b
+  l'1 :: Lens s t a b
 class Lens2 s t a b | a -> s, a t -> b where
-  _2 :: Lens s t a b
+  l'2 :: Lens s t a b
 class Lens3 s t a b | a -> s, a t -> b where
-  _3 :: Lens s t a b
+  l'3 :: Lens s t a b
 class Lens4 s t a b | a -> s, a t -> b where
-  _4 :: Lens s t a b
+  l'4 :: Lens s t a b
 class Trav1 s t a b | a -> s, a t -> b where
-  _l :: Traversal s t a b
+  t'l :: Traversal s t a b
 class Trav2 s t a b | a -> s, a t -> b where
-  _r :: Traversal s t a b
+  t'r :: Traversal s t a b
+instance Lens1 a a [a] [a] where
+  l'1 = lens (\ ~(a:_) -> a ) (\ ~(_:t) a -> a:t )
 instance Lens1 a b (a:*:c) (b:*:c) where
-  _1 = lens fst (flip (first . const))
+  l'1 = lens fst (flip (first . const))
 instance Lens1 a b (a,c,d) (b,c,d) where
-  _1 = lens (\ ~(a,_,_) -> a) (\ (_,c,d) b -> (b,c,d))
+  l'1 = lens (\ ~(a,_,_) -> a) (\ (_,c,d) b -> (b,c,d))
 instance Lens1 a b (a,c,d,e) (b,c,d,e) where
-  _1 = lens (\ ~(a,_,_,_) -> a) (\ (_,c,d,e) b -> (b,c,d,e))
+  l'1 = lens (\ ~(a,_,_,_) -> a) (\ (_,c,d,e) b -> (b,c,d,e))
 instance Lens2 a b (c:*:a) (c:*:b) where
-  _2 = lens snd (flip (second . const))
+  l'2 = lens snd (flip (second . const))
 instance Lens2 a b (c,a,d) (c,b,d) where
-  _2 = lens (\ ~(_,a,_) -> a ) (\ ~(c,_,d) b -> (c,b,d))
+  l'2 = lens (\ ~(_,a,_) -> a ) (\ ~(c,_,d) b -> (c,b,d))
 instance Lens2 a b (c,a,d,e) (c,b,d,e) where
-  _2 = lens (\ ~(_,a,_,_) -> a ) (\ ~(c,_,d,e) b -> (c,b,d,e))
+  l'2 = lens (\ ~(_,a,_,_) -> a ) (\ ~(c,_,d,e) b -> (c,b,d,e))
 instance Lens3 a b (c,d,a) (c,d,b) where
-  _3 = lens (\ ~(_,_,a) -> a ) (\ ~(c,d,_) b -> (c,d,b))
+  l'3 = lens (\ ~(_,_,a) -> a ) (\ ~(c,d,_) b -> (c,d,b))
 instance Lens3 a b (c,d,a,e) (c,d,b,e) where
-  _3 = lens (\ ~(_,_,a,_) -> a ) (\ ~(c,d,_,e) b -> (c,d,b,e))
+  l'3 = lens (\ ~(_,_,a,_) -> a ) (\ ~(c,d,_,e) b -> (c,d,b,e))
 instance Lens4 a b (c,d,e,a) (c,d,e,b) where
-  _4 = lens (\ ~(_,_,_,a) -> a ) (\ ~(c,d,e,_) b -> (c,d,e,b))
+  l'4 = lens (\ ~(_,_,_,a) -> a ) (\ ~(c,d,e,_) b -> (c,d,e,b))
 instance Trav1 a b (a:+:c) (b:+:c) where
-  _l = prism ((id ||| Right) >>> swapE) (flip (left . const))
+  t'l = prism ((id ||| Right) >>> swapE) (flip (left . const))
     where swapE :: (b:+:a) -> (a:+:b)
           swapE = Right<|>Left
 instance Trav1 a b [a] [b] where
-  _l = prism f g
+  t'l = prism f g
     where f [] = Left []
           f (a:_) = Right a
           g [] _ = []
           g _ b = [b]
 instance Trav2 a b (c:+:a) (c:+:b) where
-  _r = prism (Left ||| id) (flip (right . const))
+  t'r = prism (Left ||| id) (flip (right . const))
 instance Trav2 a b (Maybe a) (Maybe b) where
-  _r = prism (\a -> maybe (Left Nothing) Right a) (flip (<$))
+  t'r = prism (\a -> maybe (Left Nothing) Right a) (flip (<$))
 
 class Compound a b s t | s -> a, b s -> t where
   _each :: Traversal a b s t
@@ -216,15 +218,15 @@
   _each k (a,a',a'') = (,,)<$>k a<*>k a'<*>k a''
 instance Compound a b (a:+:a) (b:+:b) where
   _each k = map Left . k <|> map Right . k
-_list :: [a] :<->: (():+:(a:*:[a]))
-_list = iso (\l -> case l of
+i'list :: [a] :<->: (():+:(a:*:[a]))
+i'list = iso (\l -> case l of
                 [] -> Left ()
                 (x:t) -> Right (x,t)) (const [] <|> uncurry (:))
 
-_head :: Traversal' [a] a
-_head = _l
-_tail :: Traversal' [a] [a]
-_tail = _list._r._2
+t'head :: Traversal' [a] a
+t'head = t'l
+t'tail :: Traversal' [a] [a]
+t'tail = i'list.t'r.l'2
 
 mapping :: (Functor f,Functor f') => Iso s t a b -> Iso (f s) (f' t) (f a) (f' b)
 mapping (isoT -> IsoT u v) = map u `dimap` map (map v)
@@ -235,50 +237,55 @@
 -- ^promapping :: Bifunctor f => Iso' a b -> Iso' (f a c) (f b c)
 
 class Isomorphic b a t s | t -> b, t a -> s where
-  _iso :: Iso s t a b
+  i'_ :: Iso s t a b
 instance Isomorphic a b (Id a) (Id b) where
-  _iso = iso Id getId
+  i'_ = iso Id getId
 instance Isomorphic [a] [b] (OrdList a) (OrdList b) where
-  _iso = iso OrdList getOrdList
+  i'_ = iso OrdList getOrdList
 instance Isomorphic a b (Const a c) (Const b c) where
-  _iso = iso Const getConst
+  i'_ = iso Const getConst
 instance Isomorphic a b (Dual a) (Dual b) where
-  _iso = iso Dual getDual
+  i'_ = iso Dual getDual
+instance Isomorphic a b (Product a) (Product b) where
+  i'_ = iso Product getProduct
 instance Isomorphic a b (Max a) (Max b) where
-  _iso = iso Max getMax
+  i'_ = iso Max getMax
 instance Isomorphic (k a a) (k b b) (Endo k a) (Endo k b) where
-  _iso = iso Endo runEndo
+  i'_ = iso Endo runEndo
 instance Isomorphic (f a b) (f c d) (Flip f b a) (Flip f d c) where
-  _iso = iso Flip unFlip
+  i'_ = iso Flip unFlip
 instance Isomorphic Bool Bool (Maybe a) (Maybe Void) where
-  _iso = iso (bool (Just zero) Nothing) (maybe False (const True))
+  i'_ = iso (bool (Just zero) Nothing) (maybe False (const True))
 instance Isomorphic (f (g a)) (f' (g' b)) ((f:.:g) a) ((f':.:g') b) where
-  _iso = iso Compose getCompose
+  i'_ = iso Compose getCompose
 instance Isomorphic a b (Void,a) (Void,b) where
-  _iso = iso (zero,) snd
-_Id :: Iso (Id a) (Id b) a b
-_Id = _iso
-_OrdList :: Iso (OrdList a) (OrdList b) [a] [b]
-_OrdList = _iso
-_Dual :: Iso (Dual a) (Dual b) a b
-_Dual = _iso
-_Const :: Iso (Const a c) (Const b c) a b
-_Const = _iso
-_Max :: Iso (Max a) (Max b) a b 
-_Max = _iso
-_Endo :: Iso (Endo k a) (Endo k b) (k a a) (k b b)
-_Endo = _iso 
-_maybe :: Iso (Maybe Void) (Maybe a) Bool Bool
-_maybe = _iso 
-_Flip :: Iso (Flip f b a) (Flip f d c) (f a b) (f c d)
-_Flip = _iso
-_Compose :: Iso ((f:.:g) a) ((f':.:g') b) (f (g a)) (f' (g' b))
-_Compose = _iso
-_Backwards :: Iso (Backwards f a) (Backwards g b) (f a) (g b)
-_Backwards = iso Backwards forwards
-_Accum :: Iso (Accum a) (Accum b) (Maybe a) (Maybe b)
-_Accum = iso Accum getAccum
+  i'_ = iso (zero,) snd
+i'Id :: Iso (Id a) (Id b) a b
+i'Id = i'_
+i'OrdList :: Iso (OrdList a) (OrdList b) [a] [b]
+i'OrdList = i'_
+i'Dual :: Iso (Dual a) (Dual b) a b
+i'Dual = i'_
+i'Const :: Iso (Const a c) (Const b c) a b
+i'Const = i'_
+i'Max :: Iso (Max a) (Max b) a b 
+i'Max = i'_
+i'Endo :: Iso (Endo k a) (Endo k b) (k a a) (k b b)
+i'Endo = i'_ 
+i'maybe :: Iso (Maybe Void) (Maybe a) Bool Bool
+i'maybe = i'_ 
+i'Flip :: Iso (Flip f b a) (Flip f d c) (f a b) (f c d)
+i'Flip = i'_
+i'Compose :: Iso ((f:.:g) a) ((f':.:g') b) (f (g a)) (f' (g' b))
+i'Compose = i'_
+i'Backwards :: Iso (Backwards f a) (Backwards g b) (f a) (g b)
+i'Backwards = iso Backwards forwards
+i'Accum :: Iso (Accum a) (Accum b) (Maybe a) (Maybe b)
+i'Accum = iso Accum getAccum
 
+curried :: Iso (a -> b -> c) (a' -> b' -> c') ((a,b) -> c) ((a',b') -> c')
+curried = iso curry uncurry
+
 warp2 :: Iso s t a b -> (s -> s -> t) -> (a -> a -> b)
 warp2 i f = \a a' -> yb i (by i a`f`by i a')
 
@@ -292,10 +299,13 @@
 (<.>) = mapIso2
 infixr 9 <.>
 
+i'pair :: Iso s t a b -> Iso s' t' a' b' -> Iso (s,s') (t,t') (a,a') (b,b')
+i'pair i i' = let IsoT u v = isoT i ; IsoT u' v' = isoT i' in iso (u<#>u') (v<#>v')
+
 instance IsoFunctor ((->) a) where mapIso = mapping
 instance IsoFunctor2 (->) where mapIso2 i j = promapping i.mapping j
 instance IsoFunctor2 (,) where
-  mapIso2 i j = iso (by i <#> by j) (yb i <#> yb j)
+  mapIso2 = i'pair
 instance IsoFunctor2 Either where
   mapIso2 i j = iso (by i ||| by j) (yb i ||| yb j)
 
@@ -317,5 +327,3 @@
                         ,Applicative)
 has :: Fold' a b -> a -> Bool
 has l x = x^?l & \(Test (Const (Product b))) -> b
-
-
diff --git a/Algebra/Monad/Base.hs b/Algebra/Monad/Base.hs
--- a/Algebra/Monad/Base.hs
+++ b/Algebra/Monad/Base.hs
@@ -1,15 +1,19 @@
+{-# LANGUAGE UndecidableInstances #-}
 module Algebra.Monad.Base (
   module Algebra.Classes,module Algebra.Applicative,module Algebra.Core,
   module Algebra.Traversable,module Algebra.Lens,
   
   -- * Monad utilities
-  Kleisli(..),_Kleisli,
+  Kleisli(..),i'Kleisli,
   (=<<),joinMap,(<=<),(>=>),(>>),(<*=),only,return,
   foldlM,foldrM,findM,while,until,
   bind2,bind3,(>>>=),(>>>>=),
+
+  -- * Monadic Lenses
+  Action,Action',
   
   -- * Instance utilities
-  Compose'(..),_Compose'
+  Compose'(..),i'Compose'
   ) where
 
 import Algebra.Classes
@@ -19,6 +23,13 @@
 import Algebra.Lens
 import qualified Control.Monad.Fix as Fix
 
+type Action s t a b = forall m. Monad m => LensLike m s t a b
+type Action' a b = Action b b a a
+
+instance MonadIO IO where liftIO = id
+instance (MonadIO m,MonadTrans t,Monad (t m)) => MonadIO (t m) where
+  liftIO = lift . liftIO
+
 -- MonadFix instances
 instance MonadFix Id where mfix = cfix
 instance MonadFix ((->) b) where mfix = cfix
@@ -33,18 +44,24 @@
 instance Monad m => MonadTrans ((:.:) m) where
   lift = Compose . pure
 instance Monad m => ConcreteMonad ((:.:) m) where
-  generalize = _Compose %%~ map (pure.yb _Id)
+  generalize = i'Compose %%~ map (pure.yb i'Id)
 
 instance MonadFix m => Monad (Backwards m) where
   join (Backwards ma) = Backwards$mfixing (\a -> liftA2 (,) (forwards a) ma)
+instance MonadFuture m (Backwards m) where
+  future = Backwards
 instance MonadFix m => MonadFix (Backwards m) where
-  mfix f = by _Backwards $ mfix (yb _Backwards.f)
+  mfix f = by i'Backwards $ mfix (yb i'Backwards.f)
 instance MonadTrans Backwards where
   lift = Backwards
 instance ConcreteMonad Backwards where
-  generalize = _Backwards %%~ pure.yb _Id
+  generalize = i'Backwards %%~ pure.yb i'Id
 
 newtype Kleisli m a b = Kleisli { runKleisli :: a -> m b }
+instance Functor f => Functor (Kleisli f a) where
+  map f (Kleisli k) = Kleisli (map2 f k)
+instance Contravariant f => Contravariant (Kleisli f a) where
+  collect f = Kleisli (\a -> project (($a) . runKleisli) f)
 instance Monad m => Category (Kleisli m) where
   id = Kleisli pure
   Kleisli f . Kleisli g = Kleisli (\a -> g a >>= f)
@@ -53,7 +70,7 @@
 instance Monad m => Split (Kleisli m) where
   Kleisli f <#> Kleisli g = Kleisli (\(a,c) -> (,)<$>f a<*>g c)
 instance Isomorphic (a -> m b) (c -> m' d) (Kleisli m a b) (Kleisli m' c d) where
-  _iso = iso Kleisli runKleisli
+  i'_ = iso Kleisli runKleisli
 
 cfix :: Contravariant c => (a -> c a) -> c a
 cfix = map fix . collect
@@ -61,15 +78,15 @@
 mfixing :: MonadFix f => (b -> f (a, b)) -> f a
 mfixing f = fst<$>mfix (\ ~(_,b) -> f b )
 
-_Kleisli :: Iso (Kleisli m a b) (Kleisli m' c d) (a -> m b) (c -> m' d)
-_Kleisli = _iso 
+i'Kleisli :: Iso (Kleisli m a b) (Kleisli m' c d) (a -> m b) (c -> m' d)
+i'Kleisli = i'_ 
 
 folding :: (Foldable t,Monoid w) => Iso' (a -> c) w -> (b -> a -> c) -> a -> t b -> c  
 folding i f e t = yb i (foldMap (by i . f) t) e
 foldlM :: (Foldable t,Monad m) => (a -> b -> m a) -> a -> t b -> m a
-foldlM = folding (_Kleisli._Endo._Dual) . flip
+foldlM = folding (i'Kleisli.i'Endo) . flip
 foldrM :: (Foldable t,Monad m) => (b -> a -> m a) -> t b -> a -> m a
-foldrM = flip . folding (_Kleisli._Endo)
+foldrM = flip . folding (i'Kleisli.i'Endo.i'Dual)
 findM :: (Foldable t,Monad m) => (a -> m (Maybe b)) -> t a -> m (Maybe b)
 findM f = foldr fun (return Nothing)
   where fun a b = maybe b (return . Just) =<< f a
@@ -110,12 +127,12 @@
 
 newtype Compose' f g a = Compose' ((g:.:f) a)
                        deriving (Semigroup,Monoid,Unit,Functor,Applicative,Monad,MonadFix,Foldable,Traversable)
-_Compose' :: Iso (Compose' f g a) (Compose' h i b) (g (f a)) (i (h b))
-_Compose' = _Compose.iso Compose' (\(Compose' c) -> c)
+i'Compose' :: Iso (Compose' f g a) (Compose' h i b) (g (f a)) (i (h b))
+i'Compose' = i'Compose.iso Compose' (\(Compose' c) -> c)
 instance Monad m => MonadTrans (Compose' m) where
-  lift = by _Compose' . map pure
+  lift = by i'Compose' . map pure
 instance Monad m => ConcreteMonad (Compose' m) where
-  generalize = _Compose' %%~ pure . yb _Id
+  generalize = i'Compose' %%~ pure . yb i'Id
 
 
 
diff --git a/Algebra/Monad/Cont.hs b/Algebra/Monad/Cont.hs
--- a/Algebra/Monad/Cont.hs
+++ b/Algebra/Monad/Cont.hs
@@ -28,5 +28,5 @@
 contT :: (Monad m,Unit m') => Iso (ContT r m r) (ContT r' m' r') (m r) (m' r')
 contT = iso (\m -> ContT (m >>=)) (\c -> runContT c return)
 cont :: Iso (Cont r r) (Cont r' r') r r'
-cont = _Id.contT
+cont = i'Id.contT
 
diff --git a/Algebra/Monad/Error.hs b/Algebra/Monad/Error.hs
--- a/Algebra/Monad/Error.hs
+++ b/Algebra/Monad/Error.hs
@@ -30,7 +30,7 @@
                       deriving (Unit,Functor,Applicative,Monad,MonadFix
                                ,Foldable,Traversable,MonadTrans)
 _eitherT :: (Functor m) => Iso (EitherT e m a) (EitherT f m b) (m (e:+:a)) (m (f:+:b))                              
-_eitherT = _Compose'.iso EitherT (\(EitherT e) -> e)
+_eitherT = i'Compose'.iso EitherT (\(EitherT e) -> e)
 
 instance MonadError Void Maybe where
   throw = const Nothing
diff --git a/Algebra/Monad/Foldable.hs b/Algebra/Monad/Foldable.hs
--- a/Algebra/Monad/Foldable.hs
+++ b/Algebra/Monad/Foldable.hs
@@ -23,7 +23,7 @@
                               Functor,Applicative,Unit,Monad,
                               Foldable,Traversable,MonadTrans)
 listT :: Iso (ListT m a) (ListT m' a') (m [a]) (m' [a'])
-listT = _Compose'.iso ListT (\(ListT l) -> l)
+listT = i'Compose'.iso ListT (\(ListT l) -> l)
 instance Monad m => MonadList (ListT m) where
   fork = by listT . return 
 instance MonadFix m => MonadFix (ListT m) where
@@ -36,19 +36,21 @@
   censor = listT-.censor.map (\l -> (fst<$>l,compose (snd<$>l))).-listT
 instance Monad m => MonadError Void (ListT m) where
   throw = const zero
-  catch f mm = mm & listT %%~ (\m -> m >>= \_l -> case _l of
-                                   [] -> f zero^..listT; l -> pure l)
+  catch f mm = mm & listT %%~ (\m -> m >>= \_l -> case lazy (traverse Strict _l) of
+                                   [] -> f zero^..listT
+                                   [x] -> pure [x]
+                                   l -> pure l)
 
 newtype TreeT m a = TreeT (Compose' Tree m a)
                   deriving (Functor,Unit,Applicative,Monad,MonadFix,
                             Foldable,Traversable,MonadTrans)
 treeT :: Iso (TreeT m a) (TreeT n b) (m (Tree a)) (n (Tree b))
-treeT = _Compose'.iso TreeT (\(TreeT t) -> t)
+treeT = i'Compose'.iso TreeT (\(TreeT t) -> t)
 
 newtype MaybeT m a = MaybeT (Compose' Maybe m a)
                   deriving (Functor,Unit,Applicative,Monad,MonadFix,
                             Foldable,Traversable,MonadTrans)
 maybeT :: Iso (MaybeT m a) (MaybeT m' b) (m (Maybe a)) (m' (Maybe b))
-maybeT = _Compose'.iso MaybeT (\(MaybeT m) -> m)
+maybeT = i'Compose'.iso MaybeT (\(MaybeT m) -> m)
 
 
diff --git a/Algebra/Monad/RWS.hs b/Algebra/Monad/RWS.hs
--- a/Algebra/Monad/RWS.hs
+++ b/Algebra/Monad/RWS.hs
@@ -42,25 +42,31 @@
   tell w = RWST (\ ~(_,s) -> pure ((),s,w) )
   listen (RWST m) = RWST (m >>> map (\ ~(a,s,w) -> ((w,a),s,w) ) )
   censor (RWST m) = RWST (m >>> map (\ ~(~(a,f),s,w) -> (a,s,f w) ) )
+
 instance Foldable m => Foldable (RWST Void w Void m) where
   fold (RWST m) = foldMap (\(w,_,_) -> w).m $ (zero,zero)
 instance Traversable m => Traversable (RWST Void w Void m) where
   sequence (RWST m) = map (RWST . const . map (\((s,w),a) -> (a,s,w)))
                       . sequence . map (\(a,s,w) -> sequence ((s,w),a))
                       $ m (zero,zero)
+
 instance (Monoid w,MonadError e m) => MonadError e (RWST r w s m) where
   throw = lift.throw
   catch f (RWST m) = RWST (\x -> catch (flip runRWST x.f) (m x))
 instance (Monoid w,MonadList m) => MonadList (RWST r w s m) where
   fork = lift . fork
+
 instance Monoid w => MonadTrans (RWST r w s) where
   lift m = RWST (\ ~(_,s) -> (,s,zero) <$> m)
 instance Monoid w => ConcreteMonad (RWST r w s) where
-  generalize (RWST s) = RWST (\x -> pure (s x^.._Id))
+  generalize (RWST s) = RWST (\x -> pure (s x^..i'Id))
 instance (Monoid w) => MonadInternal (RWST r w s) where
   internal f (RWST m) = RWST (\ x -> f (m x <&> \ ~(a,s,w) -> ((s,w),a) )
                                      <&> \ ~((s,w),b) -> (b,s,w) )
-  
+
+instance (Monad m, Monoid w, MonadFuture n m) => MonadFuture n (RWST r w s m) where
+  future = lift . future
+
 class MonadTrans t => MonadInternal t where
   internal :: Monad m => (forall c. m (c,a) -> m (c,b)) ->
               (t m a -> t m b)
diff --git a/Algebra/Monad/Reader.hs b/Algebra/Monad/Reader.hs
--- a/Algebra/Monad/Reader.hs
+++ b/Algebra/Monad/Reader.hs
@@ -29,11 +29,12 @@
 deriving instance Monoid (m (a,Void,Void)) => Monoid (ReaderT r m a)
 deriving instance Semiring (m (a,Void,Void)) => Semiring (ReaderT r m a)
 deriving instance Ring (m (a,Void,Void)) => Ring (ReaderT r m a)
+deriving instance (Monad m,MonadFuture n m) => MonadFuture n (ReaderT r m)
 
 readerT :: (Functor m,Functor m') => Iso (ReaderT r m a) (ReaderT r' m' b) (r -> m a) (r' -> m' b)
-readerT = iso _readerT _runReaderT
-  where _readerT f = ReaderT (RWST (\ ~(r,_) -> f r<&>(,zero,zero) ))
-        _runReaderT (ReaderT (RWST f)) r = f (r,zero) <&> \ ~(a,_,_) -> a
+readerT = iso t'readerT t'runReaderT
+  where t'readerT f = ReaderT (RWST (\ ~(r,_) -> f r<&>(,zero,zero) ))
+        t'runReaderT (ReaderT (RWST f)) r = f (r,zero) <&> \ ~(a,_,_) -> a
 reader :: Iso (Reader r a) (Reader r' b) (r -> a) (r' -> b)
-reader = mapping _Id.readerT
+reader = mapping i'Id.readerT
 
diff --git a/Algebra/Monad/State.hs b/Algebra/Monad/State.hs
--- a/Algebra/Monad/State.hs
+++ b/Algebra/Monad/State.hs
@@ -36,18 +36,19 @@
 deriving instance Monoid (m (a,s,Void)) => Monoid (StateT s m a)
 deriving instance Semiring (m (a,s,Void)) => Semiring (StateT s m a)
 deriving instance Ring (m (a,s,Void)) => Ring (StateT s m a)
+deriving instance (Monad m,MonadFuture n m) => MonadFuture n (StateT s m)
 
 _StateT :: Iso (StateT s m a) (StateT t n b) (RWST Void Void s m a) (RWST Void Void t n b)
 _StateT = iso StateT (\ ~(StateT s) -> s)
 stateT :: (Functor m,Functor n) => Iso (StateT s m a) (StateT t n b) (s -> m (s,a)) (t -> n (t,b))
 stateT = mapping (mapping $ iso (\ ~(s,a) -> (a,s,zero) ) (\(a,s,_) -> (s,a)))
-          .promapping _iso._RWST._StateT
+          .promapping i'_._RWST._StateT
 eval :: (s ->  (a, b)) -> (s -> b)
 eval = map snd
 exec :: Functor f => f (a, b) -> f a
 exec = map fst
 state :: Iso (State s a) (State t b) (s -> (s,a)) (t -> (t,b))
-state = mapping _Id.stateT
+state = mapping i'Id.stateT
 
 (=-) :: MonadState s m => Traversal' s s' -> s' -> m ()
 infixl 0 =-,=~
@@ -75,7 +76,7 @@
 instance Monad m => Split (StateA m) where
   StateA sac <#> StateA sbd = StateA $ (^.stateT)
                               $ map2 (\((a',c),(b',d)) -> ((a',b'),(c,d)))
-                              $ (Kleisli (sac^..stateT) <#> Kleisli (sbd^..stateT)) ^.. _Kleisli
+                              $ (Kleisli (sac^..stateT) <#> Kleisli (sbd^..stateT)) ^.. i'Kleisli
 instance Monad m => Choice (StateA m) where
   StateA sac <|> StateA sbc = StateA $ (^.stateT) $
                               l Left (sac^..stateT)<|>l Right (sbc^..stateT)
@@ -86,7 +87,7 @@
 mapAccum_ :: Traversable t => (a -> s -> (s, b)) -> t a -> s -> t b
 mapAccum_ = (map.map.map) snd mapAccum
 mapAccumR :: Traversable t => (a -> s -> (s, b)) -> t a -> s -> (s, t b)
-mapAccumR f t = traverse (by (state._Backwards)<$>f) t^..state._Backwards
+mapAccumR f t = traverse (by (state.i'Backwards)<$>f) t^..state.i'Backwards
 mapAccumR_ :: Traversable t => (a -> s -> (s, b)) -> t a -> s -> t b
 mapAccumR_ = (map.map.map) snd mapAccumR
 
diff --git a/Algebra/Monad/Writer.hs b/Algebra/Monad/Writer.hs
--- a/Algebra/Monad/Writer.hs
+++ b/Algebra/Monad/Writer.hs
@@ -2,7 +2,7 @@
 module Algebra.Monad.Writer (
     -- * The Writer monad
   MonadWriter(..),
-  mute,intercept,
+  mute,intercept,intercept',eavesdrop,
 
   -- * The Writer transformer
   WriterT,Writer,
@@ -28,6 +28,10 @@
 mute m = censor (m<&>(,const zero))
 intercept :: (MonadWriter w m,Monoid w) => m a -> m (w,a)
 intercept = listen >>> mute
+eavesdrop :: (MonadWriter w m,Monoid w) => m a -> m w
+eavesdrop = map fst . listen
+intercept' :: (MonadWriter w m,Monoid w) => m a -> m w
+intercept' = map fst . intercept
 
 {-| A simple Writer monad -}
 newtype WriterT w m a = WriterT (RWST Void w Void m a)
@@ -44,13 +48,14 @@
 deriving instance Monoid (m (a,Void,w)) => Monoid (WriterT w m a)
 deriving instance Semiring (m (a,Void,w)) => Semiring (WriterT w m a)
 deriving instance Ring (m (a,Void,w)) => Ring (WriterT w m a)
+deriving instance (Monad m, Monoid w, MonadFuture n m) => MonadFuture n (WriterT w m)
 
 writerT :: (Functor m,Functor m') => Iso (WriterT w m a) (WriterT w' m' b) (m (w,a)) (m' (w',b))
-writerT = iso _writerT _runWriterT
+writerT = iso _writerT t'runWriterT
   where _writerT mw = WriterT (RWST (pure (mw <&> \ ~(w,a) -> (a,zero,w) )))
-        _runWriterT (WriterT (RWST m)) = m (zero,zero) <&> \ ~(a,_,w) -> (w,a)
+        t'runWriterT (WriterT (RWST m)) = m (zero,zero) <&> \ ~(a,_,w) -> (w,a)
 writer :: Iso (Writer w a) (Writer w' b) (w,a) (w',b)
-writer = _Id.writerT
+writer = i'Id.writerT
 pureWriter :: Monoid w => Iso (w,a) (w',b) a b
 pureWriter = iso (zero,) snd
 
@@ -72,6 +77,7 @@
 instance (MonadState s m,Monoid w,SubSemi acc w) => MonadState s (WriterAccT w acc m) where
   get = WA (lift get)
   put = WA . lift . put
+deriving instance (Monad m, Monoid w, MonadFuture n m) => MonadFuture n (WriterAccT w acc m)
 
 _WriterAccT :: Iso (WriterAccT w acc m a) (WriterAccT w' acc' m' a') (RWST () w acc m a) (RWST () w' acc' m' a')
 _WriterAccT = iso WA runWA
@@ -80,4 +86,4 @@
 writerAccT = iso (\m (_,s) -> m <&> \(a,s',w) -> (a,s+s',w)) ($zero)._RWST._WriterAccT
 writerAcc :: (SubSemi acc w,SubSemi acc' w',Monoid acc,Monoid acc',Functor m)
              => Iso (WriterAcc w acc a) (WriterAcc w' acc' a') (a,acc,w) (a',acc',w')
-writerAcc = _Id.writerAccT
+writerAcc = i'Id.writerAccT
diff --git a/Algebra/Time.hs b/Algebra/Time.hs
deleted file mode 100644
--- a/Algebra/Time.hs
+++ /dev/null
@@ -1,138 +0,0 @@
-{-# LANGUAGE TupleSections, RecursiveDo, Rank2Types, DeriveDataTypeable, ImplicitParams #-}
-module Algebra.Time (
-  -- * Unambiguous times
-  Time,
-  module Data.TimeVal,
-  timeVal,
-
-  -- * Time utilities
-  Seconds,
-  timeIO,waitTill,currentTime,timeOrigin,
-
-  -- * Conversion functions
-  ms,mus,ns,minutes,hours,days
-  ) where
-
-import Algebra
-import Control.Concurrent
-import Data.TimeVal
-import System.IO.Unsafe
-import Data.IORef
-import System.Clock
-import Control.Exception (handle,Exception(..))
-import Data.Typeable
-
-data Freezed = Freezed
-             deriving (Typeable,Show)
-instance Exception Freezed  
-
--- |A type wrappers for timestamps that can be compared unambiguously
-data Time t = Time (TimeVal t -> TimeVal t) (TimeVal t -> TimeVal t)
-instance (Eq t,Show t) => Show (Time t) where show = show . timeVal
-instance Ord t => Eq (Time t) where
-  a == b = compare a b == EQ
-instance Ord t => Ord (Time t) where
-  compare ~(Time fa fa') ~(Time fb fb') =
-    cmp fa fb' `unamb` invertOrd (cmp fb fa')
-    where cmp f f' = compare a (f' a)
-            where a = f maxBound
--- |The Time semigroup where @ta + tb == max ta tb@
-instance Ord t => Semigroup (Time t) where
-  ~(Time fa fb) + ~(Time fa' fb') = Time (mapTL mini fa fa') (mapTL maxi fb fb')
-    where mini h x x' = if h < x then x else max x x'
-          maxi h x x' = if h > x then max x x' else x
--- |The Time monoid where @zero == minBound@
-instance Ord t => Monoid (Time t) where
-  zero = minBound
--- |The Time ring where @(*) == min@ and @one == maxBound@
-instance Ord t => Semiring (Time t) where
-  ~(Time fa fb) * ~(Time fa' fb') = Time (mapTL mini fa fa') (mapTL maxi fb fb')
-    where mini h x x' = if h < x then min x x' else x
-          maxi h x x' = if h > x then x else min x x'
-instance Ord t => Ring (Time t) where
-  one = maxBound
-instance Ord t => Orderable (Time t) where
-  inOrder a b = (a*b,if z then b else a,z)
-    where z = a<=b
-
-mapTL :: Bounded c => (a -> b -> b -> c) -> (a -> b) -> (a -> b) -> a -> c
-mapTL _max fa fa' h = _max h x x'`unamb`_max h x' x
-  where x = fa h ; x' = fa' h
-
-instance Bounded (Time t) where
-  minBound = Time (pure minBound) (pure minBound)
-  maxBound = Time (pure maxBound) (pure maxBound)
-instance Unit Time where
-  pure t = Time (pure (pure t)) (pure (pure t)) 
-
-amb :: IO a -> IO a -> IO a
-ma `amb` mb = do
-  res <- newEmptyMVar
-  ta <- forkIO $ handle (\Freezed -> unit) $ ma >>= putMVar res . Left
-  tb <- forkIO $ handle (\Freezed -> unit) $ mb >>= putMVar res . Right
-
-  takeMVar res >>= \c -> case c of
-    Left a -> a <$ killThread tb
-    Right a -> a <$ killThread ta
-ambBnd :: Bounded a => IO a -> IO a -> IO a
-ambBnd a b = try (return maxBound) (a`amb`b)
-unamb :: Bounded a => a -> a -> a
-unamb = warp2 (from thunk) ambBnd
-
-type Seconds = Double
-
--- |A Time's pure value. May not be defined immediately.
-timeVal :: Time t -> TimeVal t
-timeVal (Time fa _) = fa maxBound
-
--- |Constructs a Time representing the time by which the argument terminates.
---
--- Warning: This function executes its argument, ignoring its
--- value. Thus, it would be wise to use it on idempotent blocking
--- actions, such as @readMVar@.
-timeIO :: IO a -> IO (Time Seconds)
-timeIO io = do
-  sem <- newEmptyMVar
-  ret <- newIORef id
-  
-  minAction <- newIORef $ \tm -> readIORef ret <**> amb (readMVar sem) (
-    Since<$>case tm of
-       Always -> currentTime
-       Since t -> waitTill t >> currentTime
-       Never -> throw (toException Freezed))
-  maxAction <- newIORef $ \tm -> readIORef ret <**> amb (readMVar sem) (
-    case tm of
-      Always -> throw (toException Freezed)
-      Since t -> waitTill t >> pure Never
-      Never -> Since<$>currentTime)
-    
-  let refAction ref = \t -> unsafePerformIO (join (readIORef ref<*>pure t))
-  _ <- forkIO $ void $ mfix $ \t -> do 
-    t' <- catch (\_ -> return Never) (io >> return (pure t))
-    writeIORef minAction (const (pure t'))
-    writeIORef maxAction (const (pure t'))
-    writeIORef ret (const t')
-    putMVar sem t'
-    currentTime
-    
-  return $ Time (refAction minAction) (refAction maxAction)
-  
-waitTill :: Seconds -> IO ()
-waitTill t = do
-  now <- t `seq` currentTime
-  when (t>now) $ threadDelay (floor $ (t-now)*1000000)
-
-seconds :: TimeSpec -> Seconds
-seconds t = fromIntegral (sec t) + fromIntegral (nsec t)/1000000000 :: Seconds
-currentTime :: IO Seconds
-currentTime = seconds<$>getTime Realtime
-timeOrigin :: (( ?birthTime :: Seconds ) => IO a) -> IO a
-timeOrigin m = currentTime >>= \t -> let ?birthTime = t in m
-
-ms,mus,ns,minutes,hours,days :: Seconds -> Seconds
-ms = (/1000)
-mus = (/1000000)
-ns = (/1000000000)
-minutes = (*60)
-hours = (*3600)
-days = (*(3600*24))
diff --git a/Algebra/Traversable.hs b/Algebra/Traversable.hs
--- a/Algebra/Traversable.hs
+++ b/Algebra/Traversable.hs
@@ -3,7 +3,7 @@
 
   Traversable(..),Contravariant(..),
 
-  traverse,foreach,transpose,flip,project,doTimes,converted,folded,
+  traverse,for,transpose,doTimes,converted,folded,
   ) where
 
 import Algebra.Classes
@@ -13,8 +13,6 @@
 import Algebra.Lens
 import Data.Tree
 
-class Foldable t => Traversable t where
-  sequence :: Applicative f => t (f a) -> f (t a)
 instance Traversable ((,) c) where
   sequence ~(c,m) = (,) c<$>m
 instance Traversable (Either a) where
@@ -24,10 +22,9 @@
   sequence [] = pure []
 deriving instance Traversable Interleave
 deriving instance Traversable OrdList
-deriving instance Traversable ZipList
+deriving instance Traversable f => Traversable (Zip f)
 instance Traversable Tree where
   sequence (Node a subs) = Node<$>a<*>sequence (map sequence subs)
-deriving instance Traversable ZipTree
 instance (Traversable f,Traversable g) => Traversable (f:.:g) where
   sequence = getCompose >>> map sequence >>> sequence >>> map Compose
 instance (Traversable f,Traversable g) => Traversable (f:**:g) where
@@ -39,11 +36,6 @@
   sequence Nothing = pure Nothing
   sequence (Just a) = Just<$>a
 
-class Functor t => Contravariant t where
-  collect :: Functor f => f (t a) -> t (f a)
-instance Contravariant Id where collect f = Id (map getId f)
-instance Contravariant ((->) a) where collect f = \a -> map ($a) f
-
 converted :: (Unit f,Unit g,Foldable f,Foldable g,Monoid (f a),Monoid (g b)) => Iso (f a) (f b) (g a) (g b)
 converted = iso convert convert
 folded :: (Unit f',Foldable f,Monoid m) => Iso m m' (f m) (f' m')
@@ -51,17 +43,12 @@
 
 traverse :: (Applicative f,Traversable t) => (a -> f b) -> t a -> f (t b)
 traverse f t = sequence (map f t)
-foreach :: (Applicative f,Traversable t) => t a -> (a -> f b) -> f (t b)
-foreach = flip traverse
+for :: (Applicative f,Traversable t) => t a -> (a -> f b) -> f (t b)
+for = flip traverse
 doTimes :: Applicative f => Int -> f a -> f [a]
 doTimes n m = sequence (m <$ [1..n])
 transpose :: (Applicative f,Traversable t) => t (f a) -> f (t a)
 transpose = sequence
-flip :: (Contravariant c,Functor f) => f (c a) -> c (f a)
-flip = collect
--- | The Contravariant version of 'traverse'
-project :: (Contravariant c,Functor f) => (a -> c b) -> f a -> c (f b)
-project f x = collect (map f x)
 
 instance Compound a b [a] [b] where
   _each = traverse
diff --git a/Data/Containers.hs b/Data/Containers.hs
--- a/Data/Containers.hs
+++ b/Data/Containers.hs
@@ -1,14 +1,14 @@
 {-# LANGUAGE MultiParamTypeClasses, ViewPatterns, ScopedTypeVariables #-}
 module Data.Containers(
   -- * The basic data class
-  DataMap(..),Indexed(..),OrderedMap(..),
+  DataMap(..),Indexed(..),OrderedMap(..),Container(..),
   
-  member,delete,touch,insert,singleton,fromList,
-  _set,_map,cached,
+  lookup,present,member,delete,touch,insert,singleton,singleton',fromList,fromList',(#),(#?),
+  cached,
 
   -- * Map instances
   -- ** Sets and maps
-  Set,Map,
+  Set,Map,c'setOf,c'set,c'mapOf,c'map,
   
   -- ** Bimaps
   Bimap(..),toMap,keysSet,
@@ -18,7 +18,7 @@
   )
   where
 
-import Algebra
+import Definitive.Base
 import qualified Data.Set as S
 import qualified Data.Map as M
 import Data.Map (Map)
@@ -29,33 +29,59 @@
   at :: k -> Lens' m (Maybe a)
 class Indexed f i | f -> i where
   keyed :: Iso (f (i,a)) (f (i,b)) (f a) (f b) 
+class Container c where weight :: c a -> Int
+
+instance Indexed [] Int where
+  keyed = iso (zip [0..]) (map snd)
+instance Container [] where weight = size
+instance Container Set where weight = S.size
+instance Container (Map k) where weight = M.size
 class OrderedMap m k a m' k' a' | m -> k a, m' -> k' a' where
   ascList :: Iso [(k,a)] [(k',a')] m m'
 
-_set :: Set a -> Set a
-_set = id
-_map :: Map a b -> Map a b
-_map = id
+c'setOf :: Constraint a -> Constraint (Set a)
+c'setOf _ = id
+c'mapOf :: Constraint a -> Constraint b -> Constraint (Map a b)
+c'mapOf _ _ = id
+c'set :: Constraint (Set a)
+c'set = c'setOf id
+c'map :: Constraint (Map a b)
+c'map = c'mapOf id id
 
 member :: DataMap m k Void => k -> Lens' m Bool
-member k = at k.from _maybe
+member k = at k.from i'maybe
+
+lookup :: DataMap m k a => k -> m -> Maybe a
+lookup s m = m^.at s
+present :: DataMap m k a => k -> m -> Bool
+present = map2 nonempty lookup
 delete :: DataMap m k a => k -> m -> m
 delete k = at k %- Nothing
 insert :: DataMap m k a => k -> a -> m -> m
 insert k a = at k %- Just a
+(#) :: DataMap m k a => m -> [(k,a)] -> m
+m # ks = compose [insert k a | (k,a) <- ks] m
 touch :: (Monoid a, DataMap m k a) => k -> m -> m
 touch k = insert k zero
 singleton :: DataMap m k a => k -> a -> m
 singleton = map2 ($zero) insert
+singleton' :: (Monoid a,DataMap m k a) => k -> m
+singleton' x = touch x zero
 fromList :: DataMap m k a => [(k,a)] -> m
 fromList l = compose (uncurry insert<$>l) zero
+fromList' :: (Monoid a,DataMap m k a) => [k] -> m
+fromList' l = compose (touch<$>l) zero
 
 instance Ord a => DataMap (Set a) a Void where
-  at k = lens (S.member k) (flip (bool (S.insert k) (S.delete k)))._maybe
+  at k = lens (S.member k) (flip (bool (S.insert k) (S.delete k))).i'maybe
 instance Eq b => OrderedMap (Set a) a Void (Set b) b Void where
-  ascList = iso S.toAscList S.fromAscList . mapping (_iso.commuted)
+  ascList = iso S.toAscList S.fromAscList . mapping (i'_.commuted)
 instance Ord k => DataMap (Map k a) k a where
   at k = lens (M.lookup k) (\m a -> M.alter (const a) k m)
+instance Eq k => DataMap [(k,a)] k a where
+  at k = lens (foldMap (\(k',a) -> a <$ guard (k==k'))) g
+    where g l Nothing = [(k',a) | (k',a) <- l, k' /= k ]
+          g l (Just a) = (k,a) : l
 instance Eq k' => OrderedMap (Map k a) k a (Map k' a') k' a' where 
   ascList = iso M.toAscList M.fromAscList
   
@@ -72,7 +98,7 @@
 instance (Ord k,Semigroup a) => Semiring (Map k a) where (*) = M.intersectionWith (+)
 instance Functor (Map k) where map = M.map
 instance Foldable (Map k) where fold = M.foldr (+) zero
-instance Eq k => Traversable (Map k) where sequence = (ascList._Compose) sequence
+instance Eq k => Traversable (Map k) where sequence = (ascList.i'Compose) sequence
 instance Indexed (Map k) k where keyed = iso (M.mapWithKey (,)) (map snd)
 
 -- |An invertible map
@@ -82,14 +108,14 @@
   commute (Bimap (b,a)) = Bimap (a,b)
 
 instance (Ord a,Ord b) => DataMap (Bimap a b) a b where
-  at a = lens lookup setAt
-    where lookup ma = toMap ma^.at a
+  at a = lens t'lookup setAt
+    where t'lookup ma = toMap ma^.at a
           setAt (Bimap (ma,mb)) b' = Bimap (
             maybe id delete (b' >>= \b'' -> mb^.at b'') ma & at a %- b',
             mb & maybe id delete b >>> maybe id (flip insert a) b')
             where b = ma^.at a 
 instance (Ord b,Ord a) => DataMap (Flip Bimap b a) b a where
-  at k = from (commuted._Flip).at k
+  at k = from (commuted.i'Flip).at k
 instance (Ord a,Ord b,Ord c,Ord d) => OrderedMap (Bimap a b) a b (Bimap c d) c d where
   ascList = iso (toMap >>> \m -> m^.ascList) (\l -> Bimap (l^..ascList,l^..ascList.mapping commuted))
 toMap :: Bimap a b -> Map a b
@@ -100,7 +126,12 @@
 
 --- |The Relation type
 newtype Relation a b = Relation (Map a (Set b),Map b (Set a))
-                     deriving (Show,Semigroup,Monoid,Eq,Ord)
+                     deriving (Show,Eq,Ord)
+instance (Ord a,Ord b) => Semigroup (Relation a b) where
+  Relation (x,x') + Relation (y,y') = Relation (M.unionWith (+) x y,M.unionWith (+) x' y')
+deriving instance (Ord a,Ord b) => Monoid (Relation a b)
+instance (Ord a,Ord b) => Semiring (Relation a b) where
+  Relation (x,x') * Relation (y,y') = Relation (M.intersectionWith (*) x y,M.intersectionWith (*) x' y')
 _Relation :: Iso (Relation a b) (Relation c d) (Map a (Set b),Map b (Set a)) (Map c (Set d),Map d (Set c))
 _Relation = iso Relation (\(Relation r) -> r)
 instance Commutative Relation where
@@ -132,6 +163,9 @@
 
 link :: (Ord a,Ord b) => a -> b -> Lens' (Relation a b) Bool
 link a b = related a.member b
+
+(#?) :: (Ord a,Ord b) => Relation a b -> [(a,b)] -> Relation a b
+r #? ls = compose [link a b %- True | (a,b) <- ls] r
 
 cached :: forall a b. Ord a => (a -> b) -> a -> b
 cached f = \a -> g a^.thunk
diff --git a/Data/Containers/Monad.hs b/Data/Containers/Monad.hs
new file mode 100644
--- /dev/null
+++ b/Data/Containers/Monad.hs
@@ -0,0 +1,12 @@
+module Data.Containers.Monad where
+
+import Definitive.Base
+import Data.Containers
+
+instance (Monoid k,Ord k) => Unit (Map k) where
+  pure a = singleton zero a
+instance (Monoid k,Ord k) => Applicative (Map k)
+instance (Monoid k,Ord k) => Monad (Map k) where
+  join m = foldMap fun (m^.keyed)
+    where fun (k,m') = m' & ascList %~ \l -> [(k+k',a) | (k',a) <- l]
+
diff --git a/Data/Containers/Sequence.hs b/Data/Containers/Sequence.hs
--- a/Data/Containers/Sequence.hs
+++ b/Data/Containers/Sequence.hs
@@ -4,14 +4,20 @@
   -- * Strict and lazy slices (bytestrings on arbitrary Storable types)
   Slice,Slices,slice,slices,_Slices,breadth,
 
-  V.unsafeWith
+  V.unsafeWith,sliceElt,span,break,
+
+  takeWhile,takeUntil,dropWhile,dropUntil,
+
+  (++)
   ) where
 
-import Algebra hiding (splitAt,take,drop)
+import Definitive.Base
 import qualified Data.List as L
 import qualified Data.ByteString.Lazy as Bytes
 import qualified Data.ByteString.Char8 as Char8
 import qualified Data.Vector.Storable as V
+import qualified Prelude as P
+import Unsafe.Coerce (unsafeCoerce)
 
 class Monoid t => Sequence t where
   splitAt :: Int -> t -> (t,t)
@@ -60,5 +66,34 @@
 slices :: (V.Storable a,V.Storable b) => Iso (Slices a) (Slices b) (Slice a) (Slice b)
 slices = iso pure V.concat . _Slices
 
+newtype PMonad m a = PMonad { runPMonad :: m a }
+instance Functor m => P.Functor (PMonad m) where fmap f (PMonad m) = PMonad (map f m)
+instance Monad m => P.Monad (PMonad m) where
+  PMonad m >>= k = PMonad (m >>= runPMonad . k)
+  return = PMonad . pure
+
+sliceElt :: (V.Storable a,V.Storable b) => Action a b (Slice a) (Slice b)
+sliceElt f = V.mapM (unsafeCoerce f) <&> runPMonad
+
 breadth :: V.Storable a => Slices a -> Int
 breadth s = s^.._Slices & foldMap V.length
+
+span :: Stream c s => (c -> Bool) -> s -> ([c],s)
+span p = fix $ \f s -> (case uncons s of
+                             Just (a,t) | p a -> let ~(l,t') = f t in (a:l,t')
+                             _ -> ([],s))
+break :: Stream c s => (c -> Bool) -> s -> ([c],s)
+break = span . map not
+
+takeWhile :: Stream c s => (c -> Bool) -> s -> [c]
+takeWhile p = fst . span p
+dropWhile :: Stream c s => (c -> Bool) -> s -> s
+dropWhile p = snd . span p
+takeUntil :: Stream c s => (c -> Bool) -> s -> [c]
+takeUntil = takeWhile . map not
+dropUntil :: Stream c s => (c -> Bool) -> s -> s
+dropUntil = dropWhile . map not
+
+(++) :: Stream c s => [c] -> s -> s
+(a:t) ++ c = cons a (t++c)
+[] ++ c = c
diff --git a/Data/Probability.hs b/Data/Probability.hs
--- a/Data/Probability.hs
+++ b/Data/Probability.hs
@@ -1,20 +1,26 @@
 module Data.Probability where
 
-import Algebra
+import Definitive
 
 newtype ProbT t m a = ProbT (WriterT (Product t) (ListT m) a)
                     deriving (Unit,Functor,Applicative,Monad
+                             ,Semigroup,Monoid
                              ,MonadFix,MonadWriter (Product t))
 type Prob t a = ProbT t Id a
-                             
-_ProbT :: Iso (ProbT t m a) (ProbT t' m' a') (WriterT (Product t) (ListT m) a) (WriterT (Product t') (ListT m') a')
-_ProbT = iso ProbT (\(ProbT p) -> p)
-probT :: (Functor m,Functor m') => Iso (ProbT t m a) (ProbT t' m' a') (m [(Product t,a)]) (m' [(Product t',a')])
-probT = listT.writerT._ProbT
-prob :: Iso (Prob t a) (Prob t' a') [(Product t,a)] [(Product t',a')]
-prob = _Id.probT
 
+i'ProbT :: Iso (ProbT t m a) (ProbT t' m' a') (WriterT (Product t) (ListT m) a) (WriterT (Product t') (ListT m') a')
+i'ProbT = iso ProbT (\(ProbT p) -> p)
+probT :: (Functor m,Functor m') => Iso (ProbT t m a) (ProbT t' m' a') (m [(t,a)]) (m' [(t',a')])
+probT = listT.mapping (i'pair i'_ id).writerT.i'ProbT
+prob :: Iso (Prob t a) (Prob t' a') [(t,a)] [(t',a')]
+prob = i'Id.probT
+
+c'prob :: Constraint t -> Constraint (Prob t a)
+c'prob _ = id
+
 instance (Monad m,Ring t,Fractional t) => MonadList (ProbT t m) where
-  fork l = pure [(Product x,a) | a <- l]^.probT
+  fork l = pure [(x,a) | a <- l]^.probT
     where x = 1/size l
 
+sample :: (Eq a,Monoid t) => a -> Prob t a -> (t,t)
+sample x p = foldMap (\(t,y) -> (if x==y then t else zero,t)) (p^..prob)
diff --git a/Data/Reactive.hs b/Data/Reactive.hs
deleted file mode 100644
--- a/Data/Reactive.hs
+++ /dev/null
@@ -1,209 +0,0 @@
-{-# LANGUAGE RebindableSyntax, GeneralizedNewtypeDeriving, TupleSections, FlexibleInstances, MultiParamTypeClasses, RankNTypes, ViewPatterns #-}
-module Data.Reactive (
-  -- * Reactive Modules
-  module Algebra.Time,
-
-  -- * Reactive Events
-  Event,_event,headE,Reactive(..),
-
-  -- ** Contructing events
-  atTimes,mkEvent,
-  withTime,times,times',
-  mapFutures,
-
-  -- ** Combining events
-  (//),(<|*>),(<*|>),
-               
-  -- ** Filtering events
-  groupE,mask,
-
-  -- ** Real-world event synchronization
-  realize,realtime,realizeRT,eventMay,event,react,react2,react3,
-  
-  -- * Future values
-  Future,_future,_time,_value,futureIO,
-  ) where
-
-import Algebra
-import Control.Concurrent
-import Data.TimeVal
-import System.IO.Unsafe (unsafeInterleaveIO)
-import Data.List (group)
-import Algebra.Time
-
--- |An event (a list of time-value pairs of increasing times)
-newtype Event t a = Event { getEvent :: (OrdList:.:Future t) a }
-                  deriving (Unit,Functor,Foldable,Traversable)
-data Reactive t a = Reactive a (Event t a)
-instance Ord t => Unit (Reactive t) where
-  pure a = Reactive a zero
-instance Functor (Reactive t) where 
-  map f (Reactive a e) = Reactive (f a) (map f e)
-instance Ord t => Applicative (Reactive t) where
-  Reactive f fs <*> Reactive x xs = Reactive (f x) (cons f fs<*>cons x xs)
-    where cons a = _event %%~ ((minBound,a)^._future :)
-
-instance (Ord t,Show t,Show a) => Show (Event t a) where show = show . yb _event
-instance Ord t => Semigroup (Event t a) where
-  (+) = (++)^.(_event<.>_event<.>_event)
-    where (x:xt) ++ (y:yt) = a : zs
-            where (a,b,sw) = inOrder x y
-                  zs | b==maxBound = if sw then xt else yt
-                     | sw = xt ++ (y:yt)
-                     | otherwise = (x:xt) ++ yt
-          a ++ [] = a
-          [] ++ b = b
-instance Ord t => Monoid (Event t a) where
-  zero = [(maxBound,undefined)]^.mapping _future._event
-instance Ord t => Applicative (Event t) where
-  fe@(yb _event -> ff:_) <*> xe@(yb _event -> fx:_) =
-    ste & traverse (by state) & yb state & map snd & \st ->
-    br (ff^._time + fx^._time) (st (ff^._value,fx^._value))
-    where ste = map (\f (_,x) -> ((f,x),f x)) fe
-              + map (\x (f,_) -> ((f,x),f x)) xe
-          br t (yb _event -> e) = uniq (map (_time %- t) b + a)^._event
-            where (b,a) = span (\f -> f^._time<t) e
-                  uniq = map last . group
-  _ <*> _ = zero
-instance Ord t => Monad (Event t) where
-  join = _event %%~ merge . map2 (yb _event)
-    where
-      merge [] = []
-      merge [t] = t^._value
-      merge (xs:ys:t) = xi + merge ((ys&_value%~add xe) : t) & _head._time%~(tx+)
-        where add = warp2 _OrdList (+)
-              (tx,(xi,xe)) = xs^.._future & _2%~break (ltFut ys)
-type EventRep t a = OrdList (Future t a)
-_Event :: Iso (Event t a) (Event t' b) (EventRep t a) (EventRep t' b)
-_Event = _Compose.iso Event getEvent
-_event :: Iso (Event t a) (Event t' b) [Future t a] [Future t' b]
-_event = _OrdList._Event
-atTimes :: [t] -> Event t ()
-atTimes ts = (ts <&> \t -> (pure t,())^._future)^._event
-mkEvent :: [(t,a)] -> Event t a
-mkEvent as = (as <&> by _future . (_1 %~ pure))^._event
-
-{-| The \'splice\' operator. Occurs when @a@ occurs.
-
-> by t: a // b = (a,before t: b)
--}
-(//) :: Ord t => Event t a -> Event t b -> Event t (a, Event t b)
-ea // eb = mapAccum_ fun (ea^.._event) (eb^.._event) ^. _event
-  where fun a bs = (ys,a & _value %~ (,xs^._event))
-          where (xs,ys) = span (flip ltFut a) bs
-infixl 1 //
-
-{-|
-The \'over\' operator. Occurs only when @a@ occurs.
-
-> by t: a <|*> (bi,b) = a <*> (minBound,bi):b
--}
-(<*|>) :: Ord t => Event t (a -> b) -> Reactive t a -> Event t b
-ef <*|> Reactive a ea = (traverse tr (ef // ea) ^.. state <&> snd) a
-  where tr (f,as) = traverse_ put as >> f<$>get
-infixl 1 <*|>
-(<|*>) :: Ord t => Reactive t (a -> b) -> Event t a -> Event t b
-f <|*> a = (&)<$>a<*|>f
-infixr 1 <|*>
-
--- |Group the occurences of an event by equality. Occurs when the first occurence of a group occurs. 
-groupE :: (Eq a, Ord t) => Event t a -> Event t (Event t a)
-groupE = _event %%~ group_ . (+repeat (Future (maxBound,undefined)))
-  where group_ fs = (f & _value %- (xs^._event))
-                    : (z & _time %~ (sum_ (by _time<$>xs)+)):zs
-          where (xs,ys) = span ((==f^._value) . by _value) fs ; f = head fs
-                ~(z:zs) = group_ ys
-                sum_ = foldl' (+) zero
-headE :: Event t a -> a
-headE = by _value . head . yb _event
-
-mapFutures :: (Future t a -> Future t' b) -> Event t a -> Event t' b
-mapFutures f = _event %%~ map f
-withTime :: Ord t => Event t a -> Event t (Time t,a)
-withTime = mapFutures (_future %%~ listen)
-times :: Ord t => Event t a -> Event t (Time t)
-times = map2 fst withTime
-times' :: (Ord t,Monoid t) => Event t a -> Event t t
-times' = map2 (fold . timeVal) times
-
-mask :: Ord t => Event t Bool -> Event t a -> Event t a
-mask m ea = (m // ea) `withNext` (True,zero) >>= \((b,_),(_,a)) -> guard b >> a
-
--- |Sinks an action event into the Real World. Actions are evaluated
--- as closely to their specified time as possible. However, they are
--- all executed in order, even if it means delaying the next action
--- further than its required time. For real-time realization of
--- events, see the 'realizeRT' function
-realize :: Event Seconds (IO ()) -> IO ()
-realize l = traverse_ (sink_ . first timeVal) (withTime l)
-  where sink_ (Since t,v) = waitTill t >> v
-        sink_ (Always,v) = v
-        sink_ (Never,_) = unit
-
--- |Creates a real-time action event (an event that skips "frames" as needed) from an ordinary event.
-realtime :: Event Seconds (IO ()) -> Event Seconds (IO ())
-realtime e = (e & flip withNext (maxBound,undefined).withTime) <&> \((_,m),(t,_)) -> do
-  c <- currentTime
-  when (pure c<t) m
-        
--- |Sinks a frame event into the real-world, skipping frames if they come
--- too late, thus always performing the frame closest to the current time.
-realizeRT :: Event Seconds (IO ()) -> IO ()
-realizeRT = realize . realtime
-
-eventMay :: IO (Maybe a) -> IO (Event Seconds a)
-eventMay m = by _event <$> do
-  c <- newChan
-  sem <- newEmptyMVar
-  _ <- forkIO $ do
-    while $ do
-      a <- newEmptyMVar
-      writeChan c a
-      foldMap (const True)<$>(m <*= maybe unit (putMVar a))
-    putMVar sem ()
-  let event' ~(a:as) = unsafeInterleaveIO $ do
-        (:)<$>futureIO (takeMVar a)<*>event' as
-  (event' =<< getChanContents c) <*= \e -> do
-    t <- forkIO $ traverse_ (yb thunk . timeVal . by _time) e
-    forkIO (takeMVar sem <* killThread t)
-event :: IO a -> IO (Event Seconds a)
-event = eventMay . try (pure Nothing) . map Just
-react :: IO a -> (Event Seconds a -> IO (Event Seconds (IO ()))) -> IO ()
-react a f = realize =<< join (f<$>event a)
-react2 :: IO a -> IO b -> (Event Seconds a -> Event Seconds b -> IO (Event Seconds (IO ()))) -> IO ()
-react2 a b f = realize =<< join (f<$>event a<*>event b)
-react3 :: IO a -> IO b -> IO c -> (Event Seconds a -> Event Seconds b -> Event Seconds c -> IO (Event Seconds (IO ()))) -> IO ()
-react3 a b c f = realize =<< join (f<$>event a<*>event b<*>event c)
-
--- |A Future value (a value with a timestamp)
-newtype Future t a = Future (Time t,a)
-                   deriving (Show,Functor,Unit,Applicative,Traversable,Foldable,Monad,Semigroup,Monoid)
-instance Ord t => Eq (Future t a) where f == f' = compare f f'==EQ
-instance Ord t => Ord (Future t a) where compare = cmpFut
-instance Ord t => Bounded (Future t a) where
-  minBound = (minBound,undefined)^._future
-  maxBound = (maxBound,undefined)^._future
-instance Ord t => Orderable (Future t a) where
-  inOrder (Future (t,a)) (Future (t',b)) = (Future (tx,x),Future (ty,y),z)
-    where (tx,ty,z) = inOrder t t'
-          ~(x,y) = if z then (a,b) else (b,a)
-_future :: Iso (Future t a) (Future t' b) (Time t,a) (Time t',b)
-_future = iso Future (\(Future ~(t,a)) -> (t,a))
-_time :: Lens (Time t) (Time t') (Future t a) (Future t' a)
-_time = from _future._1
-_value :: Lens a b (Future t a) (Future t b)
-_value = from _future._2
-
-cmpFut :: Ord t => Future t a -> Future t b -> Ordering
-cmpFut a b = compare (a^._time) (b^._time)
-ltFut :: Ord t => Future t a -> Future t b -> Bool
-ltFut a b = cmpFut a b == LT
-
-futureIO :: IO a -> IO (Future Seconds a)
-futureIO m = do
-  val <- newEmptyMVar
-  _ <- forkIO $ putMVar val =<< m 
-  time <- timeIO (readMVar val)
-  return (Future (time,try (return undefined) (readMVar val)^.thunk))
-
-
diff --git a/Data/TimeVal.hs b/Data/TimeVal.hs
deleted file mode 100644
--- a/Data/TimeVal.hs
+++ /dev/null
@@ -1,30 +0,0 @@
-module Data.TimeVal (
-  TimeVal(..)
-  ) where
-
-import Algebra
-
--- |A type wrapper that adds a Bounded instance for types that don't possess one.
-data TimeVal t = Always | Since t | Never
-                 deriving (Show,Eq,Ord)
-instance Functor TimeVal where
-  map f (Since a) = Since (f a)
-  map _ Always = Always
-  map _ Never = Never
-instance Unit TimeVal where pure = Since
-instance Applicative TimeVal
-instance Monad TimeVal where
-  join (Since b) = b
-  join Always = Always
-  join Never = Never
-instance Foldable TimeVal where
-  fold (Since t) = t
-  fold _ = zero
-instance Traversable TimeVal where
-  sequence (Since t) = Since<$>t
-  sequence Always = pure Always
-  sequence Never = pure Never
-
-instance Bounded (TimeVal t) where
-  minBound = Always ; maxBound = Never
-
diff --git a/Definitive.hs b/Definitive.hs
new file mode 100644
--- /dev/null
+++ b/Definitive.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE ImplicitParams #-}
+module Definitive (
+  module Definitive.Base,
+  module Data.Containers,
+  module Data.Containers.Sequence,
+  trace,trace2,mtrace,debug,
+
+  cli
+  ) where
+
+import Definitive.Base 
+import System.Environment (getArgs)
+import Data.Containers
+import Data.Containers.Sequence
+
+trace :: String -> a -> a
+trace s x = (putStrLn s^.thunk)`seq`x
+trace2 :: String -> String -> a -> a
+trace2 b a x = trace b (x`seq`trace a x)
+mtrace :: Unit f => String -> f ()
+mtrace str = trace str (pure ())
+debug :: Show a => a -> a
+debug x = trace (show x) x
+
+cli :: String -> (( ?cliargs :: [String], ?progName :: String ) => IO a) -> IO a
+cli name main = getArgs >>= \a -> let ?progName = name ; ?cliargs = a in main
diff --git a/Definitive/Base.hs b/Definitive/Base.hs
new file mode 100644
--- /dev/null
+++ b/Definitive/Base.hs
@@ -0,0 +1,12 @@
+module Definitive.Base(
+  module Algebra.Core,
+  module Algebra.Arrow,
+  module Algebra.Traversable,
+  module Algebra.Lens
+  ) where
+
+import Algebra.Arrow
+import Algebra.Core hiding (flip)
+import Algebra.Lens
+import Algebra.Traversable
+
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,69 +1,39 @@
-Bill and Ted's Public License
-=============================
-
-Everyone is permitted to copy and distribute verbatim or modified
-copies of this license document, and changing it is allowed as long as
-the name of the license is changed.
-
-PREAMBLE
+THE FREE BEER PUBLIC LICENSE
 --------
 
-The “Greater Lunduke License” is inspired, in part, by the wisdom of
-the Two Great Ones, Bill S. Preston, Esq. and Ted “Theodore” Logan.
-Namely that we should all “be excellent to each other”, that being
-“bogus” is “most non-triumphant” and that all dudes should “party on”.
+The Free Beer Public License is designed to provide free (as in beer,
+hence the name), unlimited access to any content for anyone who wishes
+it, without restrictions such as property rights or affordability.
 
-This license applies those concepts in such a way that it is
-applicable to all forms of content, including, but not limited to:
-software, books, music, movies and various works of art.
+This license embodies the philosophy that all software (and more
+generally all good ideas) is designed to solve a particular problem,
+and that the only way to judge its quality is by how well it solves
+that problem, rather than other unrelated criteria such as sellability
+or merchandability.
 
+All kinds of works may be licensed under the FBPL, as long as the
+aforementioned works are within the legal rights of the provider to
+give.
+
 TERMS AND CONDITIONS
 --------------------
 
-### 1. Be Excellent To Each Other.
-
-The consumer of this work is granted the right to utilize this work in
-conjunction with any mechanism that is capable of utilizing it, in the
-form supplied by the content creator, without limitation as to
-specific hardware or software.
-
-The consumer of this work may make copies of this work (physical or
-otherwise) for backup purposes.
-
-The consumer of this work may lend this work to another individual
-provided that the following two conditions are met :
-  
-  1. the lender no longer utilizes or possesses the work
-  2. the work is not presently lent to another individual
-
-The consumer of this work may sell this work to another individual
-provided that the following two conditions are met :
-
-  1. the seller no longer utilizes or possesses the work 
-  2. once the work is sold, the seller relinquishes all rights and
-      copies of the work to the buyer.
+### 1. Free as in Beer
 
-### 2. Don’t Be Bogus.
+The provider of this work shall make it available, free of any charge,
+monetary or otherwise, to the consumer, to use without restrictions or
+any kind of supervision.
 
-The consumer of this work shall not redistribute modified, or
-unmodified, copies of this work without explicit written permission
-from the creator of this work.  The only exceptions allowed to this
-rule are the provisions outlined in section 1 of this license
+### 2. Freely taken is freely given
 
-The consumer of this work shall not hold the creator of this work
-liable for anything the consumer does, or does not, do, or the results
-of utilizing this work.
+The consumer of this work may redistribute it as well as derived works
+in any way he or she chooses, as long as the work itself and any
+derived work remain Free as in Beer, as per the first clause.
 
-### 3. Party On, Dudes!
+### 3. The Burden of Proof
 
-The creator of this work provides the work in a form that contains no
-mechanism to disable the utilization of the work after a specific
-date, period of time or number of uses.
+The provider of this work shall also supply explanations for how the
+work was realized if requested, in the form of source code for example, or
+supply the means to access such explanations.
 
-If additional works, which are created and wholly owned by the work’s
-creator, are required to utilize this work, those additional works
-must also be made available to the consumer so long as the following
-conditions are met :
-  
-  1. doing so is possible
-  2. doing so does not cause harm to the creator of the work.
+Every such explanation shall be Free as in Beer, as per the first clause.
diff --git a/definitive-base.cabal b/definitive-base.cabal
--- a/definitive-base.cabal
+++ b/definitive-base.cabal
@@ -1,6 +1,6 @@
+-- content information
 name:          definitive-base
-version:       1.0
-
+category:      Prelude
 synopsis:      The base modules of the Definitive framework.
 description:     The Definitive framework is an attempt at harnessing the declarative
   nature of Haskell to provide a solid and simple base for writing 
@@ -21,7 +21,7 @@
   to acting on a value's representation as if it were the value itself.
   
   Packages using the Definitive framework should be compiled with the 
-  RebindableSyntax flag and include the Algebra module, which exports
+  RebindableSyntax flag and include the Definitive module, which exports
   the same interface as the Prelude, except for some extras.
   
   Here is a list of design differences between the standard Prelude
@@ -41,18 +41,21 @@
       module, which contains everything you will need to be able to use
       lenses to their full potential (except maybe a good explanation).
   
-      
+
+-- meta-information
 author:        Marc Coiffier
 maintainer:    marc.coiffier@gmail.com
+version:       1.2
 license:       OtherLicense
 license-file:  LICENSE
 
+-- build information
 build-type:    Simple
 cabal-version: >=1.10
 
 library
-  exposed-modules: Algebra Algebra.Arrow Algebra.Core Algebra.Classes Algebra.Monad Algebra.Monad.Base Algebra.Applicative Algebra.Functor Algebra.Foldable Algebra.Traversable Algebra.Lens Algebra.Monad.RWS Algebra.Monad.State Algebra.Monad.Reader Algebra.Monad.Writer Algebra.Monad.Cont Algebra.Monad.Foldable Algebra.Monad.Error Data.Containers Algebra.Time Data.TimeVal Data.Containers.Sequence Data.Probability Data.Reactive
-  build-depends: base (== 4.6.*), containers (== 0.5.*), deepseq (== 1.3.*), array (== 0.5.*), bytestring (== 0.10.*), clock (== 0.4.*), vector (== 0.10.*), primitive (== 0.5.*)
+  exposed-modules: Definitive Definitive.Base Algebra.Arrow Algebra.Core Algebra.Classes Algebra.Monad Algebra.Monad.Base Algebra.Applicative Algebra.Functor Algebra.Traversable Algebra.Foldable Algebra.Lens Algebra.Monad.RWS Algebra.Monad.State Algebra.Monad.Reader Algebra.Monad.Writer Algebra.Monad.Cont Algebra.Monad.Foldable Algebra.Monad.Error Data.Containers Data.Containers.Sequence Data.Probability Data.Containers.Monad
+  build-depends: base (== 4.6.*), containers (== 0.5.*), deepseq (== 1.3.*), array (== 0.5.*), bytestring (== 0.10.*), vector (== 0.10.*), primitive (== 0.5.*)
   default-extensions: TypeSynonymInstances NoMonomorphismRestriction StandaloneDeriving GeneralizedNewtypeDeriving TypeOperators RebindableSyntax FlexibleInstances FlexibleContexts FunctionalDependencies TupleSections MultiParamTypeClasses Rank2Types
   ghc-options: -Wall -fno-warn-orphans -threaded
   default-language: Haskell2010