diff --git a/.gitignore b/.gitignore
new file mode 100644
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,7 @@
+dist
+cabal-dev
+*.o
+*.hi
+*.chi
+*.chs.h
+.virthualenv
diff --git a/.travis.yml b/.travis.yml
new file mode 100644
--- /dev/null
+++ b/.travis.yml
@@ -0,0 +1,1 @@
+language: haskell
diff --git a/COPYING b/COPYING
new file mode 100644
--- /dev/null
+++ b/COPYING
@@ -0,0 +1,27 @@
+Copyright 2013 Masahiro Sakai. All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+   1. Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+   2. 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.
+   3. The name of the author may not be used to endorse or promote
+      products derived from this software without specific prior
+      written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``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 AUTHOR 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,2 @@
+finite-field
+============
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,4 @@
+#! /usr/bin/env runhaskell
+
+> import Distribution.Simple
+> main = defaultMain
diff --git a/finite-field.cabal b/finite-field.cabal
new file mode 100644
--- /dev/null
+++ b/finite-field.cabal
@@ -0,0 +1,55 @@
+Name:		finite-field
+Version:	0.4.0
+License:	BSD3
+License-File:	COPYING
+Author:		Masahiro Sakai (masahiro.sakai@gmail.com)
+Maintainer:	masahiro.sakai@gmail.com
+Category:	Math, Data
+Cabal-Version:	>= 1.10
+Synopsis:	Finite Fields
+Description:	Implementation of finite fields
+Bug-Reports:	https://github.com/msakai/finite-field/issues
+Extra-Source-Files:
+   README.md
+   COPYING
+   .travis.yml
+   .gitignore
+Build-Type: Simple
+
+source-repository head
+  type:     git
+  location: git://github.com/msakai/finite-field.git
+
+Library
+  Hs-source-dirs: src
+  Build-Depends:
+     base >=4 && <5, deepseq, type-level-numbers, algebra >=3.1
+  Default-Language: Haskell2010
+  Other-Extensions:
+     DeriveDataTypeable
+     MultiParamTypeClasses
+     ScopedTypeVariables
+     Rank2Types
+     GADTs
+  Exposed-Modules:
+     Data.FiniteField.PrimeField
+     Data.FiniteField.SomeNat
+
+Test-suite TestPrimeField
+  Type:              exitcode-stdio-1.0
+  HS-Source-Dirs:    test
+  Main-is:           TestPrimeField.hs
+  Build-depends:
+      base >=4 && <5,
+      containers,
+      test-framework,
+      test-framework-th,
+      test-framework-hunit,
+      test-framework-quickcheck2,
+      HUnit,
+      QuickCheck >=2 && <3,
+      finite-field,
+      primes,
+      type-level-numbers
+  Default-Language: Haskell2010
+  Other-Extensions: TemplateHaskell
diff --git a/src/Data/FiniteField/PrimeField.hs b/src/Data/FiniteField/PrimeField.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/FiniteField/PrimeField.hs
@@ -0,0 +1,134 @@
+{-# LANGUAGE ScopedTypeVariables, MultiParamTypeClasses, DeriveDataTypeable #-}
+{-# OPTIONS_GHC -Wall #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.FiniteField.PrimeField
+-- Copyright   :  (c) Masahiro Sakai 2013
+-- License     :  BSD-style
+--
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  non-portable (ScopedTypeVariables, MultiParamTypeClasses, DeriveDataTypeable)
+--
+-- Finite field of prime order Fp.
+--
+-- References:
+--
+-- * <http://en.wikipedia.org/wiki/Finite_field>
+--
+-----------------------------------------------------------------------------
+module Data.FiniteField.PrimeField
+  ( PrimeField
+  , toInteger
+  ) where
+
+import Prelude hiding (toInteger)
+import Control.DeepSeq
+import Data.Ratio (denominator, numerator)
+import Data.Typeable
+import qualified Numeric.Algebra as Alg
+import qualified TypeLevel.Number.Nat as TL
+
+-- | Finite field of prime order Fp.
+--
+-- NB: Primality of @p@ is assumed, but not checked.
+newtype PrimeField p = PrimeField Integer deriving (Eq, Typeable)
+
+-- | conversion to 'Integer'
+toInteger :: PrimeField p -> Integer
+toInteger (PrimeField a) = a
+
+toInt :: Integral a => PrimeField p -> a
+toInt = fromInteger . toInteger
+
+instance Show (PrimeField p) where
+  showsPrec n (PrimeField x) = showsPrec n x
+
+instance TL.Nat p => Read (PrimeField p) where
+  readsPrec n s = [(fromInteger a, s') | (a,s') <- readsPrec n s]
+
+instance NFData (PrimeField p) where
+  rnf (PrimeField a) = rnf a
+
+instance TL.Nat p => Num (PrimeField p) where
+  PrimeField a + PrimeField b = fromInteger $ a+b
+  PrimeField a * PrimeField b = fromInteger $ a*b
+  PrimeField a - PrimeField b = fromInteger $ a-b
+  negate (PrimeField a)       = fromInteger $ negate a
+  abs a         = a
+  signum _      = 1
+  fromInteger a = PrimeField $ a `mod` TL.toInt (undefined :: p)
+
+instance TL.Nat p => Fractional (PrimeField p) where
+  fromRational r = fromInteger (numerator r) / fromInteger (denominator r)
+  recip a = a ^ (TL.toInt (undefined :: p) - 2 :: Integer)
+
+instance TL.Nat p => Bounded (PrimeField p) where
+  minBound = PrimeField 0
+  maxBound = PrimeField (TL.toInt (undefined :: p) - 1)
+
+instance TL.Nat p => Enum (PrimeField p) where
+  toEnum x
+    | toInt (minBound :: PrimeField p) <= x && x <= toInt (maxBound :: PrimeField p) = fromIntegral x
+    | otherwise = error "PrimeField.toEnum: bad argument"
+  fromEnum = toInt
+
+instance Ord (PrimeField p) where
+  PrimeField a `compare` PrimeField b = a `compare` b
+  PrimeField a `max` PrimeField b = PrimeField (a `max` b)
+  PrimeField a `min` PrimeField b = PrimeField (a `min` b)
+
+-- ---------------------------------------------------------------------------
+
+instance TL.Nat p => Alg.Multiplicative (PrimeField p) where
+  (*) = (*)
+
+instance TL.Nat p => Alg.Commutative (PrimeField p)
+
+instance TL.Nat p => Alg.Unital (PrimeField p) where
+  one = 1
+
+instance TL.Nat p => Alg.Division (PrimeField p) where
+  recip = recip
+
+instance TL.Nat p => Alg.Additive (PrimeField p) where
+  (+) = (+)
+
+instance TL.Nat p => Alg.Abelian (PrimeField p)
+
+instance TL.Nat p => Alg.Semiring (PrimeField p)
+
+instance TL.Nat p => Alg.LeftModule Alg.Natural (PrimeField p) where
+  n .* a = fromIntegral n * a
+
+instance TL.Nat p => Alg.RightModule Alg.Natural (PrimeField p) where
+  a *. n = a * fromIntegral n
+
+instance TL.Nat p => Alg.Monoidal (PrimeField p) where
+  zero = 0
+
+instance TL.Nat p => Alg.LeftModule Integer (PrimeField p) where
+  n .* a = fromIntegral n * a
+
+instance TL.Nat p => Alg.RightModule Integer (PrimeField p) where
+  a *. n = a * fromIntegral n
+
+instance TL.Nat p => Alg.Group (PrimeField p) where
+  negate = negate
+
+instance TL.Nat p => Alg.Rig (PrimeField p)
+
+instance TL.Nat p => Alg.Ring (PrimeField p)
+
+instance TL.Nat p => Alg.Characteristic (PrimeField p) where
+  char _ = TL.toInt (undefined :: p)
+
+instance TL.Nat p => Alg.Field (PrimeField p)
+
+-- ---------------------------------------------------------------------------
+
+{-
+type GF2 = PrimeField (SuccessorTo (SuccessorTo Zero))
+type GF3 = PrimeField (SuccessorTo (SuccessorTo (SuccessorTo Zero)))
+type GF5 = PrimeField (SuccessorTo (SuccessorTo (SuccessorTo (SuccessorTo (SuccessorTo Zero)))))
+-}
diff --git a/src/Data/FiniteField/SomeNat.hs b/src/Data/FiniteField/SomeNat.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/FiniteField/SomeNat.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE ScopedTypeVariables, Rank2Types, GADTs, DeriveDataTypeable #-}
+{-# OPTIONS_GHC -Wall #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.FiniteField.SomeNat
+-- Copyright   :  (c) Masahiro Sakai 2013
+-- License     :  BSD-style
+--
+-- Maintainer  :  masahiro.sakai@gmail.com
+-- Stability   :  provisional
+-- Portability :  non-portable (ScopedTypeVariables, Rank2Types, GADTs, DeriveDataTypeable)
+--
+-- Utility for type-level manipulation of natural numbers
+--
+-----------------------------------------------------------------------------
+module Data.FiniteField.SomeNat
+  ( SomeNat (..)
+  , fromInteger
+  ) where
+
+import Prelude hiding (fromInteger)
+import Control.DeepSeq
+import Data.Bits
+import Data.Typeable
+import TypeLevel.Number.Nat
+
+data SomeNat where
+  SomeNat :: Nat n => n -> SomeNat
+  deriving Typeable
+
+instance Show SomeNat where
+  showsPrec d (SomeNat n) = showParen (d > 10) $
+    showString "fromInteger " . shows (toInt n :: Integer)
+
+instance NFData SomeNat
+
+fromInteger :: Integer -> SomeNat
+fromInteger a | a < 0  = error "Data.FiniteField.SomeNat.fromInteger: negative number"
+fromInteger 0 = SomeNat (undefined :: Z)
+fromInteger a = f a (\n -> SomeNat n) (\n -> SomeNat n)
+  where
+    f :: Integer
+      -> (forall n m. (Nat n, n ~ O m) => n -> SomeNat)
+      -> (forall n m. (Nat n, n ~ I m) => n -> SomeNat)
+      -> SomeNat
+    f 1 _  k1 = k1 (undefined :: I Z)
+    f x k0 k1 = f (x `shiftR` 1) k0' k1'
+      where
+        k0' :: forall n m. (Nat n, n ~ O m) => n -> SomeNat
+        k0' _ =
+          if testBit x 0
+          then k1 (undefined :: I n)
+          else k0 (undefined :: O n)
+        k1' :: forall n m. (Nat n, n ~ I m) => n -> SomeNat
+        k1' _ =
+          if testBit x 0
+          then k1 (undefined :: I n)
+          else k0 (undefined :: O n)
diff --git a/test/TestPrimeField.hs b/test/TestPrimeField.hs
new file mode 100644
--- /dev/null
+++ b/test/TestPrimeField.hs
@@ -0,0 +1,129 @@
+{-# LANGUAGE TemplateHaskell, ScopedTypeVariables #-}
+
+import Test.QuickCheck
+import Test.Framework.TH
+import Test.Framework.Providers.QuickCheck2
+
+import Control.Monad
+import Data.Numbers.Primes (primes)
+
+import Data.FiniteField.PrimeField (PrimeField)
+import qualified Data.FiniteField.PrimeField as PrimeField
+import Data.FiniteField.SomeNat (SomeNat (..))
+import qualified Data.FiniteField.SomeNat as SomeNat
+import TypeLevel.Number.Nat
+
+-- ----------------------------------------------------------------------
+-- addition
+
+prop_add_comm =
+  forAll smallPrimes $ \(SomeNat (_ :: p)) ->
+    forAll arbitrary $ \(a :: PrimeField p) ->
+    forAll arbitrary $ \b ->
+      a + b == b + a
+
+prop_add_assoc =
+  forAll smallPrimes $ \(SomeNat (_ :: p)) ->
+    forAll arbitrary $ \(a :: PrimeField p) ->
+    forAll arbitrary $ \b ->
+    forAll arbitrary $ \c ->
+      (a + b) + c == a + (b + c)
+
+prop_add_unitl =
+  forAll smallPrimes $ \(SomeNat (_ :: p)) ->
+    forAll arbitrary $ \(a :: PrimeField p) ->
+      0 + a == a
+
+prop_add_unitr =
+  forAll smallPrimes $ \(SomeNat (_ :: p)) ->
+    forAll arbitrary $ \(a :: PrimeField p) ->
+      a + 0 == a
+
+prop_negate =
+  forAll smallPrimes $ \(SomeNat (_ :: p)) ->
+    forAll arbitrary $ \(a :: PrimeField p) ->
+      a + negate a == 0
+
+-- ----------------------------------------------------------------------
+-- multiplication
+
+prop_mult_comm =
+  forAll smallPrimes $ \(SomeNat (_ :: p)) ->
+    forAll arbitrary $ \(a :: PrimeField p) ->
+    forAll arbitrary $ \b ->
+      a * b == b * a
+
+prop_mult_assoc =
+  forAll smallPrimes $ \(SomeNat (_ :: p)) ->
+    forAll arbitrary $ \(a :: PrimeField p) ->
+    forAll arbitrary $ \b ->
+    forAll arbitrary $ \c ->
+      (a * b) * c == a * (b * c)
+
+prop_mult_unitl =
+  forAll smallPrimes $ \(SomeNat (_ :: p)) ->
+    forAll arbitrary $ \(a :: PrimeField p) ->
+      1 * a == a
+
+prop_mult_unitr =
+  forAll smallPrimes $ \(SomeNat (_ :: p)) ->
+    forAll arbitrary $ \(a :: PrimeField p) ->
+      a * 1 == a
+
+prop_mult_zero_l =
+  forAll smallPrimes $ \(SomeNat (_ :: p)) ->
+    forAll arbitrary $ \(a :: PrimeField p) ->
+      0*a == 0
+
+prop_mult_zero_r =
+  forAll smallPrimes $ \(SomeNat (_ :: p)) ->
+        forAll arbitrary $ \(a :: PrimeField p) ->
+          a*0 == 0
+
+-- ----------------------------------------------------------------------
+-- distributivity
+
+prop_distl =
+  forAll smallPrimes $ \(SomeNat (_ :: p)) ->
+    forAll arbitrary $ \(a :: PrimeField p) ->
+    forAll arbitrary $ \b ->
+    forAll arbitrary $ \c ->
+      a * (b + c) == a*b + a*c
+
+prop_distr =
+  forAll smallPrimes $ \(SomeNat (_ :: p)) ->
+    forAll arbitrary $ \(a :: PrimeField p) ->
+    forAll arbitrary $ \b ->
+    forAll arbitrary $ \c ->
+      (b + c) * a == b*a + c*a
+
+-- ----------------------------------------------------------------------
+-- recip
+
+prop_recip =
+  forAll smallPrimes $ \(SomeNat (_ :: p)) ->
+    forAll arbitrary $ \(a :: PrimeField p) ->
+      a /= 0 ==> a * (recip a) == 1
+
+-- ----------------------------------------------------------------------
+
+prop_intToSomeNat = do
+  forAll arbitrary $ \n ->
+    case SomeNat.fromInteger (abs n) of
+      SomeNat m -> abs n == toInt m
+
+------------------------------------------------------------------------
+
+smallPrimes :: Gen SomeNat
+smallPrimes = do
+  i <- choose (0, 2^(16::Int))
+  return $ SomeNat.fromInteger $ primes !! i
+
+instance Nat p => Arbitrary (PrimeField p) where
+  arbitrary = liftM fromInteger arbitrary
+
+------------------------------------------------------------------------
+-- Test harness
+
+main :: IO ()
+main = $(defaultMainGenerator)