diff --git a/Data/Thorn.hs b/Data/Thorn.hs
--- a/Data/Thorn.hs
+++ b/Data/Thorn.hs
@@ -1,15 +1,125 @@
-{-# LANGUAGE TemplateHaskell, ViewPatterns #-}
+-- | Thorn, Datatype Manipulation with Template Haskell.
 
--- |
--- Thorn, a template haskell library.
 module Data.Thorn (
-    -- * Data.Thorn.Fmap
+    -- * Functor
+    -- $functor
     autofmap
   , Variance(..)
   , autovariance, autofunctorize
+    
+    -- * Folding and Unfolding
+    -- $fold
+  , unfixdata, unfixdataEx
+  , autoin, autoout, autohylo, autofold, autounfold
+
+    -- * Type Variants
+    -- $typevariants
+  , T0, T1, T2, T3, T4, T5, T6, T7, T8, T9    
+
+    -- * Example
+
+    -- ** Functor Example
+    -- $functorexample
+
+    -- ** Folding and Unfolding Example
+    -- $foldexample
   ) where
 
-import Data.Thorn.Fmap
+import Data.Thorn.Type
+import Data.Thorn.Functor
 import Data.Thorn.Fold
-import Data.Thorn.Zipper
+
+{- $functor
+    Thorn generates functors from various kinds of data types.
+
+    Quite surprisingly, it still works for any arities, co\/contra\/free\/fixed-variances, partially applied types, type synonyms, and mutual recursions.
+
+    For more information, see <Data-Thorn.html#FunctorExample Functor Example>.
+-}
+
+{- $fold
+    For more information, see <Data-Thorn.html#FoldExample Folding and Unfolding Example>.
+-}
+
+{- $typevariants
+    These types are used for representing type variants. For more information, see <Data-Thorn.html#FunctorExample Functor Example>.
+-}
+
+{- $functorexample
+   #FunctorExample#
+
+> import Data.Thorn
+> import Data.Char
+> import Data.Functor.Contravariant
+> import Data.Bifunctor
+> import Data.Profunctor
+> 
+> type a :<- b = b -> a
+> nuf :: Char
+> nuf = $(autofmap [t|(:<-)|]) chr ord (+1) 'a' -- 'b'
+> varnuf :: [Variance]
+> varnuf = $(autovariance [t|(:<-)|]) -- [Co,Contra]
+> 
+> data Cntr a = Cntr (a -> Int)
+> autofunctorize [t|Cntr|] -- instance Contravariant Cntr where ...
+> 
+> tuple :: (Int,Int,Int)
+> tuple = $(autofmap $[t|(,,) Int|]) (+1) (+2) (0,0,0) -- (0,1,2)
+> vartuple :: [Variance]
+> vartuple = $(autovariance [t|(,,) Int|]) -- [Co,Co]
+> 
+> data FunFun a b = FunFun ((b -> a) -> b)
+> varfunfun :: [Variance]
+> varfunfun = $(autovariance [t|FunFun|]) -- [Contra,Co]
+> autofunctorize [t|FunFun|] -- instance Profunctor FunFun where ...
+> 
+> data What a b c = What1 c (a -> c) | What2 a
+> varwhat :: [Variance]
+> varwhat = $(autovariance [t|What|]) -- [Fixed,Free,Co]
+> autofunctorize [t|What T0|]
+> -- instance Bifunctor (What a) where ... and
+> -- instance Profunctor (What a) where ...
+> 
+> data List a = Nil | a :* (List a) deriving Show
+> fromNormalList :: [a] -> List a
+> fromNormalList [] = Nil
+> fromNormalList (a : as) = a :* fromNormalList as
+> toNormalList :: List a -> [a]
+> toNormalList Nil = []
+> toNormalList (a :* as) = a : toNormalList as
+> list :: [Int]
+> list = toNormalList $ $(autofmap [t|List|]) (+10) (fromNormalList [1..5]) -- [11..15]
+> varlist :: [Variance]
+> varlist = $(autovariance [t|List|]) -- [Co]
+> autofunctorize [t|List|] -- instance Functor List where ...
+> 
+> data Rose a = Rose a (Forest a) deriving Show
+> data Forest a = Forest [Rose a] deriving Show
+> gorose n = Rose n (Forest (replicate n (gorose (n-1))))
+> rose = $(autofmap [t|Rose|]) (+1) (gorose 2)
+> varrose, varforest :: [Variance]
+> varrose = $(autovariance [t|Rose|]) -- [Co]
+> varforest = $(autovariance [t|Forest|]) -- [Co]
+> autofunctorize [t|Rose|] -- instance Functor Rose where ...
+> autofunctorize [t|Forest|] -- instance Functor Forest where ...
+
+
+
+-}
+
+{- $foldexample
+   #FoldExample#
+
+> import Data.Thorn
+> 
+> data x :$ y = Nil | (x,y) :* (x :$ y)
+> 
+> unfixdata [t|(:$)|]
+> 
+> insth = $(autoin [t|(:&$)|] [t|(:$)|])
+> outsth = $(autoout [t|(:&$)|] [t|(:$)|])
+> hylosth = $(autohylo [t|(:&$)|])
+> foldsth = $(autofold [t|(:&$)|] [t|(:$)|])
+> unfoldsth = $(autounfold [t|(:&$)|] [t|(:$)|])
+-}
 
diff --git a/Data/Thorn/Fmap.hs b/Data/Thorn/Fmap.hs
deleted file mode 100644
--- a/Data/Thorn/Fmap.hs
+++ /dev/null
@@ -1,170 +0,0 @@
-{-# LANGUAGE TemplateHaskell, ViewPatterns #-}
-
--- |
--- The module Data.Thorn.Fmap
-module Data.Thorn.Fmap (
-    autofmap
-  , Variance(..)
-  , autovariance, autovarianceRaw, autofunctorize
-  ) where
-
-import Data.Thorn.Internal
-import Language.Haskell.TH
-import Data.List
-import Data.Maybe
-import qualified Data.Sequence as S
-import qualified Data.Foldable as F
-import Control.Monad
-import Control.Applicative
-import Control.Monad.State
-import Data.Monoid
-import Data.Functor
-import Data.Functor.Contravariant
-import Data.Bifunctor
-import Data.Profunctor
-
--- |
--- @autofmap t@ generates the @fmap@ of the type @t@.
--- 
--- Quite surprisingly, it still works for any arities, co\/contra\/free\/fixed-variances, partially applied types, type synonyms, and mutual recursions.
---
--- @
---type Nuf x y = y -> x
---type a :<- b = Nuf a b
---nuf = $(autofmap [t|(:<-)|]) chr ord (+1) 'c'
---
---data List a = Nil | Cons a (List a) deriving Show
---golist 0 = Nil
---golist n = Cons n (golist (n-1))
---list = $(autofmap $[t|List|]) (+1) (golist 10)
---
---data Rose a = Rose a (Forest a) deriving Show
---data Forest a = Forest [Rose a] deriving Show
---gorose n = Rose n (Forest (replicate n (gorose (n-1))))
---rose = $(autofmap $[t|Rose|]) (+1) (gorose 3)
--- @
-autofmap :: TypeQ -> ExpQ
-autofmap t = do
-    (n,tx) <- t >>= normalizeType [] [] >>= apply 0
-    (e,txnmes) <- runStateT (autofmap' tx) []
-    return $ LamE (map newFuncP [0..n-1]) (LetE (fmap (\(tx,nm,Just e) -> ValD (VarP nm) (NormalB e) []) txnmes) e)
-
-apply :: Int -> Typex -> Q (Int,Typex)
-apply n (FuncTx f) = f (SpecialTx n) >>= apply (n+1)
-apply n tx@(VarTx _) = return (n,tx)
-apply n tx@(DataTx _ _ _) = return (n,tx)
-apply n tx@(SeenDataTx _ _) = return (n,tx)
-apply n tx@(TupleTx _) = return (n,tx)
-apply n tx@(ArrowTx _ _) = return (n,tx)
-apply n tx@(ListTx _) = return (n,tx)
-
-autofmap',autofmap'' :: Typex -> StateT [(Typex,Name,Maybe Exp)] Q Exp
-autofmap' tx = do
-    txnmes <- get
-    case find (\(tx',_,_)->tx==tx') txnmes of
-         Just (_,nm,_) -> return (VarE nm)
-         Nothing -> autofmap'' tx
-autofmap'' (VarTx _) = return $ mkNameE "id"
-autofmap'' (BasicTx _) = return $ mkNameE "id"
-autofmap'' (FuncTx _) = fail "Automap doesn't accept such a type with a kind * -> k."
-autofmap'' (DataTx nm vmp cxs) = do
-    txnmes <- get
-    put ((tx0, newFmap (length txnmes), Nothing) : txnmes)
-    e <- LamE [newVarP 0] <$> (CaseE (newVarE 0) <$> (mapM go cxs))
-    txnmes' <- get
-    put $ map (\(tx,nm,e') -> if tx==tx0 then (tx,nm,Just e) else (tx,nm,e')) txnmes'
-    return e
-    where go (NormalCx nm txs) = do
-              es <- autofmapmap txs
-              return $ Match (ConP nm (map newVarP [0..length txs-1])) (NormalB (apps (ConE nm) es)) []
-          go (InfixCx nm txa txb) = do
-              [ea,eb] <- autofmapmap [txa,txb]
-              return $ Match (InfixP (newVarP 0) nm (newVarP 1)) (NormalB (InfixE (Just ea) (ConE nm) (Just eb))) []
-          tx0 = SeenDataTx nm vmp
-autofmap'' (SeenDataTx nm vmp) = fail "Autofmap doesn't work well, sorry."
-autofmap'' (TupleTx txs) = do
-    es <- autofmapmap txs
-    return $ LamE [TupP (map newVarP [0..length txs-1])] (TupE es)
-    where go i tx = autofmap' tx >>= \e -> return $ AppE e (newVarE i)
-autofmap'' (ArrowTx txa txb) = do
-    fa <- autofmap' txa
-    fb <- autofmap' txb
-    return $ LamE [newVarP 0, newVarP 1] (AppE fb (AppE (newVarE 0) (AppE fa (newVarE 1))))
-autofmap'' (ListTx tx) = autofmap' tx >>= \f -> return $ AppE (mkNameE "map") f
-autofmap'' (SpecialTx n) = return $ newFuncE n
-
-autofmapmap txs = mapM (\(i,tx) -> autofmap' tx >>= \e -> return $ AppE e (newVarE i)) (zip [0 .. length txs - 1] txs)
-
--- |
--- @Variance@ is a variance of a parameter of a functor.
-data Variance =
-    -- | Covariance, one of a normal functor.
-    Co
-    -- | Contravariance, a dual of covariance.
-  | Contra
-    -- | Free-variance, or novariance, being supposed to satisfy either covariance or contravariance.
-  | Free
-    -- | Fixed-variance, or invariance, being suppoesed to satisfy both covariance and contravariance.
-  | Fixed deriving (Show, Read)
-
--- | @v1 `mappend` v2@ means to be supposed to satisfy both @v1@ and @v2@.
-instance Monoid Variance where
-    Free `mappend` v = v
-    v `mappend` Free = v
-    Fixed `mappend` _ = Fixed
-    _ `mappend` Fixed = Fixed
-    Co `mappend` Contra = Fixed
-    Contra `mappend` Co = Fixed
-    mempty = Free
-
-neg :: Variance -> Variance
-neg Co = Contra
-neg Contra = Co
-neg Free = Free
-neg Fixed = Fixed
-
--- |
--- @autovariance t@ provides the variances of the type @t@.
-autovariance :: TypeQ -> ExpQ
-autovariance t = do
-    vs <- autovarianceRaw t
-    return $ ListE (map go vs)
-    where go Co = mkNameCE "Co"
-          go Contra = mkNameCE "Contra"
-          go Free = mkNameCE "Free"
-          go Fixed = mkNameCE "Fixed"
-
-autovarianceRaw :: TypeQ -> Q [Variance]
-autovarianceRaw t = do
-    (n,tx) <- t >>= normalizeType [] [] >>= apply 0
-    (_,seq) <- runStateT (autovariance' Co [] tx) (S.replicate n Free)
-    return $ (F.toList seq)
-
-autovariance' :: Variance -> [(Name,[Conx])] -> Typex -> StateT (S.Seq Variance) Q ()
-autovariance' v dts (SpecialTx n) = do
-    seq <- get
-    put $ S.adjust (<>v) n seq
-autovariance' v dts (VarTx _) = return ()
-autovariance' v dts (FuncTx _) = fail "Automap doesn't accept such a type with a kind * -> k."
-autovariance' v dts (DataTx nm _ cxs) = mapM_ (mapM_ (autovariance' v ((nm,cxs):dts)) . cxtxs) cxs
-autovariance' v dts (SeenDataTx nm _) = return ()
-autovariance' v dts (TupleTx txs) = mapM_ (autovariance' v dts) txs
-autovariance' v dts (ArrowTx txa txb) = autovariance' (neg v) dts txa >> autovariance' v dts txb
-autovariance' v dts (ListTx tx) = autovariance' v dts tx
-
--- |
--- @autofunctorize t@ provides an instance delcaration of the type @t@ for the suitable functor class : Funtor, Contravariant, Bifunctor, or Profunctor
-autofunctorize :: TypeQ -> DecsQ
-autofunctorize t = do
-    vs <- autovarianceRaw t
-    case vs of
-         [Co] -> go (mkName "Functor") (mkName "fmap")
-         [Contra] -> go (mkName "Contravariant") (mkName "contramap")
-         [Co,Co] -> go (mkName "Bifunctor") (mkName "bimap")
-         [Contra,Co] -> go (mkName "Profunctor") (mkName "dimap")
-         _ -> fail "autofunctorize doesn't know the suitable functor class for this variance"
-    where go cls member = do
-              e <- autofmap t
-              t' <- t
-              return [InstanceD [] (AppT (ConT cls) t') [ValD (VarP member) (NormalB e) []]]
-
diff --git a/Data/Thorn/Fold.hs b/Data/Thorn/Fold.hs
--- a/Data/Thorn/Fold.hs
+++ b/Data/Thorn/Fold.hs
@@ -1,44 +1,150 @@
-{-# LANGUAGE TemplateHaskell, ViewPatterns #-}
+{-# LANGUAGE TemplateHaskell #-}
 
 -- |
--- The module Data.Thorn.Fold
+-- The module Data.Thorn.Fold.
 module Data.Thorn.Fold (
-    unfixdata
-  , autofold, autoMutualFold
-  , autounfold, autoMutualUnfold
+    unfixdata, unfixdataEx
+  , autoin, autoout, autohylo, autofold, autounfold
+  , unfixdataMutual, unfixdataMutualEx
+  , autoinMutual, autooutMutual, autohyloMutual, autofoldMutual, autounfoldMutual
     ) where
 
-import Data.Thorn.Internal
+import Data.Thorn.Type
+import Data.Thorn.Functor
 import Language.Haskell.TH
-import Data.List
-import Data.Maybe
-import Control.Monad
 import Control.Applicative
-import Control.Monad.State
-import Data.Monoid
 
 -- |
 -- @unfixdata t@ provides a declaration of a data whose fixpoint is the recursive type @t@.
 unfixdata :: TypeQ -> DecsQ
-unfixdata t = do fail "oh"
+unfixdata = unfixdataEx ("Uf","") ("Uf","") ("&","") ("&","")
 
 -- |
--- @autofold t@ provides a folding function for the recursive type @t@.
-autofold :: TypeQ -> ExpQ
-autofold t = do fail "oh"
+-- Special version of @unfixdata@. Note that
+--
+-- > unfixdata = unfixdataEx ("Uf","") ("Uf","") ("&","") ("&","")
+unfixdataEx ::
+    (String,String) -- ^ prefix and suffix of type constructor
+ -> (String,String) -- ^ prefix and suffix of data constructor
+ -> (String,String) -- ^ prefix and suffix of infix type constructor
+ -> (String,String) -- ^ prefix and suffix of infix data constructor
+ -> TypeQ -- ^ data type
+ -> DecsQ -- ^ declaration of data
+unfixdataEx (pretype,suftype) (predata,sufdata) (pretypeinfix,suftypeinfix) (predatainfix,sufdatainfix) t = do
+    (n, DataTx nm _ cxs) <- applyFixed 0 =<< type2typex [] [] =<< t
+    let modifytx (DataTx nm' vmp cxs') = if nm == nm' then VarTx $ mkName ("self") else DataTx nm' (map (\(nm'',tx) -> (nm'',modifytx tx)) vmp) (map modifycx cxs')
+        modifytx tx@(SeenDataTx nm' _) = if nm == nm' then VarTx $ mkName ("self") else modifytx tx
+        modifytx (TupleTx txs) = TupleTx (map modifytx txs)
+        modifytx (ArrowTx txa txb) = ArrowTx (modifytx txa) (modifytx txb)
+        modifytx (ListTx tx) = ListTx (modifytx tx)
+        modifytx tx = tx
+        modifycx (nm',txs) = (nm',map modifytx txs)
+        go (nm',txs) = do
+              ts <- map ((,) NotStrict) <$> mapM (typex2type . modifytx) txs
+              return $ NormalC (datanm nm') ts
+    cns <- mapM go cxs
+    return [DataD [] (typenm nm) (map var [0..n-1] ++ [self]) cns []]
+    where typenm nm
+            | elem (head s) ['A'..'Z'] = mkName $ pretype ++ s ++ suftype
+            | head s == '(' = mkName $ ":" ++ pretypeinfix ++ init (drop 2 s) ++ suftypeinfix
+            | otherwise = mkName $ ":" ++ pretypeinfix ++ tail s ++ suftypeinfix
+            where s = nameBase nm
+          datanm nm
+            | elem (head s) ['A'..'Z'] = mkName $ predata ++ s ++ sufdata
+            | head s == '(' = mkName $ ":" ++ predatainfix ++ init (drop 2 s) ++ sufdatainfix
+            | otherwise = mkName $ ":" ++ predatainfix ++ tail s ++ sufdatainfix
+            where s = nameBase nm
+          var i = PlainTV $ mkName ("t" ++ show i)
+          self = PlainTV $ mkName ("self")
 
+autoin ::
+    TypeQ -- ^ @u@, un-recursive datatype
+ -> TypeQ -- ^ @t@, fixpoint of @u@
+ -> ExpQ -- ^ function with a type @u a0 .. an t -> t a0 .. an@
+autoin u t = do
+    (_,DataTx _ _ cxsu) <- applyFixed 0 =<< type2typex [] [] =<< u
+    (_,DataTx _ _ cxst) <- applyFixed 0 =<< type2typex [] [] =<< t
+    u1 <- unique
+    u2 <- unique
+    let go ((nmu,txsu),(nmt,_)) = Match (ConP nmu (map newVarP [u2..u2+length txsu-1])) (NormalB (applistE (ConE nmt) (map newVarE [u2..u2+length txsu-1]))) []
+    return $ LamE [newVarP u1] (CaseE (newVarE u1) (map go (zip cxsu cxst)))
+
+autoout ::
+    TypeQ -- ^ @u@, un-recursive datatype
+ -> TypeQ -- ^ @t@, fixpoint of @u@
+ -> ExpQ -- ^ function with a type @t x0 .. xn -> u x0 .. xn t@
+autoout u t = do
+    (_,DataTx _ _ cxsu) <- applyFixed 0 =<< type2typex [] [] =<< u
+    (_,DataTx _ _ cxst) <- applyFixed 0 =<< type2typex [] [] =<< t
+    u1 <- unique
+    u2 <- unique
+    let go ((nmu,txsu),(nmt,_)) = Match (ConP nmt (map newVarP [u2..u2+length txsu-1])) (NormalB (applistE (ConE nmu) (map newVarE [u2..u2+length txsu-1]))) []
+    return $ LamE [newVarP u1] (CaseE (newVarE u1) (map go (zip cxsu cxst)))
+
+autohylo ::
+    TypeQ -- ^ @u@, un-recursive datatype
+ -> ExpQ -- ^ function with a type @(a -> u x0 .. xn a) -> (u x0 .. xn b -> b) -> (a -> b)@
+autohylo u = do
+    (n,DataTx nm _ cxs) <- applyFixed 0 =<< type2typex [] [] =<< u
+    f <- autofmap u
+    u <- unique
+    return $ LamE [newVarP u, newVarP (u+1)] (LetE [ValD (newVarP (u+3))
+        (NormalB (LamE [newVarP (u+2)] (AppE (newVarE (u+1)) (applistE f (replicate (n-1) (mkNameE "Prelude.id") ++ [newVarE (u+3)] ++ [AppE (newVarE u) (newVarE (u+2))])))))
+        []] (newVarE (u+3)))
+
 -- |
--- @autoMutualFold ts@ provides a folding function for the mutually recursive types @ts@.
-autoMutualFold :: [TypeQ] -> ExpQ
-autoMutualFold ts = do fail "oh"
+-- @autofold u t@ provides a folding function for a recursive type @t@.
+autofold ::
+    TypeQ -- ^ @u@, un-recursive datatype
+ -> TypeQ -- ^ @t@, fixpoint of @u@
+ -> ExpQ -- ^ function with a type @(u x0 .. xn a -> a) -> (t -> a)@
+autofold u t = do
+    o <- autoout u t
+    h <- autohylo u
+    return $ AppE h o
 
 -- |
 -- @autounfold t@ provides an unfolding function for the recursive type @t@.
-autounfold :: TypeQ -> ExpQ
-autounfold t = do fail "oh"
+autounfold ::
+    TypeQ -- ^ @u@, un-recursive datatype
+ -> TypeQ -- ^ @t@, fixpoint of @u@
+ -> ExpQ -- ^ function with a type @(a -> u x0 .. xn a) -> (a -> t)@
+autounfold u t = do
+    i <- autoin u t
+    h <- autohylo u
+    u1 <- unique
+    return $ LamE [newVarP u1] (AppE (AppE h (newVarE u1)) i)
 
 -- |
--- @autoMutualUnfold ts@ provides an unfolding function for the mutually recursive types @ts@.
-autoMutualUnfold :: [TypeQ] -> ExpQ
-autoMutualUnfold ts = do fail "oh"
+-- @unfixdataMutual ts@ is a mutual recursion version of @unfixdata t@.
+unfixdataMutual :: [TypeQ] -> DecsQ
+unfixdataMutual = unfixdataMutualEx ("Uf","") ("Uf","") ("&","") ("&","")
+
+unfixdataMutualEx ::
+    (String,String) -- ^ prefix and suffix of type constructor
+ -> (String,String) -- ^ prefix and suffix of data constructor
+ -> (String,String) -- ^ prefix and suffix of infix type constructor
+ -> (String,String) -- ^ prefix and suffix of infix data constructor
+ -> [TypeQ] -- ^ data types
+ -> DecsQ -- ^ declarations of data
+unfixdataMutualEx = undefined
+
+autoinMutual :: [TypeQ] -> DecsQ
+autoinMutual ts = fail "oh"
+
+autooutMutual :: [TypeQ] -> DecsQ
+autooutMutual ts = fail "oh"
+
+autohyloMutual :: [TypeQ] -> DecsQ
+autohyloMutual ts = fail "oh"
+
+-- |
+-- @autofoldMutual ts@ provides a folding function for the mutually recursive types @ts@.
+autofoldMutual :: [TypeQ] -> ExpQ
+autofoldMutual ts = do fail "oh"
+
+-- |
+-- @autounfoldMutual ts@ provides an unfolding function for the mutually recursive types @ts@.
+autounfoldMutual :: [TypeQ] -> ExpQ
+autounfoldMutual ts = do fail "oh"
 
diff --git a/Data/Thorn/FoldExample.hs b/Data/Thorn/FoldExample.hs
new file mode 100644
--- /dev/null
+++ b/Data/Thorn/FoldExample.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TemplateHaskell, TypeOperators #-}
+
+module Data.Thorn.FoldExample (module Data.Thorn.FoldExample) where
+
+import Data.Thorn
+
+data x :$ y = Nil | (x,y) :* (x :$ y)
+
+unfixdata [t|(:$)|]
+
+insth = $(autoin [t|(:&$)|] [t|(:$)|])
+outsth = $(autoout [t|(:&$)|] [t|(:$)|])
+hylosth = $(autohylo [t|(:&$)|])
+foldsth = $(autofold [t|(:&$)|] [t|(:$)|])
+unfoldsth = $(autounfold [t|(:&$)|] [t|(:$)|])
+
diff --git a/Data/Thorn/Functor.hs b/Data/Thorn/Functor.hs
new file mode 100644
--- /dev/null
+++ b/Data/Thorn/Functor.hs
@@ -0,0 +1,165 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+-- |
+-- The module Data.Thorn.Functor.
+module Data.Thorn.Functor (
+    autofmap
+  , Variance(..)
+  , autovariance, autofunctorize
+  ) where
+
+import Data.Thorn.Type
+import Language.Haskell.TH
+import Data.List
+import qualified Data.Sequence as S
+import qualified Data.Foldable as F
+import Control.Applicative
+import Control.Monad.State
+import Data.Monoid
+
+-- |
+-- @autofmap t@ generates the @fmap@ of the type @t@.
+autofmap :: TypeQ -> ExpQ
+autofmap t = do
+    (n,tx) <- t >>= type2typex [] [] >>= applySpecial 0
+    u <- unique
+    (e,txnmes) <- runStateT (autofmap' u tx) []
+    return $ LamE (map newFuncP [u..u+n-1]) (LetE (fmap (\(_,nm,Just e') -> ValD (VarP nm) (NormalB e') []) txnmes) e)
+
+autofmap',autofmap'' :: Unique -> Typex -> StateT [(Typex,Name,Maybe Exp)] Q Exp
+autofmap' u tx = do
+    txnmes <- get
+    case find (\(tx',_,_)->tx==tx') txnmes of
+         Just (_,nm,_) -> return (VarE nm)
+         Nothing -> autofmap'' u tx
+autofmap'' _ (VarTx _) = return $ mkNameE "id"
+autofmap'' _ (BasicTx _) = return $ mkNameE "id"
+autofmap'' _ (FixedTx _) = return $ mkNameE "id"
+autofmap'' _ NotTx = fail "Thorn doesn't work well, sorry."
+autofmap'' _ (FuncTx _) = fail "Thorn doesn't accept such a type with a kind * -> k, sorry."
+autofmap'' u (DataTx nm vmp cxs) = do
+    txnmes <- get
+    put ((tx0, newFmap (length txnmes), Nothing) : txnmes)
+    u2 <- unique
+    e <- LamE [newVarP u2] <$> (CaseE (newVarE u2) <$> (mapM go cxs))
+    txnmes' <- get
+    put $ map (\(tx,nm',e') -> if tx==tx0 then (tx,nm',Just e) else (tx,nm',e')) txnmes'
+    return e
+    where go (nm',txs) = do
+              (u2,es) <- autofmapmap u txs
+              return $ Match (ConP nm' (map newVarP [u2..u2+length txs-1])) (NormalB (applistE (ConE nm') es)) []
+          tx0 = SeenDataTx nm vmp
+autofmap'' _ (SeenDataTx _ _) = fail "Thorn doesn't work well, sorry."
+autofmap'' u (TupleTx txs) = do
+    (u2,es) <- autofmapmap u txs
+    return $ LamE [TupP (map newVarP [u2..u2+length txs-1])] (TupE es)
+autofmap'' u (ArrowTx txa txb) = do
+    fa <- autofmap' u txa
+    fb <- autofmap' u txb
+    u2 <- unique
+    return $ LamE [newVarP u2, newVarP (u2+1)] (AppE fb (AppE (newVarE u2) (AppE fa (newVarE (u2+1)))))
+autofmap'' u (ListTx tx) = autofmap' u tx >>= \f -> return $ AppE (mkNameE "map") f
+autofmap'' u (SpecialTx n) = return $ newFuncE (u+n)
+
+autofmapmap :: Unique -> [Typex] -> StateT [(Typex,Name,Maybe Exp)] Q (Unique,[Exp])
+autofmapmap u txs = do
+    u2 <- unique
+    es <- mapM (\(i,tx) -> autofmap' u tx >>= \e -> return $ AppE e (newVarE i)) (zip [u2..u2+length txs-1] txs)
+    return (u2,es)
+
+-- |
+-- @Variance@ is a variance of a parameter of a functor.
+data Variance =
+    -- | Covariance, one of a normal functor.
+    Co
+    -- | Contravariance, a dual of covariance.
+  | Contra
+    -- | Free-variance, or novariance, being supposed to satisfy either covariance or contravariance.
+  | Free
+    -- | Fixed-variance, or invariance, being suppoesed to satisfy both covariance and contravariance.
+  | Fixed deriving (Show, Read)
+
+-- | @v1 `mappend` v2@ means to be supposed to satisfy both @v1@ and @v2@.
+instance Monoid Variance where
+    Free `mappend` v = v
+    v `mappend` Free = v
+    Fixed `mappend` _ = Fixed
+    _ `mappend` Fixed = Fixed
+    Co `mappend` Co = Co
+    Contra `mappend` Contra = Contra
+    _ `mappend` _ = Fixed
+    mempty = Free
+
+neg :: Variance -> Variance
+neg Co = Contra
+neg Contra = Co
+neg Free = Free
+neg Fixed = Fixed
+
+includes :: Variance -> Variance -> Bool
+includes _ Free = True
+includes Free _ = False
+includes Fixed _ = True
+includes _ Fixed = False
+includes Co Co = True
+includes Contra Contra = True
+includes _ _ = False
+
+-- |
+-- @autovariance t@ provides the variances of the type @t@.
+autovariance :: TypeQ -> ExpQ
+autovariance t = do
+    vs <- autovarianceRaw t
+    return $ ListE (map go vs)
+    where go Co = mkNameCE "Co"
+          go Contra = mkNameCE "Contra"
+          go Free = mkNameCE "Free"
+          go Fixed = mkNameCE "Fixed"
+
+autovarianceRaw :: TypeQ -> Q [Variance]
+autovarianceRaw t = do
+    (n,tx) <- t >>= type2typex [] [] >>= applySpecial 0
+    (_,sq) <- runStateT (autovariance' Co [] tx) (S.replicate n Free)
+    return $ (F.toList sq)
+
+autovariance' :: Variance -> [(Name,[Conx],Variance)] -> Typex -> StateT (S.Seq Variance) Q ()
+autovariance' _ _ (VarTx _) = return ()
+autovariance' _ _ (BasicTx _) = return ()
+autovariance' v _ (SpecialTx n) = do
+    sq <- get
+    put $ S.adjust (<>v) n sq
+autovariance' _ _ (FixedTx _) = return ()
+autovariance' _ _ NotTx = fail "Thorn doesn't work well, sorry."
+autovariance' _ _ (FuncTx _) = fail "Thorn doesn't accept such a type with a kind * -> k, sorry."
+autovariance' v dts (DataTx nm _ cxs) = mapM_ (mapM_ (autovariance' v ((nm,cxs,v):dts)) . cxtxs) cxs
+autovariance' v dts (SeenDataTx nm _)
+    | v' `includes` v = return ()
+    | otherwise = mapM_ (mapM_ (autovariance' v dts') . cxtxs) cxs
+    where Just (_,cxs,v') = find (\(nm',_,_) -> nm==nm') dts
+          dts' = map (\tpl@(nm',_,_) -> if nm==nm' then (nm',cxs,v<>v') else tpl) dts
+autovariance' v dts (TupleTx txs) = mapM_ (autovariance' v dts) txs
+autovariance' v dts (ArrowTx txa txb) = autovariance' (neg v) dts txa >> autovariance' v dts txb
+autovariance' v dts (ListTx tx) = autovariance' v dts tx
+
+-- |
+-- @autofunctorize t@ provides instance delcarations of the type @t@, for the suitable functor classes : Funtor, Contravariant, Bifunctor, or Profunctor.
+autofunctorize :: TypeQ -> DecsQ
+autofunctorize t = do
+    vs <- autovarianceRaw t
+    case vs of
+         [Co] -> functor
+         [Contra] -> contravariant
+         [Free] -> (++) <$> functor <*> contravariant
+         [Co,Co] -> bifunctor
+         [Contra,Co] -> profunctor
+         [Free,Co] -> (++) <$> bifunctor <*> profunctor
+         _ -> fail "Thorn doesn't know any suitable functor class for this variance, sorry."
+    where go cls member = do
+              e <- autofmap t
+              t' <- normalizetype =<< t
+              return [InstanceD [] (AppT (ConT cls) t') [ValD (VarP member) (NormalB e) []]]
+          functor = go (mkName "Prelude.Functor") (mkName "fmap")
+          contravariant = go (mkName "Data.Functor.Contravariant.Contravariant") (mkName "contramap")
+          bifunctor = go (mkName "Data.Bifunctor.Bifunctor") (mkName "bimap")
+          profunctor = go (mkName "Data.Profunctor.Profunctor") (mkName "dimap")
+
diff --git a/Data/Thorn/FunctorExample.hs b/Data/Thorn/FunctorExample.hs
new file mode 100644
--- /dev/null
+++ b/Data/Thorn/FunctorExample.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE TemplateHaskell, TypeOperators #-}
+
+module Data.Thorn.FunctorExample (module Data.Thorn.FunctorExample) where
+
+import Data.Thorn
+import Data.Char
+import Data.Functor.Contravariant
+import Data.Bifunctor
+import Data.Profunctor
+
+type a :<- b = b -> a
+nuf :: Char
+nuf = $(autofmap [t|(:<-)|]) chr ord (+1) 'a' -- 'b'
+varnuf :: [Variance]
+varnuf = $(autovariance [t|(:<-)|]) -- [Co,Contra]
+
+data Cntr a = Cntr (a -> Int)
+autofunctorize [t|Cntr|] -- instance Contravariant Cntr where ...
+
+tuple :: (Int,Int,Int)
+tuple = $(autofmap $[t|(,,) Int|]) (+1) (+2) (0,0,0) -- (0,1,2)
+vartuple :: [Variance]
+vartuple = $(autovariance [t|(,,) Int|]) -- [Co,Co]
+
+data FunFun a b = FunFun ((b -> a) -> b)
+varfunfun :: [Variance]
+varfunfun = $(autovariance [t|FunFun|]) -- [Contra,Co]
+autofunctorize [t|FunFun|] -- instance Profunctor FunFun where ...
+
+data What a b c = What1 c (a -> c) | What2 a
+varwhat :: [Variance]
+varwhat = $(autovariance [t|What|]) -- [Fixed,Free,Co]
+autofunctorize [t|What T0|]
+-- instance Bifunctor (What a) where ... and
+-- instance Profunctor (What a) where ...
+
+data List a = Nil | a :* (List a) deriving Show
+fromNormalList :: [a] -> List a
+fromNormalList [] = Nil
+fromNormalList (a : as) = a :* fromNormalList as
+toNormalList :: List a -> [a]
+toNormalList Nil = []
+toNormalList (a :* as) = a : toNormalList as
+list :: [Int]
+list = toNormalList $ $(autofmap [t|List|]) (+10) (fromNormalList [1..5]) -- [11..15]
+varlist :: [Variance]
+varlist = $(autovariance [t|List|]) -- [Co]
+autofunctorize [t|List|] -- instance Functor List where ...
+
+data Rose a = Rose a (Forest a) deriving Show
+data Forest a = Forest [Rose a] deriving Show
+gorose n = Rose n (Forest (replicate n (gorose (n-1))))
+rose = $(autofmap [t|Rose|]) (+1) (gorose 2)
+varrose, varforest :: [Variance]
+varrose = $(autovariance [t|Rose|]) -- [Co]
+varforest = $(autovariance [t|Forest|]) -- [Co]
+autofunctorize [t|Rose|] -- instance Functor Rose where ...
+autofunctorize [t|Forest|] -- instance Functor Forest where ...
+
diff --git a/Data/Thorn/Internal.hs b/Data/Thorn/Internal.hs
deleted file mode 100644
--- a/Data/Thorn/Internal.hs
+++ /dev/null
@@ -1,131 +0,0 @@
-{-# LANGUAGE TemplateHaskell, ViewPatterns #-}
-
-module Data.Thorn.Internal (
-    newVar, newVarP, newVarE
-  , newFunc, newFuncP, newFuncE
-  , newFmap, newFmapP, newFmapE
-  , mkNameE, mkNameCE, mkNameP
-  , Typex(..)
-  , Conx(..)
-  , cxtxs
-  , normalizeType
-  , apps
-  ) where
-
-import Language.Haskell.TH
-import Data.List
-import Data.Maybe
-import Control.Monad
-import Control.Applicative
-
-newVar,newFunc,newFmap :: Int -> Name
-newVar n = mkName $ "thornvariant" ++ show n
-newVarP = VarP . newVar
-newVarE = VarE . newVar
-newFunc n = mkName $ "thornfunction" ++ show n
-newFuncP = VarP . newFunc
-newFuncE = VarE . newFunc
-newFmap n = mkName $ "thornfmap" ++ show n
-newFmapP = VarP . newFmap
-newFmapE = VarE . newFmap
-
-mkNameE = VarE . mkName
-mkNameCE = ConE . mkName
-mkNameP = VarP . mkName
-
-data Typex =
-    VarTx Name
-  | FuncTx (Typex -> TypexQ)
-  | DataTx Name VarMap [Conx]
-  | SeenDataTx Name VarMap
-  | BasicTx Name
-  | TupleTx [Typex]
-  | ArrowTx Typex Typex
-  | ListTx Typex
-  | SpecialTx Int
-type TypexQ = Q Typex
-
-data Conx =
-    NormalCx Name [Typex]
-  | InfixCx Name Typex Typex
-  deriving Eq
-
-cxtxs :: Conx -> [Typex]
-cxtxs (NormalCx _ txs) = txs
-cxtxs (InfixCx _ txa txb) = [txa,txb]
-
-type VarMap = [(Name,Typex)]
-type Datas = [(Name,VarMap)]
-
-instance Eq Typex where
-    VarTx t == VarTx t' = t==t'
-    DataTx nm vmp cons == DataTx nm' vmp' cons' = nm==nm'&&vmp==vmp'&&cons==cons'
-    SeenDataTx nm vmp == SeenDataTx nm' vmp' = nm==nm'&&vmp==vmp'
-    BasicTx nm == BasicTx nm' = nm==nm'
-    TupleTx txs == TupleTx txs' = txs==txs'
-    ArrowTx txa txb == ArrowTx txa' txb' = txa==txa'&&txb==txb'
-    ListTx tx == ListTx tx' = tx==tx'
-    SpecialTx n == SpecialTx n' = n==n'
-    _ == _ = False
-
-instance Show Typex where
-    show (DataTx _ _ _) = "DataTx"
-    show (SeenDataTx _ _) = "SeenDataTx"
-    show _ = "Foo"
-
-normalizeType :: VarMap -> Datas -> Type -> TypexQ
-normalizeType vmp dts (ForallT tvs _ t) = normalizeType vmp' dts t
-    where vmp' = filter (\(nm,_) -> notElem nm (map nameTV tvs)) vmp
-normalizeType vmp dts (AppT t u) = do
-    FuncTx f <- normalizeType vmp dts t
-    ux <- normalizeType vmp dts u
-    f ux
-normalizeType vmp dts (SigT t _) = normalizeType vmp dts t
-normalizeType vmp dts (VarT nm) = case (find (\(nm',_) -> nm==nm') vmp) of
-    Nothing -> return $ VarTx nm
-    Just (_,tx) -> return tx
-normalizeType vmp dts (ConT nm)
-    | s == "()" = normalizeType vmp dts (TupleT 0)
-    | head s == '(' && dropWhile (==',') (tail s) == ")" = normalizeType vmp dts (TupleT (length s - 1))
-    | s == "(->)" = normalizeType vmp dts ArrowT
-    | s == "[]" = normalizeType vmp dts ListT
-    | elem s ["Int","Word","Float","Double","Char","Ptr","FunPtr"] = return $ BasicTx nm
-    | otherwise = reify nm >>= go
-    where s = nameBase nm
-          go (TyConI (TySynD _ tvs u)) = ho (length tvs) []
-            where ho 0 txs = normalizeType (zip (map nameTV tvs) (reverse txs)) dts u
-                  ho n txs = return $ FuncTx $ \tx -> ho (n-1) (tx:txs)
-          go (TyConI (DataD _ _ tvs cons _)) = ho (length tvs) []
-            where ho 0 txs = fromData nm (zip (map nameTV tvs) (reverse txs)) dts cons
-                  ho n txs = return $ FuncTx $ \tx -> ho (n-1) (tx:txs)
-          go (TyConI (NewtypeD _ _ tvs con _)) = ho (length tvs) []
-            where ho 0 txs = fromData nm (zip (map nameTV tvs) (reverse txs)) dts [con]
-                  ho n txs = return $ FuncTx $ \tx -> ho (n-1) (tx:txs)
-          go (PrimTyConI _ _ _) = fail "Autofmap doesn't support such primitive types, sorry."
-          go (FamilyI _ _) = fail "Autofmap doesn't support type families, sorry."
-normalizeType vmp dts (TupleT n) = go n []
-    where go 0 txs = return $ TupleTx (reverse txs)
-          go n txs = return $ FuncTx $ \tx -> go (n-1) (tx:txs)
-normalizeType vmp dts ArrowT = return $ FuncTx $ \txa -> return $ FuncTx $ \txb -> return $ ArrowTx txa txb
-normalizeType vmp dts ListT = return $ FuncTx $ \tx -> return $ ListTx tx
-normalizeType _ _ _ = fail "Autofmap doesn't support such types, sorry."
-
-fromData :: Name -> VarMap -> Datas -> [Con] -> TypexQ
-fromData nm vmp dts cons = case find (\(nm',vmp')->nm==nm') dts of
-        Just (_,vmp')
-            | vmp == vmp' -> return $ SeenDataTx nm vmp
-            | otherwise -> fail "Autofmap doesn't support irregular types, sorry."
-        Nothing -> DataTx nm vmp <$> mapM normalizeCon cons
-    where dts' = (nm,vmp) : dts
-          normalizeCon (NormalC nm sts) = NormalCx nm <$> mapM normalizeStrictType sts
-          normalizeCon (RecC nm vsts) = NormalCx nm <$> mapM normalizeVarStrictType vsts
-          normalizeCon (InfixC sta nm stb) = InfixCx nm <$> normalizeStrictType sta <*> normalizeStrictType stb
-          normalizeStrictType (_,t) = normalizeType vmp dts' t
-          normalizeVarStrictType (_,_,t) = normalizeType vmp dts' t
-
-nameTV :: TyVarBndr -> Name
-nameTV (PlainTV nm) = nm
-nameTV (KindedTV nm _) = nm
-
-apps e es = foldl (\e es -> AppE e es) e es
-
diff --git a/Data/Thorn/Type.hs b/Data/Thorn/Type.hs
new file mode 100644
--- /dev/null
+++ b/Data/Thorn/Type.hs
@@ -0,0 +1,241 @@
+{-# LANGUAGE TemplateHaskell, EmptyDataDecls #-}
+
+-- | The module Data.Thorn.Type.
+module Data.Thorn.Type (
+    Unique, unique
+  , newVar, newSubvar, newFunc, newFmap
+  , newVarP, newSubvarP, newFuncP, newFmapP
+  , newVarE, newSubvarE, newFuncE, newFmapE
+  , mkNameE, mkNameCE, mkNameP
+  , applistE, applistT
+  , Typex(..)
+  , Conx(..)
+  , cxtxs
+  , type2typex, typex2type, normalizetype
+  , T0, T1, T2, T3, T4, T5, T6, T7, T8, T9
+  , applySpecial, applyFixed
+  ) where
+
+import Language.Haskell.TH
+import Data.List
+import Data.Maybe
+import Control.Monad.Trans
+import Control.Applicative
+import System.Random
+
+instance MonadIO Q where
+    liftIO = runIO
+
+type Unique = Int
+
+unique :: MonadIO m => m Unique
+unique = liftIO $ getStdRandom (randomR (0,1000000000))
+
+newVar, newSubvar, newFunc, newFmap :: Int -> Name
+newVarP, newSubvarP, newFuncP, newFmapP :: Int -> Pat
+newVarE, newSubvarE, newFuncE, newFmapE :: Int -> Exp
+newVar n = mkName $ "var" ++ show n
+newVarP = VarP . newVar
+newVarE = VarE . newVar
+newSubvar n = mkName $ "subvar" ++ show n
+newSubvarP = VarP . newSubvar
+newSubvarE = VarE . newSubvar
+newFunc n = mkName $ "func" ++ show n
+newFuncP = VarP . newFunc
+newFuncE = VarE . newFunc
+newFmap n = mkName $ "fmap" ++ show n
+newFmapP = VarP . newFmap
+newFmapE = VarE . newFmap
+
+mkNameE, mkNameCE :: String -> Exp
+mkNameP :: String -> Pat
+mkNameE = VarE . mkName
+mkNameCE = ConE . mkName
+mkNameP = VarP . mkName
+
+applistE :: Exp -> [Exp] -> Exp
+applistT :: Type -> [Type] -> Type
+applistE e es = foldl (\e' es' -> AppE e' es') e es
+applistT t ts = foldl (\t' ts' -> AppT t' ts') t ts
+
+data Typex =
+    VarTx Name
+  | BasicTx Name
+  | FixedTx Int
+  | SpecialTx Int
+  | NotTx
+  | FuncTx (Typex -> TypexQ)
+  | DataTx Name VarMap [Conx]
+  | SeenDataTx Name VarMap
+  | TupleTx [Typex]
+  | ArrowTx Typex Typex
+  | ListTx Typex
+type TypexQ = Q Typex
+
+type Conx = (Name,[Typex])
+
+cxtxs :: Conx -> [Typex]
+cxtxs = snd
+
+type VarMap = [(Name,Typex)]
+type Datas = [(Name,VarMap)]
+
+instance Eq Typex where
+    VarTx t == VarTx t' = t==t'
+    BasicTx nm == BasicTx nm' = nm==nm'
+    SpecialTx n == SpecialTx n' = n==n'
+    FixedTx n == FixedTx n' = n==n'
+    NotTx == NotTx = True
+    DataTx nm vmp cons == DataTx nm' vmp' cons' = nm==nm'&&vmp==vmp'&&cons==cons'
+    SeenDataTx nm vmp == SeenDataTx nm' vmp' = nm==nm'&&vmp==vmp'
+    TupleTx txs == TupleTx txs' = txs==txs'
+    ArrowTx txa txb == ArrowTx txa' txb' = txa==txa'&&txb==txb'
+    ListTx tx == ListTx tx' = tx==tx'
+    _ == _ = False
+
+instance Show Typex where
+    show (DataTx _ _ _) = "DataTx"
+    show (SeenDataTx _ _) = "SeenDataTx"
+    show _ = "Foo"
+
+type2typex :: VarMap -> Datas -> Type -> TypexQ
+type2typex vmp dts (ForallT tvs _ t) = type2typex vmp' dts t
+    where vmp' = filter (\(nm,_) -> notElem nm (map nameTV tvs)) vmp
+type2typex vmp dts (AppT t u) = do
+    FuncTx f <- type2typex vmp dts t
+    ux <- type2typex vmp dts u
+    f ux
+type2typex vmp dts (SigT t _) = type2typex vmp dts t
+type2typex vmp _ (VarT nm) = case (find (\(nm',_) -> nm==nm') vmp) of
+    Nothing -> return $ VarTx nm
+    Just (_,tx) -> return tx
+type2typex vmp dts (ConT nm)
+    | s == "()" = type2typex vmp dts (TupleT 0)
+    | head s == '(' && dropWhile (==',') (tail s) == ")" = type2typex vmp dts (TupleT (length s - 1))
+    | s == "(->)" = type2typex vmp dts ArrowT
+    | s == "[]" = type2typex vmp dts ListT
+    | elem s ["Int","Word","Float","Double","Char","Ptr","FunPtr"] = return $ BasicTx nm
+    | otherwise = reify nm >>= go
+    where s = nameBase nm
+          go (TyConI (TySynD _ tvs u)) = ho (length tvs) []
+            where ho 0 txs = type2typex (zip (map nameTV tvs) (reverse txs)) dts u
+                  ho n txs = return $ FuncTx $ \tx -> ho (n-1) (tx:txs)
+          go (TyConI (DataD _ nm' tvs cons _)) = do
+              b <- istypevariant nm'
+              if b then tofixed nm' else ho (length tvs) []
+            where ho 0 txs = fromData nm' (zip (map nameTV tvs) (reverse txs)) dts cons
+                  ho n txs = return $ FuncTx $ \tx -> ho (n-1) (tx:txs)
+          go (TyConI (NewtypeD _ _ tvs con _)) = ho (length tvs) []
+            where ho 0 txs = fromData nm (zip (map nameTV tvs) (reverse txs)) dts [con]
+                  ho n txs = return $ FuncTx $ \tx -> ho (n-1) (tx:txs)
+          go (PrimTyConI _ _ _) = fail "Thorn doesn't support such primitive types, sorry."
+          go (FamilyI _ _) = fail "Thorn doesn't support type families, sorry."
+          go _ = fail "Thorn doesn't work well, sorry."
+type2typex _ _ (TupleT n) = go n []
+    where go 0 txs = return $ TupleTx (reverse txs)
+          go k txs = return $ FuncTx $ \tx -> go (k-1) (tx:txs)
+type2typex _ _ ArrowT = return $ FuncTx $ \txa -> return $ FuncTx $ \txb -> return $ ArrowTx txa txb
+type2typex _ _ ListT = return $ FuncTx $ \tx -> return $ ListTx tx
+type2typex _ _ _ = fail "Thorn doesn't support such types, sorry."
+
+fromData :: Name -> VarMap -> Datas -> [Con] -> TypexQ
+fromData nm vmp dts cons = case find (\(nm',_)->nm==nm') dts of
+        Just (_,vmp')
+            | vmp == vmp' -> return $ SeenDataTx nm vmp
+            | otherwise -> fail "Thorn doesn't support irregular types, sorry."
+        Nothing -> DataTx nm vmp <$> mapM con2conx cons
+    where dts' = (nm,vmp) : dts
+          con2conx (NormalC nm' sts) = (,) nm' <$> mapM stype2typex sts
+          con2conx (RecC nm' vsts) = (,) nm' <$> mapM vstype2typex vsts
+          con2conx (InfixC sta nm' stb) = do
+              txa <- stype2typex sta
+              txb <- stype2typex stb
+              return (nm',[txa,txb])
+          con2conx (ForallC _ _ _) = fail "Thorn doesn't support existential types, sorry."
+          stype2typex (_,t) = type2typex vmp dts' t
+          vstype2typex (_,_,t) = type2typex vmp dts' t
+
+nameTV :: TyVarBndr -> Name
+nameTV (PlainTV nm) = nm
+nameTV (KindedTV nm _) = nm
+
+typex2type :: Typex -> TypeQ
+typex2type (VarTx nm) = return $ VarT nm
+typex2type (SpecialTx _) = return StarT
+typex2type (FixedTx n) = return $ VarT (mkName $ "t" ++ show n)
+typex2type NotTx = return StarT
+typex2type (FuncTx f) = do
+    AppT t StarT <- typex2type =<< f NotTx
+    return t
+typex2type (DataTx nm vmp _) = do
+    ts <- mapM (typex2type . snd) vmp
+    return $ applistT (ConT nm) ts
+typex2type (SeenDataTx nm vmp) = do
+    ts <- mapM (typex2type . snd) vmp
+    return $ applistT (ConT nm) ts
+typex2type (BasicTx nm) = return $ ConT nm
+typex2type (TupleTx txs) = do
+    ts <- mapM typex2type txs
+    return $ applistT (TupleT (length txs)) ts
+typex2type (ArrowTx txa txb) = do
+    ta <- typex2type txa
+    tb <- typex2type txb
+    return $ applistT ArrowT [ta,tb]
+typex2type (ListTx tx) = do
+    t <- typex2type tx
+    return $ AppT ListT t
+normalizetype :: Type -> TypeQ
+normalizetype t = typex2type =<< type2typex [] [] t
+
+data T0
+data T1
+data T2
+data T3
+data T4
+data T5
+data T6
+data T7
+data T8
+data T9
+
+typevariants :: Q [Name]
+typevariants = mapM (\n -> getnm <$> (reify . mkName $ 'T' : show n)) ([0..9] :: [Int])
+    where getnm (TyConI (DataD _ nm _ _ _)) = nm
+          getnm _ = error "Thorn doesn't work well, sorry."
+
+istypevariant :: Name -> Q Bool
+istypevariant nm = do
+    typevariants' <- typevariants
+    return $ elem nm typevariants'
+
+tofixed :: Name -> Q Typex
+tofixed nm = do
+    typevariants' <- typevariants
+    return $ FixedTx (fromJust $ elemIndex nm typevariants')
+
+applySpecial :: Int -> Typex -> Q (Int,Typex)
+applySpecial n (FuncTx f) = f (SpecialTx n) >>= applySpecial (n+1)
+applySpecial n tx@(VarTx _) = return (n,tx)
+applySpecial n tx@(BasicTx _) = return (n,tx)
+applySpecial n tx@(FixedTx _) = return (n,tx)
+applySpecial n tx@(SpecialTx _) = return (n,tx)
+applySpecial n tx@NotTx = return (n,tx)
+applySpecial n tx@(DataTx _ _ _) = return (n,tx)
+applySpecial n tx@(SeenDataTx _ _) = return (n,tx)
+applySpecial n tx@(TupleTx _) = return (n,tx)
+applySpecial n tx@(ArrowTx _ _) = return (n,tx)
+applySpecial n tx@(ListTx _) = return (n,tx)
+
+applyFixed :: Int -> Typex -> Q (Int,Typex)
+applyFixed n (FuncTx f) = f (FixedTx n) >>= applyFixed (n+1)
+applyFixed n tx@(VarTx _) = return (n,tx)
+applyFixed n tx@(BasicTx _) = return (n,tx)
+applyFixed n tx@(FixedTx _) = return (n,tx)
+applyFixed n tx@(SpecialTx _) = return (n,tx)
+applyFixed n tx@NotTx = return (n,tx)
+applyFixed n tx@(DataTx _ _ _) = return (n,tx)
+applyFixed n tx@(SeenDataTx _ _) = return (n,tx)
+applyFixed n tx@(TupleTx _) = return (n,tx)
+applyFixed n tx@(ArrowTx _ _) = return (n,tx)
+applyFixed n tx@(ListTx _) = return (n,tx)
+
diff --git a/Data/Thorn/Zipper.hs b/Data/Thorn/Zipper.hs
deleted file mode 100644
--- a/Data/Thorn/Zipper.hs
+++ /dev/null
@@ -1,15 +0,0 @@
-{-# LANGUAGE TemplateHaskell, ViewPatterns #-}
-
--- |
--- The module Data.Thorn.Zipper
-module Data.Thorn.Zipper (
-    autozipper
-  ) where
-
-import Data.Thorn.Internal
-import Data.Thorn.Fmap
-import Language.Haskell.TH
-
-autozipper :: TypeQ -> DecsQ
-autozipper t = fail "oh"
-
diff --git a/thorn.cabal b/thorn.cabal
--- a/thorn.cabal
+++ b/thorn.cabal
@@ -1,8 +1,8 @@
 name: thorn
-synopsis: Template Haskell Library
-description: Template Haskell Library
+synopsis: Datatype Manipulation with Template Haskell
+description: Datatype Manipulation with Template Haskell
 category: Data, Generics
-version: 0.1.0.2
+version: 0.1.0.3
 stability: experimental
 license: BSD3
 license-file: LICENSE
@@ -19,10 +19,11 @@
     location: git://github.com/Kinokkory/Thorn.git
 
 library
-    exposed-modules: Data.Thorn
-    other-modules: Data.Thorn.Fmap, Data.Thorn.Fold, Data.Thorn.Zipper, Data.Thorn.Internal
+    exposed-modules: Data.Thorn, Data.Thorn.FunctorExample, Data.Thorn.FoldExample
+    other-modules: Data.Thorn.Functor, Data.Thorn.Fold, Data.Thorn.Type
     build-depends:
         base >= 4 && < 5,
+        random > 1,
         template-haskell < 3,
         mtl < 3,
         containers < 1,