diff --git a/Data/Fin.hs b/Data/Fin.hs
new file mode 100644
--- /dev/null
+++ b/Data/Fin.hs
@@ -0,0 +1,155 @@
+{-# LANGUAGE KindSignatures,
+             DataKinds,
+             StandaloneDeriving,
+             TypeOperators,
+             TypeFamilies,
+             DeriveDataTypeable,
+             RankNTypes,
+             ScopedTypeVariables,
+             FlexibleContexts,
+             FlexibleInstances #-}
+module Data.Fin (
+  Fin (..),
+  natToFin, toFin, unsafeToFin, fromFin,
+  finZ, finS, finLast,
+  absurd,
+  weaken, weakenN, strengthen,
+  shift,
+  finAdd, finAddN,
+  finSub, finSubN,
+  finMult
+  ) where
+
+import GHC.TypeLits
+import Data.Proxy
+import Data.Typeable
+import Unsafe.Coerce
+
+newtype Fin s (n :: Nat) = Fin s
+                         deriving (Typeable)
+
+deriving instance Ord s => Ord (Fin s n)
+deriving instance Eq s => Eq (Fin s n)
+deriving instance Show s => Show (Fin s n)
+
+-- instance (Integral s, KnownNat (n + 1)) => Enum (Fin s (n + 1)) where
+--   succ = finS
+--   pred x@(Fin x')
+--     | x == 0 = x
+--     | otherwise = Fin (x - 1)
+--  toEnum x = toFin . fromIntegral
+--  fromEnum (Fin x) = fromIntegral x
+
+finZ :: (Integral s, KnownNat (n + 1)) => Fin s (n + 1)
+finZ = Fin 0
+{-# INLINE finZ #-}
+
+finS :: (Integral s, KnownNat n, KnownNat (n + 1)) => Fin s n -> Fin s (n + 1)
+finS (Fin x) = Fin x
+{-# INLINE finS #-}
+
+-- |
+-- >>> (finLast :: Fin Int 5)
+-- Fin 4
+--
+finLast :: forall s n. (Integral s, KnownNat n, KnownNat (n + 1)) => Fin s (n + 1)
+finLast = unsafeToFin $ fromIntegral $ natVal (Proxy :: Proxy n)
+{-# INLINE finLast #-}
+
+absurd :: Fin s 0 -> a
+absurd = unsafeCoerce
+{-# INLINE absurd #-}
+
+-- |
+-- >>> (natToFin (Proxy :: Proxy 10) :: Fin Int 11)
+-- Fin 10
+--
+natToFin :: (Integral s, KnownNat n, KnownNat (m + 1), n <= m) => proxy n -> Fin s (m + 1)
+natToFin = unsafeToFin . fromIntegral . natVal
+{-# INLINE natToFin #-}
+
+
+-- |
+-- >>> (toFin 0 :: Maybe (Fin Int 4))
+-- Just (Fin 0)
+--
+-- >>> (toFin 4 :: Maybe (Fin Int 4))
+-- Nothing
+--
+toFin :: forall s n. (Integral s, KnownNat (n :: Nat)) => s -> Maybe (Fin s n)
+toFin x
+  | x < 0 = Nothing
+  | x < fromIntegral (natVal (Proxy :: Proxy n)) = Just $ Fin x
+  | otherwise = Nothing
+
+-- |
+-- >>> (unsafeToFin 10 :: Fin Int 5)
+-- Fin 10
+--
+unsafeToFin :: (Integral s, KnownNat n) => s -> Fin s n
+unsafeToFin = Fin
+{-# INLINE unsafeToFin #-}
+
+
+-- |
+-- >>> fromFin (finZ :: Fin Int 10)
+-- 0
+--
+-- >>> fromFin (finLast :: Fin Int 10)
+-- 9
+--
+fromFin :: Fin s n -> s
+fromFin (Fin x) = x
+{-# INLINE fromFin #-}
+
+
+weaken :: (Integral s, KnownNat (n + 1)) => Fin s n -> Fin s (n + 1)
+weaken (Fin x) = unsafeToFin x
+{-# INLINE weaken #-}
+
+weakenN :: (Integral s, KnownNat (n + m)) => proxy m -> Fin s n -> Fin s (n + m)
+weakenN _ (Fin x) = unsafeToFin x
+{-# INLINE weakenN #-}
+
+strengthen :: forall n s. (KnownNat n, Integral s, Ord s) => Fin s (n + 1) -> Either (Fin s (n + 1)) (Fin s n)
+strengthen x'@(Fin x)
+  | x < fromIntegral (natVal (Proxy :: Proxy n)) = Right $ unsafeToFin x
+  | otherwise = Left x'
+{-# INLINE strengthen #-}
+
+-- |
+-- >>> shift (Proxy :: Proxy 1) (finZ :: Fin Int 20)
+-- Fin 0
+--
+-- >>> (shift (Proxy :: Proxy 10) (finLast :: Fin Int 10) :: Fin Int 20)
+-- Fin 9
+--
+shift :: (KnownNat (m + n), Integral s) => proxy m -> Fin s n -> Fin s (m + n)
+shift _ (Fin x) = unsafeToFin x
+{-# INLINE shift #-}
+
+finAdd :: (Integral s, KnownNat (n + m)) => Fin s n -> Fin s m -> Fin s (n + m)
+finAdd (Fin x) (Fin y) = unsafeToFin $ x + y
+{-# INLINE finAdd #-}
+
+finAddN :: forall n s. (KnownNat n, Integral s, Ord s) => Fin s n -> s -> Either (Fin s n) (Fin s n)
+finAddN x@(Fin x') y
+  | fromIntegral (natVal (Proxy :: Proxy n)) - x' > y = Right $ Fin (x' + y)
+  | otherwise = Left x
+{-# INLINE finAddN #-}
+
+finSub :: (KnownNat n, Ord s, Integral s) => Fin s n -> Fin s m -> Either (Fin s n) (Fin s n)
+finSub x (Fin y) = finSubN x y
+{-# INLINE finSub #-}
+
+finSubN :: (KnownNat n, Ord s, Integral s) => Fin s n -> s -> Either (Fin s n) (Fin s n)
+finSubN x'@(Fin x) y
+  | y <= x = Right $ unsafeToFin $ x - y
+  | otherwise = Left $ x'
+{-# INLINE finSubN #-}
+
+
+finMult :: (KnownNat (n * m), Integral s) => Fin s n -> Fin s m -> Fin s (n * m)
+finMult (Fin x) (Fin y) = unsafeToFin $ x * y
+{-# INLINE finMult #-}
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, Hiroki Hattori
+
+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 Hiroki Hattori 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,5 @@
+# data-fin-simple
+[![Build Status](https://travis-ci.org/seagull-kamome/data-fin-simple.svg)](https
+://travis-ci.org/seagull-kamome/data-fin-simple)
+
+有限集合
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/data-fin-simple.cabal b/data-fin-simple.cabal
new file mode 100644
--- /dev/null
+++ b/data-fin-simple.cabal
@@ -0,0 +1,39 @@
+-- Initial data-fin-simple.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                data-fin-simple
+version:             0.1.0.0
+synopsis:            Simple integral finite set
+description:         Typesafe finite unsigned-integral
+license:             BSD3
+license-file:        LICENSE
+author:              Hiroki Hattori
+maintainer:          seagull.kamome@gmail.com
+-- copyright:           
+homepage:            https://github.com/seagull-kamome/data-fin-simple
+bug-reports:         https://github.com/seagull-kamome/data-fin-simple/issues
+category:            Data
+build-type:          Simple
+extra-source-files:  
+  README.md
+cabal-version:       >=1.10
+
+source-repository head
+  type:                git
+  location:            http://github.com/seagull-kamome/data-fin-simple.git
+
+library
+  exposed-modules:     Data.Fin
+  -- other-modules:       
+  other-extensions:    KindSignatures, DataKinds, StandaloneDeriving
+  build-depends:       base >=4.7 && <4.9
+  -- hs-source-dirs:      
+  default-language:    Haskell2010
+
+test-suite doctest
+  type:                exitcode-stdio-1.0
+  default-language:    Haskell2010
+  hs-source-dirs:      test
+  main-is:             doctest.hs
+  build-depends:       base >=4.7 && <4.9, doctest >= 0.9.3
+
diff --git a/test/doctest.hs b/test/doctest.hs
new file mode 100644
--- /dev/null
+++ b/test/doctest.hs
@@ -0,0 +1,12 @@
+module Main where
+
+import Test.DocTest
+
+main :: IO ()
+main = doctest [
+       "-XKindSignatures",
+       "-XDataKinds",
+       "-idist/build",
+       "Data/Fin.hs"
+       ]
+