diff --git a/Algebra/Applicative.hs b/Algebra/Applicative.hs
--- a/Algebra/Applicative.hs
+++ b/Algebra/Applicative.hs
@@ -12,7 +12,8 @@
   between,
   
   liftA,liftA2,liftA3,liftA4,forever,
-
+  zipWith,zipWith3,
+  
   plusA,zeroA
   ) where
 
@@ -33,6 +34,18 @@
 instance Monoid w => Applicative ((,) w)
 instance Monoid w => Monad ((,) w) where
   join ~(w,~(w',a)) = (w+w',a)
+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
@@ -51,8 +64,13 @@
 -}
 newtype Zip f a = Zip { deZip :: f a }
 c'zip :: Constraint (f a) -> Constraint (Zip f a)
-c'zip _ = id
+c'zip _ = c'_
 
+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
 
@@ -76,7 +94,7 @@
 -- |A wrapper for applicative functors with actions executed in the reverse order
 newtype Backwards f a = Backwards { forwards :: f a }
 c'backwards :: Constraint (f a) -> Constraint (Backwards f a)
-c'backwards _ = id
+c'backwards _ = c'_
 
 deriving instance Semigroup (f a) => Semigroup (Backwards f a)
 deriving instance Monoid (f a) => Monoid (Backwards f a)
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
@@ -17,7 +17,15 @@
   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
@@ -44,18 +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 MonadFuture m t | t -> m where
+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,17 +1,17 @@
 {-# LANGUAGE NoRebindableSyntax, MultiParamTypeClasses, DefaultSignatures, TupleSections, EmptyDataDecls #-}
 module Algebra.Core(
   -- * Raw data
-  Handle,
-  Bytes,readBytes,writeBytes,contentBytes,
-  Chunk,readChunk,writeChunk,contentChunk,
-  readString,writeString,contentString,
+  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(..),
 
@@ -24,16 +24,16 @@
   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(..),
   
   -- * Expression-level type constraints
-  Constraint,c'listOf,c'list,c'int,c'float,
+  Constraint,c'listOf,c'list,c'int,c'char,c'string,c'float,c'_,
   
   -- * Miscellaneous functions
   const,(&),($^),is,fix,
@@ -47,14 +47,17 @@
   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 (
@@ -65,27 +68,42 @@
   sequence,mapM,mapM_,sequence_,(=<<),
 
   map,(++),foldl,foldr,foldr1,concat,filter,length,sum,lookup,
-  (+),(*),(.),id,const,(-),
+  (+),(*),(.),id,const,(-),(/),recip,
 
   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,hGetContents)
+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 _ = id
+c'listOf _ = c'_
 c'list :: Constraint [a]
-c'list = id
+c'list = c'listOf c'_
 c'int :: Constraint Int
-c'int = id
+c'int = c'_
+c'char :: Constraint Char
+c'char = c'_
+c'string :: Constraint String
+c'string = c'_
 c'float :: Constraint Float
-c'float = id
+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
@@ -102,12 +120,18 @@
 writeChunk = BSS.writeFile
 writeString :: String -> String -> IO ()
 writeString = P.writeFile
-contentBytes :: Handle -> IO Bytes
-contentBytes = BSL.hGetContents
-contentChunk :: Handle -> IO Chunk
-contentChunk = BSS.hGetContents
-contentString :: Handle -> IO String
-contentString = hGetContents
+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)
@@ -121,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')
@@ -150,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
@@ -165,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
@@ -196,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
@@ -210,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
@@ -220,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
@@ -277,15 +329,29 @@
 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)
@@ -297,23 +363,31 @@
 -- 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
@@ -401,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)
@@ -417,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
@@ -7,6 +7,7 @@
 import Data.Tree
 
 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
@@ -16,16 +17,18 @@
   -- | 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 [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
@@ -50,10 +53,24 @@
 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 ())
@@ -78,6 +95,8 @@
 
 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
 
@@ -110,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
@@ -4,8 +4,9 @@
   Functor(..),Cofunctor(..),Bifunctor(..),Commutative(..),Contravariant(..),
   
   Strict(..),Id(..),Const(..),Flip(..),(:.:)(..),(:**:)(..),(:++:)(..),
