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,26 @@
 -- |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,
+  zipWith,zipWith3,
+  
   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 +34,18 @@
 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 Monoid k => Unit (Assoc k) where pure = Assoc zero
+deriving instance Monoid k => Unit (Increasing k)
+instance (Monoid k,Ord k) => Applicative (Increasing k)
+instance (Monoid k,Ord k) => Monad (Increasing k) where
+  join l = Increasing (Compose (OrdList (join' $ fromAscList (map fromAscList l))))
+    where join' (Assoc k (Assoc k' a:as):ass) = Assoc (k+k') a:join' (insert (Assoc k' as) ass)
+          join' (Assoc _ []:ass) = join' ass
+          join' [] = []
+          insert x [] = [x]
+          insert x (a:as) | x<=a = x:a:as
+                          | otherwise = a:insert x as
+          fromAscList (Increasing (Compose (OrdList l'))) = l'
 
 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 +54,48 @@
 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 _ = c'_
 
-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)
+zipWith :: Applicative (Zip f) => (a -> b -> c) -> f a -> f b -> f c
+zipWith f a b = deZip (f<$>Zip a<*>Zip b)
+zipWith3 :: Applicative (Zip f) => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
+zipWith3 f a b c = deZip (f<$>Zip a<*>Zip b<*>Zip c)
+
+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 _ = c'_
+
 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 +105,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 +122,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/Arrow.hs b/Algebra/Arrow.hs
--- a/Algebra/Arrow.hs
+++ b/Algebra/Arrow.hs
@@ -39,9 +39,10 @@
   arr a = Kleisli (pure . a)
 
 newtype ListA k a b = ListA { runListA :: k [a] [b] }
+instance Deductive k => Deductive (ListA k) where
+  ListA a . ListA b = ListA (a . b)
 instance Category k => Category (ListA k) where
   id = ListA id
-  ListA a . ListA b = ListA (a . b)
 instance Arrow k => Choice (ListA k) where
   ListA f <|> ListA g = ListA (arr partitionEithers >>> (f<#>g) >>> arr (uncurry (+)))
 instance Arrow k => Split (ListA k) where
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
@@ -16,6 +17,19 @@
   infixl 1 >>=
   (>>=) :: m a -> (a -> m b) -> m b
   ma >>= k = join (map k ma)
+class Counit w where 
+  extract :: w a -> a
+class (Functor w,Counit w) => Comonad w where
+  duplicate :: w a -> w (w a)
+  duplicate = (=>> id)
+  infixl 1 =>>
+  (=>>) :: w a -> (w a -> b) -> w b
+  wa =>> k = map k (duplicate wa)
+  
+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
@@ -38,13 +52,18 @@
   tell :: w -> m ()
   listen :: m a -> m (w,a)
   censor :: m (a,w -> w) -> m a
-class (SubSemi acc w,MonadWriter w m) => MonadWriterAcc w acc m where
-  getAcc :: m acc
+class (SubSemi acc w,MonadWriter w m) => MonadCounter w acc m | m -> acc where
+  getCounter :: m acc
+class Monad m => MonadIO m where
+  liftIO :: IO a -> m a
 
 class Monad m => MonadList m where
   fork :: [a] -> m a
 class Monad m => MonadCont m where
-  callCC :: ((a -> m b) -> m a) -> m a
+  callCC :: (forall b. (a -> m b) -> m b) -> m a
 class Monad m => MonadError e m | m -> e where
   throw :: e -> m a
   catch :: (e -> m a) -> m a -> m a
+
+class MonadFix t => 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
@@ -1,16 +1,17 @@
 {-# LANGUAGE NoRebindableSyntax, MultiParamTypeClasses, DefaultSignatures, TupleSections, EmptyDataDecls #-}
 module Algebra.Core(
   -- * Raw data
-  Handle,
-  Bytes,readBytes,writeBytes,contentBytes,
-  Chunk,readChunk,writeChunk,contentChunk,
+  Handle,stdin,stdout,stderr,
+  Bytes,readBytes,writeBytes,readHBytes,writeHBytes,
+  Chunk,readChunk,writeChunk,readHChunk,writeHChunk,
+  readString,writeString,readHString,writeHString,
   
   -- * Basic union and product types
   Void,(:*:),(:+:),
   
   -- * Basic group and ring structure
   -- ** Classes
-  Semigroup(..),Monoid(..),Negative(..),Disjonctive(..),Semiring(..),Ring(..),
+  Semigroup(..),Monoid(..),Disjonctive(..),Semiring(..),Ring(..),Invertible(..),
   SubSemi(..),
   Unit(..),
 
@@ -23,31 +24,40 @@
   Dual(..),Product(..),
 
   -- *** Accumulating monoids
-  OrdList(..),Interleave(..),Accum(..),Max(..),Id(..),
+  OrdList(..),Interleave(..),Accum(..),Max(..),Min(..),Id(..),
   
   -- * Fundamental control operations
-  Category(..),(<<<),(>>>),(+++),
+  Deductive(..),Category(..),(<<<),(>>>),(+++),
 
   -- ** Splitting and Choosing
   Choice(..),Split(..),
   
-  -- * Misc functions
+  -- * Expression-level type constraints
+  Constraint,c'listOf,c'list,c'int,c'char,c'string,c'float,c'_,
+  
+  -- * 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,
 
   rmod,inside,swap,
 
   -- ** Lazily ordering values
-  Orderable(..),
-  comparing,insertOrd,invertOrd,
+  comparing,inOrder,insertOrd,invertOrd,
+  Assoc(..),assoc,
   
+  -- ** Ranges
+  Range(..),
+
+  -- ** Parallel short-circuit evaluation
+  amb,unamb,
+
   -- * The rest is imported from the Prelude
-  module Prelude
+  module Prelude,IsString(..)
   ) where
 
 import Prelude hiding (
@@ -58,18 +68,43 @@
   sequence,mapM,mapM_,sequence_,(=<<),
 
   map,(++),foldl,foldr,foldr1,concat,filter,length,sum,lookup,
-  (+),(*),(.),id,const,(-),
+  (+),(*),(.),id,const,(-),(/),recip,
 
-  or,any,and,all,elem,
+  or,any,and,all,elem,span,break,splitAt,take,drop,takeWhile,dropWhile,
 
-  until,negate)
+  until,negate,zipWith,zipWith3,
+
+  minimum,maximum,product)
+import Control.Concurrent (killThread,newEmptyMVar,forkIO,putMVar,takeMVar)
+import Control.Exception (evaluate)
+import System.IO.Unsafe (unsafePerformIO)
+import System.IO (stdin,stdout,stderr)
 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,hPutStr)
 import Data.Ord (comparing)
+import GHC.Exts (IsString(..))
 
+type Constraint a = a -> a
+c'listOf :: Constraint a -> Constraint [a]
+c'listOf _ = c'_
+c'list :: Constraint [a]
+c'list = c'listOf c'_
+c'int :: Constraint Int
+c'int = c'_
+c'char :: Constraint Char
+c'char = c'_
+c'string :: Constraint String
+c'string = c'_
+c'float :: Constraint Float
+c'float = c'_
+c'couple :: Constraint a -> Constraint b -> Constraint (a,b)
+c'couple _ _ = c'_
+c'_ :: Constraint a
+c'_ = id
+
 type Chunk = BSS.ByteString
 type Bytes = BSL.ByteString
 
@@ -77,14 +112,26 @@
 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
-contentBytes :: Handle -> IO Bytes
-contentBytes = BSL.hGetContents
-contentChunk :: Handle -> IO Chunk
-contentChunk = BSS.hGetContents
+writeString :: String -> String -> IO ()
+writeString = P.writeFile
+readHBytes :: Handle -> IO Bytes
+readHBytes = BSL.hGetContents
+readHChunk :: Handle -> IO Chunk
+readHChunk = BSS.hGetContents
+readHString :: Handle -> IO String
+readHString = hGetContents
+writeHBytes :: Handle -> Bytes -> IO ()
+writeHBytes = BSL.hPut
+writeHChunk :: Handle -> Chunk -> IO ()
+writeHChunk = BSS.hPut
+writeHString :: Handle -> String -> IO ()
+writeHString = hPutStr
 
 data Void
 type a:*:b = (a,b)
@@ -98,17 +145,21 @@
   (+) :: m -> m -> m
   default (+) :: Num m => m -> m -> m
   (+) = (P.+)
-infixl 6 +
+infixr 6 +
 instance Semigroup Void where _+_ = undefined
 instance Semigroup () where _+_ = ()
 instance Semigroup Bool where (+) = (||)
 instance Semigroup Int
+instance Semigroup Integer
+instance Semigroup Rational
 instance Semigroup Float
 instance Semigroup Double
-instance Semigroup Integer
 instance Semigroup Bytes where (+) = BSL.append
 instance Semigroup Chunk where (+) = BSS.append
-instance Semigroup [a] where []+l = l ; (x:t)+l = x:(t+l)
+instance Semigroup [a] where
+  {-# INLINE[2] (+) #-}
+  (+) (x:t) = \l -> x:(t+l)
+  (+) [] = \l -> l
 instance (Semigroup a,Semigroup b) => Semigroup (a:*:b) where ~(a,b) + ~(c,d) = (a+c,b+d)
 instance (Semigroup a,Semigroup b,Semigroup c) => Semigroup (a,b,c) where
   ~(a,b,c) + ~(a',b',c') = (a+a',b+b',c+c')
@@ -127,6 +178,7 @@
 instance Monoid Void where zero = undefined
 instance Monoid () where zero = ()
 instance Monoid Int ; instance Monoid Integer
+instance Monoid Rational
 instance Monoid Float ; instance Monoid Double
 instance Monoid Bytes where zero = BSL.empty
 instance Monoid Chunk where zero = BSS.empty
@@ -142,24 +194,31 @@
   cast :: b -> a
 instance Monoid a => SubSemi a () where cast _ = zero
 instance Monoid a => SubSemi a Void where cast _ = zero
-
-class Monoid m => Negative m where
-  negate :: m -> m
-  default negate :: Num m => m -> m
-  negate = P.negate
-instance Negative Int ; instance Negative Integer
-instance Negative Float ; instance Negative Double
-instance Negative Bool where negate = not
+instance Semigroup a => SubSemi a a where cast = id
 
 class Monoid m => Disjonctive m where
+  negate :: m -> m
+  negate = (zero -)
   (-) :: m -> m -> m
-  default (-) :: Num m => m -> m -> m
-  (-) = (P.-)
-instance Disjonctive Int ; instance Disjonctive Integer
-instance Disjonctive Float ; instance Disjonctive Double
-instance Disjonctive Bool where a - b = not (a==b)
-instance (Disjonctive a,Disjonctive b) => Disjonctive (a:*:b) where (a,b)-(c,d) = (a-c,b-d)
+  a-b = a+negate b
+instance Disjonctive Int where
+  negate = P.negate ; (-) = (P.-)
+instance Disjonctive Integer where
+  negate = P.negate ; (-) = (P.-)
+instance Disjonctive Rational where
+  negate = P.negate ; (-) = (P.-)
+instance Disjonctive Float where
+  negate = P.negate ; (-) = (P.-)
+instance Disjonctive Double where
+  negate = P.negate ; (-) = (P.-)
 
+instance Disjonctive Bool where
+  negate = not
+  a - b = not (a==b)
+instance (Disjonctive a,Disjonctive b) => Disjonctive (a:*:b) where
+  negate (a,b) = (negate a,negate b)
+  (a,b)-(c,d) = (a-c,b-d)
+
 class Monoid m => Semiring m where
   (*) :: m -> m -> m
   default (*) :: Num m => m -> m -> m
@@ -173,6 +232,7 @@
 instance Semiring Bool where (*) = (&&)
 instance Ring Bool where one = True 
 instance Semiring Int ; instance Ring Int
+instance Semiring Rational ; instance Ring Rational
 instance Semiring Integer ; instance Ring Integer
 instance Semiring Float ; instance Ring Float
 instance Semiring Double ; instance Ring Double
@@ -187,6 +247,18 @@
 instance (Ring a,Ring b) => Ring (a:*:b) where
   one = (one,one)
 
+class (Ring m,Disjonctive m) => Invertible m where
+  recip :: m -> m
+  recip = (one /)
+  (/) :: m -> m -> m
+  a / b = a * recip b
+instance Invertible Rational where
+  recip = P.recip ; (/) = (P./)
+instance Invertible Float where
+  recip = P.recip ; (/) = (P./)
+instance Invertible Double where
+  recip = P.recip ; (/) = (P./)
+
 class Unit f where
   pure :: a -> f a
 instance Unit (Either a) where pure = Right
@@ -197,12 +269,15 @@
 instance Unit Tree where pure a = Node a []
 instance Unit IO where pure = P.return
 
-class Category k where
-  id :: k a a
+class Deductive k where
   (.) :: k b c -> k a b -> k a c
+class Deductive k => Category k where
+  id :: k a a
+
+instance Deductive (->) where
+    (.) = (P..)
 instance Category (->) where
   id = P.id
-  (.) = (P..)
 (<<<) :: Category k => k b c -> k a b -> k a c
 (<<<) = (.)
 (>>>) :: Category k => k a b -> k b c -> k a c
@@ -251,17 +326,32 @@
 
 -- |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
+instance Semigroup (Id a) where a + _ = a                                
 
 {-| The Max monoid, where @(+) =~ max@ -}
 newtype Max a = Max { getMax :: a }
               deriving (Eq,Ord,Bounded,Show)
-instance Ord a => Semigroup (Max a) where Max a+Max b = Max (max a b)
-instance (Ord a,Bounded a) => Monoid (Max a) where zero = Max minBound
-instance (Ord a,Bounded a) => Semiring (Max a) where Max a * Max b = Max (min a b)
-instance (Ord a,Bounded a) => Ring (Max a) where one = Max maxBound
+instance Ord a => Semigroup (Max a) where a + b = max a b
+instance (Ord a,Bounded a) => Monoid (Max a) where zero = minBound
+instance (Ord a,Bounded a) => Semiring (Max a) where a * b = min a b
+instance (Ord a,Bounded a) => Ring (Max a) where one = maxBound
 
+{-| The Min monoid, where @(+) =~ min@ -}
+newtype Min a = Min { getMin :: a }
+              deriving (Eq,Show)
+instance Ord a => Ord (Min a) where
+  compare (Min a) (Min b) = compare b a
+instance Bounded a => Bounded (Min a) where
+  minBound = Min maxBound
+  maxBound = Min minBound
+instance Ord a => Semigroup (Min a) where a + b = max a b
+instance (Ord a,Bounded a) => Monoid (Min a) where zero = minBound
+instance (Ord a,Bounded a) => Semiring (Min a) where a * b = min a b
+instance (Ord a,Bounded a) => Ring (Min a) where one = maxBound
+
 {-| The dual of a monoid is the same as the original, with arguments reversed -}
 newtype Dual m = Dual { getDual :: m }
 instance Semigroup m => Semigroup (Dual m) where Dual a+Dual b = Dual (b+a)
@@ -273,28 +363,66 @@
 -- the result remains in ascending order.
 newtype OrdList a = OrdList { getOrdList :: [a] }
                   deriving (Eq,Ord,Show)
-instance Orderable a => Semigroup (OrdList a) where
+instance Ord a => Semigroup (OrdList a) where
   OrdList oa + OrdList ob = OrdList (oa ++ ob)
     where (x:xt) ++ (y:yt) = a : c : cs
             where (a,_,z) = inOrder x y
                   ~(c:cs) = if z then xt ++ (y:yt) else (x:xt) ++ yt
           a ++ b = a + b
-deriving instance Orderable a => Monoid (OrdList a)
+deriving instance Ord a => Monoid (OrdList a)
 deriving instance Unit OrdList
 
-class Ord t => Orderable t where
-  inOrder :: t -> t -> (t,t,Bool)
-instance Ord t => Orderable (Max t) where
-  inOrder (Max a) (Max b) = (Max x,Max y,z)
+data Assoc k a = Assoc k a
+               deriving Show
+instance Ord k => Eq (Assoc k a) where
+  a == b = compare a b == EQ
+instance Ord k => Ord (Assoc k a) where
+  compare (Assoc k _) (Assoc k' _) = compare k k'
+assoc :: a -> Assoc a a
+assoc a = Assoc a a
+
+inOrder :: Ord t => t -> t -> (t,t,Bool)
+inOrder a b = (x,y,z)
     where ~(x,y) | z = (a,b)
                  | otherwise = (b,a)
           z = a<=b
-insertOrd :: Orderable t => t -> [t] -> [t]
+
+insertOrd :: Ord t => t -> [t] -> [t]
 insertOrd e [] = [e]
 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
   Interleave ia + Interleave ib = Interleave (inter ia ib)
@@ -347,12 +475,11 @@
 invertOrd GT = LT ; invertOrd LT = GT ; invertOrd EQ = EQ
 
 inside :: Ord t => t -> t -> (t -> Bool)
-inside x y = \z -> x<z && z<y
+inside x y = \z -> x<=z && z<=y
 
-rmod :: (RealFrac m,Ring m) => m -> m -> m
+rmod :: (RealFloat m,Invertible m) => m -> m -> m
 a`rmod`b = b * r 
-  where _n :: Int
-        (_n,r) = properFraction (a/b)
+  where (_n,r) = c'couple c'int c'_ $ properFraction (a/b)
 infixl 7 `rmod`
 
 swap :: (a,b) -> (b,a)
@@ -363,3 +490,16 @@
 
 ($^) :: (a -> b -> c) -> b -> a -> c
 ($^) = flip
+
+amb :: IO a -> IO a -> IO a
+ma `amb` mb = do
+  res <- newEmptyMVar
+  ta <- forkIO $ ma P.>>= putMVar res . Left
+  tb <- forkIO $ mb P.>>= putMVar res . Right
+
+  takeMVar res P.>>= \c -> case c of
+    Left a -> P.fmap (const a) (killThread tb)
+    Right a -> P.fmap (const a) (killThread ta)
+unamb :: a -> a -> a
+unamb a b = unsafePerformIO (evaluate a `amb` evaluate b)
+
diff --git a/Algebra/Foldable.hs b/Algebra/Foldable.hs
--- a/Algebra/Foldable.hs
+++ b/Algebra/Foldable.hs
@@ -1,29 +1,34 @@
 {-# 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 Strict where fold = lazy
 instance Foldable (Either a) where
   fold = pure zero <|> id
 instance Foldable Maybe where
   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
+deriving instance Foldable (Increasing k)
+instance Foldable (Assoc k) where fold (Assoc _ a) = a
 instance (Foldable f,Foldable g) => Foldable (f:.:g) where
   fold = getCompose >>> map fold >>> fold
 
-instance (Foldable f,Semigroup (f a),Monoid n,Num n) => SubSemi n (f a) where
+instance (Foldable f,Semigroup (f a),Ring n) => SubSemi n (f a) where
   cast = size
 
 instance (Foldable f,Foldable g) => Foldable (f:**:g) where
@@ -32,6 +37,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
@@ -40,11 +53,32 @@
 concat = fold
 sum :: (Monoid m, Foldable t) => t m -> m
 sum = fold
-size :: (Foldable f,Num n,Monoid n) => f a -> n
-size c = foldl' (+) 0 (1<$c)
+product :: (Ring m,Foldable t) => t m -> m
+product = getProduct . foldMap Product
+nzsum :: Semigroup m => [m] -> m
+nzsum = foldr1 (+)
+size :: (Foldable f,Ring n) => f a -> n
+size c = foldl' (+) zero (one<$c)
 length :: [a] -> Int
 length = size
+maximum :: (Bounded a,Ord a,Foldable t) => t a -> a
+maximum = getMax . foldMap Max
+maximumBy :: (Ord a,Foldable t) => (b -> a) -> b -> t b -> b
+maximumBy f x = foldl' g x
+  where g a b = if f a > f b then a else b
+minimum :: (Bounded a,Ord a,Foldable t) => t a -> a
+minimum = getMax . getProduct . foldMap (Product . Max)
+minimumBy :: (Ord a,Foldable t) => (b -> a) -> b -> t b -> b
+minimumBy f x = foldl' g x
+  where g a b = if f a < f b then a else b
 
+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 +95,10 @@
 
 compose :: (Category k, Foldable t) => t (k a a) -> k a a
 compose = runEndo . foldMap Endo
+composing :: (Category k,Foldable t) => (a -> k b b) -> t a -> k b b
+composing f = compose . map f
+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
@@ -91,3 +129,9 @@
 empty = foldr (const (const False)) True
 nonempty :: Foldable f => f a -> Bool
 nonempty = not . empty
+
+-- | Lazily counts the number of elements in a structure up to a certain size
+sizeTo :: Foldable f => Int -> f a -> Int
+sizeTo n f = foldr g (min n) f 0
+  where g _ k = \s -> if s>=n then n else k (s+1)
+          
diff --git a/Algebra/Functor.hs b/Algebra/Functor.hs
--- a/Algebra/Functor.hs
+++ b/Algebra/Functor.hs
@@ -1,10 +1,12 @@
 {-# 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(..),(:.:)(..),(:**:)(..),(:++:)(..),
+  Increasing(..),
+  
+  emerge,flip,project,factor,
   (<$>),(|||),(<$),(<&>),void,left,right,
   promap,map2,map3
   ) where
@@ -12,7 +14,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 +25,19 @@
   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 Strict where collect f = Strict (map lazy 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)
+factor :: (Contravariant c,Unit c,Bifunctor f,Functor (f a)) => f (c a) (c b) -> c (f a b)
+factor = collect . dimap pure id
+
 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
@@ -41,6 +56,12 @@
 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
+instance Monad Strict where join = lazy
+
 -- |The Constant Functor
 newtype Const a b = Const { getConst :: a }
 instance Semigroup a => Semigroup (Const a b) where Const a+Const b = Const (a+b)
@@ -50,6 +71,15 @@
 instance Monoid a => Applicative (Const a) where
   Const a <*> Const b = Const (a+b)
 
+-- |A functor for ordered lists
+newtype Increasing k a = Increasing ((OrdList:.:Assoc k) a)
+                      deriving Functor
+instance Functor (Assoc k) where map f (Assoc k a) = Assoc k (f a)
+instance Ord k => Semigroup (Increasing k a) where
+  Increasing (Compose l) + Increasing (Compose l') = Increasing (Compose (l+l'))
+instance Ord k => Monoid (Increasing k a) where
+  zero = Increasing (Compose zero)
+
 -- |A motherflippin' functor
 newtype Flip f a b = Flip { unFlip :: f b a }
                   deriving (Semigroup,Monoid)
@@ -59,6 +89,11 @@
 instance (Unit f,Unit g) => Unit (f:.:g) where pure = Compose . pure . pure
 instance (Functor f,Functor g) => Functor (f:.:g) where
   map f (Compose c) = Compose (map2 f c)
+instance (Contravariant f,Contravariant g) => Contravariant (f:.:g) where
+  collect = Compose . map collect . collect . map getCompose
+
+emerge :: (Functor f,Unit g) => (f:.:g) a -> (f:.:g) (g a)
+emerge (Compose fga) = Compose (map pure fga)
 
 data (f:**:g) a = f a:**:g a
 instance (Functor f,Functor g) => Functor (f:**:g) where
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_,
 
@@ -30,30 +30,30 @@
   (-.),(.-),
   
   -- * Basic lenses
-  Lens1(..),Lens2(..),Lens3(..),Lens4(..),
+  Lens1(..),Lens2(..),Lens3(..),Lens4(..),Lens5(..),
   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,
+  warp2,mapping,mapping',promapping,applying,
 
   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,67 +164,82 @@
 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 Lens5 s t a b | a -> s, a t -> b where
+  l'5 :: 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 Lens1 a b (a,c,d,e,f) (b,c,d,e,f) where
+  l'1 = lens (\ ~(a,_,_,_,_) -> a) (\ (_,c,d,e,f) b -> (b,c,d,e,f))
 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 Lens2 a b (c,a,d,e,f) (c,b,d,e,f) where
+  l'2 = lens (\ ~(_,a,_,_,_) -> a ) (\ ~(c,_,d,e,f) b -> (c,b,d,e,f))
 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 Lens3 a b (c,d,a,e,f) (c,d,b,e,f) where
+  l'3 = lens (\ ~(_,_,a,_,_) -> a ) (\ ~(c,d,_,e,f) b -> (c,d,b,e,f))
 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 Lens4 a b (c,d,e,a,f) (c,d,e,b,f) where
+  l'4 = lens (\ ~(_,_,_,a,_) -> a ) (\ ~(c,d,e,_,f) b -> (c,d,e,b,f))
+instance Lens5 a b (c,d,e,f,a) (c,d,e,f,b) where
+  l'5 = lens (\ ~(_,_,_,_,a) -> a ) (\ ~(c,d,e,f,_) b -> (c,d,e,f,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
+  each :: Traversal a b s t
 instance Compound a b (a,a) (b,b) where
-  _each k (a,a') = (,)<$>k a<*>k a'
+  each k (a,a') = (,)<$>k a<*>k a'
 instance Compound a b (a,a,a) (b,b,b) where
-  _each k (a,a',a'') = (,,)<$>k a<*>k a'<*>k a''
+  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
+  each k = map Left . k <|> map Right . k
+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)
@@ -233,52 +248,60 @@
 promapping :: Bifunctor f => Iso s t a b -> Iso (f t x) (f s y) (f b x) (f a y)
 promapping (isoT -> IsoT u v) = dimap v id`dimap` map (dimap u id)
 -- ^promapping :: Bifunctor f => Iso' a b -> Iso' (f a c) (f b c)
+applying :: Applicative f => Lens s t a b -> Lens (f s) (f t) (f a) (f b)
+applying l = lens _to _from
+  where _to = map (by l) ; _from = flip $ liftA2 (set l) 
 
 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 +315,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)
 
@@ -307,7 +333,7 @@
 chunk :: Bytes:<->:Chunk
 chunk = iso toStrict fromStrict
 
-negated :: (Negative a,Negative b) => Iso a b a b
+negated :: (Disjonctive a,Disjonctive b) => Iso a b a b
 negated = iso negate negate
 commuted :: Commutative f => Iso (f a b) (f c d) (f b a) (f d c)
 commuted = iso commute commute
@@ -317,5 +343,3 @@
                         ,Applicative)
 has :: Fold' a b -> a -> Bool
 has l x = x^?l & \(Test (Const (Product b))) -> b
-
-
diff --git a/Algebra/Monad.hs b/Algebra/Monad.hs
--- a/Algebra/Monad.hs
+++ b/Algebra/Monad.hs
@@ -8,7 +8,9 @@
   module Algebra.Monad.Writer,
   module Algebra.Monad.Cont,
   module Algebra.Monad.Foldable,
-  module Algebra.Monad.Error
+  module Algebra.Monad.Error,
+  module Algebra.Monad.Free,
+  module Algebra.Monad.Logic
   ) where
 
 import Algebra.Monad.Base
@@ -20,4 +22,5 @@
 import Algebra.Monad.Cont
 import Algebra.Monad.Foldable
 import Algebra.Monad.Error
-
+import Algebra.Monad.Free
+import Algebra.Monad.Logic
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,20 @@
+{-# LANGUAGE UndecidableInstances, ScopedTypeVariables #-}
 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,(>>>=),(>>>>=),
+  mfix_,mfixing,
   
+  -- * Monadic Lenses
+  Action,Action',
+  
   -- * Instance utilities
-  Compose'(..),_Compose'
+  Compose'(..),i'Compose',coerceJoin,coerceDuplicate
   ) where
 
 import Algebra.Classes
@@ -18,13 +23,24 @@
 import Algebra.Traversable
 import Algebra.Lens
 import qualified Control.Monad.Fix as Fix
+import Unsafe.Coerce
 
+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 Strict where mfix = cfix
 instance MonadFix ((->) b) where mfix = cfix
 instance MonadFix [] where mfix f = fix (f . head)
 instance MonadFix (Either e) where mfix f = fix (f . either undefined id)
 instance MonadFix IO where mfix = Fix.mfix
+mfix_ :: MonadFix m => (a -> m a) -> m ()
+mfix_ = void . mfix
 
 instance (Traversable g,Monad f,Monad g) => Monad (f:.:g) where
   join = Compose .map join.join.map sequence.getCompose.map getCompose
@@ -33,27 +49,45 @@
 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 (Traversable g,Monad g,MonadState s f) => MonadState s (f:.:g) where
+  get = Compose (pure<$>get)
+  put x = Compose (pure<$>put x)
+  modify f = Compose (pure<$>modify f)
+instance (Traversable g,Monad g,MonadWriter w f) => MonadWriter w (f:.:g) where
+  tell w = Compose (pure<$>tell w)
+  listen (Compose fga) = Compose (listen fga <&> (\ (w,ga) -> (w, )<$>ga))
+  censor (Compose fgc) = Compose (censor $ map (swap . first runEndo . sequence . map (first Endo . swap)) fgc)
+instance (Traversable g,Monad g,MonadReader r f) => MonadReader r (f:.:g) where
+  ask = Compose (pure<$>ask)
+  local f (Compose fga) = Compose (local f fga)
 
 instance MonadFix m => Monad (Backwards m) where
   join (Backwards ma) = Backwards$mfixing (\a -> liftA2 (,) (forwards a) ma)
+instance MonadFix m => 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 => Deductive (Kleisli m) where
+  Kleisli f . Kleisli g = Kleisli (\a -> g a >>= f)
 instance Monad m => Category (Kleisli m) where
   id = Kleisli pure
-  Kleisli f . Kleisli g = Kleisli (\a -> g a >>= f)
 instance Monad m => Choice (Kleisli m) where
   Kleisli f <|> Kleisli g = Kleisli (f <|> g)
 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 +95,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
@@ -108,14 +142,24 @@
 joinMap :: Monad m => (a -> m b) -> m a -> m b
 joinMap = (=<<)
 
+coerceJoin :: forall m m' a. Monad m => (forall b. m b -> m' b) -> (m' (m' a) -> m' a)
+coerceJoin _ = unsafeCoerce (join :: m (m a) -> m a)
+coerceDuplicate :: forall m m' a. Comonad m => (forall b. m b -> m' b) -> (m' a -> m' (m' a))
+coerceDuplicate _ = unsafeCoerce (duplicate :: m a -> m (m a))
+
 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)
+                       deriving (Semigroup,Monoid,Unit,Functor,Applicative,MonadFix,Foldable)
+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
+instance (Monad f,Monad g,Traversable f) => Monad (Compose' f g) where join = coerceJoin Compose'
+instance (Traversable g,Traversable f) => Traversable (Compose' f g) where sequence = coerceSeq Compose'
+deriving instance (Traversable f,Monad f,MonadState s g) => MonadState s (Compose' f g)
+deriving instance (Traversable f,Monad f,MonadReader r g) => MonadReader r (Compose' f g)
+deriving instance (Traversable f,Monad f,MonadWriter w g) => MonadWriter w (Compose' f g)
 
 
 
diff --git a/Algebra/Monad/Cont.hs b/Algebra/Monad/Cont.hs
--- a/Algebra/Monad/Cont.hs
+++ b/Algebra/Monad/Cont.hs
@@ -4,29 +4,32 @@
   
   -- * The Continuation transformer
   ContT(..),Cont,
-  contT, cont
+  contT, cont, (>>~)
   ) where
 
 import Algebra.Monad.Base
 
 {-| A simple continuation monad implementation  -}
-newtype ContT r m a = ContT { runContT :: (a -> m r) -> m r }
-                      deriving (Semigroup,Monoid,Semiring,Ring)
-type Cont r a = ContT r Id a
-instance Unit m => Unit (ContT r m) where pure a = ContT ($a)
-instance Functor f => Functor (ContT r f) where
+newtype ContT m a = ContT { runContT :: forall r. (a -> m r) -> m r }
+
+type Cont a = ContT Id a
+instance Unit (ContT m) where pure a = ContT ($a)
+instance Functor (ContT f) where
   map f (ContT c) = ContT (\kb -> c (kb . f))
-instance Applicative m => Applicative (ContT r m) where
-  ContT cf <*> ContT ca = ContT (\kb -> cf (\f -> ca (\a -> kb (f a))))
-instance Monad m => Monad (ContT r m) where
-  ContT k >>= f = ContT (\cc -> k (\a -> runContT (f a) cc))
-instance MonadTrans (ContT r) where
+instance Applicative (ContT m)
+instance Monad (ContT m) where
+  join (ContT kk) = ContT (\ka -> kk (\(ContT k) -> k ka))
+instance MonadTrans ContT where
   lift m = ContT (m >>=)
-instance Monad m => MonadCont (ContT r m) where
-  callCC f = ContT (\k -> runContT (f (\a -> ContT (\_ -> k a))) k)
+instance MonadCont (ContT m) where
+  callCC f = ContT (runContT (f pure))
+instance MonadFix m => MonadFix (ContT m) where
+  mfix f = ContT (\ka -> mfixing (\a -> runContT (f a) ka<&>(,a)))
 
-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
+(>>~) :: ContT m a -> (a -> m b) -> m b
+(>>~) = runContT
 
+contT :: (Monad m,Unit m') => Iso (ContT m a) (ContT m' a') (m a) (m' a')
+contT = iso lift (>>~ pure)
+cont :: Iso (Cont a) (Cont a') a a'
+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
@@ -1,10 +1,10 @@
 module Algebra.Monad.Error (
   -- * The MonadError class
-  MonadError(..),try,(!+),tryMay,throwIO,
+  MonadError(..),try,(!+),optional,throwIO,
 
   -- * The Either transformer
   EitherT,
-  _eitherT
+  eitherT
   ) where
 
 import Algebra.Monad.Base
@@ -12,8 +12,8 @@
 
 try :: MonadError e m => m a -> m a -> m a
 try = catch . const
-tryMay :: MonadError e m => m a -> m (Maybe a)
-tryMay m = catch (\_ -> return Nothing) (Just<$>m)
+optional :: MonadError e m => m a -> m (Maybe a)
+optional m = catch (\_ -> return Nothing) (Just<$>m)
 
 (!+) :: MonadError Void m => m a -> m a -> m a
 (!+) = flip try
@@ -27,10 +27,11 @@
   catch f [] = f zero
   catch _ l = l
 newtype EitherT e m a = EitherT (Compose' (Either e) m a)
-                      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)
+                      deriving (Unit,Functor,Applicative,MonadFix,Foldable,MonadTrans)
+instance Monad m => Monad (EitherT e m) where join = coerceJoin EitherT
+instance Traversable m => Traversable (EitherT e m) where sequence = coerceSeq EitherT
+eitherT :: (Functor m) => Iso (EitherT e m a) (EitherT f m b) (m (e:+:a)) (m (f:+:b))                              
+eitherT = i'Compose'.iso EitherT (\(EitherT e) -> e)
 
 instance MonadError Void Maybe where
   throw = const Nothing
@@ -39,6 +40,7 @@
 instance MonadError Ex.SomeException IO where
   throw = Ex.throw
   catch = flip Ex.catch
-throwIO :: Ex.Exception e => e -> IO ()
+
+throwIO :: (MonadError Ex.SomeException m,Ex.Exception e) => e -> m ()
 throwIO = throw . Ex.toException
 
diff --git a/Algebra/Monad/Foldable.hs b/Algebra/Monad/Foldable.hs
--- a/Algebra/Monad/Foldable.hs
+++ b/Algebra/Monad/Foldable.hs
@@ -9,7 +9,9 @@
   -- ** The Tree transformer
   TreeT(..),treeT,
   -- ** The Maybe transformer
-  MaybeT(..),maybeT
+  MaybeT(..),maybeT,
+  -- ** The Strict Monad transformer
+  StrictT(..),strictT
   ) where
 
 import Algebra.Monad.Base
@@ -20,10 +22,11 @@
 
 newtype ListT m a = ListT (Compose' [] m a)
                     deriving (Semigroup,Monoid,
-                              Functor,Applicative,Unit,Monad,
-                              Foldable,Traversable,MonadTrans)
+                              Functor,Applicative,Unit,Foldable,MonadTrans)
+instance Monad m => Monad (ListT m) where join = coerceJoin ListT
+instance Traversable m => Traversable (ListT m) where sequence = coerceSeq ListT
 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 +39,28 @@
   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)
+                  deriving (Functor,Unit,Applicative,MonadFix,Foldable,MonadTrans)
+instance Monad m => Monad (TreeT m) where join = coerceJoin TreeT
+instance Traversable m => Traversable (TreeT m) where sequence = coerceSeq TreeT
 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)
+                  deriving (Functor,Unit,Applicative,MonadFix,Foldable,MonadTrans)
+instance Monad m => Monad (MaybeT m) where join = coerceJoin MaybeT
+instance Traversable m => Traversable (MaybeT m) where sequence = coerceSeq MaybeT
 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)
 
+newtype StrictT m a = StrictT (Compose' Strict m a)
+                    deriving (Functor,Unit,Applicative,MonadFix,Foldable,MonadTrans)
+instance Monad m => Monad (StrictT m) where join = coerceJoin StrictT
+instance Traversable m => Traversable (StrictT m) where sequence = coerceSeq StrictT
+strictT :: Iso (StrictT m a) (StrictT m' b) (m (Strict a)) (m' (Strict b))
+strictT = i'Compose'.iso StrictT (\(StrictT s) -> s)
diff --git a/Algebra/Monad/Free.hs b/Algebra/Monad/Free.hs
new file mode 100644
--- /dev/null
+++ b/Algebra/Monad/Free.hs
@@ -0,0 +1,129 @@
+{-# LANGUAGE UndecidableInstances, ScopedTypeVariables #-}
+module Algebra.Monad.Free where
+
+import Algebra.Monad.Base
+import Unsafe.Coerce (unsafeCoerce)
+
+data Free f a = Join (f (Free f a))
+              | Pure a
+deriving instance (Show (f (Free f a)),Show a) => Show (Free f a)
+
+instance Functor f => Functor (Free f) where
+  map f (Join fa) = Join (map2 f fa)
+  map f (Pure a) = Pure (f a)
+instance Unit (Free f) where pure = Pure
+instance Functor f => Applicative (Free f)
+instance Functor f => Monad (Free f) where
+  join (Join f) = Join (map join f)
+  join (Pure f) = f
+instance Counit f => Counit (Free f) where
+  extract (Join f) = extract (extract f)
+  extract (Pure a) = a
+instance Comonad f => Comonad (Free f) where
+  duplicate (Pure a) = Pure (Pure a)
+  duplicate (Join f) = Join (f =>> liftF)
+
+instance (Ord (f (Free f a)),Ord a,Unit f) => Eq (Free f a) where
+  a == b = compare a b == EQ
+instance (Ord (f (Free f a)),Ord a,Unit f) => Ord (Free f a) where
+  compare (Join fa) (Join fb) = compare fa fb
+  compare (Pure a) (Pure b) = compare a b
+  compare (Pure a) x = compare (Join (pure (Pure a))) x
+  compare x (Pure a) = compare x (Join (pure (Pure a)))
+
+instance MonadFix f => MonadFix (Free f) where
+  mfix f = Join (Pure<$>mfix (\a -> perform (f a)))
+
+instance Foldable f => Foldable (Free f) where
+  fold (Join f) = foldMap fold f
+  fold (Pure a) = a
+instance Traversable f => Traversable (Free f) where
+  sequence (Join f) = Join<$>(traverse sequence f)
+  sequence (Pure a) = Pure<$>a
+
+instance MonadTrans Free where lift = liftF
+instance ConcreteMonad Free where
+  generalize (Join f) = Join ((pure . generalize . getId) f)
+  generalize (Pure a) = Pure a
+instance MonadState s m => MonadState s (Free m) where
+  get = lift get
+  put a = lift (put a)
+  modify f = lift (modify f)
+instance MonadReader r m => MonadReader r (Free m) where
+  ask = lift ask
+  local f (Join m) = Join (local f m)
+  local _ (Pure a) = Pure a
+instance MonadWriter w m => MonadWriter w (Free m) where
+  tell w = lift (tell w)
+  listen m = lift (listen (perform m))
+  censor m = lift (censor (perform m))
+instance MonadCounter w a m => MonadCounter w a (Free m) where
+  getCounter = lift getCounter
+instance MonadIO m => MonadIO (Free m) where
+  liftIO = lift . liftIO
+instance MonadList m => MonadList (Free m) where
+  fork l = lift (fork l)
+instance MonadFuture m t => MonadFuture m (Free t) where
+  future = lift . future
+
+instance MonadError e m => MonadError e (Free m) where
+  throw e = lift (throw e)
+  catch k m = lift (catch (map perform k) (perform m))
+
+concrete :: Monad m => Free m a -> m (Free Id a)
+concrete = map Pure . perform 
+unliftF :: Monad m => Free m a -> Free m (m a)
+unliftF = Pure . perform
+
+mapF :: (Functor f,Functor g) => (forall a. f a -> g a) -> Free f b -> Free g b
+mapF f (Join a) = Join (f (map (mapF f) a))
+mapF _ (Pure a) = Pure a
+
+class MonadFree m f | f -> m where
+  step :: Monad m => f a -> m (f a)
+  perform :: Monad m => f a -> m a
+  liftF :: Functor m => m a -> f a
+
+instance MonadFree m (Free m) where
+  step (Join j) = j
+  step (Pure a) = pure (Pure a)
+  perform (Join fa) = fa >>= perform
+  perform (Pure a) = pure a
+  liftF = Join . map Pure
+coerceStep :: forall m f g a. (Monad m,MonadFree m f) => (f a -> g a) -> (g a -> m (g a))
+coerceStep _ = unsafeCoerce (step :: f a -> m (f a))
+coercePerform :: forall m f g a. (Monad m,MonadFree m f) => (f a -> g a) -> (g a -> m a)
+coercePerform _ = unsafeCoerce (perform :: f a -> m a)
+coerceLiftF :: forall m f g a. (Functor m,MonadFree m f) => (f a -> g a) -> (m a -> g a)
+coerceLiftF _ = unsafeCoerce (liftF :: m a -> f a)
+
+data Cofree w a = Step a (w (Cofree w a))
+
+type Infinite a = Cofree Id a
+type Colist a = Cofree Maybe a
+
+instance Functor w => Functor (Cofree w) where
+  map f (Step a wca) = Step (f a) (map2 f wca)
+instance Counit (Cofree w) where
+  extract (Step a _) = a
+instance Functor w => Comonad (Cofree w) where
+  duplicate d@(Step _ wca) = Step d (map duplicate wca)
+instance Foldable w => Foldable (Cofree w) where
+  fold (Step a wca) = a + foldMap fold wca
+instance Traversable w => Traversable (Cofree w) where
+  sequence (Step fa wcfa) = Step<$>fa<*>traverse sequence wcfa
+instance Unit m => Unit (Cofree m) where
+  pure a = Step a (pure (pure a))
+instance Applicative m => Applicative (Cofree m) where
+instance Applicative m => Monad (Cofree m) where
+  join (Step (Step a _) ww) = Step a (map join ww)
+
+type Bifree f a = Cofree (Free f) a
+newtype ContC k a b = ContC { runContC :: forall c. k b c -> k a c }
+contC :: (Category k,Category k') => Iso (ContC k a b) (ContC k' a' b') (k a b) (k' a' b')
+contC = iso (\x -> ContC (x >>>)) (($id) . runContC)
+
+instance Deductive (ContC k) where
+  ContC cxbx . ContC bxax = ContC (\kcx -> bxax (cxbx kcx))
+instance Category (ContC k) where
+  id = ContC id
diff --git a/Algebra/Monad/Logic.hs b/Algebra/Monad/Logic.hs
new file mode 100644
--- /dev/null
+++ b/Algebra/Monad/Logic.hs
@@ -0,0 +1,54 @@
+{-# LANGUAGE UndecidableInstances #-}
+module Algebra.Monad.Logic where
+
+import Algebra.Monad.Base
+
+newtype LogicT m a = LogicT { runLogicT :: forall r. (a -> m r -> m r) -> m r -> m r }
+
+instance Functor (LogicT m) where
+  map f (LogicT l) = LogicT (\k -> l (\a -> k (f a)))
+instance Unit (LogicT m) where
+  pure a = LogicT ($a)
+instance Applicative (LogicT m)
+instance Monad (LogicT m) where
+  join (LogicT l) = LogicT (\k -> l (\(LogicT l') -> l' k))
+instance MonadFix (LogicT m) where
+  mfix f = fix (\(LogicT l) -> LogicT (\k -> l (\a m -> runLogicT (f a) k m)))
+instance MonadTrans LogicT where
+  lift ma = LogicT (\k mr -> ma >>= \a -> k a mr)
+
+instance Semigroup (LogicT m a) where
+  LogicT l + LogicT l' = LogicT (\k -> l k . l' k)
+instance Monoid (LogicT m a) where
+  zero = LogicT (pure id)
+instance Semigroup a => Semiring (LogicT m a) where
+  (*) = plusA
+instance Monoid a => Ring (LogicT m a) where
+  one = zeroA
+
+instance MonadState s m => MonadState s (LogicT m) where
+  get = lift get
+  modify f = lift (modify f)
+
+class Monad m => MonadLogic l m | l -> m where
+  deduce :: l a -> m (Maybe (a,l a))
+  induce :: m (Maybe (a,l a)) -> l a
+instance Monad m => MonadLogic (LogicT m) m where
+  deduce l = runLogicT l (\a m -> pure (pure (a,induce m))) (pure zero)
+  induce mm = LogicT (\k m -> mm >>= maybe m (\(a,l) -> k a (runLogicT l k m)))
+
+listLogic :: (MonadLogic l m,MonadLogic l' n) => Iso (l a) (l' b) (m [a]) (n [b])
+listLogic = iso alts deduceAll
+  where alts m = induce (m <&> \l -> case l of
+          [] -> Nothing
+          (a:t) -> Just (a,alts (pure t)))
+
+deduceMany :: MonadLogic l m => Int -> l a -> m [a]
+deduceMany 0 _ = pure []
+deduceMany n l = deduce l >>= maybe (pure []) (\(a,t) -> (a:)<$>deduceMany (n-1) t)
+deduceAll :: MonadLogic l m => l a -> m [a]
+deduceAll l = deduce l >>= maybe (pure []) (\(a,t) -> (a:)<$>deduceAll t)
+
+choose :: MonadLogic l m => [a] -> l a
+choose l = pure l^.listLogic
+
diff --git a/Algebra/Monad/RWS.hs b/Algebra/Monad/RWS.hs
--- a/Algebra/Monad/RWS.hs
+++ b/Algebra/Monad/RWS.hs
@@ -3,7 +3,7 @@
   RWST(..),RWS,MonadInternal(..),_RWST,
 
   -- * Default methods
-  get_,put_,modify_,local_,ask_,tell_,listen_,censor_,getAcc_
+  get_,put_,modify_,local_,ask_,tell_,listen_,censor_,getCounter_
   ) where
 
 import Algebra.Monad.Base
@@ -25,8 +25,8 @@
 instance (Monoid w,MonadFix m) => MonadFix (RWST r w s m) where
   mfix f = RWST (\x -> mfix (\ ~(a,_,_) -> runRWST (f a) x))
 instance (Monoid w,MonadCont m) => MonadCont (RWST r w s m) where
-  callCC f = RWST $ \(r,s) ->
-    callCC $ \k -> runRWST (f (\a -> lift (k (a,s,zero)))) (r,s)
+  callCC f = RWST $ \i ->
+    callCC (\k -> runRWST (f (\a -> RWST (\(_,s) -> k (a,s,zero)<&>(,s,zero)))) i<&> \(b,_,_) -> b)
 deriving instance Semigroup (m (a,s,w)) => Semigroup (RWST r w s m a)
 deriving instance Monoid (m (a,s,w)) => Monoid (RWST r w s m a)
 deriving instance Semiring (m (a,s,w)) => Semiring (RWST r w s m a)
@@ -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)
@@ -85,5 +91,5 @@
 listen_ = internal (\m -> listen m <&> \(w,(c,a)) -> (c,(w,a)) )
 censor_ :: (MonadInternal t, MonadWriter w m) => t m (a, w -> w) -> t m a
 censor_ = internal (\m -> censor (m <&> \(c,(a,f)) -> ((c,a),f)))
-getAcc_ :: (MonadTrans t,MonadWriterAcc w acc m) => t m acc
-getAcc_ = lift getAcc
+getCounter_ :: (MonadTrans t,MonadCounter w acc m) => t m acc
+getCounter_ = lift getCounter
diff --git a/Algebra/Monad/Reader.hs b/Algebra/Monad/Reader.hs
--- a/Algebra/Monad/Reader.hs
+++ b/Algebra/Monad/Reader.hs
@@ -14,26 +14,28 @@
 
 {-| A simple Reader monad -}
 newtype ReaderT r m a = ReaderT (RWST r Void Void m a) 
-                      deriving (Functor,Unit,Applicative,Monad,MonadFix,
+                      deriving (Functor,Unit,Applicative,MonadFix,
                                 MonadTrans,MonadInternal,
                                 MonadReader r,MonadCont,MonadList)
+instance Monad m => Monad (ReaderT r m) where join = coerceJoin ReaderT
 type Reader r a = ReaderT r Id a
 
 instance MonadState s m => MonadState s (ReaderT r m) where
   get = get_ ; put = put_ ; modify = modify_
 instance MonadWriter w m => MonadWriter w (ReaderT r m) where
   tell = tell_ ; listen = listen_ ; censor = censor_
-instance MonadWriterAcc w acc m => MonadWriterAcc w acc (ReaderT r m) where
-  getAcc = getAcc_
+instance MonadCounter w acc m => MonadCounter w acc (ReaderT r m) where
+  getCounter = getCounter_
 deriving instance Semigroup (m (a,Void,Void)) => Semigroup (ReaderT r m a)
 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
@@ -4,7 +4,7 @@
   MonadState(..),
   StateT,State,
   stateT,eval,exec,state,
-  (=~),(=-),(^>=),gets,getl,saving,
+  (=~),(=-),(^>=),gets,use,saving,
   Next,Prev,
   mapAccum,mapAccum_,mapAccumR,mapAccumR_,push,pop,withPrev,withNext,
 
@@ -21,33 +21,35 @@
   modify f = put (f unit)
 
 newtype StateT s m a = StateT (RWST Void Void s m a)
-                     deriving (Unit,Functor,Applicative,Monad,MonadFix,
+                     deriving (Unit,Functor,Applicative,MonadFix,
                                MonadTrans,MonadInternal,
                                MonadCont,MonadState s,MonadList)
 type State s a = StateT s Id a
+instance Monad m => Monad (StateT s m) where join = coerceJoin StateT
 instance MonadReader r m => MonadReader r (StateT s m) where
   ask = ask_ ; local = local_
 instance MonadWriter w m => MonadWriter w (StateT s m) where
   tell = tell_ ; listen = listen_ ; censor = censor_
-instance (MonadWriterAcc w acc m) => MonadWriterAcc w acc (StateT s m) where
-  getAcc = lift getAcc
+instance (MonadCounter w acc m) => MonadCounter w acc (StateT s m) where
+  getCounter = lift getCounter
 deriving instance MonadError e m => MonadError e (StateT s m)
 deriving instance Semigroup (m (a,s,Void)) => Semigroup (StateT s m a)
 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 =-,=~
@@ -58,24 +60,26 @@
 l ^>= k = get >>= \s -> forl_ l s k
 gets :: MonadState s m => (s -> a) -> m a
 gets = (get<&>) 
-getl :: MonadState s m => Getter' s a -> m a
-getl l = by l<$>get
+use :: MonadState s m => Getter' s a -> m a
+use l = by l<$>get
 
 saving :: MonadState s m => Lens' s s' -> m a -> m a
-saving l st = getl l >>= \s -> st <* (l =- s)
+saving l st = use l >>= \s -> st <* (l =- s)
 
 -- * The State Arrow
 newtype StateA m s a = StateA (StateT s m a)
 stateA :: Iso (StateA m s a) (StateA m' s' a') (StateT s m a) (StateT s' m' a')
 stateA = iso StateA (\(StateA s) -> s)
-instance Monad m => Category (StateA m) where
-  id = StateA get
+
+instance Monad m => Deductive (StateA m) where
   StateA sbc . StateA sab = StateA $ (^.stateT) $ \a ->
     (sab^..stateT) a >>= \(a',b) -> (a',).snd <$> (sbc^..stateT) b
+instance Monad m => Category (StateA m) where
+  id = StateA get
 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 +90,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,18 +2,18 @@
 module Algebra.Monad.Writer (
     -- * The Writer monad
   MonadWriter(..),
-  mute,intercept,
+  mute,intercept,intercept',eavesdrop,
 
   -- * The Writer transformer
   WriterT,Writer,
   writerT,writer,pureWriter,
 
   -- * Keeping track of where we are
-  MonadWriterAcc(..),
+  MonadCounter(..),
 
   -- ** Implementation
-  WriterAccT,WriterAcc,
-  writerAccT,writerAcc
+  CounterT,Counter,
+  i'counterT,i'counter
   ) where
 
 import Algebra.Monad.Base
@@ -28,13 +28,19 @@
 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)
-                      deriving (Unit,Functor,Applicative,Monad,MonadFix
-                               ,Foldable,Traversable
+                      deriving (Unit,Functor,Applicative,MonadFix
+                               ,Foldable
                                ,MonadTrans,MonadInternal
                                ,MonadWriter w,MonadCont,MonadList)
+instance (Monoid w,Monad m) => Monad (WriterT w m) where join = coerceJoin WriterT
+instance Traversable m => Traversable (WriterT e m) where sequence = coerceSeq WriterT
 type Writer w a = WriterT w Id a
 instance (Monoid w,MonadReader r m) => MonadReader r (WriterT w m) where
   ask = ask_ ; local = local_
@@ -44,22 +50,24 @@
 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
 
-{-| The canonical representation of a WriterAcc Monad -}
-newtype WriterAccT w acc m a = WA { runWA :: RWST () w acc m a }
-                             deriving (Functor,Unit,Monad,Applicative,MonadFix,MonadTrans)
-type WriterAcc w acc a = WriterAccT w acc Id a
+{-| The canonical representsation of a WriterAcc Monad -}
+newtype CounterT w acc m a = WA { runWA :: RWST () w acc m a }
+                             deriving (Functor,Unit,Applicative,MonadFix,MonadTrans)
+instance (Monoid w,SubSemi a w,Monad m) => Monad (CounterT w a m) where join = coerceJoin WA
+type Counter w acc a = CounterT w acc Id a
 
-instance (Monad m,SubSemi acc w,Monoid w) => MonadWriter w (WriterAccT w acc m) where
+instance (Monad m,SubSemi acc w,Monoid w) => MonadWriter w (CounterT w acc m) where
   tell w = WA (tell w >> modify (+ cast w))
   listen = WA . listen . runWA
   censor (WA m) = WA $ do
@@ -67,17 +75,18 @@
     (w,a) <- listen (censor m)
     put $ cur + cast w
     return a
-instance (Monad m,Monoid w,SubSemi acc w) => MonadWriterAcc w acc (WriterAccT w acc m) where
-  getAcc = WA get  
-instance (MonadState s m,Monoid w,SubSemi acc w) => MonadState s (WriterAccT w acc m) where
+instance (Monad m,Monoid w,SubSemi acc w) => MonadCounter w acc (CounterT w acc m) where
+  getCounter = WA get  
+instance (MonadState s m,Monoid w,SubSemi acc w) => MonadState s (CounterT w acc m) where
   get = WA (lift get)
   put = WA . lift . put
+deriving instance (Monad m, Monoid w, SubSemi acc w, MonadFuture n m) => MonadFuture n (CounterT 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
-writerAccT :: (SubSemi acc w,SubSemi acc' w',Monoid acc,Monoid acc',Functor m)
-              => Iso (WriterAccT w acc m a) (WriterAccT w' acc' m' a') (m (a,acc,w)) (m' (a',acc',w'))
-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
+i'CounterT :: Iso (CounterT w acc m a) (CounterT w' acc' m' a') (RWST () w acc m a) (RWST () w' acc' m' a')
+i'CounterT = iso WA runWA
+i'counterT :: (SubSemi acc w,SubSemi acc' w',Monoid acc,Monoid acc',Functor m)
+              => Iso (CounterT w acc m a) (CounterT w' acc' m' a') (m (a,acc,w)) (m' (a',acc',w'))
+i'counterT = iso (\m (_,s) -> m <&> \(a,s',w) -> (a,s+s',w)) ($zero)._RWST.i'CounterT
+i'counter :: (SubSemi acc w,SubSemi acc' w',Monoid acc,Monoid acc',Functor m)
+             => Iso (Counter w acc a) (Counter w' acc' a') (a,acc,w) (a',acc',w')
+i'counter = i'Id.i'counterT
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
@@ -1,9 +1,13 @@
+{-# LANGUAGE ScopedTypeVariables #-}
 module Algebra.Traversable(
   module Algebra.Applicative, module Algebra.Foldable,
 
   Traversable(..),Contravariant(..),
 
-  traverse,foreach,transpose,flip,project,doTimes,converted,folded,
+  traverse,for,transpose,doTimes,converted,folded,
+
+  -- * Instance utilities
+  coerceSeq
   ) where
 
 import Algebra.Classes
@@ -12,9 +16,8 @@
 import Algebra.Foldable
 import Algebra.Lens
 import Data.Tree
+import Unsafe.Coerce
 
-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
@@ -22,12 +25,16 @@
 instance Traversable [] where
   sequence (x:xs) = (:)<$>x<*>sequence xs
   sequence [] = pure []
-deriving instance Traversable Interleave
-deriving instance Traversable OrdList
-deriving instance Traversable ZipList
+
+coerceSeq :: forall f t' t a. (Applicative f,Traversable t) => (forall b. t b -> t' b) -> (t' (f a) -> f (t' a))
+coerceSeq _ = unsafeCoerce (sequence :: t (f a) -> f (t a))
+instance Traversable Interleave where sequence = coerceSeq Interleave
+instance Traversable OrdList where sequence = coerceSeq OrdList
+instance Traversable (Increasing k) where sequence = coerceSeq Increasing
+instance Traversable (Assoc k) where sequence (Assoc k fa) = Assoc k<$>fa
+instance Traversable f => Traversable (Zip f) where sequence = coerceSeq Zip
 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
@@ -38,11 +45,8 @@
 instance Traversable Maybe where
   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
+instance Traversable Strict where
+  sequence (Strict fa) = Strict<$>fa
 
 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
@@ -51,17 +55,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
+  each = traverse
diff --git a/Data/Containers.hs b/Data/Containers.hs
--- a/Data/Containers.hs
+++ b/Data/Containers.hs
@@ -1,24 +1,24 @@
 {-# 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,resides,member,delete,touch,insert,singleton,singleton',fromAList,fromKList,(#),(#?),
+  cached,
 
   -- * Map instances
   -- ** Sets and maps
-  Set,Map,
+  Set,Map,c'setOf,c'set,c'mapOf,c'map,
   
   -- ** Bimaps
   Bimap(..),toMap,keysSet,
 
   -- ** Relations
-  Relation(..),domains,ranges,related,link
+  Relation(..),i'Relation,i'domains,i'ranges,l'domain,l'range,link,(*>>>)
   )
   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
+resides :: DataMap m k a => k -> m -> Bool
+resides = 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
-fromList :: DataMap m k a => [(k,a)] -> m
-fromList l = compose (uncurry insert<$>l) zero
+singleton' :: (Monoid a,DataMap m k a) => k -> m
+singleton' x = touch x zero
+fromAList :: DataMap m k a => [(k,a)] -> m
+fromAList l = compose (uncurry insert<$>l) zero
+fromKList :: (Monoid a,DataMap m k a) => [k] -> m
+fromKList 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
   
@@ -69,12 +95,17 @@
 instance Ord k => Semigroup (Map k a) where (+) = M.union
 instance Ord k => Monoid (Map k a) where zero = M.empty
 instance Ord k => Disjonctive (Map k a) where (-) = M.difference
-instance (Ord k,Semigroup a) => Semiring (Map k a) where (*) = M.intersectionWith (+)
+instance (Ord k,Semigroup a) => Semiring (Map k a) where (*) = M.unionWith (+)
 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)
 
+instance Ord k => Unit (Zip (Map k)) where
+  pure = undefined
+instance Ord k => Applicative (Zip (Map k)) where
+  Zip fs <*> Zip xs = Zip (M.intersectionWith ($) fs xs)
+
 -- |An invertible map
 newtype Bimap a b = Bimap (Map a b,Map b a)
                   deriving (Show,Semigroup,Monoid,Disjonctive,Semiring)
@@ -82,38 +113,43 @@
   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
 toMap (Bimap (a,_)) = a
 
-keysSet :: (Eq a,Eq b) => Iso (Set a) (Set b) (Map a Void) (Map b Void)
-keysSet = ascList.from ascList
+keysSet :: (Eq k,OrderedMap m k a m k a) => m -> Set k
+keysSet m = map (second (const zero)) (m^.ascList)^.from ascList
 
 --- |The Relation type
 newtype Relation a b = Relation (Map a (Set b),Map b (Set a))
-                     deriving (Show,Semigroup,Monoid,Eq,Ord)
-_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)
+                     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 (zipWith (*) x y,zipWith (*) x' y')
+i'Relation :: Iso (Relation a b) (Relation c d) (Map a (Set b),Map b (Set a)) (Map c (Set d),Map d (Set c))
+i'Relation = iso Relation (\(Relation r) -> r)
 instance Commutative Relation where
   commute (Relation (a,b)) = Relation (b,a)
 
 -- |Define a Relation from its ranges. O(1) <-> O(1,n*ln(n)) 
-ranges :: (Ord c,Ord d) => Iso (Map a (Set b)) (Map c (Set d)) (Relation a b) (Relation c d)
-ranges = iso (\(Relation (rs,_)) -> rs) fromRanges
+i'ranges :: (Ord c,Ord d) => Iso (Map a (Set b)) (Map c (Set d)) (Relation a b) (Relation c d)
+i'ranges = iso (\(Relation (rs,_)) -> rs) fromRanges
   where fromRanges rs = Relation (rs,compose (rs^.keyed <&> \ (a,bs) -> compose $ bs <&> \b ->
                                               at b%~Just . touch a . fold) zero)
 -- |Define a Relation from its domain (uses the Commutative instance)
-domains :: (Ord c,Ord d) => Iso (Map b (Set a)) (Map d (Set c)) (Relation a b) (Relation c d)
-domains = commuted.ranges
+i'domains :: (Ord c,Ord d) => Iso (Map b (Set a)) (Map d (Set c)) (Relation a b) (Relation c d)
+i'domains = commuted.i'ranges
 
 instance (Ord k,Ord a) => DataMap (Relation k a) k (Set a) where
   at a = lens (\(Relation (rs,_)) -> rs^.at a) setRan
@@ -127,12 +163,17 @@
 may :: (Monoid (f b),Foldable f) => Iso (Maybe (f a)) (Maybe (f b)) (f a) (f b)
 may = iso (\f -> if empty f then Nothing else Just f) (maybe zero id)
 
-related :: (Ord a,Ord b) => a -> Lens' (Relation a b) (Set b)
-related a = at a.from may
+l'domain :: (Ord a,Ord b) => a -> Lens' (Relation a b) (Set b)
+l'domain a = at a.from may
+l'range :: (Ord a,Ord b) => b -> Lens' (Relation a b) (Set a)
+l'range a = commuted.l'domain a
 
 link :: (Ord a,Ord b) => a -> b -> Lens' (Relation a b) Bool
-link a b = related a.member b
+link a b = l'domain 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
   where g a = do
@@ -142,3 +183,5 @@
             Nothing -> let b = f a in putMVar vm (insert a b m) >> return b
         vm = newMVar (zero :: Map a b)^.thunk
 
+(*>>>) :: (Ord a,Ord b,Ord c) => Relation a b -> Relation b c -> Relation a c
+r *>>> r' = r & i'ranges %~ map (foldMap (\b -> r'^.l'domain b))
diff --git a/Data/Containers/Sequence.hs b/Data/Containers/Sequence.hs
--- a/Data/Containers/Sequence.hs
+++ b/Data/Containers/Sequence.hs
@@ -1,17 +1,27 @@
+{-# LANGUAGE ScopedTypeVariables #-}
 module Data.Containers.Sequence (
-  Sequence(..),Stream(..),take,drop,
+  Sequence(..),Stream(..),i'elems,take,drop,
 
   -- * Strict and lazy slices (bytestrings on arbitrary Storable types)
-  Slice,Slices,slice,slices,_Slices,breadth,
+  Slice,Slices,slice,slices,i'storables,_Slices,breadth,
 
-  V.unsafeWith
+  V.unsafeWith,sliceElt,span,break,
+
+  takeWhile,takeUntil,dropWhile,dropUntil,pry,
+
+  (++)
   ) where
 
-import Algebra hiding (splitAt,take,drop)
-import qualified Data.List as L
+import Definitive.Base
+import Data.Containers
 import qualified Data.ByteString.Lazy as Bytes
 import qualified Data.ByteString.Char8 as Char8
+import qualified Data.ByteString.Internal as BSI
 import qualified Data.Vector.Storable as V
+import Foreign.Storable (sizeOf)
+import qualified Prelude as P
+import Foreign.ForeignPtr (ForeignPtr,castForeignPtr)
+import Unsafe.Coerce (unsafeCoerce)
 
 class Monoid t => Sequence t where
   splitAt :: Int -> t -> (t,t)
@@ -25,7 +35,12 @@
 instance V.Storable a => Monoid (V.Vector a) where zero = V.empty
   
 instance Sequence [a] where
-  splitAt = L.splitAt
+  splitAt n l = (h,t)
+    where ~(h,t) = case (n,l) of
+            (0,_) -> ([],l)
+            (_,[]) -> ([],[])
+            (_,(x:l')) -> let (h',t') = splitAt (n-1) l' in (x:h',t')
+                  
 instance Sequence Bytes where
   splitAt = Bytes.splitAt . fromIntegral
 instance V.Storable a => Sequence (V.Vector a) where
@@ -43,6 +58,16 @@
   cons = Char8.cons
 
 type Slice a = V.Vector a
+i'storables :: forall a b. (V.Storable a,V.Storable b) => Iso (Slice a) (Slice b) Chunk Chunk
+i'storables = iso toV fromV
+  where toV bs = vec
+          where
+            vec = V.unsafeFromForeignPtr (castForeignPtr fptr :: ForeignPtr a) (scale off) (scale len)
+            (fptr, off, len) = BSI.toForeignPtr bs
+            scale = (`div` sizeOf (V.head vec))
+        fromV v = BSI.fromForeignPtr (castForeignPtr fptr) 0 (len * sizeOf (undefined :: b))
+          where (fptr, len) = V.unsafeToForeignPtr0 v
+
 newtype Slices a = Slices [Slice a]
                     deriving (Semigroup,Monoid)
 _Slices :: Iso (Slices a) (Slices b) [Slice a] [Slice b]
@@ -60,5 +85,53 @@
 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
+instance V.Storable a => DataMap (Slice a) Int a where
+  at i = lens (\v -> v V.!? i) (\v e -> case e of
+                                   Just a -> v V.// [(i,a)]
+                                   Nothing -> take i v)
+
+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
+
+pry :: Stream c s => Int -> s -> ([c],s)
+pry 0 s = ([],s)
+pry n s = case uncons s of
+  Just (a,s') -> let ~(t,l') = pry (n-1) s' in (a:t,l')
+  Nothing -> ([],s)
+
+(++) :: Stream c s => [c] -> s -> s
+(a:t) ++ c = cons a (t++c)
+[] ++ c = c
+
+i'elems :: (Monoid s',Stream c s,Stream c' s') => Iso [c] [c'] s s'
+i'elems = iso (takeUntil (const False)) (++zero)
+
+newtype StreamC a = StreamC (forall x. (a -> x -> x) -> x)
+
+instance Stream a (StreamC a) where
+  cons a (StreamC l) = StreamC (\c -> c a (l c))
+  uncons (StreamC l) = Just (l const,l (flip const))
diff --git a/Data/Probability.hs b/Data/Probability.hs
--- a/Data/Probability.hs
+++ b/Data/Probability.hs
@@ -1,20 +1,27 @@
 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
+                    deriving (Unit,Functor,Applicative
+                             ,Semigroup,Monoid
                              ,MonadFix,MonadWriter (Product t))
+instance (Ring t,Monad m) => Monad (ProbT t m) where join = coerceJoin ProbT
 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
 
-instance (Monad m,Ring t,Fractional t) => MonadList (ProbT t m) where
-  fork l = pure [(Product x,a) | a <- l]^.probT
-    where x = 1/size l
+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 _ = c'_
+
+instance (Monad m,Invertible t) => MonadList (ProbT t m) where
+  fork l = pure [(x,a) | a <- l]^.probT
+    where x = recip (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/Queue.hs b/Data/Queue.hs
new file mode 100644
--- /dev/null
+++ b/Data/Queue.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+module Data.Queue where
+
+import Definitive
+
+data Front
+data Back
+newtype DeQue a = DeQue ([a],[a])
+instance Semigroup (DeQue a) where
+  DeQue (h,t) + DeQue (h',t') = DeQue (h+reverse t,t'+reverse h')
+deriving instance Monoid (DeQue a)
+instance Functor DeQue where
+  map f (DeQue (h,t)) = DeQue (map f h,map f t)
+instance Foldable DeQue where
+  fold (DeQue (h,t)) = fold h + fold t
+instance Traversable DeQue where
+  sequence (DeQue (fh,ft)) = liftA2 (map2 DeQue (,)) (sequence fh) (sequence ft)
+
+newtype Queue push pop a = Queue { deque :: DeQue a }
+                           deriving (Semigroup,Monoid,Functor,Foldable)
+instance Traversable (Queue push pop) where sequence = coerceSeq Queue
+c'queue :: Constraint push -> Constraint pop -> Constraint (Queue push pop a)
+c'queue _ _ = c'_
+c'front :: Constraint Front
+c'front = c'_
+c'back :: Constraint Back
+c'back = c'_
+
+queue :: Queue x y a -> Queue s t a
+queue (Queue q) = Queue q
+
+class Direction t where
+  isFront :: t -> Bool
+instance Direction Front where isFront _ = True
+instance Direction Back where isFront _ = False
+instance forall push pop a. (Direction push,Direction pop) => Stream a (Queue push pop a) where
+  cons = if isFront (undefined :: push) then pushFront else pushBack 
+    where
+      pushFront a (Queue (DeQue (h,t))) = Queue (DeQue (a:h,t))
+      pushBack a (Queue (DeQue (h,t))) = Queue (DeQue (h,a:t))
+  uncons = l $ if isFront (undefined :: pop) then popFront else popBack
+    where
+      l f = f . deque
+      popFront (DeQue (a:h,t)) = Just (a,Queue (DeQue (h,t)))
+      popFront (DeQue ([],[])) = Nothing
+      popFront (DeQue ([],t)) = popFront (DeQue (reverse t,[]))
+      popBack (DeQue (h,a:t)) = Just (a,Queue (DeQue (h,t)))
+      popBack (DeQue ([],[])) = Nothing
+      popBack (DeQue (h,[])) = popBack (DeQue ([],reverse h))
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
--- a/Data/TimeVal.hs
+++ b/Data/TimeVal.hs
@@ -2,7 +2,7 @@
   TimeVal(..)
   ) where
 
-import Algebra
+import Definitive
 
 -- |A type wrapper that adds a Bounded instance for types that don't possess one.
 data TimeVal t = Always | Since t | Never
@@ -28,3 +28,48 @@
 instance Bounded (TimeVal t) where
   minBound = Always ; maxBound = Never
 
+data BoolNode a = Maximum a a
+                | Minimum a a
+                | Truth a
+
+instance Unit BoolNode where pure = Truth
+instance Functor BoolNode where
+  map f (Maximum a b) = Maximum (f a) (f b)
+  map f (Minimum a b) = Minimum (f a) (f b)
+  map f (Truth a) = Truth (f a)
+instance Foldable BoolNode where
+  fold (Maximum a b) = a+b
+  fold (Minimum a b) = a+b
+  fold (Truth a) = a
+instance Traversable BoolNode where
+  sequence (Maximum fa fb) = liftA2 Maximum fa fb
+  sequence (Minimum fa fb) = liftA2 Minimum fa fb
+  sequence (Truth fa) = Truth<$>fa
+
+instance Ord a => Eq (BoolNode a) where
+  a == b = compare a b == EQ
+instance Ord a => Ord (BoolNode a) where
+  compare = cmp
+    where
+      cmp (Minimum a b) = cmpTo
+        where cmpTo (Truth c) = scmax ac bc
+                where ac = compare a c ; bc = compare b c
+              cmpTo (Minimum c d) = scmin (cmpTo (Truth c)) (cmpTo (Truth d))
+              cmpTo (Maximum c d) = scmax (cmpTo (Truth c)) (cmpTo (Truth d))
+      cmp (Maximum a b) = cmpTo
+        where cmpTo (Truth c) = scmin ac bc
+                where ac = compare a c ; bc = compare b c
+              cmpTo (Minimum c d) = scmin (cmpTo (Truth c)) (cmpTo (Truth d))
+              cmpTo (Maximum c d) = scmax (cmpTo (Truth c)) (cmpTo (Truth d))
+      cmp x = \y -> invertOrd (cmp y x)
+      scmax = shortCircuit max
+      scmin = shortCircuit min
+
+shortCircuit :: (a -> a -> a) -> (a -> a -> a)
+shortCircuit f = \a b -> f a b`unamb`f b a
+
+newtype Boolean a = Boolean (Free BoolNode a)
+               deriving (Eq,Ord,Functor,Foldable,Unit,Applicative)
+instance Monad Boolean where join = coerceJoin Boolean
+instance Traversable Boolean where sequence = coerceSeq Boolean
+-- CONTINUE
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,16 +1,18 @@
+-- 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
+homepage:      http://coiffier.net/projects/definitive-framework.html
+description:
+  The Definitive framework is an attempt at harnessing the declarative
   nature of Haskell to provide a solid and simple base for writing 
   real-world programs, as well as complex algorithms.
-  
+  .
   This package contains the base modules of the framework, and provides
   only the most basic functionality, ranging from basic algebraic
   structures, such as monoids and rings, to functors, applicative functors,
   monads and transformers.
-  
+  .
   Lenses are used heavily in all the framework's abstractions, replacing
   more traditional functions ('WriterT' and 'runWriterT' are implemented
   in the same isomorphism 'writerT', for example). When used wisely,
@@ -19,40 +21,44 @@
   defining them as soon as possible. Isomorphisms in particular are
   surprisingly useful in many instances, from converting between types
   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
   and the Definitive framework :
-  
-    - The '+', '-', 'negate', and '*' are now part of the Semigroup,
-      Disjonctive, Negative, Semiring classes instead of Num (default
-      instances are defined to reimplement the Prelude, making it easy
-      to adjust your code for compatibility) 
-    
-    - The mapM, traverseM, liftM, and such functions have been hidden,
-      since they only reimplement the traverse, map, and other simpler
-      functions.
-  
-    - Lenses are used whenever possible instead of more usual functions.
-      You are encouraged to read the interface for the Algebra.Lens
-      module, which contains everything you will need to be able to use
-      lenses to their full potential (except maybe a good explanation).
-  
-      
+  .
+  * The '+', '-', 'negate', and '*' are now part of the Semigroup,
+    Disjonctive, Negative, Semiring classes instead of Num (default
+    instances are defined to reimplement the Prelude, making it easy
+    to adjust your code for compatibility) 
+  .
+  * The mapM, traverseM, liftM, and such functions have been hidden,
+    since they only reimplement the traverse, map, and other simpler
+    functions.
+  .
+  * Lenses are used whenever possible instead of more usual functions.
+    You are encouraged to read the interface for the Algebra.Lens
+    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:       2.3
 license:       OtherLicense
 license-file:  LICENSE
 
+-- build information
 build-type:    Simple
 cabal-version: >=1.10
+tested-with:   GHC (== 7.8.3)
 
 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.*)
-  default-extensions: TypeSynonymInstances NoMonomorphismRestriction StandaloneDeriving GeneralizedNewtypeDeriving TypeOperators RebindableSyntax FlexibleInstances FlexibleContexts FunctionalDependencies TupleSections MultiParamTypeClasses Rank2Types
-  ghc-options: -Wall -fno-warn-orphans -threaded
+  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 Algebra.Monad.Free Algebra.Monad.Logic Data.Containers Data.Containers.Sequence Data.TimeVal Data.Queue Data.Probability
+  build-depends: base (== 4.7.*), ghc-prim (== 0.3.*), GLURaw (== 1.4.*), OpenGL (== 2.9.*), OpenGLRaw (== 1.5.*), 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 AllowAmbiguousTypes RoleAnnotations
+  ghc-options: -Wall -fno-warn-orphans -threaded -O2
   default-language: Haskell2010
+  include-dirs: