diff --git a/Control/Invertible/BiArrow.hs b/Control/Invertible/BiArrow.hs
--- a/Control/Invertible/BiArrow.hs
+++ b/Control/Invertible/BiArrow.hs
@@ -14,6 +14,7 @@
   , (>>^^)
   , (<<^^)
   , (^^<<)
+  , BiKleisli
   ) where
 
 import Prelude hiding ((.))
@@ -106,6 +107,9 @@
   invert (f :<->: g) = g :<->: f
 
 instance SemigroupoidArrowA => BiArrow' (Bijection a)
+
+-- |Bidirectional 'Control.Arrow.Kleisli' monad arrow transformer.
+type BiKleisli m = Bijection (Kleisli m)
 
 #ifdef VERSION_semigroupoids
 instance (Semigroupoid a, Arrow a) => BiArrow (Semigroupoid.Iso a) where
diff --git a/Control/Invertible/Functor.hs b/Control/Invertible/Functor.hs
--- a/Control/Invertible/Functor.hs
+++ b/Control/Invertible/Functor.hs
@@ -8,9 +8,11 @@
 {-# LANGUAGE CPP, Safe, TypeOperators, FlexibleInstances #-}
 module Control.Invertible.Functor
   ( Functor(..)
+  , fmapDefault
   , (<$>)
   ) where
 
+import qualified Prelude
 import Prelude hiding ((.), Functor(..), (<$>))
 import Control.Arrow (Arrow)
 import Control.Category ((.))
@@ -26,6 +28,10 @@
 -- |An invariant version of 'Data.Functor.Functor', equivalent to 'Data.Functor.Inviarant.Invariant'.
 class Functor f where
   fmap :: a <-> b -> f a -> f b
+
+-- |Default invertible 'Functor' implementation for simple non-invertible 'Prelude.Functor's.
+fmapDefault :: Prelude.Functor f => a <-> b -> f a -> f b
+fmapDefault (f :<->: _) x = f Prelude.<$> x
 
 -- |An infix synnonym for 'fmap'.
 (<$>) :: Functor f => a <-> b -> f a -> f b
diff --git a/Control/Invertible/MonadArrow.hs b/Control/Invertible/MonadArrow.hs
--- a/Control/Invertible/MonadArrow.hs
+++ b/Control/Invertible/MonadArrow.hs
@@ -1,12 +1,23 @@
 -- |
 -- A symmetric version of the Kleisli monad transformer arrow.
--- BiKleisli provides this Kleisli-like arrow over bijections.
+-- This admits three isomorphic 'MonadBijection' types:
 --
+-- * @'MonadArrow' ('<->') m a b@
+-- * @'Bijection' ('MonadFunction' m) a b@
+-- * @m a '<->' m b@
+--
 -- The Alimarine paper just calls it \"MoT\" for Monad Transformer.
 {-# LANGUAGE CPP, Safe, TupleSections, FlexibleInstances, FlexibleContexts #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TypeOperators #-}
 module Control.Invertible.MonadArrow
   ( MonadArrow(..)
-  , BiKleisli
+  , MonadFunction
+  , MonadBijection
+  , MonadBijection'
+  , MonadBijection''
+  , monadBijection
+  , monadBijection'
   ) where
 
 import Prelude hiding (id, (.))
@@ -20,13 +31,26 @@
 #endif
 
 import Data.Invertible.Bijection
+import Data.Invertible.TH
 import Control.Invertible.BiArrow
 
 -- |Bidirectional 'Control.Arrow.Kleisli'-like monad arrow transformer.
 newtype MonadArrow a m b c = MonadArrow { runMonadArrow :: a (m b) (m c) }
 
--- |A MonadArrow over bijections.
-type BiKleisli m a b = MonadArrow (<->) m a b
+-- |Specialization of 'MonadArrow' to function arrows.
+type MonadFunction = MonadArrow (->)
+
+type MonadBijection m = MonadArrow (<->) m
+type MonadBijection' m = Bijection (MonadFunction m)
+type MonadBijection'' m a b = m a <-> m b
+
+-- |Convert between isomorphic representations of 'MonadBijection's.
+monadBijection :: MonadBijection' m a b <-> MonadBijection m a b
+monadBijection = [biCase|MonadArrow f :<->: MonadArrow g <-> (MonadArrow (f :<->: g))|]
+
+-- |Convert between isomorphic representations of 'MonadBijection's.
+monadBijection' :: MonadBijection'' m a b <-> MonadBijection' m a b
+monadBijection' = [biCase|f :<->: g <-> MonadArrow f :<->: MonadArrow g|]
 
 instance Category a => Category (MonadArrow a m) where
   id = MonadArrow id
diff --git a/Control/Invertible/Monoidal.hs b/Control/Invertible/Monoidal.hs
--- a/Control/Invertible/Monoidal.hs
+++ b/Control/Invertible/Monoidal.hs
@@ -4,11 +4,15 @@
 -- This roughly corresponds to "Control.Applicative", but exposes a non-overlapping API so can be imported unqualified.  It does, however, use operators similar to those provided by contravariant.
 {-# LANGUAGE CPP, Safe, TypeOperators, FlexibleInstances #-}
 module Control.Invertible.Monoidal
-  ( -- * Functor
-    (>$<)
+  ( Bijection(..)
+  , I.biCase
+    -- * Functor
+  , (>$<)
   , (>$), ($<)
   -- * Monoidal
   , Monoidal(..)
+  , unitDefault
+  , pairADefault
   , (>*), (*<)
   -- ** Tuple combinators
   , liftI2
@@ -23,6 +27,7 @@
   , (>>>>*<)
   , (>>*<<)
   , pureI
+  , constI
   , sequenceI_
   , mapI_
   , forI_
@@ -30,6 +35,7 @@
   , mapMaybeI
   -- * MonoidalAlt
   , MonoidalAlt(..)
+  , eitherADefault
   , (>|), (|<)
   , optionalI
   , defaulting
@@ -40,7 +46,10 @@
   ) where
 
 import Prelude
+import Control.Applicative (liftA2, Alternative, (<|>))
 import Control.Arrow ((&&&), (***))
+import Control.Monad.Trans.Maybe (MaybeT(..))
+import Data.Void (Void)
 
 import Data.Invertible.Bijection
 import qualified Data.Invertible as I
@@ -69,6 +78,14 @@
   -- |Merge two functors into a tuple, analogous to @'Control.Applicative.liftA2' (,)@. (Sometimes known as @**@.)
   (>*<) :: f a -> f b -> f (a, b)
 
+-- |Default 'unit' implementation for non-invertible 'Applicative's.
+unitDefault :: Applicative f => f ()
+unitDefault = pure ()
+
+-- |Default '>*< implementation for non-invertible 'Applicative's.
+pairADefault :: Applicative f => f a -> f b -> f (a, b)
+pairADefault = liftA2 (,)
+
 -- |Sequence actions, discarding/inhabiting the unit value of the second argument.
 (>*) :: Monoidal f => f a -> f () -> f a
 (>*) = liftI2 I.fst
@@ -123,6 +140,10 @@
 pureI :: Monoidal f => a -> f a
 pureI a = I.const a >$< unit
 
+-- |Supply a constant value to a monoidal and ignore whatever is produced.
+constI :: Monoidal f => a -> f a -> f ()
+constI a = (>$<) $ I.invert $ I.const a
+
 -- |Sequence (like 'Data.Foldable.sequenceA_') a list of monoidals, ignoring (@'I.const' ()@) all the results.
 sequenceI_ :: (Foldable t, Monoidal f) => t (f ()) -> f ()
 sequenceI_ = foldr (*<) unit
@@ -147,9 +168,15 @@
 
 -- |Monoidal functors that allow choice.
 class Monoidal f => MonoidalAlt f where
+  -- |An always-failing (and thus impossible) value.
+  zero :: f Void
   -- |Associative binary choice.
   (>|<) :: f a -> f b -> f (Either a b)
 
+-- |Default '>|<' implementation for non-invertible 'Alternative's.
+eitherADefault :: Alternative f => f a -> f b -> f (Either a b)
+eitherADefault a b = Left <$> a <|> Right <$> b
+
 -- |Assymetric (and therefore probably not bijective) version of '>|<' that returns whichever action succeeds but always uses the left one on inputs.
 (>|) :: MonoidalAlt f => f a -> f a -> f a
 a >| b = (either id id :<->: Left) >$< (a >|< b)
@@ -160,7 +187,7 @@
 
 infixl 3 >|, >|<, |<
 
--- |Analogous to 'Control.Applicative.optional'.
+-- |Analogous to 'Control.Applicative.optional': always succeeds.
 optionalI :: MonoidalAlt f => f a -> f (Maybe a)
 optionalI f = I.lft >$< (f >|< unit)
 
@@ -201,3 +228,22 @@
   unit = I.id
   -- |Uses the 'Monoid' instance to combine '()'s.
   (ua :<->: au) >*< (ub :<->: bu) = ua &&& ub :<->: uncurry mappend . (au *** bu)
+
+instance I.Functor m => I.Functor (MaybeT m) where
+  fmap f (MaybeT m) = MaybeT $ I.fmap (I.bifmap f) m
+
+instance Monoidal m => Monoidal (MaybeT m) where
+  unit = MaybeT $ I.invert I.fromJust >$< unit
+  MaybeT f >*< MaybeT g = MaybeT
+    $ (uncurry pairADefault :<->: maybe (Nothing, Nothing) (Just *** Just))
+    >$< (f >*< g)
+
+instance Monoidal m => MonoidalAlt (MaybeT m) where
+  zero = MaybeT $ I.const Nothing >$< unit
+  MaybeT f >|< MaybeT g = MaybeT
+    $ (uncurry eitherADefault :<->: ue)
+    >$< (f >*< g)
+    where
+    ue Nothing = (Nothing, Nothing)
+    ue (Just (Left a)) = (Just a, Nothing)
+    ue (Just (Right b)) = (Nothing, Just b)
diff --git a/Control/Invertible/Monoidal/Free.hs b/Control/Invertible/Monoidal/Free.hs
--- a/Control/Invertible/Monoidal/Free.hs
+++ b/Control/Invertible/Monoidal/Free.hs
@@ -23,6 +23,7 @@
 import Control.Monad.Trans.State (StateT(..))
 import Data.Functor.Classes (Show1, showsPrec1)
 import Data.Monoid ((<>), Alt(..))
+import Data.Void (Void, absurd)
 
 import Control.Invertible.Monoidal
 import qualified Data.Invertible as I
@@ -30,6 +31,7 @@
 -- |Produce a 'MonoidalAlt' out of any type constructor, simply by converting each monoidal operation into a constructor.
 -- Although a version more analogous to a free monad could be defined for instances of 'I.Functor' and restricted to 'Monoidal', including the Yoneda transform makes this the more general case.
 data Free f a where
+  Void :: Free f Void
   Empty :: Free f ()
   Free :: !(f a) -> Free f a
   Join :: Free f a -> Free f b -> Free f (a, b)
@@ -45,10 +47,12 @@
   (>*<) = Join
 
 instance MonoidalAlt (Free f) where
+  zero = Void
   (>|<) = Choose
 
 -- |Construct a string representation of a 'Free' structure, given a way to show any @f a@.
 showsPrecFree :: (forall a' . f a' -> ShowS) -> Int -> Free f a -> ShowS
+showsPrecFree _ _ Void = showString "Void"
 showsPrecFree _ _ Empty = showString "Empty"
 showsPrecFree fs d (Free f) = showParen (d > 10)
   $ showString "Free "
@@ -78,6 +82,7 @@
 
 -- |Transform the type constructor within a 'Free'.
 mapFree :: (forall a' . f a' -> m a') -> Free f a -> Free m a
+mapFree _ Void = Void
 mapFree _ Empty = Empty
 mapFree t (Transform f p) = Transform f $ mapFree t p
 mapFree t (Join p q) = Join (mapFree t p) (mapFree t q)
@@ -86,6 +91,7 @@
 
 -- |Given a way to extract a @b@ from any @f a@, use a 'Free' applied to a value to produce a @b@ by converting '>*<' to '<>'.
 foldFree :: Monoid b => (forall a' . f a' -> a' -> b) -> Free f a -> a -> b
+foldFree _ Void a = absurd a
 foldFree _ Empty () = mempty
 foldFree t (Transform f p) a = foldFree t p $ I.biFrom f a
 foldFree t (Join p q) (a, b) = foldFree t p a <> foldFree t q b
@@ -99,6 +105,7 @@
 
 -- |Evaluate a 'Free' into an underlying 'Alternative', by evaluating '>|<' with '<|>'.
 runFree :: Alternative f => Free f a -> f a
+runFree Void = empty
 runFree Empty = pure ()
 runFree (Transform f p) = I.biTo f <$> runFree p
 runFree (Join p q) = (,) <$> runFree p <*> runFree q
diff --git a/Data/Invertible/Maybe.hs b/Data/Invertible/Maybe.hs
--- a/Data/Invertible/Maybe.hs
+++ b/Data/Invertible/Maybe.hs
@@ -7,6 +7,7 @@
   , listToMaybe
   , maybeToList
   , fromMaybe
+  , fromJust
   ) where
 
 import qualified Data.Maybe as M
@@ -42,3 +43,7 @@
 -- |Convert between 'Nothing' and a default value, or 'Just' and its value (not a true bijection).
 fromMaybe :: Eq a => a -> Maybe a <-> a
 fromMaybe d = M.fromMaybe d :<->: \a -> if a == d then Nothing else Just a
+
+-- |Convert between 'Just' and its value.
+fromJust :: Maybe a <-> a
+fromJust = M.fromJust :<->: Just
diff --git a/Data/Invertible/Monad.hs b/Data/Invertible/Monad.hs
--- a/Data/Invertible/Monad.hs
+++ b/Data/Invertible/Monad.hs
@@ -11,7 +11,7 @@
 
 import Data.Invertible.Bijection
 
--- |Bind two functions to create a 'Control.Invertible.MonadArrow.BiKleisli'-form bijection.
+-- |Bind two functions to create a "Control.Invertible.MonadArrow"-form bijection.
 bind :: Monad m => (a -> m b) -> (b -> m a) -> m a <-> m b
 bind f g = (f =<<) :<->: (g =<<)
 
@@ -21,7 +21,7 @@
 
 infix 2 =<<->>=
 
--- |Promote a bijection to a 'Control.Invertible.MonadArrow.BiKleisli'-form bijection.
--- (Equivalent to 'Data.Invertible.Functor.bifmap'.)
+-- |Promote a bijection to a "Control.Invertible.MonadArrow"-form bijection.
+-- (Equivalent to 'Data.Invertible.Functor.bifmap' and 'Control.Invertible.BiArrow.biarr'.)
 liftM :: Monad m => a <-> b -> m a <-> m b
 liftM (f :<->: g) = M.liftM f :<->: M.liftM g
diff --git a/Data/Invertible/TH.hs b/Data/Invertible/TH.hs
--- a/Data/Invertible/TH.hs
+++ b/Data/Invertible/TH.hs
@@ -16,15 +16,20 @@
 import Language.Haskell.Meta.Parse (parsePat)
 import qualified Language.Haskell.TH as TH
 import Language.Haskell.TH.Quote (QuasiQuoter(..))
+import Text.Read.Lex (isSymbolChar)
 
 import Data.Invertible.Bijection
 
-split :: Eq a => [a] -> [a] -> [[a]]
+split :: String -> String -> [String]
 split _ [] = []
-split t s@(c:r)
-  | Just s' <- stripPrefix t s = [] : split t s'
-  | p:l <- split t r = (c:p):l
-  | otherwise = [s]
+split d (p:s)
+  | not (isSymbolChar p)
+  , Just (p':s') <- stripPrefix d s
+  , not (isSymbolChar p') = [p] : conshead p' (split d s')
+  | otherwise = conshead p $ split d s
+  where
+  conshead c [] = [[c]]
+  conshead c (h:t) = (c:h):t
 
 patToPat :: TH.Pat -> TH.Pat
 patToPat = ptp . gmapT pta where
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2016, Dylan Simon
+Copyright (c) 2016-2017, Dylan Simon
 
 All rights reserved.
 
diff --git a/invertible.cabal b/invertible.cabal
--- a/invertible.cabal
+++ b/invertible.cabal
@@ -1,5 +1,5 @@
 name:                invertible
-version:             0.1.2
+version:             0.2.0
 synopsis:            bidirectional arrows, bijective functions, and invariant functors
 description:
   Representations and operations for bidirectional arrows (total isomorphisms: an
@@ -70,7 +70,7 @@
   build-depends:
     base >= 4.8 && <5,
     transformers,
-    haskell-src-meta == 0.6.*,
+    haskell-src-meta >= 0.6 && < 0.8,
     template-haskell == 2.*
   default-language:    Haskell2010
   ghc-options: -Wall
@@ -110,6 +110,8 @@
   type: exitcode-stdio-1.0
   hs-source-dirs: test
   main-is: Main.hs
+  other-modules:
+    FreeMonoidal
   default-language: Haskell2010
   ghc-options: -Wall
   build-depends:
diff --git a/test/FreeMonoidal.hs b/test/FreeMonoidal.hs
new file mode 100644
--- /dev/null
+++ b/test/FreeMonoidal.hs
@@ -0,0 +1,159 @@
+{-# LANGUAGE CPP, GADTs, FlexibleContexts, FlexibleInstances, TypeOperators, TupleSections, ConstraintKinds, GeneralizedNewtypeDeriving, QuasiQuotes #-}
+module FreeMonoidal (tests) where
+
+import Control.Monad (join, guard)
+import Data.Functor.Classes (Show1(..))
+import Data.Maybe (isJust)
+import qualified Test.QuickCheck as Q
+import Unsafe.Coerce (unsafeCoerce)
+
+import Control.Invertible.Monoidal.Free
+import qualified Data.Invertible as I
+
+genTree :: [Q.Gen a] -> Q.Gen a
+genTree = Q.scale (max 0 . pred) . join . Q.growingElements
+
+newtype Const a b = Const a
+  deriving (Eq, Ord, Show, Q.Arbitrary)
+
+instance Functor (Const a) where
+  fmap _ (Const x) = Const x
+
+instance Show a => Show1 (Const a) where
+#if MIN_VERSION_base(4,9,0)
+  liftShowsPrec _ _ =
+#else
+  showsPrec1 =
+#endif
+    showsPrec
+
+data Tree a
+  = TreeEmpty
+  | TreeFree a
+  | TreeJoin !(Tree a, Tree a)
+  | TreeChoose !(Either (Tree a) (Tree a))
+  deriving (Eq, Show)
+
+instance Q.Arbitrary a => Q.Arbitrary (Tree a) where
+  arbitrary = genTree
+    [ return TreeEmpty
+    , TreeFree <$> Q.arbitrary
+    , TreeJoin <$> Q.arbitrary
+    , TreeChoose <$> Q.arbitrary
+    ]
+
+  shrink TreeEmpty = []
+  shrink (TreeFree x) = TreeEmpty : map TreeFree (Q.shrink x) 
+  shrink (TreeJoin (p, q)) =
+    [TreeEmpty, p, q] ++ map TreeJoin (Q.shrink (p, q))
+  shrink (TreeChoose (Left p)) =
+    [TreeEmpty, p] ++ map (TreeChoose . Left) (Q.shrink p)
+  shrink (TreeChoose (Right p)) =
+    [TreeEmpty, p] ++ map (TreeChoose . Right) (Q.shrink p)
+
+type FreeTree a = Free (Const a) (Tree a)
+
+emptyTree :: FreeTree a
+emptyTree = Transform (I.const TreeEmpty) Empty
+
+leaf :: a -> FreeTree a
+leaf = Free . Const
+
+unJoin :: (Tree a, Tree a) I.<-> Tree a
+unJoin = [I.biCase|t <-> TreeJoin t|]
+
+unChoose :: Either (Tree a) (Tree a) I.<-> Tree a
+unChoose = [I.biCase|t <-> TreeChoose t|]
+
+instance Q.Arbitrary a => Q.Arbitrary (FreeTree a) where
+  arbitrary = genTree
+    [ return emptyTree
+    , leaf <$> Q.arbitrary
+    , Transform unJoin   <$> (Join   <$> Q.arbitrary <*> Q.arbitrary)
+    , Transform unChoose <$> (Choose <$> Q.arbitrary <*> Q.arbitrary)
+    , Transform I.id <$> Q.arbitrary
+    ]
+
+  shrink (Free x) = map Free (Q.shrink x) 
+  shrink (Transform _ Empty) = []
+  shrink (Transform _ (Join p q)) =
+    [emptyTree, pt, qt] ++ map (Transform unJoin . uncurry Join) (Q.shrink (pt, qt)) where
+    pt = unsafeCoerce p :: FreeTree a
+    qt = unsafeCoerce q :: FreeTree a
+  shrink (Transform _ (Choose p q)) =
+    [emptyTree, pt, qt] ++ map (Transform unChoose . uncurry Choose) (Q.shrink (pt, qt)) where
+    pt = unsafeCoerce p :: FreeTree a
+    qt = unsafeCoerce q :: FreeTree a
+  shrink (Transform _ p) = [pt] where
+    pt = unsafeCoerce p :: FreeTree a
+
+type ShowFree f = (Functor f, Show1 f)
+
+ok :: Q.Property
+ok = Q.property True
+
+bad :: ShowFree f => Free f a -> Q.Property
+bad f = Q.counterexample (show f) False
+
+checkNoT :: ShowFree f => Free f a -> Q.Property
+checkNoT t@(Transform _ _) = bad t
+checkNoT (Join p q) = checkNoT p Q..&&. checkNoT q
+checkNoT (Choose p q) = checkNoT p Q..&&. checkNoT q
+checkNoT _ = ok
+
+checkTNF :: ShowFree f => Free f a -> Q.Property
+checkTNF (Transform _ p) = checkNoT p
+checkTNF p = checkNoT p
+
+joinDNF :: ShowFree f => Free f a -> Q.Property
+joinDNF t@(Transform _ _) = bad t
+joinDNF c@(Choose _ _) = bad c
+joinDNF (Join p q) = joinDNF p Q..&&. joinDNF q
+joinDNF _ = ok
+
+checkDNF :: ShowFree f => Free f a -> Q.Property
+checkDNF t@(Transform _ _) = bad t
+checkDNF (Choose p q) = checkDNF p Q..&&. checkDNF q
+checkDNF p = joinDNF p
+
+checkTDNF :: ShowFree f => Free f a -> Q.Property
+checkTDNF (Transform _ p) = checkDNF p
+checkTDNF p = checkDNF p
+
+produceParse :: FreeTree Int -> [Int] -> Q.Property
+produceParse f l = isJust p Q.==> check where
+  check = prod f r ++ t Q.=== l Q..&&. reverse t ++ prod (reverseFree f) r Q.=== reverse l
+  Just (r, t) = p
+  p = pars f l
+  pars = parseFree parse
+  parse (Const i) j = unsafeCoerce (TreeFree j) <$ guard (j >= i)
+  prod = produceFree produce
+  produce (Const _) x = case unsafeCoerce x of { ~(TreeFree j) -> j }
+
+joinSorted :: (Show a, Ord a) => Maybe a -> Free (Const a) b -> (Maybe a, Q.Property)
+joinSorted b (Join p q) = (qb, pr Q..&&. qr) where
+  (pb, pr) = joinSorted b p
+  (qb, qr) = joinSorted pb q
+joinSorted b (Free (Const x)) = (Just x, Q.counterexample (show x ++ " < " ++ show b) $ all (x >=) b)
+joinSorted b Empty = (b, ok)
+joinSorted b o = (b, bad o)
+
+chooseSorted :: (Show a, Ord a) => Free (Const a) b -> Q.Property
+chooseSorted t@(Transform _ _) = bad t
+chooseSorted (Choose p q) = chooseSorted p Q..&&. chooseSorted q
+chooseSorted p = snd $ joinSorted Nothing p
+
+checkSorted :: (Show a, Ord a) => Free (Const a) b -> Q.Property
+checkSorted (Transform _ p) = chooseSorted p
+checkSorted p = chooseSorted p
+
+compareConst :: Ord a => Const a b -> Const a c -> Ordering
+compareConst (Const x) (Const y) = compare x y
+
+tests :: Q.Property
+tests = Q.conjoin
+  [ Q.label "TNF" $ checkTNF . (freeTNF :: FreeTree Int -> FreeTree Int)
+  , Q.label "TDNF" $ checkTDNF . (freeTDNF :: FreeTree Int -> FreeTree Int)
+  , Q.label "parseProduce" $ produceParse
+  , Q.label "sort" $ checkSorted . (sortFreeTDNF compareConst :: FreeTree Int -> FreeTree Int)
+  ]