diff --git a/Data/Type/Monomorphic.hs b/Data/Type/Monomorphic.hs
new file mode 100644
--- /dev/null
+++ b/Data/Type/Monomorphic.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE DataKinds, ExistentialQuantification, FlexibleContexts, GADTs #-}
+{-# LANGUAGE PolyKinds, RankNTypes, TypeFamilies, TypeOperators            #-}
+{-# LANGUAGE UndecidableInstances                                          #-}
+module Data.Type.Monomorphic ( (:.:), Monomorphic (..), Monomorphicable(..)
+                             , demote', demoteComposed, monomorphicCompose
+                             , withPolymorhic, liftPoly, viaPoly, Compose(..)
+                             ) where
+import Control.Arrow
+import Data.Functor.Compose
+
+type (:.:) f g = Compose f g
+
+-- | A wrapper type for polymophic types.
+data Monomorphic k = forall a. Monomorphic (k a)
+
+-- | A types which have the monomorphic representation.
+class Monomorphicable k where
+  -- | Monomorphic representation
+  type MonomorphicRep k :: *
+  -- | Promote the monomorphic value to the polymophic one.
+  promote :: MonomorphicRep k -> Monomorphic k
+  -- | Demote the polymorphic value to the monomorphic representation.
+  demote  :: Monomorphic k -> MonomorphicRep k
+
+-- | Convinience function to demote polymorphic types into monomorphic one directly.
+demote' :: Monomorphicable k => k a -> MonomorphicRep k
+demote' = demote . Monomorphic
+
+-- | Demote polymorphic nested types directly into monomorphic representation.
+demoteComposed :: Monomorphicable (f :.: g) => f (g a) -> MonomorphicRep (f :.: g)
+demoteComposed = demote . Monomorphic . Compose
+
+monomorphicCompose :: f (g a) -> Monomorphic (f :.: g)
+monomorphicCompose = Monomorphic . Compose
+
+-- | Apply dependently-typed function to the monomorphic representation.
+withPolymorhic :: Monomorphicable k
+               => MonomorphicRep k -> (forall a. k a -> b) -> b
+withPolymorhic k trans =
+  case promote k of
+    Monomorphic a -> trans a
+
+-- | Flipped version of 'withPolymorhic'.
+liftPoly :: Monomorphicable k
+         => (forall a. k a -> b) -> MonomorphicRep k -> b
+liftPoly = flip withPolymorhic
+
+-- | Demote the function between polymorphic types into the one between monomorphic one.
+viaPoly :: (Monomorphicable k, Monomorphicable k')
+        => (forall x y. k x -> k' y) -> MonomorphicRep k -> MonomorphicRep k'
+viaPoly f a = demote $ Monomorphic $ liftPoly f a
+
+instance (Show (MonomorphicRep k), Monomorphicable k) => Show (Monomorphic k) where
+  showsPrec d x = showString "Polymorphic " . showsPrec (d + 1) (demote x)
+
+instance (Read (MonomorphicRep k), Monomorphicable k) => Read (Monomorphic k) where
+  readsPrec i = map (first promote) . readsPrec i
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2013, Hiromi ISHII
+
+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 Hiromi ISHII 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/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,46 @@
+The `monomorphic` library
+==========================
+
+What is this?
+-------------
+This library provides the type-class and functions to convert polymorphic data-types to/from its monomorphic representation types.
+It is convenient to provide a monomorphic interface for dependently-typed programs.
+
+Usage
+-----
+Consider the following example:
+
+```haskell
+data Nat = Z | S Nat
+data SNat (n :: Nat) where
+  SZ :: SNat Z
+  SS :: SNat n -> SNat (S n)
+
+instance Monomorphicable SNat where
+  type MonomorphicRep SNat = Int
+  promote 0     = Monomorphic SZ
+  promote n
+    | n < 0     = error "negative number"
+    | otherwise =
+        case promote (n - 1) of
+          Monomorphic sn -> Monomorphic (SS sn)
+  demote (Monomorphic sn) = toInt sn
+
+data Vector (a :: *) (n :: Nat) where
+  VNil :: Vector a Z
+  (:-) :: a -> Vector a n -> Vector a (S n)
+
+instance Monomorphicable (Vector a) whre
+  type MonomorphicRep (Vector a) = [a]
+  demote  (Monomorphic n) = toList n
+  promote [] = Monomorphic Nil
+  promote (x:xs) =
+    case promote xs of
+      Monomorphic xs' -> Monomorphic $ x :- xs'
+```
+
+`Monomorphic k` is the wrapper type to eliminate the polymorphic part of the types.
+The `Monomorphicable` type-class provides the functions to convert polymorphic value from/to its monomorphic representation, say `MonomorphicRep k` associated type.
+
+In the example above, `SNat n` can be monomorphically represented by `Int`.
+There are some convenient functions to manipulate monomorphic types and functions. For more detail, see API documentation.
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/monomorphic.cabal b/monomorphic.cabal
new file mode 100644
--- /dev/null
+++ b/monomorphic.cabal
@@ -0,0 +1,25 @@
+-- Initial monomorphic.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                monomorphic
+version:             0.0.1.0
+synopsis:            Library to convert polymorphic datatypes to/from its monomorphic represetation
+description:         This library provides the type-class and functions to convert between polymorphic data-types and its monomorphic representation type, such as length-indexed vectors, singletons for type-level natural numbers, etc.
+homepage:            https://github.com/konn/monomorphic
+license:             BSD3
+license-file:        LICENSE
+extra-source-files:  README.md
+author:              Hiromi ISHII
+maintainer:          konn.jinro_at_gmail.com
+-- copyright:           
+category:            Data
+build-type:          Simple
+cabal-version:       >=1.8
+source-repository head
+  Type: git
+  Location: git://github.com/kazu-yamamoto
+
+library
+  exposed-modules:     Data.Type.Monomorphic
+  -- other-modules:       
+  build-depends:       base ==4.5.*, transformers ==0.3.*