diff --git a/.gitignore b/.gitignore
new file mode 100644
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,58 @@
+dist
+cabal-dev
+*.o
+*.hi
+*.chi
+*.chs.h
+.virtualenv
+.hsenv
+.cabal-sandbox/
+cabal.sandbox.config
+cabal.config
+
+# =========================
+# Operating System Files
+# =========================
+
+# OSX
+# =========================
+
+.DS_Store
+.AppleDouble
+.LSOverride
+
+# Thumbnails
+._*
+
+# Files that might appear on external disk
+.Spotlight-V100
+.Trashes
+
+# Directories potentially created on remote AFP share
+.AppleDB
+.AppleDesktop
+Network Trash Folder
+Temporary Items
+.apdisk
+
+# Windows
+# =========================
+
+# Windows image file caches
+Thumbs.db
+ehthumbs.db
+
+# Folder config file
+Desktop.ini
+
+# Recycle Bin used on file shares
+$RECYCLE.BIN/
+
+# Windows Installer files
+*.cab
+*.msi
+*.msm
+*.msp
+
+# Windows shortcuts
+*.lnk
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, Fumiaki Kinoshita
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Fumiaki Kinoshita nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/extensible.cabal b/extensible.cabal
new file mode 100644
--- /dev/null
+++ b/extensible.cabal
@@ -0,0 +1,24 @@
+name:                extensible
+version:             0.0
+synopsis:            Extensible ADTs
+homepage:            https://github.com/fumieval/extensible
+license:             BSD3
+license-file:        LICENSE
+author:              Fumiaki Kinoshita
+maintainer:          Fumiaki Kinoshita <fumiexcel@gmail.com>
+copyright:           Copyright (C) 2015 Fumiaki Kinoshita
+category:            Data
+build-type:          Simple
+extra-source-files:
+    .gitignore
+cabal-version:       >=1.10
+
+source-repository head
+  type: git
+  location: https://github.com/fumieval/extensible.git
+
+library
+  exposed-modules:     Data.Extensible
+  build-depends:       base == 4.*
+  hs-source-dirs:      src
+  default-language:    Haskell2010
diff --git a/src/Data/Extensible.hs b/src/Data/Extensible.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Extensible.hs
@@ -0,0 +1,194 @@
+{-# LANGUAGE DataKinds, TypeOperators, PolyKinds, KindSignatures, GADTs, MultiParamTypeClasses, TypeFamilies, FlexibleInstances, FlexibleContexts, UndecidableInstances, ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE ViewPatterns #-}
+module Data.Extensible (
+  -- * Lookup
+  Position
+  , (∈)(..)
+  -- * Product
+  , (:*)(..)
+  , (<:*)
+  , unconsP
+  , outP
+  , record
+  , recordAt
+  -- * Sum
+  , (:|)(..)
+  , (<:|)
+  , exhaust
+  , inS
+  -- * Utilities
+  , K0(..)
+  , platter
+  , (<%)
+  , K1(..)
+  , Union(..)
+  , liftU
+  , Match(..)
+  , match
+  , (<?%)
+  , (<?!)
+  ) 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 :: h :* (x ': xs) -> (h x, h :* xs)
+unconsP (Tree a Nil _) = (a, unsafeCoerce Nil)
+unconsP (Tree a bd c) = (a, let (b, d) = unconsP (unsafeCoerce bd) in unsafeCoerce $ Tree b (unsafeCoerce c) d)
+
+-- | /O(log n)/ Add an element to a product.
+(<:*) :: h x -> h :* xs -> h :* (x ': xs)
+a <:* Nil = Tree a Nil Nil
+a <:* Tree b c d = Tree a (unsafeCoerce (<:*) b d) c --  (Half (x1 : xs1) ~ (x1 : Half (Tail xs1)))
+infixr 5 <:*
+
+-- | /O(log n)/ Pick a specific element.
+outP :: forall h x xs. (x ∈ xs) => h :* xs -> h x
+outP = getConst . recordAt (position :: Position x xs) Const
+
+-- | /O(log n)/ A lens for a specific element.
+record :: forall h x xs f. (Functor f, x ∈ xs) => (h x -> f (h x)) -> h :* xs -> f (h :* xs)
+record = recordAt (position :: Position x xs)
+
+view :: ((a -> Const a a) -> (s -> Const a s)) -> s -> a
+view l = getConst . l Const
+
+recordAt :: forall h x xs f. (Functor f) => Position x xs -> (h x -> f (h x)) -> h :* xs -> f (h :* xs)
+recordAt (Position x) f = go x where
+  go 0 (Tree h a b) = fmap (\h' -> Tree h' a b) $ unsafeCoerce f $ h
+  go n (Tree h a b) = case divMod (n - 1) 2 of
+    (m, 0) -> fmap (\a' -> Tree h a' b) $ unsafeCoerce go m a
+    (m, _) -> fmap (\b' -> Tree h a b') $ unsafeCoerce go m b
+  go _ Nil = error "Impossible"
+
+-- | /O(log n)/
+inS :: (x ∈ xs) => h x -> h :| xs
+inS = UnionAt position
+
+-- | /O(n)/ Naive pattern match
+(<:|) :: (h x -> r) -> (h :| xs -> r) -> h :| (x ': xs) -> r
+(<:|) r _ (UnionAt (Position 0) h) = r (unsafeCoerce h)
+(<:|) _ c (UnionAt (Position n) h) = c $ unsafeCoerce $ UnionAt (Position (n - 1)) h
+
+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 _ = undefined
+
+instance (Show (h x), Show (h :| xs)) => Show (h :| (x ': xs)) where
+  showsPrec d = (\h -> showParen (d > 10) $ showString "inS " . showsPrec d h)
+    <:| showsPrec d
+
+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 (<:*)
+infixr 5 <%
+
+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.
+platter :: (x ∈ xs, Functor f) => (x -> f x) -> (K0 :* xs -> f (K0 :* xs))
+platter f = record (fmap K0 . f . getK0)
+
+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 }
+
+-- | /O(log n)/ Perform pattern match.
+match :: Match h a :* xs -> h :| xs -> a
+match p (UnionAt pos h) = runMatch (view (recordAt pos) p) h
+
+(<?%) :: (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 #-}
+
+deriving instance Show (K1 a :| fs) => Show (Union fs a)
+
+---------------------------------------------------------------------
+
+newtype Position x xs = Position Int deriving Show
+
+class (x :: k) ∈ (xs :: [k]) where
+  position :: Position x xs
+
+instance Record (Lookup x xs) => x ∈ xs where
+  position = Position $ theInt (Proxy :: Proxy (Lookup x xs))
+  {-# INLINE position #-}
+
+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
+
+class Record n where
+  theInt :: Proxy n -> Int
+
+instance Record Zero where
+  theInt _ = 0
+
+instance Record n => Record (DNat n) where
+  theInt _ = theInt (Proxy :: Proxy n) `shiftL` 1
+
+instance Record n => Record (SDNat n) where
+  theInt _ = (theInt (Proxy :: Proxy n) `shiftL` 1) .|. 1
+
+instance Record n => Record (Just n) where
+  theInt _ = theInt (Proxy :: Proxy n)
+
+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