-
-  flip,project,
+  Increasing(..),
+  
+  emerge,flip,project,factor,
   (<$>),(|||),(<$),(<&>),void,left,right,
   promap,map2,map3
   ) where
@@ -27,12 +28,15 @@
 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
@@ -54,11 +58,9 @@
 
 newtype Strict a = Strict { lazy :: a }
 instance Unit Strict where pure = Strict
-instance Functor Strict where map f (Strict a) = Strict (f a)
-instance Applicative Strict where
-  Strict f <*> Strict x = Strict (f$!x)
-instance Monad Strict where
-  join (Strict x) = x
+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 }
@@ -69,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)
@@ -78,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
@@ -30,7 +30,7 @@
   (-.),(.-),
   
   -- * Basic lenses
-  Lens1(..),Lens2(..),Lens3(..),Lens4(..),
+  Lens1(..),Lens2(..),Lens3(..),Lens4(..),Lens5(..),
   Trav1(..),Trav2(..),
   Compound(..),
   i'list,i'pair,t'head,t'tail,
@@ -48,7 +48,7 @@
   negated,commuted,adding,
   
   -- ** Higher-order isomorphisms
-  warp2,mapping,mapping',promapping,
+  warp2,mapping,mapping',promapping,applying,
 
   IsoFunctor(..),(<.>),IsoFunctor2(..)
   ) where
@@ -171,6 +171,8 @@
   l'3 :: Lens s t a b
 class Lens4 s t a b | a -> s, a t -> b where
   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
   t'l :: Traversal s t a b
 class Trav2 s t a b | a -> s, a t -> b where
@@ -183,18 +185,29 @@
   l'1 = lens (\ ~(a,_,_) -> a) (\ (_,c,d) b -> (b,c,d))
 instance Lens1 a b (a,c,d,e) (b,c,d,e) where
   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
   l'2 = lens snd (flip (second . const))
 instance Lens2 a b (c,a,d) (c,b,d) where
   l'2 = lens (\ ~(_,a,_) -> a ) (\ ~(c,_,d) b -> (c,b,d))
 instance Lens2 a b (c,a,d,e) (c,b,d,e) where
   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
   l'3 = lens (\ ~(_,_,a) -> a ) (\ ~(c,d,_) b -> (c,d,b))
 instance Lens3 a b (c,d,a,e) (c,d,b,e) where
   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
   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
   t'l = prism ((id ||| Right) >>> swapE) (flip (left . const))
     where swapE :: (b:+:a) -> (a:+:b)
@@ -211,13 +224,13 @@
   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
+  each k = map Left . k <|> map Right . k
 i'list :: [a] :<->: (():+:(a:*:[a]))
 i'list = iso (\l -> case l of
                 [] -> Left ()
@@ -235,6 +248,9 @@
 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
   i'_ :: Iso s t a b
@@ -317,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
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,4 +1,4 @@
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableInstances, ScopedTypeVariables #-}
 module Algebra.Monad.Base (
   module Algebra.Classes,module Algebra.Applicative,module Algebra.Core,
   module Algebra.Traversable,module Algebra.Lens,
@@ -8,12 +8,13 @@
   (=<<),joinMap,(<=<),(>=>),(>>),(<*=),only,return,
   foldlM,foldrM,findM,while,until,
   bind2,bind3,(>>>=),(>>>>=),
-
+  mfix_,mfixing,
+  
   -- * Monadic Lenses
   Action,Action',
   
   -- * Instance utilities
-  Compose'(..),i'Compose'
+  Compose'(..),i'Compose',coerceJoin,coerceDuplicate
   ) where
 
 import Algebra.Classes
@@ -22,6 +23,7 @@
 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
@@ -32,10 +34,13 @@
 
 -- 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
@@ -45,10 +50,21 @@
   lift = Compose . pure
 instance Monad m => ConcreteMonad ((:.:) m) where
   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 MonadFuture m (Backwards m) where
+instance MonadFix m => MonadFuture m (Backwards m) where
   future = Backwards
 instance MonadFix m => MonadFix (Backwards m) where
   mfix f = by i'Backwards $ mfix (yb i'Backwards.f)
@@ -62,9 +78,10 @@
   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
