diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs
new file mode 100644
--- /dev/null
+++ b/Data/Type/Natural.hs
@@ -0,0 +1,390 @@
+{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs        #-}
+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude     #-}
+{-# LANGUAGE PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}
+-- | Type level peano natural number, some arithmetic functions and their singletons.
+module Data.Type.Natural (
+                         -- * Natural numbers and its singleton type
+                           Nat(..), SNat(..)
+                         -- ** Smart constructors
+                         , sZ, sS
+                         -- ** Arithmetic functions and thir singletons.
+                         , min, Min, sMin, max, Max, sMax, (:+:), (%+), (:*:), (%*), (:-:), (%-)
+                         -- ** Type-level predicate & judgements
+                         , Leq(..), (:<=), (:<<=), LeqInstance, leqRefl, leqSucc
+                         , boolToPropLeq, boolToClassLeq, propToClassLeq
+                         -- * Type-classes for singletons
+                         --   (These will be removed once singletons package available for the latest singletons package)
+                         , Sing(..), SingInstance(..), singInstance
+                         -- * Conversion functions
+                         , natToInt, intToNat, sNatToInt
+                         -- * Useful type synonyms and constructors
+                         , Zero, One, Two, Three, Four, Five, Six, Seven, Eight, Nine, Ten
+                         , Eleven, Twelve, Thirteen, Fourteen, Fifteen, Sixteen, Seventeen, Eighteen, Nineteen, Twenty
+                         , sZero, sOne, sTwo, sThree, sFour, sFive, sSix, sSeven, sEight, sNine, sTen, sEleven
+                         , sTwelve, sThirteen, sFourteen, sFifteen, sSixteen, sSeventeen, sEighteen, sNineteen, sTwenty
+                         , N0, N1, N2, N3, N4, N5, N6, N7, N8, N9, N10, N11, N12, N13, N14, N15, N16, N17, N18, N19, N20
+                         , sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14
+                         , sN15, sN16, sN17, sN18, sN19, sN20
+                         ) where
+import Prelude (Eq (..), Integral (..), Num (..), Ord ((<)), Show (..), error,
+                id, otherwise, ($), Bool(..))
+
+--------------------------------------------------
+-- * Natural numbers and its singleton type
+--------------------------------------------------
+
+-- | Peano natural numbers. It will be promoted to the type-level natural number.
+data Nat = Z | S Nat
+           deriving (Show, Eq, Ord)
+
+-- | Singleton type for 'Nat'.
+--   When constructing data, use smart constructors such as 'sZ' and 'sS'.
+data SNat (n :: Nat) where
+  SZ :: SNat Z
+  SS :: SNat n -> SNat (S n)
+
+--------------------------------------------------
+-- ** Smart constructors.
+--------------------------------------------------
+
+-- | The smart constructor for @SZ@.
+sZ :: SNat Z
+sZ = case singInstance SZ of
+       SingInstance -> SZ
+
+-- | The smart constructor for @SS n@.
+sS :: SNat n -> SNat (S n)
+sS n = case singInstance n of
+         SingInstance -> SS n
+
+--------------------------------------------------
+-- ** Arithmetic functions.
+--------------------------------------------------
+
+-- | Minimum function.
+min :: Nat -> Nat -> Nat
+min Z     Z     = Z
+min Z     (S _) = Z
+min (S _) Z     = Z
+min (S m) (S n) = S (min m n)
+
+-- | Type-level minimum function.
+type family Min (n :: Nat) (m :: Nat) :: Nat
+type instance Min Z Z     = Z
+type instance Min Z (S n) = Z
+type instance Min (S m) Z = Z
+type instance Min (S n) (S m) = S (Min n m)
+
+-- | Singleton function for minimum function.
+sMin :: SNat n -> SNat m -> SNat (Min n m)
+sMin SZ     SZ     = sZ
+sMin SZ     (SS _) = sZ
+sMin (SS _) SZ     = sZ
+sMin (SS m) (SS n) = sS (sMin m n)
+
+-- | Maximum function.
+max :: Nat -> Nat -> Nat
+max Z     Z     = Z
+max Z     (S n) = S n
+max (S n) Z     = S n
+max (S n) (S m) = S (max n m)
+
+-- | Type-level maximum function.
+type family Max (n :: Nat) (m :: Nat) :: Nat
+type instance Max Z Z     = Z
+type instance Max Z (S n) = S n
+type instance Max (S n) Z = S n
+type instance Max (S n) (S m) = S (Max n m)
+
+-- | Singleton function for maximum.
+sMax :: SNat n -> SNat m -> SNat (Max n m)
+sMax SZ     SZ     = SZ
+sMax (SS n) SZ     = SS n
+sMax SZ     (SS n) = SS n
+sMax (SS n) (SS m) = SS (sMax n m)
+
+instance Num Nat where
+  n   - Z   = n
+  S n - S m = n - m
+  Z     + n = n
+  (S m) + n = S (m + n)
+  Z     * _ = 0
+  (S m) * n = m * n + n
+  abs = id
+  signum Z = Z
+  signum _ = S Z
+  fromInteger 0             = Z
+  fromInteger n | n < 0     = error "negative integer"
+                | otherwise = S $ fromInteger (n - 1)
+
+infixl 6 :-:, %-
+type family (n :: Nat) :-: (m :: Nat) :: Nat
+type instance n     :-: Z     = n
+type instance (S n) :-: (S m) = n :-: m
+
+(%-) :: (n :<<= m) ~ True => SNat n -> SNat m -> SNat (n :-: m)
+n   %- SZ    = n
+SS n %- SS m = n %- m
+_    %- _    = error "impossible!"
+
+infix 6 :+:, %+
+
+-- | Type-level addition.
+type family (n :: Nat) :+: (m :: Nat) :: Nat
+type instance  Z   :+: n = n
+type instance  S m :+: n = S (m :+: n)
+
+-- | Addition for singleton numbers.
+(%+) :: SNat n -> SNat m -> SNat (n :+: m)
+SZ   %+ n = n
+SS n %+ m = sS (n %+ m)
+
+infix 7 :*:, %*
+
+-- | Type-level multiplication.
+type family   (n :: Nat) :*: (m :: Nat) :: Nat
+type instance Z   :*: n = Z
+type instance S m :*: n = m :*: n :+: n
+
+-- | Multiplication for singleton numbers.
+(%*) :: SNat n -> SNat m -> SNat (n :*: m)
+SZ   %* _ = sZ
+SS n %* m = n %* m %+ m
+
+--------------------------------------------------
+-- ** Type-level predicate & judgements.
+--------------------------------------------------
+-- | Comparison via type-class.
+class (n :: Nat) :<= (m :: Nat)
+instance Z :<= n
+instance (n :<= m) => S n :<= S m
+
+-- | Comparison function
+type family   (n :: Nat) :<<= (m :: Nat) :: Bool
+type instance Z   :<<= n   = True
+type instance S n :<<= Z   = False
+type instance S n :<<= S m = n :<<= m
+
+-- | Comparison witness via GADTs.
+data Leq (n :: Nat) (m :: Nat) where
+  ZeroLeq     :: SNat m -> Leq Zero m
+  SuccLeqSucc :: Leq n m -> Leq (S n) (S m)
+
+data LeqInstance n m where
+  LeqInstance :: (n :<= m) => LeqInstance n m
+
+boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m
+boolToPropLeq SZ     m      = ZeroLeq m
+boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m
+boolToPropLeq _      _      = error "impossible happend!"
+
+boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m
+boolToClassLeq SZ     _      = LeqInstance
+boolToClassLeq (SS n) (SS m) =
+  case boolToClassLeq n m of
+    LeqInstance -> LeqInstance
+boolToClassLeq _ _ = error "impossible!"
+
+propToClassLeq :: Leq n m -> LeqInstance n m
+propToClassLeq (ZeroLeq _) = LeqInstance
+propToClassLeq (SuccLeqSucc leq) =
+  case propToClassLeq leq of
+    LeqInstance -> LeqInstance
+
+leqRefl :: SNat n -> LeqInstance n n
+leqRefl SZ = LeqInstance
+leqRefl (SS n) =
+  case leqRefl n of
+    LeqInstance -> LeqInstance
+
+leqSucc :: SNat n -> LeqInstance n (S n)
+leqSucc SZ = LeqInstance
+leqSucc (SS n) =
+    case leqSucc n of
+      LeqInstance -> LeqInstance
+
+
+--------------------------------------------------
+-- * Type classes for singletons.
+--------------------------------------------------
+
+-- | Singleton type-class.
+-- This class will be removed soon after singletons package available for the latest Haskell Paltform.
+class Sing n where
+  -- | Automatically compute singletons.
+  sing :: SNat n
+
+instance Sing Z where
+  sing = SZ
+
+instance Sing n => Sing (S n) where
+  sing = SS sing
+
+-- | Witness for 'Sing' instance.
+--   This type will be removed soon after singletons package available for the latest Haskell Paltform.
+data SingInstance a where
+  SingInstance :: Sing a => SingInstance a
+
+-- | Get witness for singleton integers.
+--   This function will be removed soon after singletons package available for the latest Haskell Paltform.
+singInstance :: SNat n -> SingInstance n
+singInstance SZ = SingInstance
+singInstance (SS n) =
+    case singInstance n of
+      SingInstance -> SingInstance
+
+--------------------------------------------------
+-- * Conversion functions.
+--------------------------------------------------
+
+-- | Convert integral numbers into 'Nat'
+intToNat :: (Integral a, Ord a) => a -> Nat
+intToNat 0 = Z
+intToNat n
+    | n < 0     = error "negative integer"
+    | otherwise = S $ intToNat (n - 1)
+
+-- | Convert 'Nat' into normal integers.
+natToInt :: Integral n => Nat -> n
+natToInt Z     = 0
+natToInt (S n) = natToInt n + 1
+
+-- | Convert 'SNat n' into normal integers.
+sNatToInt :: Num n => SNat x -> n
+sNatToInt SZ     = 0
+sNatToInt (SS n) = sNatToInt n + 1
+
+--------------------------------------------------
+-- Useful type synonyms and constructors.
+--------------------------------------------------
+
+type Zero      = Z
+type One       = S Zero
+type Two       = S One
+type Three     = S Two
+type Four      = S Three
+type Five      = S Four
+type Six       = S Five
+type Seven     = S Six
+type Eight     = S Seven
+type Nine      = S Eight
+type Ten       = S Nine
+type Eleven    = S Ten
+type Twelve    = S Eleven
+type Thirteen  = S Twelve
+type Fourteen  = S Thirteen
+type Fifteen   = S Fourteen
+type Sixteen   = S Fifteen
+type Seventeen = S Sixteen
+type Eighteen  = S Seventeen
+type Nineteen  = S Eighteen
+type Twenty    = S Nineteen
+
+type N0  = Z
+type N1  = One
+type N2  = Two
+type N3  = Three
+type N4  = Four
+type N5  = Five
+type N6  = Six
+type N7  = Seven
+type N8  = Eight
+type N9  = Nine
+type N10 = Ten
+type N11 = Eleven
+type N12 = Twelve
+type N13 = Thirteen
+type N14 = Fourteen
+type N15 = Fifteen
+type N16 = Sixteen
+type N17 = Seventeen
+type N18 = Eighteen
+type N19 = Nineteen
+type N20 = Twenty
+
+sZero :: SNat 'Z
+sZero = sZ
+
+sOne :: SNat One
+sOne = sS sZero
+sTwo :: SNat Two
+sTwo = sS sOne
+sThree :: SNat Three
+sThree = sS sTwo
+sFour :: SNat Four
+sFour = sS sThree
+sFive :: SNat Five
+sFive = sS sFour
+sSix :: SNat Six
+sSix = sS sFive
+sSeven :: SNat Seven
+sSeven = sS sSix
+sEight :: SNat Eight
+sEight = sS sSeven
+sNine :: SNat Nine
+sNine = sS sEight
+sTen :: SNat Ten
+sTen = sS sNine
+sEleven :: SNat Eleven
+sEleven = sS sTen
+sTwelve :: SNat Twelve
+sTwelve = sS sEleven
+sThirteen :: SNat Thirteen
+sThirteen = sS sTwelve
+sFourteen :: SNat Fourteen
+sFourteen = sS sThirteen
+sFifteen :: SNat Fifteen
+sFifteen = sS sFourteen
+sSixteen :: SNat Sixteen
+sSixteen = sS sFifteen
+sSeventeen :: SNat Seventeen
+sSeventeen = sS sSixteen
+sEighteen :: SNat Eighteen
+sEighteen = sS sSeventeen
+sNineteen :: SNat Nineteen
+sNineteen = sS sEighteen
+sTwenty :: SNat Twenty
+sTwenty = sS sNineteen
+
+sN0 :: SNat 'Z
+sN0  = sZ
+sN1 :: SNat One
+sN1  = sOne
+sN2 :: SNat Two
+sN2  = sTwo
+sN3 :: SNat Three
+sN3  = sThree
+sN4 :: SNat Four
+sN4  = sFour
+sN5 :: SNat Five
+sN5  = sFive
+sN6 :: SNat Six
+sN6  = sSix
+sN7 :: SNat Seven
+sN7  = sSeven
+sN8 :: SNat Eight
+sN8  = sEight
+sN9 :: SNat Nine
+sN9  = sNine
+sN10 :: SNat Ten
+sN10 = sTen
+sN11 :: SNat Eleven
+sN11 = sEleven
+sN12 :: SNat Twelve
+sN12 = sTwelve
+sN13 :: SNat Thirteen
+sN13 = sThirteen
+sN14 :: SNat Fourteen
+sN14 = sFourteen
+sN15 :: SNat Fifteen
+sN15 = sFifteen
+sN16 :: SNat Sixteen
+sN16 = sSixteen
+sN17 :: SNat Seventeen
+sN17 = sSeventeen
+sN18 :: SNat Eighteen
+sN18 = sEighteen
+sN19 :: SNat Nineteen
+sN19 = sNineteen
+sN20 :: SNat Twenty
+sN20 = sTwenty
diff --git a/Data/Vector/Sized.hs b/Data/Vector/Sized.hs
new file mode 100644
--- /dev/null
+++ b/Data/Vector/Sized.hs
@@ -0,0 +1,98 @@
+{-# LANGUAGE DataKinds, GADTs, MultiParamTypeClasses, PolyKinds #-}
+{-# LANGUAGE StandaloneDeriving, TypeFamilies, TypeOperators    #-}
+-- | Size-parameterized vector types and functions.
+module Data.Vector.Sized where
+import Control.Applicative
+import Data.Maybe
+import Data.Type.Natural
+import Prelude             hiding (map, foldl, foldr, head, splitAt, tail, zipWith, take)
+
+data Vector (a :: *) (n :: Nat)  where
+  Nil  :: Vector a Z
+  (:-) :: a -> Vector a n -> Vector a (S n)
+
+infixr 5 :-
+
+deriving instance Show a => Show (Vector a n)
+instance (Eq a) => Eq (Vector a n) where
+  Nil == Nil = True
+  (x :- xs) == (y :- ys) = x == y && xs == ys
+  _ == _ = error "impossible!"
+
+sLength :: Vector a n -> SNat n
+sLength Nil       = sZ
+sLength (_ :- xs) = sS $ sLength xs
+
+length :: Vector a n -> Int
+length = sNatToInt . sLength
+
+append :: Vector a n -> Vector a m -> Vector a (n :+: m)
+append (x :- xs) ys = x :- append xs ys
+append Nil       ys = ys
+
+foldr :: (a -> b -> b) -> b -> Vector a n -> b
+foldr _ b Nil       = b
+foldr f a (x :- xs) = f x (foldr f a xs)
+
+foldl :: (a -> b -> a) -> a -> Vector b n -> a
+foldl _ a Nil       = a
+foldl f a (b :- bs) = foldl f (f a b) bs
+
+singleton :: a -> Vector a (S Z)
+singleton = (:- Nil)
+
+zipWithSame :: (a -> b -> c) -> Vector a n -> Vector b n -> Vector c n
+zipWithSame _ Nil Nil = Nil
+zipWithSame f (x :- xs) (y :- ys) = f x y :- zipWithSame f xs ys
+zipWithSame _ _ _ = error "cannot happen"
+
+zipWith :: (a -> b -> c) -> Vector a n -> Vector b m -> Vector c (Min n m)
+zipWith _ Nil Nil             = Nil
+zipWith _ Nil (_ :- _)        = Nil
+zipWith _ (_ :- _) Nil        = Nil
+zipWith f (x :- xs) (y :- ys) = f x y :- zipWith f xs ys
+
+toList :: Vector a n -> [a]
+toList = foldr (:) []
+
+fromList :: SNat n -> [a] -> Maybe (Vector a n)
+fromList SZ     _      = Just Nil
+fromList (SS n) (x:xs) = (x :-) <$> fromList n xs
+fromList _      _      = Nothing
+
+unsafeFromList :: SNat n -> [a] -> Vector a n
+unsafeFromList len = fromMaybe (error "Length too short") . fromList len
+
+fromList' :: Sing n => [a] -> Maybe (Vector a n)
+fromList' = fromList sing
+
+unsafeFromList' :: Sing n => [a] -> Vector a n
+unsafeFromList' = unsafeFromList sing
+
+all :: (a -> Bool) -> Vector a n -> Bool
+all p = foldr ((&&) . p) False
+
+splitAt :: (n :<<= m) ~ True => SNat n -> Vector a m -> (Vector a n, Vector a (m :-: n))
+splitAt SZ     xs        = (Nil, xs)
+splitAt (SS n) (x :- xs) =
+  case splitAt n xs of
+    (xs', ys') -> (x :- xs', ys')
+splitAt _ _ = error "could not happen!"
+
+drop :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a (m :-: n)
+drop n = snd . splitAt n
+
+take :: (n :<<= m) ~ True => SNat n -> Vector a m -> Vector a n
+take SZ     _         = Nil
+take (SS n) (x :- xs) = x :- take n xs
+take _ _ = error "imposible!"
+
+map :: (a -> b) -> Vector a n -> Vector b n
+map _ Nil       = Nil
+map f (x :- xs) = f x :- map f xs
+
+head :: Vector a (S n) -> a
+head (x :- _) = x
+
+tail :: Vector a (S n) -> Vector a n
+tail (_ :- xs) = xs
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,4 @@
+Type-level sized vector library
+================================
+
+
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/sized-vector.cabal b/sized-vector.cabal
new file mode 100644
--- /dev/null
+++ b/sized-vector.cabal
@@ -0,0 +1,25 @@
+-- Initial sized-vector.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                sized-vector
+version:             0.0.1.0
+synopsis:            Size-parameterized vector types and functions.
+description:         Size-parameterized vector types and functions using a data-type promotion.
+homepage:            https://github.com/konn/sized-vector
+license:             BSD3
+license-file:        LICENSE
+extra-source-files:  README.md
+author:              Hiromi ISHII
+maintainer:          konn.jinro_at_gmail.com
+copyright:           (C) Hiromi ISHII 2013
+category:            Data
+build-type:          Simple
+cabal-version:       >=1.8
+source-repository head
+  Type: git
+  Location: git://github.com/konn/sized-vector.git
+
+library
+  exposed-modules:     Data.Type.Natural, Data.Vector.Sized
+  -- other-modules:       
+  build-depends:       base >= 2.0 && < 5