diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright 2008-2011 Edward Kmett
+Copyright 2008-2012 Edward Kmett
 
 All rights reserved.
 
diff --git a/free.cabal b/free.cabal
--- a/free.cabal
+++ b/free.cabal
@@ -1,6 +1,6 @@
 name:          free
 category:      Control, Monads
-version:       3.0
+version:       3.1
 license:       BSD3
 cabal-version: >= 1.6
 license-file:  LICENSE
@@ -9,9 +9,22 @@
 stability:     provisional
 homepage:      http://github.com/ekmett/free/
 bug-reports:   http://github.com/ekmett/free/issues
-copyright:     Copyright (C) 2008-2011 Edward A. Kmett
+copyright:     Copyright (C) 2008-2012 Edward A. Kmett
 synopsis:      Monads for free
-description:   Monads for free
+description:
+  Free monads are useful for many tree-like structures and domain specific languages.
+  .
+  A 'Monad' @n@ is a free 'Monad' for @f@ if every 'Monad' homomorphism
+  from @n@ to another monad @m@ is equivalent to a natural transformation
+  from @f@ to @m@.
+  .
+  Cofree comonads provide convenient ways to talk about branching streams and rose-trees,
+  and can be used to annotate syntax trees.
+  .
+  A 'Comonad' @v@ is a cofree 'Comonad' for @f@ if every 'Comonad' homomorphism
+  another comonad @w@ to @v@ is equivalent to a natural transformation
+  from @w@ to @f@.
+
 build-type:    Simple
 extra-source-files: .travis.yml
 
@@ -30,13 +43,14 @@
 
   build-depends:
     base                 >= 4       && < 5,
+    bifunctors           == 3.0.*,
     distributive         >= 0.2.1   && < 0.3,
     transformers         >= 0.2.0   && < 0.4,
     mtl                  >= 2.0.1.0 && < 2.2,
-    semigroupoids        >= 3.0     && < 3.1,
-    comonad              >= 3.0     && < 3.1,
-    comonad-transformers >= 3.0     && < 3.1,
-    comonads-fd          >= 3.0     && < 3.1,
+    semigroupoids        == 3.0.*,
+    comonad              == 3.0.*,
+    comonad-transformers == 3.0.*,
+    comonads-fd          == 3.0.*,
     semigroups           >= 0.8.3.1 && < 0.9
 
   if impl(ghc)
@@ -47,7 +61,9 @@
   exposed-modules:
     Control.Monad.Free
     Control.Monad.Free.Class
+    Control.Monad.Trans.Free
     Control.Comonad.Cofree
     Control.Comonad.Cofree.Class
+    Control.Comonad.Trans.Cofree
 
   ghc-options:      -Wall
diff --git a/src/Control/Comonad/Cofree.hs b/src/Control/Comonad/Cofree.hs
--- a/src/Control/Comonad/Cofree.hs
+++ b/src/Control/Comonad/Cofree.hs
@@ -6,7 +6,7 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Control.Comonad.Cofree
--- Copyright   :  (C) 2008-2011 Edward Kmett,
+-- Copyright   :  (C) 2008-2012 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
@@ -18,14 +18,14 @@
 ----------------------------------------------------------------------------
 module Control.Comonad.Cofree
   ( Cofree(..)
+  , ComonadCofree(..)
   , section
-  , unwrap
   , coiter
   , unfold
   -- * Lenses into cofree comonads
-  , extracting
-  , unwrapping
-  , telescoping
+  , extracted
+  , unwrapped
+  , telescoped
   ) where
 
 import Control.Applicative
@@ -52,11 +52,45 @@
 
 infixr 5 :<
 
+-- | The 'Cofree' 'Comonad' of a functor @f@.
+--
+-- /Formally/
+--
+-- A 'Comonad' @v@ is a cofree 'Comonad' for @f@ if every comonad homomorphism
+-- another comonad @w@ to @v@ is equivalent to a natural transformation
+-- from @w@ to @f@.
+--
+-- A 'cofree' functor is right adjoint to a forgetful functor.
+--
+-- Cofree is a functor from the category of functors to the category of comonads
+-- that is right adjoint to the forgetful functor from the category of comonads
+-- to the category of functors that forgets how to 'extract' and
+-- 'duplicate', leaving you with only a 'Functor'.
+--
+-- In practice, cofree comonads are quite useful for annotating syntax trees,
+-- or talking about streams.
+--
+-- A number of common comonads arise directly as cofree comonads.
+--
+-- For instance,
+--
+-- * @'Cofree' 'Maybe'@ forms the a comonad for a non-empty list.
+--
+-- * @'Cofree' ('Const' b)@ is a product.
+--
+-- * @'Cofree' 'Identity'@ forms an infinite stream.
+--
+-- * @'Cofree' ((->) b)'@ describes a Moore machine with states labeled with values of type a, and transitions on edges of type b.
+--
 data Cofree f a = a :< f (Cofree f a)
 
+-- | Use coiteration to generate a cofree comonad from a seed.
+--
+-- @'coiter' f = 'unfold' ('id' 'Control.Arrow.&&&' f)@
 coiter :: Functor f => (a -> f a) -> a -> Cofree f a
 coiter psi a = a :< (coiter psi <$> psi a)
 
+-- | Unfold a cofree comonad from a seed.
 unfold :: Functor f => (b -> (a, f b)) -> b -> Cofree f a
 unfold f c = case f c of
   (x, d) -> x :< fmap (unfold f) d
@@ -80,10 +114,13 @@
   duplicate w = w :< fmap duplicate (unwrap w)
   extract (a :< _) = a
 
+-- | This is not a true 'Comonad' transformer, but this instance is convenient.
 instance ComonadTrans Cofree where
   lower (_ :< as) = fmap extract as
 
--- | lower . section = id
+-- |
+--
+-- @'lower' . 'section' = 'id'@
 section :: Comonad f => f a -> Cofree f a
 section as = extract as :< extend section as
 
@@ -182,20 +219,38 @@
   pos (_ :< as) = Class.pos as
   peek s (_ :< as) = extract (Class.peek s as)
 
-
 instance ComonadTraced m w => ComonadTraced m (Cofree w) where
   trace m = trace m . lower
 