@@ -125,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)
+                       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 i'Compose' . map pure
 instance Monad m => ConcreteMonad (Compose' m) where
   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 = i'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 = i'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,8 +22,9 @@
 
 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 = i'Compose'.iso ListT (\(ListT l) -> l)
 instance Monad m => MonadList (ListT m) where
@@ -42,15 +45,22 @@
                                    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 = 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 = 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)
@@ -91,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,17 +14,18 @@
 
 {-| 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)
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,16 +21,17 @@
   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)
@@ -59,20 +60,22 @@
 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)))
diff --git a/Algebra/Monad/Writer.hs b/Algebra/Monad/Writer.hs
--- a/Algebra/Monad/Writer.hs
+++ b/Algebra/Monad/Writer.hs
@@ -9,11 +9,11 @@
   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
@@ -35,10 +35,12 @@
 
 {-| 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_
@@ -59,12 +61,13 @@
 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
@@ -72,18 +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, MonadFuture n m) => MonadFuture n (WriterAccT w acc m)
+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 = i'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/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,for,transpose,doTimes,converted,folded,
+
+  -- * Instance utilities
+  coerceSeq
   ) where
 
 import Algebra.Classes
@@ -12,6 +16,7 @@
 import Algebra.Foldable
 import Algebra.Lens
 import Data.Tree
+import Unsafe.Coerce
 
 instance Traversable ((,) c) where
   sequence ~(c,m) = (,) c<$>m
@@ -20,9 +25,14 @@
 instance Traversable [] where
   sequence (x:xs) = (:)<$>x<*>sequence xs
   sequence [] = pure []
-deriving instance Traversable Interleave
-deriving instance Traversable OrdList
-deriving instance Traversable f => Traversable (Zip f)
+
+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)
 instance (Traversable f,Traversable g) => Traversable (f:.:g) where
@@ -35,6 +45,8 @@
 instance Traversable Maybe where
   sequence Nothing = pure Nothing
   sequence (Just a) = Just<$>a
+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,4 +63,4 @@
 transpose = sequence
 
 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
@@ -3,7 +3,7 @@
   -- * The basic data class
   DataMap(..),Indexed(..),OrderedMap(..),Container(..),
   
-  lookup,present,member,delete,touch,insert,singleton,singleton',fromList,fromList',(#),(#?),
+  lookup,resides,member,delete,touch,insert,singleton,singleton',fromAList,fromKList,(#),(#?),
   cached,
 
   -- * Map instances
@@ -14,7 +14,7 @@
   Bimap(..),toMap,keysSet,
 
   -- ** Relations
-  Relation(..),domains,ranges,related,link
+  Relation(..),i'Relation,i'domains,i'ranges,l'domain,l'range,link,(*>>>)
   )
   where
 
@@ -53,8 +53,8 @@
 
 lookup :: DataMap m k a => k -> m -> Maybe a
 lookup s m = m^.at s
-present :: DataMap m k a => k -> m -> Bool
-present = map2 nonempty lookup
+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
@@ -67,10 +67,10 @@
 singleton = map2 ($zero) insert
 singleton' :: (Monoid a,DataMap m k a) => k -> m
 singleton' x = touch x zero
-fromList :: DataMap m k a => [(k,a)] -> m
-fromList l = compose (uncurry insert<$>l) zero
-fromList' :: (Monoid a,DataMap m k a) => [k] -> m
-fromList' l = compose (touch<$>l) zero
+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))).i'maybe
@@ -95,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.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)
@@ -121,8 +126,8 @@
 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))
@@ -131,20 +136,20 @@
   Relation (x,x') + Relation (y,y') = Relation (M.unionWith (+) x y,M.unionWith (+) x' y')
 deriving instance (Ord a,Ord b) => Monoid (Relation a b)
 instance (Ord a,Ord b) => Semiring (Relation a b) where
-  Relation (x,x') * Relation (y,y') = Relation (M.intersectionWith (*) x y,M.intersectionWith (*) x' y')
-_Relation :: Iso (Relation a b) (Relation c d) (Map a (Set b),Map b (Set a)) (Map c (Set d),Map d (Set c))
-_Relation = iso Relation (\(Relation r) -> r)
+  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
@@ -158,11 +163,13 @@
 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
