diff --git a/extensible.cabal b/extensible.cabal
--- a/extensible.cabal
+++ b/extensible.cabal
@@ -1,5 +1,5 @@
 name:                extensible
-version:             0.1
+version:             0.2
 synopsis:            Poly-kinded, extensible ADTs
 homepage:            https://github.com/fumieval/extensible
 description:         Extensible Products/Unions
@@ -19,8 +19,18 @@
   location: https://github.com/fumieval/extensible.git
 
 library
-  exposed-modules:     Data.Extensible
-  build-depends:       base == 4.*
+  exposed-modules:
+    Data.Extensible
+    Data.Extensible.Inclusion
+    Data.Extensible.Internal
+    Data.Extensible.League
+    Data.Extensible.Match
+    Data.Extensible.Plain
+    Data.Extensible.Product
+    Data.Extensible.Sum
+    Data.Extensible.Union
+  default-extensions: TypeOperators, DeriveDataTypeable
+  build-depends:       base == 4.*, ghc-prim
   hs-source-dirs:      src
   ghc-options: -Wall
   default-language:    Haskell2010
diff --git a/src/Data/Extensible.hs b/src/Data/Extensible.hs
--- a/src/Data/Extensible.hs
+++ b/src/Data/Extensible.hs
@@ -1,9 +1,3 @@
-{-# LANGUAGE DataKinds, TypeOperators, PolyKinds, KindSignatures, GADTs, MultiParamTypeClasses, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE Rank2Types #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE ViewPatterns, BangPatterns #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Extensible
@@ -15,8 +9,8 @@
 -- Portability :  non-portable
 --
 -- This package defines an extensible type-indexed product type and a union type.
--- Both are determined from the type-level list of elements which has kind @[k]@
--- and a wrapper (k -> *).
+-- Both are determined from the type-level list @[k]@
+-- and a wrapper @k -> *@.
 -- We can define ADTs not only for plain values, but also parameterized ones.
 --
 -- >>> let t = K0 (42 :: Int) <:* K0 "foo" <:* K0 (Just "bar") <:* Nil
@@ -28,307 +22,23 @@
 -- 42
 -----------------------------------------------------------------------------
 module Data.Extensible (
+  -- * Reexport
+  module Data.Extensible.Inclusion
+  , module Data.Extensible.Match
+  , module Data.Extensible.Plain
+  , module Data.Extensible.Product
+  , module Data.Extensible.Sum
   -- * Lookup
-    Position
+  , Position
   , runPosition
   , (∈)()
   , Member(..)
-  -- * Product
-  , (:*)(..)
-  , (<:*)
-  , unconsP
-  , hoistP
-  , outP
-  , sector
-  , sectorAt
-  , Generate(..)
-  -- * Sum
-  , (:|)(..)
-  , (<:|)
-  , exhaust
-  , inS
-  , picked
-  -- * Inclusion/Permutation
-  , Include(..)
-  -- * Pattern match
-  , Match(..)
-  , match
-  , mapMatch
-  -- * Monomorphic
-  , K0(..)
-  , (<%)
-  , pluck
-  , bury
-  , (<%|)
-  , record
-  , (<?%)
-  -- * Parameterized
-  , K1(..)
-  , Union(..)
-  , liftU
-  , (<?!)
   ) where
-import Unsafe.Coerce
-import Data.Bits
-import Data.Typeable
-import Control.Applicative
-
--- | The extensible product type
-data (h :: k -> *) :* (s :: [k]) where
-  Nil :: h :* '[]
-  Tree :: h x
-    -> h :* Half xs
-    -> h :* Half (Tail xs)
-    -> h :* (x ': xs)
-
-instance Show (h :* '[]) where
-  show Nil = "Nil"
-
-instance (Show (h :* xs), Show (h x)) => Show (h :* (x ': xs)) where
-  showsPrec d (unconsP -> (x, xs)) = showParen (d > 10) $
-     showsPrec 6 x
-    . showString " <:* "
-    . showsPrec 6 xs
-
-unconsP :: forall h x xs. h :* (x ': xs) -> (h x, h :* xs)
-unconsP (Tree a Nil _) = (a, lemmaHalfEmpty (Proxy :: Proxy xs) Nil)
-unconsP (Tree a bd c) = (a, let (b, d) = unconsP (unsafeCoerce bd) in unsafeCoerce $ Tree b (unsafeCoerce c) d)
-
-lemmaHalfEmpty :: (Half xs ~ '[]) => Proxy xs -> p '[] -> p xs
-lemmaHalfEmpty _ = unsafeCoerce
-
-lemmaHalfTail :: Proxy xs -> p (x ': Half (Tail xs)) -> p (Half (x ': xs))
-lemmaHalfTail _ = unsafeCoerce
-
--- | /O(log n)/ Add an element to a product.
-(<:*) :: forall h x xs. h x -> h :* xs -> h :* (x ': xs)
-a <:* Tree b c d = Tree a (lemmaHalfTail (Proxy :: Proxy (Tail xs)) $! b <:* d) c
-a <:* Nil = Tree a Nil Nil
-infixr 5 <:*
-
-hoistP :: (forall x. g x -> h x) -> g :* xs -> h :* xs
-hoistP t (Tree h a b) = Tree (t h) (hoistP t a) (hoistP t b)
-hoistP _ Nil = Nil
-
--- | /O(log n)/ Pick a specific element.
-outP :: forall h x xs. (x ∈ xs) => h :* xs -> h x
-outP = view $ sectorAt (position :: Position x xs)
-{-# INLINE outP #-}
-
--- | /O(log n)/ A lens for a specific element.
-sector :: forall h x xs f. (Functor f, x ∈ xs) => (h x -> f (h x)) -> h :* xs -> f (h :* xs)
-sector = sectorAt (position :: Position x xs)
-{-# INLINE sector #-}
-
-view :: ((a -> Const a a) -> (s -> Const a s)) -> s -> a
-view l = unsafeCoerce (l Const)
-{-# INLINE view #-}
-
--- | /O(log n)/
-sectorAt :: forall h x xs f. (Functor f) => Position x xs -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)
-sectorAt pos0 f = go pos0 where
-  go :: forall t. Position x t -> h :* t -> f (h :* t)
-  go pos (Tree h a b) = case runPosition pos of
-    Left Refl -> fmap (\h' -> Tree h' a b) (f h)
-    Right (Position m) -> case m .&. 1 of
-      0 -> fmap (\a' -> Tree h a' b)
-        $ go (Position (shiftR m 1) :: Position x (Half (Tail t))) a
-      _ -> fmap (\b' -> Tree h a b')
-        $ go (Position (shiftR m 1) :: Position x (Half (Tail (Tail t)))) b
-  go _ Nil = error "Impossible"
-{-# INLINE sectorAt #-}
-
--- | /O(log n)/ lift a value.
-inS :: (x ∈ xs) => h x -> h :| xs
-inS = UnionAt position
-{-# INLINE inS #-}
-
-picked :: forall f h x xs. (x ∈ xs, Applicative f) => (h x -> f (h x)) -> h :| xs -> f (h :| xs)
-picked f u@(UnionAt (Position n) h)
-  | n == m = fmap (UnionAt (Position n)) $ f (unsafeCoerce h)
-  | otherwise = pure u
-  where
-    Position m = position :: Position x xs
-
-runPosition :: Position x (y ': xs) -> Either (x :~: y) (Position x xs)
-runPosition (Position 0) = Left (unsafeCoerce Refl)
-runPosition (Position n) = Right (Position (n - 1))
-{-# INLINE runPosition #-}
-
--- | /O(1)/ Naive pattern match
-(<:|) :: (h x -> r) -> (h :| xs -> r) -> h :| (x ': xs) -> r
-(<:|) r c = \(UnionAt pos h) -> case runPosition pos of
-  Left Refl -> r h
-  Right pos' -> c (UnionAt pos' h)
-infixr 1 <:|
-{-# INLINE (<:|) #-}
-
-exhaust :: h :| '[] -> r
-exhaust _ = error "Impossible"
-
--- | The extensible sum type
-data (h :: k -> *) :| (s :: [k]) where
-  UnionAt :: Position x xs -> h x -> h :| xs
-
-instance Show (h :| '[]) where
-  show = exhaust
-
-instance (Show (h x), Show (h :| xs)) => Show (h :| (x ': xs)) where
-  showsPrec d = (\h -> showParen (d > 10) $ showString "inS " . showsPrec 11 h)
-    <:| showsPrec d
-
-class Generate (xs :: [k]) where
-  generate :: (forall x. Position x xs -> h x) -> h :* xs
-
-instance Generate '[] where
-  generate _ = Nil
-  {-# INLINE generate #-}
-instance Generate xs => Generate (x ': xs) where
-  generate f = f (Position 0) <:* generate (f . succPos) where
-    succPos (Position n) = Position (n + 1)
-    {-# INLINE succPos #-}
-  {-# INLINE generate #-}
-
-newtype K0 a = K0 { getK0 :: a } deriving (Eq, Ord, Read, Typeable)
-
--- | /O(log n)/ Add a plain value to a product.
-(<%) :: x -> K0 :* xs -> K0 :* (x ': xs)
-(<%) = unsafeCoerce (<:*)
-{-# INLINE (<%) #-}
-infixr 5 <%
-
-pluck :: (x ∈ xs) => K0 :* xs -> x
-pluck = getK0 . outP
-
-bury :: (x ∈ xs) => x -> K0 :| xs
-bury = inS . K0
-
-(<%|) :: (x -> r) -> (K0 :| xs -> r) -> K0 :| (x ': xs) -> r
-(<%|) = unsafeCoerce (<:|)
-
-instance Show a => Show (K0 a) where
-  showsPrec d (K0 a) = showParen (d > 10) $ showString "K0 " . showsPrec 11 a
-
--- | /O(log n)/ A lens for a plain value in a product.
-record :: forall f x xs. (x ∈ xs, Functor f) => (x -> f x) -> (K0 :* xs -> f (K0 :* xs))
-record = unsafeCoerce (sector :: (K0 x -> f (K0 x)) -> (K0 :* xs -> f (K0 :* xs)))
-{-# INLINE record #-}
-
-newtype K1 a f = K1 { getK1 :: f a } deriving (Eq, Ord, Read, Typeable)
-
-instance Show (f a) => Show (K1 a f) where
-  showsPrec d (K1 a) = showParen (d > 10) $ showString "K1 " . showsPrec 11 a
-
-newtype Match h a x = Match { runMatch :: h x -> a }
-
-mapMatch :: (a -> b) -> Match h a x -> Match h b x
-mapMatch f (Match g) = Match (f . g)
-{-# INLINE mapMatch #-}
-
--- | /O(log n)/ Perform pattern match.
-match :: Match h a :* xs -> h :| xs -> a
-match p (UnionAt pos h) = runMatch (view (sectorAt pos) p) h
-{-# INLINE match #-}
-
-(<?%) :: (x -> a) -> Match K0 a :* xs -> Match K0 a :* (x ': xs)
-(<?%) = unsafeCoerce (<:*)
-infixr 1 <?%
-
-(<?!) :: (f x -> a) -> Match (K1 x) a :* xs -> Match (K1 x) a :* (f ': fs)
-(<?!) = unsafeCoerce (<:*)
-infixr 1 <?!
-
-newtype Union fs a = Union { getUnion :: K1 a :| fs }
-
-liftU :: (f ∈ fs) => f a -> Union fs a
-liftU = Union . inS . K1
-{-# INLINE liftU #-}
-
-instance Show (Union '[] a) where
-  show (Union u) = exhaust u
-
-instance (Show (f a), Show (Union fs a)) => Show (Union (f ': fs) a) where
-  showsPrec d (Union u) = (\(K1 f) -> showParen (d > 10) $ showString "liftU " . showsPrec 11 f)
-    <:| showsPrec d . Union
-    $ u
-
-instance Functor (Union '[]) where
-  fmap _ = exhaust . getUnion
-
-instance (Functor f, Functor (Union fs)) => Functor (Union (f ': fs)) where
-  fmap f (Union (UnionAt pos@(Position n) (K1 h))) = case runPosition pos of
-    Left Refl -> Union $ UnionAt pos $ K1 (fmap f h)
-    Right pos' -> case fmap f (Union (UnionAt pos' (K1 h))) of
-      Union (UnionAt _ h') -> Union (UnionAt (Position n) h')
-
----------------------------------------------------------------------
-
-newtype Position (x :: k) (xs :: [k]) = Position Int deriving (Show, Eq, Ord)
-
-type (∈) = Member
-
-class Member (x :: k) (xs :: [k]) where
-  position :: Position x xs
-
-instance Record (Lookup x xs) => Member x xs where
-  position = Position $ theInt (Proxy :: Proxy (Lookup x xs))
-  {-# INLINE position #-}
-
-class Include (xs :: [k]) (ys :: [k]) where
-  -- | /O(m log n)/ Select some elements.
-  shrink :: h :* ys -> h :* xs
-  -- | /O(m log n)/ Embed to a larger union.
-  spread :: h :| xs -> h :| ys
-
-instance Include '[] xs where
-  shrink _ = Nil
-  spread = exhaust
-
-instance (x ∈ ys, Include xs ys) => Include (x ': xs) ys where
-  shrink ys = outP ys <:* shrink ys
-  spread xs = inS <:| spread $ xs
-
-type family Half (xs :: [k]) :: [k] where
-  Half '[] = '[]
-  Half (x ': y ': zs) = x ': zs
-  Half (x ': '[]) = x ': '[]
-
-type family Tail (xs :: [k]) :: [k] where
-  Tail (x ': xs) = xs
-  Tail '[] = '[]
-
-data Nat = Zero | DNat Nat | SDNat Nat | NotFound
-
-retagD :: (Proxy n -> a) -> proxy (DNat n) -> a
-retagD f _ = f Proxy
-{-# INLINE retagD #-}
-
-retagSD :: (Proxy n -> a) -> proxy (SDNat n) -> a
-retagSD f _ = f Proxy
-{-# INLINE retagSD #-}
-
-class Record n where
-  theInt :: Proxy n -> Int
-
-instance Record Zero where
-  theInt _ = 0
-  {-# INLINE theInt #-}
-
-instance Record n => Record (DNat n) where
-  theInt = (\n -> n + n) <$> retagD theInt
-  {-# INLINE theInt #-}
-
-instance Record n => Record (SDNat n) where
-  theInt = (\n -> n + n + 1) <$> retagSD theInt
-  {-# INLINE theInt #-}
-
-type family Lookup (x :: k) (xs :: [k]) :: Nat where
-  Lookup x (x ': xs) = Zero
-  Lookup x (y ': ys) = Succ (Lookup x ys)
-  Lookup x '[] = NotFound
+import Data.Extensible.Internal
+import Data.Extensible.Inclusion
+import Data.Extensible.Match
+import Data.Extensible.Plain
+import Data.Extensible.Product
+import Data.Extensible.Sum
+-------------------------------------------------------------
 
-type family Succ (x :: Nat) :: Nat where
-  Succ Zero = SDNat Zero
-  Succ (DNat n) = SDNat n
-  Succ (SDNat n) = DNat (Succ n)
-  Succ NotFound = NotFound
diff --git a/src/Data/Extensible/Inclusion.hs b/src/Data/Extensible/Inclusion.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Inclusion.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE ScopedTypeVariables, ConstraintKinds, FlexibleContexts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Inclusion
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+------------------------------------------------------------------------
+module Data.Extensible.Inclusion where
+
+import Data.Extensible.Product
+import Data.Extensible.Sum
+import Data.Extensible.Internal
+import Data.Proxy
+
+-- | Unicode alias for 'Include'
+type xs ⊆ ys = Include ys xs
+
+-- | @ys@ contains @xs@
+type Include ys xs = Forall (Member ys) xs
+
+-- | Reify the inclusion of type level sets.
+inclusion :: forall xs ys. Include ys xs => Position ys :* xs
+inclusion = generateFor (Proxy :: Proxy (Member ys)) (const membership)
+
+-- | /O(m log n)/ Select some elements.
+shrink :: (xs ⊆ ys) => h :* ys -> h :* xs
+shrink h = hmap (\pos -> hlookup pos h) inclusion
+
+-- | /O(m log n)/ Embed to a larger union.
+spread :: (xs ⊆ ys) => h :| xs -> h :| ys
+spread (UnionAt pos h) = UnionAt (hlookup pos inclusion) h
diff --git a/src/Data/Extensible/Internal.hs b/src/Data/Extensible/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Internal.hs
@@ -0,0 +1,120 @@
+{-# LANGUAGE DataKinds, ConstraintKinds, KindSignatures, PolyKinds #-}
+{-# LANGUAGE GADTs, TypeFamilies, TypeOperators #-}
+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Data.Extensible.Internal (Position
+  , runPosition
+  , comparePosition
+  , Nav(..)
+  , navigate
+  , here
+  , navL
+  , navR
+  , Member(..)
+  , (∈)()
+  , Nat(..)
+  , Record(..)
+  , Lookup
+  , Succ
+  , Half
+  , Tail
+  , lemmaHalfTail) where
+import Data.Type.Equality
+import Data.Proxy
+import Control.Applicative
+import Unsafe.Coerce
+import Data.Typeable
+
+-- | The position of @x@ in the type level set @xs@.
+newtype Position (xs :: [k]) (x :: k) = Position Int deriving (Show, Eq, Ord, Typeable)
+
+-- | Embodies a type equivalence to ensure that the 'Position' points the first element.
+runPosition :: Position (y ': xs) x -> Either (x :~: y) (Position xs x)
+runPosition (Position 0) = Left (unsafeCoerce Refl)
+runPosition (Position n) = Right (Position (n - 1))
+{-# INLINE runPosition #-}
+
+comparePosition :: Position xs x -> Position xs y -> Maybe (x :~: y)
+comparePosition (Position m) (Position n)
+  | m == n = Just (unsafeCoerce Refl)
+  | otherwise = Nothing
+
+navigate :: Position xs x -> Nav xs x
+navigate (Position 0) = unsafeCoerce Here
+navigate (Position n) = let (m, r) = divMod n 2 in case r of
+  0 -> unsafeCoerce $ NavL $ Position m
+  _ -> unsafeCoerce $ NavR $ Position m
+
+data Nav xs x where
+  Here :: Nav (x ': xs) x
+  NavL :: Position (Half xs) x -> Nav (e ': xs) x
+  NavR :: Position (Half (Tail xs)) x -> Nav (e ': xs) x
+
+here :: Position (x ': xs) x
+here = Position 0
+
+navL :: Position (Half xs) y -> Position (x ': xs) y
+navL (Position x) = Position (x * 2 + 1)
+
+navR :: Position (Half (Tail xs)) y -> Position (x ': xs) y
+navR (Position x) = Position ((x + 1) * 2)
+
+-- | Unicode flipped alias for 'Member'
+type x ∈ xs = Member xs x
+
+-- | @Member x xs@ or @x ∈ xs@ indicates that @x@ is an element of @xs@.
+class Member (xs :: [k]) (x :: k) where
+  membership :: Position xs x
+
+instance Record (Lookup x xs) => Member xs x where
+  membership = Position $ theInt (Proxy :: Proxy (Lookup x xs))
+  {-# INLINE membership #-}
+
+type family Half (xs :: [k]) :: [k] where
+  Half '[] = '[]
+  Half (x ': y ': zs) = x ': zs
+  Half (x ': '[]) = x ': '[]
+
+type family Tail (xs :: [k]) :: [k] where
+  Tail (x ': xs) = xs
+  Tail '[] = '[]
+
+data Nat = Zero | DNat Nat | SDNat Nat | NotFound
+
+retagD :: (Proxy n -> a) -> proxy (DNat n) -> a
+retagD f _ = f Proxy
+{-# INLINE retagD #-}
+
+retagSD :: (Proxy n -> a) -> proxy (SDNat n) -> a
+retagSD f _ = f Proxy
+{-# INLINE retagSD #-}
+
+class Record n where
+  theInt :: Proxy n -> Int
+
+instance Record Zero where
+  theInt _ = 0
+  {-# INLINE theInt #-}
+
+instance Record n => Record (DNat n) where
+  theInt = (*2) <$> retagD theInt
+  {-# INLINE theInt #-}
+
+instance Record n => Record (SDNat n) where
+  theInt = (+1) <$> (*2) <$> retagSD theInt
+  {-# INLINE theInt #-}
+
+type family Lookup (x :: k) (xs :: [k]) :: Nat where
+  Lookup x (x ': xs) = Zero
+  Lookup x (y ': ys) = Succ (Lookup x ys)
+  Lookup x '[] = NotFound
+
+type family Succ (x :: Nat) :: Nat where
+  Succ Zero = SDNat Zero
+  Succ (DNat n) = SDNat n
+  Succ (SDNat n) = DNat (Succ n)
+  Succ NotFound = NotFound
+
+-- GHC can't prove this
+lemmaHalfTail :: Proxy xs -> p (x ': Half (Tail xs)) -> p (Half (x ': xs))
+lemmaHalfTail _ = unsafeCoerce
diff --git a/src/Data/Extensible/League.hs b/src/Data/Extensible/League.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/League.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE Rank2Types, DataKinds #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.League
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Efficient extensible functor
+------------------------------------------------------------------------
+module Data.Extensible.League where
+
+import Data.Extensible.Internal
+import Data.Extensible.Sum
+import Data.Extensible.Product
+import Data.Extensible.Match
+import Data.Typeable
+
+-- | A much more efficient representation for 'Union' of 'Functor's.
+newtype League fs a = League { getLeague :: Fuse a :| fs } deriving Typeable
+
+-- | fast fmap
+instance Functor (League fs) where
+  fmap f (League (UnionAt pos s)) = League (UnionAt pos (mapFuse f s))
+  {-# INLINE fmap #-}
+
+-- | /O(log n)/ Embed a functor.
+liftL :: (Functor f, f ∈ fs) => f a -> League fs a
+liftL f = League $ embed $ Fuse $ \g -> fmap g f
+{-# INLINE liftL #-}
+
+-- | Flipped <http://hackage.haskell.org/package/kan-extensions-4.1.0.1/docs/Data-Functor-Yoneda.html Yoneda>
+newtype Fuse a f = Fuse { getFuse :: forall b. (a -> b) -> f b }
+
+-- | Fuse 'Fuse' to retract a substantial functor.
+meltdown :: Fuse a f -> f a
+meltdown (Fuse f) = f id
+{-# INLINE meltdown #-}
+
+-- | 'fmap' for the content.
+mapFuse :: (a -> b) -> Fuse a f -> Fuse b f
+mapFuse f (Fuse g) = Fuse (\h -> g (h . f))
+{-# INLINE mapFuse #-}
+
+-- | Prepend a clause for @'Match' ('Fuse' x)@ as well as ('<?!').
+(<?~) :: (f x -> a) -> Match (Fuse x) a :* fs -> Match (Fuse x) a :* (f ': fs)
+(<?~) f = (<:*) (Match (f . meltdown))
+infixr 1 <?~
diff --git a/src/Data/Extensible/Match.hs b/src/Data/Extensible/Match.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Match.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE PolyKinds #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.League
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- Pattern matching
+------------------------------------------------------------------------
+module Data.Extensible.Match (
+  Match(..)
+  , match
+  , mapMatch
+  , caseOf) where
+
+import Data.Extensible.Product
+import Data.Extensible.Sum
+import Data.Typeable
+
+-- | Turn a wrapper type into one clause that returns @a@.
+newtype Match h a x = Match { runMatch :: h x -> a } deriving Typeable
+
+-- | Applies a function to the result of 'Match'.
+mapMatch :: (a -> b) -> Match h a x -> Match h b x
+mapMatch f (Match g) = Match (f . g)
+{-# INLINE mapMatch #-}
+
+-- | /O(log n)/ Perform pattern matching.
+match :: Match h a :* xs -> h :| xs -> a
+match p (UnionAt pos h) = runMatch (hlookup pos p) h
+{-# INLINE match #-}
+
+-- | Flipped `match`
+caseOf :: h :| xs -> Match h a :* xs -> a
+caseOf = flip match
+{-# INLINE caseOf #-}
+infix 0 `caseOf`
diff --git a/src/Data/Extensible/Plain.hs b/src/Data/Extensible/Plain.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Plain.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE DataKinds #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Plain
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+------------------------------------------------------------------------
+module Data.Extensible.Plain (
+  K0(..)
+  , (<%)
+  , pluck
+  , bury
+  , (<%|)
+  , record
+  , (<?%)
+  )where
+import Data.Extensible.Internal
+import Data.Extensible.Product
+import Data.Extensible.Sum
+import Data.Extensible.Match
+import Data.Typeable
+import Unsafe.Coerce
+-- | Just a value.
+newtype K0 a = K0 { getK0 :: a } deriving (Eq, Ord, Read, Typeable)
+
+instance Show a => Show (K0 a) where
+  showsPrec d (K0 a) = showParen (d > 10) $ showString "K0 " . showsPrec 11 a
+
+-- | /O(log n)/ Add a plain value to a product.
+(<%) :: x -> K0 :* xs -> K0 :* (x ': xs)
+(<%) = unsafeCoerce (<:*)
+{-# INLINE (<%) #-}
+infixr 5 <%
+
+-- | Extract a plain value.
+pluck :: (x ∈ xs) => K0 :* xs -> x
+pluck = getK0 . hlookup membership
+
+-- | Embed a plain value.
+bury :: (x ∈ xs) => x -> K0 :| xs
+bury = embed . K0
+
+-- | Naive pattern matching for a plain value.
+(<%|) :: (x -> r) -> (K0 :| xs -> r) -> K0 :| (x ': xs) -> r
+(<%|) = unsafeCoerce (<:|)
+
+-- | /O(log n)/ A lens for a plain value in a product.
+record :: (x ∈ xs, Functor f) => (x -> f x) -> (K0 :* xs -> f (K0 :* xs))
+record f = sector $ unsafeCoerce f `asTypeOf` (fmap K0 . f . getK0)
+{-# INLINE record #-}
+
+-- | Prepend a clause for a plain value.
+(<?%) :: (x -> a) -> Match K0 a :* xs -> Match K0 a :* (x ': xs)
+(<?%) = unsafeCoerce (<:*)
+infixr 1 <?%
diff --git a/src/Data/Extensible/Product.hs b/src/Data/Extensible/Product.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Product.hs
@@ -0,0 +1,172 @@
+{-# LANGUAGE Rank2Types, GADTs #-}
+{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, ConstraintKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Product
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+------------------------------------------------------------------------
+module Data.Extensible.Product (
+  -- * Product
+  (:*)(..)
+  , (<:*)
+  , huncons
+  , hmap
+  , hzipWith
+  , hzipWith3
+  , hfoldMap
+  , htraverse
+  , hlookup
+  , sector
+  , sectorAt
+  , Generate(..)
+  , Forall(..)) where
+
+import Data.Extensible.Internal
+import Unsafe.Coerce
+import Data.Typeable
+import Control.Applicative
+import Data.Monoid
+
+-- | The extensible product type
+data (h :: k -> *) :* (s :: [k]) where
+  Nil :: h :* '[]
+  Tree :: h x
+    -> h :* Half xs
+    -> h :* Half (Tail xs)
+    -> h :* (x ': xs)
+
+deriving instance Typeable (:*)
+
+instance Show (h :* '[]) where
+  show Nil = "Nil"
+
+instance (Show (h :* xs), Show (h x)) => Show (h :* (x ': xs)) where
+  showsPrec d t = let (x, xs) = huncons t in showParen (d > 10) $
+     showsPrec 6 x
+    . showString " <:* "
+    . showsPrec 6 xs
+
+-- | Extract the tail of the product.
+htail :: h :* (x ': xs) -> h :* xs
+htail (Tree _ a@(Tree h _ _) b) = unsafeCoerce (Tree h) b (htail a)
+htail (Tree _ Nil _) = unsafeCoerce Nil
+
+-- | Split a product to the head and the tail.
+huncons :: forall h x xs. h :* (x ': xs) -> (h x, h :* xs)
+huncons t@(Tree a _ _) = (a, htail t)
+
+-- | /O(log n)/ Add an element to a product.
+(<:*) :: forall h x xs. h x -> h :* xs -> h :* (x ': xs)
+a <:* Tree b c d = Tree a (lemmaHalfTail (Proxy :: Proxy (Tail xs)) $! b <:* d) c
+a <:* Nil = Tree a Nil Nil
+infixr 5 <:*
+
+-- | Transform every elements in a union, preserving the order.
+hmap :: (forall x. g x -> h x) -> g :* xs -> h :* xs
+hmap t (Tree h a b) = Tree (t h) (hmap t a) (hmap t b)
+hmap _ Nil = Nil
+
+-- | 'zipWith' for heterogeneous product
+hzipWith :: (forall x. f x -> g x -> h x) -> f :* xs -> g :* xs -> h :* xs
+hzipWith t (Tree f a b) (Tree g c d) = Tree (t f g) (hzipWith t a c) (hzipWith t b d)
+hzipWith _ Nil _ = Nil
+hzipWith _ _ Nil = Nil
+
+-- | 'zipWith3' for heterogeneous product
+hzipWith3 :: (forall x. f x -> g x -> h x -> i x) -> f :* xs -> g :* xs -> h :* xs -> i :* xs
+hzipWith3 t (Tree f a b) (Tree g c d) (Tree h e f') = Tree (t f g h) (hzipWith3 t a c e) (hzipWith3 t b d f')
+hzipWith3 _ Nil _ _ = Nil
+hzipWith3 _ _ Nil _ = Nil
+hzipWith3 _ _ _ Nil = Nil
+
+-- | Combine all elements.
+hfoldMap :: Monoid a => (forall x. h x -> a) -> h :* xs -> a
+hfoldMap f (Tree h a b) = f h <> hfoldMap f a <> hfoldMap f b
+hfoldMap _ Nil = mempty
+
+-- | Traverse all elements.
+htraverse :: Applicative f => (forall x. h x -> f (h x)) -> h :* xs -> f (h :* xs)
+htraverse f (Tree h a b) = Tree <$> f h <*> htraverse f a <*> htraverse f b
+htraverse _ Nil = pure Nil
+
+-- | Pick up an elemtnt.
+hlookup :: Position xs x -> h :* xs -> h x
+hlookup = view . sectorAt
+{-# INLINE hlookup #-}
+
+-- | Composition for a class and a wrapper,
+class c (h x) => ClassComp c h x
+instance c (h x) => ClassComp c h x
+
+instance Forall (ClassComp Eq h) xs => Eq (h :* xs) where
+  (==) = (aggr.) . hzipWith3 (\pos -> (Const' .) . unwrapEq (view (sectorAt pos) dic))
+    (generateFor c id) where
+      dic = generateFor c $ const $ WrapEq (==)
+      aggr = getAll . hfoldMap (All . getConst')
+      c = Proxy :: Proxy (ClassComp Eq h)
+
+instance (Forall (ClassComp Eq h) xs, Forall (ClassComp Ord h) xs) => Ord (h :* xs) where
+  compare = (aggr.) . hzipWith3 (\pos -> (Const' .) . unwrapOrd (view (sectorAt pos) dic))
+    (generateFor c id) where
+      dic = generateFor c $ const $ WrapOrd compare
+      aggr = hfoldMap getConst'
+      c = Proxy :: Proxy (ClassComp Ord h)
+
+newtype Const' a x = Const' { getConst' :: a } deriving Show
+
+newtype WrapEq h x = WrapEq { unwrapEq :: h x -> h x -> Bool }
+
+newtype WrapOrd h x = WrapOrd { unwrapOrd :: h x -> h x -> Ordering }
+
+-- | /O(log n)/ A lens for a specific element.
+sector :: forall h x xs f. (Functor f, x ∈ xs) => (h x -> f (h x)) -> h :* xs -> f (h :* xs)
+sector = sectorAt (membership :: Position xs x)
+{-# INLINE sector #-}
+
+view :: ((a -> Const a a) -> (s -> Const a s)) -> s -> a
+view l = unsafeCoerce (l Const)
+{-# INLINE view #-}
+
+-- | /O(log n)/ A lens for a value in a known position.
+sectorAt :: forall h x xs f. (Functor f) => Position xs x -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)
+sectorAt pos0 f = go pos0 where
+  go :: forall t. Position t x -> h :* t -> f (h :* t)
+  go pos (Tree h a b) = case navigate pos of
+    Here -> fmap (\h' -> Tree h' a b) (f h)
+    NavL p -> fmap (\a' -> Tree h a' b) $ go p a
+    NavR p -> fmap (\b' -> Tree h a b') $ go p b
+  go _ Nil = error "Impossible"
+{-# INLINE sectorAt #-}
+
+-- | Given a function that maps types to values, we can "collect" entities all you want.
+class Generate (xs :: [k]) where
+  generate :: (forall x. Position xs x -> h x) -> h :* xs
+
+instance Generate '[] where
+  generate _ = Nil
+  {-# INLINE generate #-}
+
+instance (Generate (Half xs), Generate (Half (Tail xs))) => Generate (x ': xs) where
+  generate f = Tree (f here) (generate (f . navL)) (generate (f . navR)) where
+  {-# INLINE generate #-}
+
+-- | Guarantees the all elements satisfies the predicate.
+class Forall c (xs :: [k]) where
+  generateFor :: Proxy c -> (forall x. c x => Position xs x -> h x) -> h :* xs
+
+instance Forall c '[] where
+  generateFor _ _ = Nil
+  {-# INLINE generateFor #-}
+
+instance (c x, Forall c (Half xs), Forall c (Half (Tail xs))) => Forall c (x ': xs) where
+  generateFor proxy f = Tree (f here) (generateFor proxy (f . navL)) (generateFor proxy (f . navR)) where
+  {-# INLINE generateFor #-}
diff --git a/src/Data/Extensible/Sum.hs b/src/Data/Extensible/Sum.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Sum.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE Rank2Types, GADTs #-}
+{-# LANGUAGE DataKinds, KindSignatures, PolyKinds, ConstraintKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Sum
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+------------------------------------------------------------------------
+module Data.Extensible.Sum (
+   (:|)(..)
+  , hoist
+  , embed
+  , (<:|)
+  , exhaust
+  , picked
+  ) where
+
+import Data.Extensible.Internal
+import Data.Type.Equality
+import Control.Applicative
+import Data.Typeable
+
+-- | The extensible sum type
+data (h :: k -> *) :| (s :: [k]) where
+  UnionAt :: Position xs x -> h x -> h :| xs
+deriving instance Typeable (:|)
+
+-- | Change the wrapper.
+hoist :: (forall x. g x -> h x) -> g :| xs -> h :| xs
+hoist f (UnionAt pos h) = UnionAt pos (f h)
+{-# INLINE hoist #-}
+
+-- | /O(log n)/ lift a value.
+embed :: (x ∈ xs) => h x -> h :| xs
+embed = UnionAt membership
+{-# INLINE embed #-}
+
+instance Show (h :| '[]) where
+  show = exhaust
+
+instance (Show (h x), Show (h :| xs)) => Show (h :| (x ': xs)) where
+  showsPrec d = (\h -> showParen (d > 10) $ showString "inS " . showsPrec 11 h)
+    <:| showsPrec d
+
+-- | /O(1)/ Naive pattern match
+(<:|) :: (h x -> r) -> (h :| xs -> r) -> h :| (x ': xs) -> r
+(<:|) r c = \(UnionAt pos h) -> case runPosition pos of
+  Left Refl -> r h
+  Right pos' -> c (UnionAt pos' h)
+infixr 1 <:|
+{-# INLINE (<:|) #-}
+
+-- | There is no empty union.
+exhaust :: h :| '[] -> r
+exhaust _ = error "Impossible"
+
+-- | A traversal that tries to point a specific element.
+picked :: forall f h x xs. (x ∈ xs, Applicative f) => (h x -> f (h x)) -> h :| xs -> f (h :| xs)
+picked f u@(UnionAt pos h) = case comparePosition (membership :: Position xs x) pos of
+  Just Refl -> fmap (UnionAt pos) (f h)
+  Nothing -> pure u
diff --git a/src/Data/Extensible/Union.hs b/src/Data/Extensible/Union.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible/Union.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Extensible.Union
+-- Copyright   :  (c) Fumiaki Kinoshita 2015
+-- License     :  BSD3
+--
+-- Maintainer  :  Fumiaki Kinoshita <fumiexcel@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+------------------------------------------------------------------------
+module Data.Extensible.Union (K1(..)
+  , (<?!)
+  , Union(..)
+  , liftU
+  ) where
+
+import Data.Typeable
+import Data.Extensible.Internal
+import Data.Extensible.Sum
+import Data.Extensible.Product
+import Data.Extensible.Match
+import Unsafe.Coerce
+
+-- | Wrap a type that has a kind @* -> *@.
+newtype K1 a f = K1 { getK1 :: f a } deriving (Eq, Ord, Read, Typeable)
+
+instance Show (f a) => Show (K1 a f) where
+  showsPrec d (K1 a) = showParen (d > 10) $ showString "K1 " . showsPrec 11 a
+
+-- | Prepend a clause for a parameterized value.
+(<?!) :: (f x -> a) -> Match (K1 x) a :* xs -> Match (K1 x) a :* (f ': fs)
+(<?!) = unsafeCoerce (<:*)
+infixr 1 <?!
+
+-- | A wrapper for @'K1' a ':|'' fs@ for having a kind @* -> *@.
+newtype Union fs a = Union { getUnion :: K1 a :| fs } deriving Typeable
+
+-- | /O(log n)/ Lift a value.
+liftU :: (f ∈ fs) => f a -> Union fs a
+liftU = Union . embed . K1
+{-# INLINE liftU #-}
+
+instance Show (Union '[] a) where
+  show (Union u) = exhaust u
+
+instance (Show (f a), Show (Union fs a)) => Show (Union (f ': fs) a) where
+  showsPrec d (Union u) = (\(K1 f) -> showParen (d > 10) $ showString "liftU " . showsPrec 11 f)
+    <:| showsPrec d . Union
+    $ u
+
+instance Functor (Union '[]) where
+  fmap _ = exhaust . getUnion
+
+-- | slow fmap
+instance (Functor f, Functor (Union fs)) => Functor (Union (f ': fs)) where
+  fmap f (Union (UnionAt pos (K1 h))) = case runPosition pos of
+    Left Refl -> Union $ UnionAt pos $ K1 (fmap f h)
+    Right pos' -> case fmap f (Union (UnionAt pos' (K1 h))) of
+      Union (UnionAt _ h') -> Union (UnionAt (unsafeCoerce pos) h')