-extracting :: Functor f => (a -> f a) -> Cofree g a -> f (Cofree g a)
-extracting f (a :< as) = (:< as) <$> f a
-{-# INLINE extracting #-}
+-- | This is a lens that can be used to read or write from the target of 'extract'.
+--
+-- @foo ^. 'extracted' == 'extract' foo@
+--
+-- For more on lenses see the 'lens' package on hackage
+--
+-- @extracted :: Simple Lens (Cofree g a) a@
+extracted :: Functor f => (a -> f a) -> Cofree g a -> f (Cofree g a)
+extracted f (a :< as) = (:< as) <$> f a
+{-# INLINE extracted #-}
 
-unwrapping :: Functor f => (g (Cofree g a) -> f (g (Cofree g a))) -> Cofree g a -> f (Cofree g a)
-unwrapping f (a :< as) = (a :<) <$> f as
-{-# INLINE unwrapping #-}
+-- | This is a lens that can be used to read or write to the tails of a 'Cofree' 'Comonad'.
+--
+-- @foo ^. 'unwrapped' == 'unwrap' foo@
+--
+-- For more on lenses see the 'lens' package on hackage
+--
+-- @unwrapped :: Simple Lens (Cofree g a) (g (Cofree g a))@
+unwrapped :: Functor f => (g (Cofree g a) -> f (g (Cofree g a))) -> Cofree g a -> f (Cofree g a)
+unwrapped  f (a :< as) = (a :<) <$> f as
+{-# INLINE unwrapped #-}
 
-telescoping :: (Functor f, Functor g) =>
+-- | Construct a @Lens@ into a @'Cofree' f@ given a list of lenses into the base functor.
+--
+-- For more on lenses see the 'lens' package on hackage.
+--
+-- @telescoped :: Functor g => [Rep g] -> Simple Lens (Cofree g a) a@
+telescoped :: (Functor f, Functor g) =>
              [(Cofree g a -> f (Cofree g a)) -> g (Cofree g a) -> f (g (Cofree g a))] ->
               (a -> f a) -> Cofree g a -> f (Cofree g a)
-telescoping [] = extracting
-telescoping (l:ls) = unwrapping . l . telescoping ls
+telescoped [] = extracted
+telescoped (l:ls) = unwrapped . l . telescoped ls
diff --git a/src/Control/Comonad/Cofree/Class.hs b/src/Control/Comonad/Cofree/Class.hs
--- a/src/Control/Comonad/Cofree/Class.hs
+++ b/src/Control/Comonad/Cofree/Class.hs
@@ -24,7 +24,9 @@
 import Control.Comonad.Trans.Identity
 import Data.Semigroup
 
+-- | Allows you to peel a layer off a cofree comonad.
 class (Functor f, Comonad w) => ComonadCofree f w | w -> f where
+  -- | Remove a layer.
   unwrap :: w a -> f (w a)
 
 instance ComonadCofree f w => ComonadCofree f (IdentityT w) where
diff --git a/src/Control/Comonad/Trans/Cofree.hs b/src/Control/Comonad/Trans/Cofree.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Comonad/Trans/Cofree.hs
@@ -0,0 +1,175 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Comonad.Trans.Cofree
+-- Copyright   :  (C) 2008-2012 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  MPTCs, fundeps
+--
+-- The cofree comonad transformer
+----------------------------------------------------------------------------
+module Control.Comonad.Trans.Cofree
+  ( CofreeT(..)
+  , CofreeF(..)
+  , ComonadCofree(..)
+  , headF
+  , tailF
+  ) where
+
+import Control.Applicative
+import Control.Comonad
+import Control.Comonad.Trans.Class
+import Control.Comonad.Cofree.Class
+import Control.Category
+import Data.Bifunctor
+import Data.Bifoldable
+import Data.Bitraversable
+import Data.Foldable
+import Data.Semigroup
+import Data.Traversable
+import Prelude hiding (id,(.))
+
+#ifdef GHC_TYPEABLE
+import Data.Data
+#endif
+
+infixr 5 :<
+
+-- | This is the base functor of the cofree comonad transformer.
+data CofreeF f a b = a :< f b
+  deriving (Eq,Ord,Show,Read)
+
+-- | Extract the head of the base functor
+headF :: CofreeF f a b -> a
+headF (a :< _) = a
+
+-- | Extract the tails of the base functor
+tailF :: CofreeF f a b -> f b
+tailF (_ :< as) = as
+
+instance Functor f => Functor (CofreeF f a) where
+  fmap f (a :< as)  = a :< fmap f as
+
+instance Foldable f => Foldable (CofreeF f a) where
+  foldMap f (_ :< as) = foldMap f as
+
+instance Traversable f => Traversable (CofreeF f a) where
+  traverse f (a :< as) = (a :<) <$> traverse f as
+
+instance Functor f => Bifunctor (CofreeF f) where
+  bimap f g (a :< as)  = f a :< fmap g as
+
+instance Foldable f => Bifoldable (CofreeF f) where
+  bifoldMap f g (a :< as)  = f a `mappend` foldMap g as
+
+instance Traversable f => Bitraversable (CofreeF f) where
+  bitraverse f g (a :< as) = (:<) <$> f a <*> traverse g as
+
+-- | This is a cofree comonad of some functor @f@, with a comonad @w@ threaded through it at each level.
+newtype CofreeT f w a = CofreeT { runCofreeT :: w (CofreeF f a (CofreeT f w a)) }
+
+instance (Functor f, Functor w) => Functor (CofreeT f w) where
+  fmap f = CofreeT . fmap (bimap f (fmap f)) . runCofreeT
+
+instance (Functor f, Comonad w) => Comonad (CofreeT f w) where
+  extract = headF . extract . runCofreeT
+  extend f = CofreeT . extend (\w -> f (CofreeT w) :< (extend f <$> tailF (extract w))) . runCofreeT
+
+instance (Foldable f, Foldable w) => Foldable (CofreeT f w) where
+  foldMap f = foldMap (bifoldMap f (foldMap f)) . runCofreeT
+
+instance (Traversable f, Traversable w) => Traversable (CofreeT f w) where
+  traverse f = fmap CofreeT . traverse (bitraverse f (traverse f)) . runCofreeT
+
+instance Functor f => ComonadTrans (CofreeT f) where
+  lower = fmap headF . runCofreeT
+
+instance (Functor f, Comonad w) => ComonadCofree f (CofreeT f w) where
+  unwrap = tailF . extract . runCofreeT
+
+instance Show (w (CofreeF f a (CofreeT f w a))) => Show (CofreeT f w a) where
+  showsPrec d w = showParen (d > 10) $
+    showString "CofreeT " . showsPrec 11 w
+
+instance Read (w (CofreeF f a (CofreeT f w a))) => Read (CofreeT f w a) where
+  readsPrec d = readParen (d > 10) $ \r ->
+     [(CofreeT w, t) | ("CofreeT", s) <- lex r, (w, t) <- readsPrec 11 s]
+
+instance Eq (w (CofreeF f a (CofreeT f w a))) => Eq (CofreeT f w a) where
+  CofreeT a == CofreeT b = a == b
+
+instance Ord (w (CofreeF f a (CofreeT f w a))) => Ord (CofreeT f w a) where
+  compare (CofreeT a) (CofreeT b) = compare a b
+
+#ifdef GHC_TYPEABLE
+
+instance Typeable1 f => Typeable2 (CofreeF f) where
+  typeOf2 t = mkTyConApp cofreeFTyCon [typeOf1 (f t)] where
+    f :: CofreeF f a b -> f a
+    f = undefined
+
+instance (Typeable1 f, Typeable1 w) => Typeable1 (CofreeT f w) where
+  typeOf1 t = mkTyConApp cofreeTTyCon [typeOf1 (f t), typeOf1 (w t)] where
+    f :: CofreeT f w a -> f a
+    f = undefined
+    w :: CofreeT f w a -> w a
+    w = undefined
+
+cofreeFTyCon, cofreeTTyCon :: TyCon
+#if __GLASGOW_HASKELL__ < 704
+cofreeTTyCon = mkTyCon "Control.Comonad.Trans.Cofree.CofreeT"
+cofreeFTyCon = mkTyCon "Control.Comonad.Trans.Cofree.CofreeF"
+#else
+cofreeTTyCon = mkTyCon3 "free" "Control.Comonad.Trans.Cofree" "CofreeT"
+cofreeFTyCon = mkTyCon3 "free" "Control.Comonad.Trans.Cofree" "CofreeF"
+#endif
+{-# NOINLINE cofreeTTyCon #-}
+{-# NOINLINE cofreeFTyCon #-}
+
+instance
+  ( Typeable1 f, Typeable a, Typeable b
+  , Data a, Data (f b), Data b
+  ) => Data (CofreeF f a b) where
+    gfoldl f z (a :< as) = z (:<) `f` a `f` as
+    toConstr _ = cofreeFConstr
+    gunfold k z c = case constrIndex c of
+        1 -> k (k (z (:<)))
+        _ -> error "gunfold"
+    dataTypeOf _ = cofreeFDataType
+    dataCast1 f = gcast1 f
+
+instance
+  ( Typeable1 f, Typeable1 w, Typeable a
+  , Data (w (CofreeF f a (CofreeT f w a)))
+  , Data a
+  ) => Data (CofreeT f w a) where
+    gfoldl f z (CofreeT w) = z CofreeT `f` w
+    toConstr _ = cofreeTConstr
+    gunfold k z c = case constrIndex c of
+        1 -> k (z CofreeT)
+        _ -> error "gunfold"
+    dataTypeOf _ = cofreeTDataType
+    dataCast1 f = gcast1 f
+
+cofreeFConstr, cofreeTConstr :: Constr
+cofreeFConstr = mkConstr cofreeFDataType ":<" [] Infix
+cofreeTConstr = mkConstr cofreeTDataType "CofreeT" [] Prefix
+{-# NOINLINE cofreeFConstr #-}
+{-# NOINLINE cofreeTConstr #-}
+
+cofreeFDataType, cofreeTDataType :: DataType
+cofreeFDataType = mkDataType "Control.Comonad.Trans.Cofree.CofreeF" [cofreeFConstr]
+cofreeTDataType = mkDataType "Control.Comonad.Trans.Cofree.CofreeT" [cofreeTConstr]
+{-# NOINLINE cofreeFDataType #-}
+{-# NOINLINE cofreeTDataType #-}
+#endif
+
+-- lowerF :: (Functor f, Comonad w) => CofreeT f w a -> f a
+-- lowerF = fmap extract . unwrap
diff --git a/src/Control/Monad/Free.hs b/src/Control/Monad/Free.hs
--- a/src/Control/Monad/Free.hs
+++ b/src/Control/Monad/Free.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -5,14 +6,14 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Control.Monad.Free
--- Copyright   :  (C) 2008-2011 Edward Kmett
+-- Copyright   :  (C) 2008-2012 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
 -- Stability   :  provisional
 -- Portability :  MPTCs, fundeps
 --
--- Free monads
+-- Monads for free
 --
 ----------------------------------------------------------------------------
 module Control.Monad.Free
@@ -38,6 +39,54 @@
 import Data.Semigroup.Foldable
 import Data.Semigroup.Traversable
 
+#ifdef GHC_TYPEABLE
+import Data.Data
+#endif
+
+-- | The 'Free' 'Monad' for a 'Functor' @f@.
+--
+-- /Formally/
+--
+-- A 'Monad' @n@ is a free 'Monad' for @f@ if every monad homomorphism
+-- from @n@ to another monad @m@ is equivalent to a natural transformation
+-- from @f@ to @m@.
+--
+-- /Why Free?/
+--
+-- Every \"free\" functor is left adjoint to some \"forgetful\" functor.
+--
+-- If we define a forgetful functor @U@ from the category of monads to the category of functors
+-- that just forgets the 'Monad', leaving only the 'Functor'. i.e.
+--
+-- @U (M,'return','Control.Monad.join') = M@
+--
+-- then 'Free' is the left adjoint to @U@.
+--
+-- Being 'Free' being left adjoint to @U@ means that there is an isomorphism between
+--
+-- @'Free' f -> m@ in the category of monads and @f -> U m@ in the category of functors.
+--
+-- Morphisms in the category of monads are 'Monad' homomorphisms (natural transformations that respect 'return' and 'Control.Monad.join').
+--
+-- Morphisms in the category of functors are 'Functor' homomorphisms (natural transformations).
+--
+-- Given this isomorphism, every monad homomorphism from @'Free' f@ to @m@ is equivalent to a natural transformation from @f@ to @m@
+--
+-- Showing that this isomorphism holds is left as an exercise.
+--
+-- In practice, you can just view a @'Free' f a@ as many layers of @f@ wrapped around values of type @a@, where
+-- @('>>=')@ performs substitution and grafts new layers of @f@ in for each of the free variables.
+--
+-- This can be very useful for modeling domain specific languages, trees, or other constructs.
+--
+-- This instance of 'MonadFree' is fairly naive about the encoding. For more efficient free monad implementations that require additional
+-- extensions and thus aren't included here, you may want to look at the @kan-extensions@ package.
+--
+-- A number of common monads arise as free monads,
+--
+-- * Given @data Empty a@, @'Free' Empty@ is isomorphic to the 'Data.Functor.Identity' monad.
+--
+-- * @'Free' 'Maybe'@ can be used to model a partiality monad where each layer represents running the computation for a while longer.
 data Free f a = Pure a | Free (f (Free f a))
 
 instance (Eq (f (Free f a)), Eq a) => Eq (Free f a) where
@@ -91,14 +140,17 @@
   Pure a >>= f = f a
   Free m >>= f = Free ((>>= f) <$> m)
 
+-- | This violates the Alternative laws, handle with care.
 instance Alternative v => Alternative (Free v) where
   empty = Free empty
   a <|> b = Free (pure a <|> pure b)
 
+-- | This violates the MonadPlus laws, handle with care.
 instance (Functor v, MonadPlus v) => MonadPlus (Free v) where
   mzero = Free mzero
   a `mplus` b = Free (return a `mplus` return b)
 
+-- | This is not a true monad transformer. It is only a monad transformer \"up to 'retract'\".
 instance MonadTrans Free where
   lift = Free . liftM Pure
 
@@ -138,6 +190,7 @@
 instance (Functor m, MonadCont m) => MonadCont (Free m) where
   callCC f = lift (callCC (retract . f . liftM lift))
 
+-- | A version of 'lift' that can be used with just a 'Functor' for @f@.
 liftF :: Functor f => f a -> Free f a
 liftF = Free . fmap Pure
 
@@ -145,13 +198,58 @@
   wrap = Free
 
 -- |
+-- 'retract' is the left inverse of 'lift' and 'liftF'
 --
--- > retract . lift = id
--- > retract . liftF = id
+-- @
+-- 'retract' . 'lift' = 'id'
+-- 'retract' . 'liftF' = 'id'
+-- @
 retract :: Monad f => Free f a -> f a
 retract (Pure a) = return a
 retract (Free as) = as >>= retract
 
+-- | Tear down a 'Free' 'Monad' using iteration.
 iter :: Functor f => (f a -> a) -> Free f a -> a
 iter _ (Pure a) = a
 iter phi (Free m) = phi (iter phi <$> m)
+
+#ifdef GHC_TYPEABLE
+instance Typeable1 f => Typeable1 (Free f) where
+  typeOf1 t = mkTyConApp freeTyCon [typeOf1 (f t)] where
+    f :: Free f a -> f a
+    f = undefined
+
+freeTyCon :: TyCon
+#if __GLASGOW_HASKELL__ < 704
+freeTyCon = mkTyCon "Control.Monad.Free.Free"
+#else
+freeTyCon = mkTyCon3 "free" "Control.Monad.Free" "Free"
+#endif
+{-# NOINLINE freeTyCon #-}
+
+instance
+  ( Typeable1 f, Typeable a
+  , Data a, Data (f (Free f a))
+  ) => Data (Free f a) where
+    gfoldl f z (Pure a) = z Pure `f` a
+    gfoldl f z (Free as) = z Free `f` as
+    toConstr Pure{} = pureConstr
+    toConstr Free{} = freeConstr
+    gunfold k z c = case constrIndex c of
+        1 -> k (z Pure)
+        2 -> k (z Free)
+        _ -> error "gunfold"
+    dataTypeOf _ = freeDataType
+    dataCast1 f = gcast1 f
+
+pureConstr, freeConstr :: Constr
+pureConstr = mkConstr freeDataType "Pure" [] Prefix
+freeConstr = mkConstr freeDataType "Free" [] Prefix
+{-# NOINLINE pureConstr #-}
+{-# NOINLINE freeConstr #-}
+
+freeDataType :: DataType
+freeDataType = mkDataType "Control.Monad.Free.FreeF" [pureConstr, freeConstr]
+{-# NOINLINE freeDataType #-}
+
+#endif
diff --git a/src/Control/Monad/Free/Class.hs b/src/Control/Monad/Free/Class.hs
--- a/src/Control/Monad/Free/Class.hs
+++ b/src/Control/Monad/Free/Class.hs
@@ -11,6 +11,8 @@
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
 -- Stability   :  experimental
 -- Portability :  non-portable (fundeps, MPTCs)
+--
+-- Monads for free.
 ----------------------------------------------------------------------------
 module Control.Monad.Free.Class
   ( MonadFree(..)
@@ -30,7 +32,52 @@
 import Control.Monad.Trans.Identity
 import Data.Monoid
 
+-- |
+-- Monads provide substitution ('fmap') and renormalization ('Control.Monad.join'):
+--
+-- @m '>>=' f = 'Control.Monad.join' . 'fmap' f m@
+--
+-- A free 'Monad' is one that does no work during the normalization step beyond simply grafting the two monadic values together.
+--
+-- @[]@ is not a free 'Monad' (in this sense) because @'Control.Monad.join' [[a]]@ smashes the lists flat.
+--
+-- On the other hand, consider:
+--
+-- @
+-- data Tree a = Bin (Tree a) (Tree a) | Tip a
+-- @
+--
+-- @
+-- instance 'Monad' Tree where
+--   'return' = Tip
+--   Tip a '>>=' f = f a
+--   Bin l r '>>=' f = Bin (l '>>=' f) (r '>>=' f)
+-- @
+--
+-- This 'Monad' is the free 'Monad' of Pair:
+--
+-- @
+-- data Pair a = Pair a a
+-- @
+--
+-- And we could make an instance of 'MonadFree' for it directly:
+--
+-- @
+-- instance 'MonadFree' Pair Tree where
+--    'wrap' (Pair l r) = Bin l r
+-- @
+--
+-- Or we could choose to program with @'Control.Monad.Free.Free' Pair@ instead of 'Tree'
+-- and thereby avoid having to define our own 'Monad' instance.
+--
+-- Moreover, the @kan-extensions@ package provides 'MonadFree' instances that can
+-- improve the /asymptotic/ complexity of code that constructors free monads by
+-- effectively reassociating the use of ('>>=').
+--
+-- See 'Control.Monad.Free.Free' for a more formal definition of the free 'Monad'
+-- for a 'Functor'.
 class Monad m => MonadFree f m | m -> f where
+  -- | Add a layer.
   wrap :: f (m a) -> m a
 
 instance (Functor f, MonadFree f m) => MonadFree f (ReaderT e m) where
diff --git a/src/Control/Monad/Trans/Free.hs b/src/Control/Monad/Trans/Free.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Trans/Free.hs
@@ -0,0 +1,196 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Monad.Trans.Free
+-- Copyright   :  (C) 2008-2012 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  MPTCs, fundeps
+--
+-- The free monad transformer
+--
+----------------------------------------------------------------------------
+module Control.Monad.Trans.Free
+  ( FreeT(..)
+  , MonadFree(..)
+  , liftF
+  ) where
+
+import Control.Applicative
+import Control.Monad (liftM, MonadPlus(..), ap)
+import Control.Monad.Trans.Class
+import Control.Monad.Free.Class
+import Control.Monad.IO.Class
+import Data.Monoid
+import Data.Foldable
+import Data.Traversable
+import Data.Bifunctor
+import Data.Bifoldable
+import Data.Bitraversable
+#ifdef GHC_TYPEABLE
+import Data.Data
+#endif
+
+-- | The base functor for a free monad.
+data FreeF f a b = Pure a | Free (f b)
+  deriving (Eq,Ord,Show,Read)
+
+instance Functor f => Functor (FreeF f a) where
+  fmap _ (Pure a)  = Pure a
+  fmap f (Free as) = Free (fmap f as)
+
+instance Foldable f => Foldable (FreeF f a) where
+  foldMap f (Free as) = foldMap f as
+  foldMap _ _         = mempty
+
+instance Traversable f => Traversable (FreeF f a) where
+  traverse _ (Pure a)  = pure (Pure a)
+  traverse f (Free as) = Free <$> traverse f as
+
+instance Functor f => Bifunctor (FreeF f) where
+  bimap f _ (Pure a)  = Pure (f a)
+  bimap _ g (Free as) = Free (fmap g as)
+
+instance Foldable f => Bifoldable (FreeF f) where
+  bifoldMap f _ (Pure a)  = f a
+  bifoldMap _ g (Free as) = foldMap g as
+
+instance Traversable f => Bitraversable (FreeF f) where
+  bitraverse f _ (Pure a)  = Pure <$> f a
+  bitraverse _ g (Free as) = Free <$> traverse g as
+
+-- | The \"free monad transformer\" for a functor @f@.
+newtype FreeT f m a = FreeT { runFreeT :: m (FreeF f a (FreeT f m a)) }
+
+instance Eq (m (FreeF f a (FreeT f m a))) => Eq (FreeT f m a) where
+  FreeT m == FreeT n = m == n
+
+instance Ord (m (FreeF f a (FreeT f m a))) => Ord (FreeT f m a) where
+  compare (FreeT m) (FreeT n) = compare m n
+
+instance Show (m (FreeF f a (FreeT f m a))) => Show (FreeT f m a) where
+  showsPrec d (FreeT m) = showParen (d > 10) $
+    showString "FreeT " . showsPrec 11 m
+
+instance Read (m (FreeF f a (FreeT f m a))) => Read (FreeT f m a) where
+  readsPrec d =  readParen (d > 10) $ \r ->
+    [ (FreeT m,t) | ("FreeT",s) <- lex r, (m,t) <- readsPrec 11 s]
+
+instance (Functor f, Monad m) => Functor (FreeT f m) where
+  fmap f (FreeT m) = FreeT (liftM f' m) where
+    f' (Pure a)  = Pure (f a)
+    f' (Free as) = Free (fmap (fmap f) as)
+
+instance (Functor f, Monad m) => Applicative (FreeT f m) where
+  pure a = FreeT (return (Pure a))
+  (<*>) = ap
+
+instance (Functor f, Monad m) => Monad (FreeT f m) where
+  return a = FreeT (return (Pure a))
+  FreeT m >>= f = FreeT $ m >>= \v -> case v of
+    Pure a -> runFreeT (f a)
+    Free w -> return (Free (fmap (>>= f) w))
+
+instance MonadTrans (FreeT f) where
+  lift = FreeT . liftM Pure
+
+instance (Functor f, MonadIO m) => MonadIO (FreeT f m) where
+  liftIO = lift . liftIO
+
+instance (Functor f, MonadPlus m) => Alternative (FreeT f m) where
+  empty = FreeT mzero
+  FreeT ma <|> FreeT mb = FreeT (mplus ma mb)
+
+instance (Functor f, MonadPlus m) => MonadPlus (FreeT f m) where
+  mzero = FreeT mzero
+  mplus (FreeT ma) (FreeT mb) = FreeT (mplus ma mb)
+
+instance (Functor f, Monad m) => MonadFree f (FreeT f m) where
+  wrap = FreeT . return . Free
+
+-- | FreeT is a functor from the category of functors to the category of monads.
+--
+-- This provides the mapping.
+liftF :: (Functor f, Monad m) => f a -> FreeT f m a
+liftF = wrap . fmap return
+
+instance (Foldable m, Foldable f) => Foldable (FreeT f m) where
+  foldMap f (FreeT m) = foldMap (bifoldMap f (foldMap f)) m
+
+instance (Monad m, Traversable m, Traversable f) => Traversable (FreeT f m) where
+  traverse f (FreeT m) = FreeT <$> traverse (bitraverse f (traverse f)) m
+
+#ifdef GHC_TYPEABLE
+
+instance Typeable1 f => Typeable2 (FreeF f) where
+  typeOf2 t = mkTyConApp freeFTyCon [typeOf1 (f t)] where
+    f :: FreeF f a b -> f a
+    f = undefined
+
+instance (Typeable1 f, Typeable1 w) => Typeable1 (FreeT f w) where
+  typeOf1 t = mkTyConApp freeTTyCon [typeOf1 (f t), typeOf1 (w t)] where
+    f :: FreeT f w a -> f a
+    f = undefined
+    w :: FreeT f w a -> w a
+    w = undefined
+
+freeFTyCon, freeTTyCon :: TyCon
+#if __GLASGOW_HASKELL__ < 704
+freeTTyCon = mkTyCon "Control.Monad.Trans.Free.FreeT"
+freeFTyCon = mkTyCon "Control.Monad.Trans.Free.FreeF"
+#else
+freeTTyCon = mkTyCon3 "free" "Control.Monad.Trans.Free" "FreeT"
+freeFTyCon = mkTyCon3 "free" "Control.Monad.Trans.Free" "FreeF"
+#endif
+{-# NOINLINE freeTTyCon #-}
+{-# NOINLINE freeFTyCon #-}
+
+instance
+  ( Typeable1 f, Typeable a, Typeable b
+  , Data a, Data (f b), Data b
+  ) => Data (FreeF f a b) where
+    gfoldl f z (Pure a) = z Pure `f` a
+    gfoldl f z (Free as) = z Free `f` as
+    toConstr Pure{} = pureConstr
+    toConstr Free{} = freeConstr
+    gunfold k z c = case constrIndex c of
+        1 -> k (z Pure)
+        2 -> k (z Free)
+        _ -> error "gunfold"
+    dataTypeOf _ = freeFDataType
+    dataCast1 f = gcast1 f
+
+instance
+  ( Typeable1 f, Typeable1 w, Typeable a
+  , Data (w (FreeF f a (FreeT f w a)))
+  , Data a
+  ) => Data (FreeT f w a) where
+    gfoldl f z (FreeT w) = z FreeT `f` w
+    toConstr _ = freeTConstr
+    gunfold k z c = case constrIndex c of
+        1 -> k (z FreeT)
+        _ -> error "gunfold"
+    dataTypeOf _ = freeTDataType
+    dataCast1 f = gcast1 f
+
+pureConstr, freeConstr, freeTConstr :: Constr
+pureConstr = mkConstr freeFDataType "Pure" [] Prefix
+freeConstr = mkConstr freeFDataType "Free" [] Prefix
+freeTConstr = mkConstr freeTDataType "FreeT" [] Prefix
+{-# NOINLINE pureConstr #-}
+{-# NOINLINE freeConstr #-}
+{-# NOINLINE freeTConstr #-}
+
+freeFDataType, freeTDataType :: DataType
+freeFDataType = mkDataType "Control.Monad.Trans.Free.FreeF" [pureConstr, freeConstr]
+freeTDataType = mkDataType "Control.Monad.Trans.Free.FreeT" [freeTConstr]
+{-# NOINLINE freeFDataType #-}
+{-# NOINLINE freeTDataType #-}
+#endif
+