@@ -176,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,22 +1,26 @@
+{-# 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,sliceElt,span,break,
 
-  takeWhile,takeUntil,dropWhile,dropUntil,
+  takeWhile,takeUntil,dropWhile,dropUntil,pry,
 
   (++)
   ) where
 
 import Definitive.Base
-import qualified Data.List as L
+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
@@ -31,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
@@ -49,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]
@@ -71,6 +90,10 @@
 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
@@ -94,6 +117,21 @@
 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
@@ -3,9 +3,10 @@
 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
 
 i'ProbT :: Iso (ProbT t m a) (ProbT t' m' a') (WriterT (Product t) (ListT m) a) (WriterT (Product t') (ListT m') a')
@@ -16,11 +17,11 @@
 prob = i'Id.probT
 
 c'prob :: Constraint t -> Constraint (Prob t a)
-c'prob _ = id
+c'prob _ = c'_
 
-instance (Monad m,Ring t,Fractional t) => MonadList (ProbT t m) where
+instance (Monad m,Invertible t) => MonadList (ProbT t m) where
   fork l = pure [(x,a) | a <- l]^.probT
-    where x = 1/size l
+    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/TimeVal.hs b/Data/TimeVal.hs
new file mode 100644
--- /dev/null
+++ b/Data/TimeVal.hs
@@ -0,0 +1,75 @@
+module Data.TimeVal (
+  TimeVal(..)
+  ) where
+
+import Definitive
+
+-- |A type wrapper that adds a Bounded instance for types that don't possess one.
+data TimeVal t = Always | Since t | Never
+                 deriving (Show,Eq,Ord)
+instance Functor TimeVal where
+  map f (Since a) = Since (f a)
+  map _ Always = Always
+  map _ Never = Never
+instance Unit TimeVal where pure = Since
+instance Applicative TimeVal
+instance Monad TimeVal where
+  join (Since b) = b
+  join Always = Always
+  join Never = Never
+instance Foldable TimeVal where
+  fold (Since t) = t
+  fold _ = zero
+instance Traversable TimeVal where
+  sequence (Since t) = Since<$>t
+  sequence Always = pure Always
+  sequence Never = pure Never
+
+instance Bounded (TimeVal t) where
+  minBound = Always ; maxBound = Never
+
+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-base.cabal b/definitive-base.cabal
--- a/definitive-base.cabal
+++ b/definitive-base.cabal
@@ -2,59 +2,63 @@
 name:          definitive-base
 category:      Prelude
 synopsis:      The base modules of the Definitive framework.
-description:   The Definitive framework is an attempt at harnessing the declarative
-               nature of Haskell to provide a solid and simple base for writing 
-               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,
-               lenses can greatly improve clarity in both code and thought, so I
-               tried to provide for them in the most ubiquitous way possible,
-               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 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).
+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,
+  lenses can greatly improve clarity in both code and thought, so I
+  tried to provide for them in the most ubiquitous way possible,
+  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 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).
 
 -- meta-information
 author:        Marc Coiffier
 maintainer:    marc.coiffier@gmail.com
-version:       1.2.1
+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: Definitive Definitive.Base Algebra.Arrow Algebra.Core Algebra.Classes Algebra.Monad Algebra.Monad.Base Algebra.Applicative Algebra.Functor Algebra.Traversable Algebra.Foldable Algebra.Lens Algebra.Monad.RWS Algebra.Monad.State Algebra.Monad.Reader Algebra.Monad.Writer Algebra.Monad.Cont Algebra.Monad.Foldable Algebra.Monad.Error Data.Containers Data.Containers.Sequence Data.Probability
-  build-depends: base (== 4.6.*), containers (== 0.5.*), deepseq (== 1.3.*), array (== 0.5.*), bytestring (== 0.10.*), vector (== 0.10.*), primitive (== 0.5.*)
-  default-extensions: TypeSynonymInstances NoMonomorphismRestriction StandaloneDeriving GeneralizedNewtypeDeriving TypeOperators RebindableSyntax FlexibleInstances FlexibleContexts FunctionalDependencies TupleSections MultiParamTypeClasses Rank2Types
-  ghc-options: -Wall -fno-warn-orphans -threaded
+  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: