diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) Alexey Khudyakov
+
+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. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE 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 AUTHORS 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/TypeLevel/Boolean.hs b/TypeLevel/Boolean.hs
new file mode 100644
--- /dev/null
+++ b/TypeLevel/Boolean.hs
@@ -0,0 +1,75 @@
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE EmptyDataDecls        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+module TypeLevel.Boolean ( True
+                     , False
+                       -- * Boolean operations
+                     , Not
+                     , notT
+                     , And
+                     , andT
+                     , Or
+                     , orT
+                     , Xor
+                     , xorT
+                     ) where
+
+import TypeLevel.Reify
+
+-- | Data type for truth
+data True
+-- | Data type for false.
+data False
+
+instance Show False where show _ = "False"
+instance Show True  where show _ = "True"
+
+instance Reify True  Bool where witness = Witness True
+instance Reify False Bool where witness = Witness False
+
+----------------------------------------------------------------
+-- | Negation
+
+type family Not a :: *
+
+notT :: a -> Not a
+notT _ = undefined
+
+type instance Not False = True
+type instance Not True  = False
+
+----------------------------------------------------------------
+-- | And for boolean types
+type family And a b :: *
+
+andT :: a -> b -> And a b
+andT _ _ = undefined
+
+type instance And False False = False
+type instance And False True  = False
+type instance And True  False = False
+type instance And True  True  = True
+
+----------------------------------------------------------------
+-- | Or for boolean types
+type family Or a b :: *
+
+orT :: a -> b -> Or a b
+orT _ _ = undefined
+
+type instance Or False False = True
+type instance Or False True  = True
+type instance Or True  False = True
+type instance Or True  True  = False
+
+----------------------------------------------------------------
+-- | Exlusive or for boolean types
+type family Xor a b :: *
+
+xorT :: a -> b -> Xor a b
+xorT _ _ = undefined
+
+type instance Xor False False = False
+type instance Xor False True  = True
+type instance Xor True  False = True
+type instance Xor True  True  = False
diff --git a/TypeLevel/Number/Classes.hs b/TypeLevel/Number/Classes.hs
new file mode 100644
--- /dev/null
+++ b/TypeLevel/Number/Classes.hs
@@ -0,0 +1,169 @@
+{-# LANGUAGE EmptyDataDecls        #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE UndecidableInstances  #-}
+-- |
+-- Module      : TypeLevel.Number.Classes
+-- Copyright   : Alexey Khudyakov
+-- License     : BSD3-style (see LICENSE)
+--
+-- Maintainer  : Alexey Khudyakov <alexey.skladnoy@gmail.com>
+-- Stability   : unstable
+-- Portability : unportable (GHC only)
+--
+-- This module contain interface type classes for operations with type
+-- level numbers.
+module TypeLevel.Number.Classes ( -- * Comparison of numbers
+                                  Compare
+                                , compareN
+                                  -- ** Data labels for types comparison
+                                , IsLesser
+                                , IsEqual
+                                , IsGreater
+                                  -- ** Specialized type classes
+                                  -- $comparing
+                                , Lesser
+                                , LesserEq
+                                , Greater
+                                , GreaterEq
+                                  -- ** Special traits
+                                , Positive
+                                , NonZero
+                                  -- * Arithmetic operations on numbers
+                                , Next
+                                , nextN
+                                , Prev
+                                , prevN
+                                , Negate
+                                , negateN
+                                , Add
+                                , addN
+                                , Sub
+                                , subN
+                                , Mul
+                                , mulN
+                                , Div
+                                , divN
+                                  -- * Special classes
+                                , Normalized
+                                ) where
+
+----------------------------------------------------------------
+-- Comparison
+----------------------------------------------------------------
+
+-- | Type family for comparing two numbers. It's expected that for any
+-- two valid 'n' and 'm' 'Compare n m' is equal to IsLess when 'n<m', IsEqual
+-- when 'n=m' and IsGreater when 'n>m'.
+type family Compare n m :: *
+
+compareN :: n -> m -> Compare n m
+compareN _ _ = undefined
+
+data IsLesser
+data IsEqual
+data IsGreater
+
+instance Show IsLesser  where show _  = "IsLesser"
+instance Show IsEqual   where show _  = "IsEqual"
+instance Show IsGreater where show _  = "IsGreater"
+
+----------------------------------------------------------------
+
+-- $comparing
+-- These type classes are meant to be used in contexts to ensure
+-- relations between numbers. For example:
+-- 
+-- > someFunction :: Lesser n m => Data n -> Data m -> Data n
+-- > someFunction = ...
+--
+-- They have generic instances and every number which is instance of
+-- Compare type family is instance of these type classes.
+-- 
+-- These instance could have problems. They weren't exensively tested.
+-- Also error messages are really unhelpful.
+
+-- | Numbers n and m are instances of this class if and only is n < m.
+class Lesser n m
+
+-- | Numbers n and m are instances of this class if and only is n > m.
+class Greater n m
+
+-- | Numbers n and m are instances of this class if and only is n <= m.
+class LesserEq n m
+
+-- | Numbers n and m are instances of this class if and only is n >= m.
+class GreaterEq n m
+
+-- a b c are instance of class only when a ~ b or a ~ c. Require ovelapping.
+class    OneOfTwo a b c
+instance OneOfTwo a a b
+instance OneOfTwo a b a
+instance OneOfTwo a a a
+
+instance (Compare n m ~ IsLesser ) => Lesser n m
+instance (Compare n m ~ IsGreater) => Greater n m
+-- Instances for LessEq and GreaterEq are trickier.
+instance (OneOfTwo (Compare n m) IsLesser  IsEqual) => LesserEq n m
+instance (OneOfTwo (Compare n m) IsGreater IsEqual) => GreaterEq n m
+
+-- | Non-zero number. For naturals it's same as positive
+class NonZero n
+
+-- | Positive number. 
+class Positive n
+
+----------------------------------------------------------------
+
+-- | Next number.
+type family Next n :: *
+
+nextN :: n -> Next n
+nextN _ = undefined
+
+-- | Previous number
+type family Prev n :: *
+
+prevN :: n -> Prev n
+prevN _ = undefined
+
+-- | Negate number.
+type family Negate n :: *
+
+negateN :: n -> Negate n
+negateN _ = undefined
+
+----------------------------------------------------------------
+
+-- | Sum of two numbers.
+type family  Add n m :: *
+
+addN :: n -> m -> Add n m
+addN _ _ = undefined
+
+-- | Difference of two numbers.
+type family Sub n m :: *
+
+subN :: n -> m -> Sub n m
+subN _ _ = undefined
+
+-- | Product of two numbers.
+type family Mul n m :: *
+       
+mulN :: n -> m -> Mul n m
+mulN _ _ = undefined
+
+-- | Division of two numbers. 'n' and 'm' should be instances of this
+-- class only if remainder of 'n/m' is zero.
+type family Div n m :: *
+
+divN :: n -> m -> Div n m
+divN _ _ = undefined
+
+----------------------------------------------------------------
+
+-- | Usually numbers have non-unique representation. This type family
+-- is canonical representation of number.
+type family Normalized n :: *
diff --git a/TypeLevel/Number/Int.hs b/TypeLevel/Number/Int.hs
new file mode 100644
--- /dev/null
+++ b/TypeLevel/Number/Int.hs
@@ -0,0 +1,253 @@
+{-# LANGUAGE EmptyDataDecls        #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+-- |
+-- Module      : TypeLevel.Number.Int
+-- Copyright   : Alexey Khudyakov
+-- License     : BSD3-style (see LICENSE)
+--
+-- Maintainer  : Alexey Khudyakov <alexey.skladnoy@gmail.com>
+-- Stability   : unstable
+-- Portability : unportable (GHC only)
+--
+-- Type level signed integer numbers are implemented using balanced
+-- ternary encoding much in the same way as natural numbers.
+--
+-- Currently following operations are supported: Next, Prev, Add, Sub,
+-- Mul.
+module TypeLevel.Number.Int ( -- * Integer numbers
+                          ZZ
+                        , Dn
+                        , D0
+                        , D1
+                        , IntT
+                          -- * Template haskell utilities
+                        , intT
+                        , module TypeLevel.Number.Classes
+                        ) where
+
+import Language.Haskell.TH
+
+import TypeLevel.Number.Classes
+import TypeLevel.Number.Int.Types
+import TypeLevel.Util
+
+
+splitToTrits :: Integer -> [Int]
+splitToTrits 0 = []
+splitToTrits x | n == 0 =  0 : splitToTrits  rest
+               | n == 1 =  1 : splitToTrits  rest
+               | n == 2 = -1 : splitToTrits (rest + 1)
+                 where
+                   (rest,n) = divMod x 3
+
+-- | Generate type for integer number.
+intT :: Integer -> TypeQ
+intT = foldr appT [t| ZZ |] . map con . splitToTrits
+  where
+    con (-1) = [t| Dn |]
+    con   0 = [t| D0 |]
+    con   1 = [t| D1 |]
+    con   x = error $ "Strange trit: " ++ show x
+
+----------------------------------------------------------------
+--
+
+-- | Type class for type level integers. Only numbers without leading
+-- zeroes are members of the class.
+class IntT n where
+  -- | Convert natural number to integral value. It's not checked
+  -- whether value could be represented.
+  toInt :: Integral i => n -> i
+
+instance IntT     ZZ  where toInt _ =  0
+instance IntT (D1 ZZ) where toInt _ =  1
+instance IntT (Dn ZZ) where toInt _ = -1
+
+instance IntT (Dn n) => IntT (Dn (Dn n)) where toInt n = -1 + 3 * toInt' n
+instance IntT (Dn n) => IntT (D0 (Dn n)) where toInt n =  0 + 3 * toInt' n
+instance IntT (Dn n) => IntT (D1 (Dn n)) where toInt n =  1 + 3 * toInt' n
+instance IntT (D0 n) => IntT (Dn (D0 n)) where toInt n = -1 + 3 * toInt' n
+instance IntT (D0 n) => IntT (D0 (D0 n)) where toInt n =  0 + 3 * toInt' n
+instance IntT (D0 n) => IntT (D1 (D0 n)) where toInt n =  1 + 3 * toInt' n
+instance IntT (D1 n) => IntT (Dn (D1 n)) where toInt n = -1 + 3 * toInt' n
+instance IntT (D1 n) => IntT (D0 (D1 n)) where toInt n =  0 + 3 * toInt' n
+instance IntT (D1 n) => IntT (D1 (D1 n)) where toInt n =  1 + 3 * toInt' n
+
+toInt' :: (IntT n, Integral i) => t n -> i
+toInt' = toInt . cdr
+
+
+instance                Show    ZZ  where show _ = "[0:Z]"
+instance IntT (Dn n) => Show (Dn n) where show n = "["++show (toInt n)++":Z]"
+instance IntT (D0 n) => Show (D0 n) where show n = "["++show (toInt n)++":Z]"
+instance IntT (D1 n) => Show (D1 n) where show n = "["++show (toInt n)++":Z]"
+
+----------------------------------------------------------------
+-- Number normalization
+
+type family   AddBit n :: *
+type instance AddBit    ZZ = ZZ
+type instance AddBit (a b) = D0 (a b)
+
+type instance Normalized     ZZ = ZZ
+type instance Normalized (Dn n) = Dn     (Normalized n)
+type instance Normalized (D0 n) = AddBit (Normalized n)
+type instance Normalized (D1 n) = D1     (Normalized n)
+
+----------------------------------------------------------------
+-- Next Number
+type instance Next     ZZ = D1 ZZ
+type instance Next (Dn n) = Normalized (D0 n)
+type instance Next (D0 n) = D1 n
+type instance Next (D1 n) = Normalized (Dn (Next n))
+
+----------------------------------------------------------------
+-- Previous number
+type instance Prev     ZZ = Dn ZZ
+type instance Prev (Dn n) = Normalized (D1 (Prev n))
+type instance Prev (D0 n) = Dn n
+type instance Prev (D1 n) = Normalized (D0 n)
+
+----------------------------------------------------------------
+-- Negate number
+type instance Negate    ZZ  = ZZ
+type instance Negate (Dn n) = D1 (Negate n)
+type instance Negate (D0 n) = D0 (Negate n)
+type instance Negate (D1 n) = Dn (Negate n)
+
+
+----------------------------------------------------------------
+-- Addition
+
+-- Type class which actually implement addtition of natural numbers
+type family Add' n m carry :: *
+
+data CarryN
+data Carry0
+data Carry1
+
+-- Special cases with ZZ
+type instance Add'     ZZ     ZZ Carry0 = ZZ
+type instance Add'     ZZ (Dn n) Carry0 = (Dn n)
+type instance Add'     ZZ (D0 n) Carry0 = (D0 n)
+type instance Add'     ZZ (D1 n) Carry0 = (D1 n)
+type instance Add' (Dn n)     ZZ Carry0 = (Dn n)
+type instance Add' (D0 n)     ZZ Carry0 = (D0 n)
+type instance Add' (D1 n)     ZZ Carry0 = (D1 n)
+--
+type instance Add'     ZZ     ZZ CarryN = Dn ZZ
+type instance Add'     ZZ (Dn n) CarryN = Prev (Dn n)
+type instance Add'     ZZ (D0 n) CarryN = (Dn n)
+type instance Add'     ZZ (D1 n) CarryN = (D0 n)
+type instance Add' (Dn n)     ZZ CarryN = Prev (Dn n)
+type instance Add' (D0 n)     ZZ CarryN = (Dn n)
+type instance Add' (D1 n)     ZZ CarryN = (D0 n)
+--
+type instance Add'     ZZ     ZZ Carry1 = D1 ZZ
+type instance Add'     ZZ (Dn n) Carry1 = (D0 n)
+type instance Add'     ZZ (D0 n) Carry1 = (D1 n)
+type instance Add'     ZZ (D1 n) Carry1 = Next (D1 n)
+type instance Add' (Dn n)     ZZ Carry1 = (D0 n)
+type instance Add' (D0 n)     ZZ Carry1 = (D1 n)
+type instance Add' (D1 n)     ZZ Carry1 = Next (D1 n)
+
+-- == General recursion ==
+-- No carry
+type instance Add' (Dn n) (Dn m) Carry0 = D1 (Add' n m CarryN)
+type instance Add' (D0 n) (Dn m) Carry0 = Dn (Add' n m Carry0)
+type instance Add' (D1 n) (Dn m) Carry0 = D0 (Add' n m Carry0)
+--
+type instance Add' (Dn n) (D0 m) Carry0 = Dn (Add' n m Carry0)
+type instance Add' (D0 n) (D0 m) Carry0 = D0 (Add' n m Carry0)
+type instance Add' (D1 n) (D0 m) Carry0 = D1 (Add' n m Carry0)
+--
+type instance Add' (Dn n) (D1 m) Carry0 = D0 (Add' n m Carry0)
+type instance Add' (D0 n) (D1 m) Carry0 = D1 (Add' n m Carry0)
+type instance Add' (D1 n) (D1 m) Carry0 = Dn (Add' n m Carry1)
+-- Carry '-'
+type instance Add' (Dn n) (Dn m) CarryN = D0 (Add' n m CarryN)
+type instance Add' (D0 n) (Dn m) CarryN = D1 (Add' n m CarryN)
+type instance Add' (D1 n) (Dn m) CarryN = Dn (Add' n m Carry0)
+--
+type instance Add' (Dn n) (D0 m) CarryN = D1 (Add' n m CarryN)
+type instance Add' (D0 n) (D0 m) CarryN = Dn (Add' n m Carry0)
+type instance Add' (D1 n) (D0 m) CarryN = D0 (Add' n m Carry0)
+--
+type instance Add' (Dn n) (D1 m) CarryN = Dn (Add' n m Carry0)
+type instance Add' (D0 n) (D1 m) CarryN = D0 (Add' n m Carry0)
+type instance Add' (D1 n) (D1 m) CarryN = D1 (Add' n m Carry0)
+-- Carry '+'
+type instance Add' (Dn n) (Dn m) Carry1 = Dn (Add' n m Carry0)
+type instance Add' (D0 n) (Dn m) Carry1 = D0 (Add' n m Carry0)
+type instance Add' (D1 n) (Dn m) Carry1 = D1 (Add' n m Carry0)
+--
+type instance Add' (Dn n) (D0 m) Carry1 = D0 (Add' n m Carry0)
+type instance Add' (D0 n) (D0 m) Carry1 = D1 (Add' n m Carry0)
+type instance Add' (D1 n) (D0 m) Carry1 = Dn (Add' n m Carry1)
+--
+type instance Add' (Dn n) (D1 m) Carry1 = D1 (Add' n m Carry0)
+type instance Add' (D0 n) (D1 m) Carry1 = Dn (Add' n m Carry1)
+type instance Add' (D1 n) (D1 m) Carry1 = D0 (Add' n m Carry1)
+
+-- Instances for AddN
+type instance Add     ZZ     ZZ = ZZ
+type instance Add     ZZ (Dn n) = Normalized (Dn n)
+type instance Add     ZZ (D0 n) = Normalized (D0 n)
+type instance Add     ZZ (D1 n) = Normalized (D1 n)
+type instance Add (Dn n)     ZZ = Normalized (Dn n)
+type instance Add (D0 n)     ZZ = Normalized (D0 n)
+type instance Add (D1 n)     ZZ = Normalized (D1 n)
+--
+type instance Add (Dn n) (Dn m) = Normalized (Add' (Dn n) (Dn m) Carry0)
+type instance Add (D0 n) (Dn m) = Normalized (Add' (D0 n) (Dn m) Carry0)
+type instance Add (D1 n) (Dn m) = Normalized (Add' (D1 n) (Dn m) Carry0)
+--
+type instance Add (Dn n) (D0 m) = Normalized (Add' (Dn n) (D0 m) Carry0)
+type instance Add (D0 n) (D0 m) = Normalized (Add' (D0 n) (D0 m) Carry0)
+type instance Add (D1 n) (D0 m) = Normalized (Add' (D1 n) (D0 m) Carry0)
+--
+type instance Add (Dn n) (D1 m) = Normalized (Add' (Dn n) (D1 m) Carry0)
+type instance Add (D0 n) (D1 m) = Normalized (Add' (D0 n) (D1 m) Carry0)
+type instance Add (D1 n) (D1 m) = Normalized (Add' (D1 n) (D1 m) Carry0)
+
+
+----------------------------------------------------------------
+-- Subtraction.
+--
+-- Subtraction is much easier since is ise defined using
+-- addition and negation
+
+type instance Sub     ZZ     ZZ = ZZ
+type instance Sub     ZZ (Dn n) = Negate (Dn n)
+type instance Sub     ZZ (D0 n) = Negate (D0 n)
+type instance Sub     ZZ (D1 n) = Negate (D1 n)
+type instance Sub (Dn n)     ZZ = (Dn n)
+type instance Sub (D0 n)     ZZ = (D0 n)
+type instance Sub (D1 n)     ZZ = (D1 n)
+
+type instance Sub (Dn n) (Dn m) = Add (Dn n) (Negate (Dn m))
+type instance Sub (D0 n) (Dn m) = Add (D0 n) (Negate (Dn m))
+type instance Sub (D1 n) (Dn m) = Add (D1 n) (Negate (Dn m))
+--
+type instance Sub (Dn n) (D0 m) = Add (Dn n) (Negate (D0 m))
+type instance Sub (D0 n) (D0 m) = Add (D0 n) (Negate (D0 m))
+type instance Sub (D1 n) (D0 m) = Add (D1 n) (Negate (D0 m))
+--
+type instance Sub (Dn n) (D1 m) = Add (Dn n) (Negate (D1 m))
+type instance Sub (D0 n) (D1 m) = Add (D0 n) (Negate (D1 m))
+type instance Sub (D1 n) (D1 m) = Add (D1 n) (Negate (D1 m))
+
+
+----------------------------------------------------------------
+-- Multiplication
+
+type instance Mul n    ZZ  = ZZ
+type instance Mul n (Dn m) = Normalized (Add' (Negate n) (D0 (Mul n m)) Carry0)
+type instance Mul n (D0 m) = Normalized (D0 (Mul n m))
+type instance Mul n (D1 m) = Normalized (Add'         n  (D0 (Mul n m)) Carry0)
diff --git a/TypeLevel/Number/Int/Types.hs b/TypeLevel/Number/Int/Types.hs
new file mode 100644
--- /dev/null
+++ b/TypeLevel/Number/Int/Types.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE EmptyDataDecls #-}
+module TypeLevel.Number.Int.Types where
+  
+-- | Digit -1
+data Dn n
+-- | Digit 0
+data D0 n
+-- | Digit 1
+data D1 n
+-- | Digit stream terminator
+data ZZ
diff --git a/TypeLevel/Number/Nat.hs b/TypeLevel/Number/Nat.hs
new file mode 100644
--- /dev/null
+++ b/TypeLevel/Number/Nat.hs
@@ -0,0 +1,313 @@
+{-# LANGUAGE EmptyDataDecls        #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE UndecidableInstances  #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+-- |
+-- Module      : TypeLevel.Number.Nat
+-- Copyright   : Alexey Khudyakov
+-- License     : BSD3-style (see LICENSE)
+--
+-- Maintainer  : Alexey Khudyakov <alexey.skladnoy@gmail.com>
+-- Stability   : unstable
+-- Portability : unportable (GHC only)
+--
+--
+-- This is type level natural numbers. They are represented using
+-- binary encoding which means that reasonable large numbers could be
+-- represented. With default context stack depth (20) maximal number
+-- is 2^18-1 (262143).
+--
+-- > Z           = 0
+-- > I Z         = 1
+-- > O (I Z)     = 2
+-- > I (I Z)     = 3
+-- > O (O (I Z)) = 4
+-- > ...
+--
+-- It's easy to see that representation for each number is not
+-- unique. One could add any numbers of leading zeroes:
+--
+-- > I Z = I (O Z) = I (O (O Z)) = 1
+--
+-- In order to enforce uniqueness of representation only numbers
+-- without leading zeroes are members of Nat type class. This means
+-- than types are equal if and only if numbers are equal.
+--
+-- Natural numbers support comparison and following operations: Next,
+-- Prev, Add, Sub, Mul. All operations on numbers return normalized
+-- numbers.
+--
+-- Interface type classes are reexported from TypeLevel.Number.Classes
+module TypeLevel.Number.Nat ( -- * Natural numbers
+                          I
+                        , O
+                        , Z
+                        , Nat(..)
+                          -- * Template haskell utilities
+                          -- $TH
+                        , natT
+                        , nat
+                        , module TypeLevel.Number.Classes
+                        ) where
+
+import Data.Word (Word8,Word16,Word32,Word64)
+import Data.Int  (Int8, Int16, Int32, Int64 )
+
+
+import Language.Haskell.TH
+
+import TypeLevel.Number.Classes
+import TypeLevel.Number.Nat.Types
+import TypeLevel.Number.Nat.TH
+import TypeLevel.Reify
+
+-- $TH
+-- Here is usage example for natT:
+--
+-- > n123 :: $(natT 123)
+-- > n123 = undefined
+
+----------------------------------------------------------------
+
+-- | Type class for natural numbers. Only numbers without leading
+-- zeroes are members of this type class.
+class Nat n where
+  -- | Convert natural number to integral value. It's not checked
+  -- whether value could be represented.
+  toInt :: Integral i => n -> i
+
+-- | Type class for positive natural numbers. It's synonym for
+-- Positive and Nat.
+class Pos n
+
+instance              Nat       Z   where toInt _ = 0
+instance              Nat    (I Z)  where toInt _ = 1
+instance Nat (O n) => Nat (O (O n)) where toInt n = 0 + 2 * toInt (undefined :: (O n))
+instance Nat (O n) => Nat (I (O n)) where toInt n = 1 + 2 * toInt (undefined :: (O n))
+instance Nat (I n) => Nat (O (I n)) where toInt n = 0 + 2 * toInt (undefined :: (I n))
+instance Nat (I n) => Nat (I (I n)) where toInt n = 1 + 2 * toInt (undefined :: (I n))
+-- Error reporting. Stop for denormalized numbers
+class    Number_Is_Denormalized a
+instance (Number_Is_Denormalized Z) => Nat (O Z) where
+  toInt = error "quench warning"
+
+-- Synonym for positive
+instance (Nat n, Positive n) => Pos n
+
+
+----------------------------------------------------------------
+-- Data conversion
+
+-- To Integer
+instance                Reify    Z  Integer where witness = Witness 0
+instance (Nat (O n)) => Reify (O n) Integer where witness = Witness $ toInt (undefined :: O n)
+instance (Nat (I n)) => Reify (I n) Integer where witness = Witness $ toInt (undefined :: I n)
+
+-- To Int
+instance                Reify    Z  Int where witness = Witness 0
+instance (Nat (O n)) => Reify (O n) Int where witness = Witness $ toInt (undefined :: O n)
+instance (Nat (I n)) => Reify (I n) Int where witness = Witness $ toInt (undefined :: I n)
+
+-- To Word8
+instance                                              Reify    Z  Word8 where witness = Witness 0
+instance (Nat (O n), (O n) `Lesser` $(natT 0x100)) => Reify (O n) Word8 where witness = Witness $ toInt (undefined :: O n)
+instance (Nat (I n), (I n) `Lesser` $(natT 0x100)) => Reify (I n) Word8 where witness = Witness $ toInt (undefined :: I n)
+
+-- To Word16
+instance                                                Reify    Z  Word16 where witness = Witness 0
+instance (Nat (O n), (O n) `Lesser` $(natT 0x10000)) => Reify (O n) Word16 where witness = Witness $ toInt (undefined :: O n)
+instance (Nat (I n), (I n) `Lesser` $(natT 0x10000)) => Reify (I n) Word16 where witness = Witness $ toInt (undefined :: I n)
+
+-- To Word32 (No checks. Won't to default centext stack length)
+instance                Reify    Z  Word32 where witness = Witness 0
+instance (Nat (O n)) => Reify (O n) Word32 where witness = Witness $ toInt (undefined :: O n)
+instance (Nat (I n)) => Reify (I n) Word32 where witness = Witness $ toInt (undefined :: I n)
+
+-- To Word64 (No checks. Won't to default centext stack length)
+instance                Reify    Z  Word64 where witness = Witness 0
+instance (Nat (O n)) => Reify (O n) Word64 where witness = Witness $ toInt (undefined :: O n)
+instance (Nat (I n)) => Reify (I n) Word64 where witness = Witness $ toInt (undefined :: I n)
+
+-- To Int8
+instance                                             Reify    Z  Int8 where witness = Witness 0
+instance (Nat (O n), (O n) `Lesser` $(natT 0x80)) => Reify (O n) Int8 where witness = Witness $ toInt (undefined :: O n)
+instance (Nat (I n), (I n) `Lesser` $(natT 0x80)) => Reify (I n) Int8 where witness = Witness $ toInt (undefined :: I n)
+
+-- To Int16
+instance                                               Reify    Z  Int16 where witness = Witness 0
+instance (Nat (O n), (O n) `Lesser` $(natT 0x8000)) => Reify (O n) Int16 where witness = Witness $ toInt (undefined :: O n)
+instance (Nat (I n), (I n) `Lesser` $(natT 0x8000)) => Reify (I n) Int16 where witness = Witness $ toInt (undefined :: I n)
+
+-- To Int32 (No checks. Won't to default centext stack length)
+instance                Reify    Z  Int32 where witness = Witness 0
+instance (Nat (O n)) => Reify (O n) Int32 where witness = Witness $ toInt (undefined :: O n)
+instance (Nat (I n)) => Reify (I n) Int32 where witness = Witness $ toInt (undefined :: I n)
+
+-- To Int64 (No checks. Won't to default centext stack length)
+instance                Reify    Z  Int64 where witness = Witness 0
+instance (Nat (O n)) => Reify (O n) Int64 where witness = Witness $ toInt (undefined :: O n)
+instance (Nat (I n)) => Reify (I n) Int64 where witness = Witness $ toInt (undefined :: I n)
+
+----------------------------------------------------------------
+-- Number normalization
+
+-- Add trailing zero bit to number. It's added only if number is not
+-- equal to zero. Actual normalization is done here.
+type family   Add0Bit n :: *
+type instance Add0Bit    Z  = Z
+type instance Add0Bit (a b) = (O (a b))
+
+type instance Normalized    Z  = Z
+type instance Normalized (I n) = I (Normalized n)
+type instance Normalized (O n) = Add0Bit (Normalized n)
+
+----------------------------------------------------------------
+-- Show instances.
+-- Nat contexts are used to ensure correctness of numbers.
+instance              Show    Z  where show _ = "[0:N]"
+instance Nat (O n) => Show (O n) where show n = "["++show (toInt n)++":N]"
+instance Nat (I n) => Show (I n) where show n = "["++show (toInt n)++":N]"
+
+----------------------------------------------------------------
+-- Next number.
+-- Number normalization is not required.
+type instance Next    Z  = I Z
+type instance Next (I n) = O (Next n)
+type instance Next (O n) = I n
+
+----------------------------------------------------------------
+-- Previous number.
+-- Normalization isn't requred too. It's done manually in (I Z) case.
+type instance Prev    (I Z)   = Z
+type instance Prev (O (O n))  = I (Prev (O n))
+type instance Prev (I (O n))  = O (O n)
+type instance Prev (O (I n))  = I (Prev (I n))
+type instance Prev (I (I n))  = O (I n)
+
+
+----------------------------------------------------------------
+-- Comparison
+
+-- Join compare results. a is result of comparison of low digits b is
+-- result of comparion of higher digits.
+type family Join a b :: *
+
+type instance Join IsLesser  IsEqual   = IsLesser
+type instance Join IsEqual   IsEqual   = IsEqual
+type instance Join IsGreater IsEqual   = IsGreater
+type instance Join a         IsLesser  = IsLesser
+type instance Join a         IsGreater = IsGreater
+
+-- Instances for comparison
+type instance Compare    Z     Z  = IsEqual
+type instance Compare (O n)    Z  = IsGreater
+type instance Compare (I n)    Z  = IsGreater
+type instance Compare    Z  (O n) = IsLesser
+type instance Compare    Z  (I n) = IsLesser
+
+type instance Compare (O n) (O m) = Compare n m
+type instance Compare (O n) (I m) = Join IsLesser  (Compare n m)
+type instance Compare (I n) (O m) = Join IsGreater (Compare n m)
+type instance Compare (I n) (I m) = Compare n m
+
+----------------------------------------------------------------
+-- Positive and Non-zero numbers
+
+instance Nat (I n) => Positive (I n)
+instance Nat (O n) => Positive (O n)
+
+instance Nat (I n) => NonZero (I n)
+instance Nat (O n) => NonZero (O n)
+
+----------------------------------------------------------------
+-- Addition
+data Carry      -- Designate carry bit
+data NoCarry    -- No carry bit in addition
+
+-- Type family which actually implement addtition of natural numbers
+type family Add' n m c :: *
+
+-- Recursion termination without carry bit. Full enumeration is
+-- required to avoid overlapping instances
+type instance Add'    Z     Z  NoCarry = Z
+type instance Add' (O n)    Z  NoCarry = O n
+type instance Add' (I n)    Z  NoCarry = I n
+type instance Add'    Z  (O n) NoCarry = O n
+type instance Add'    Z  (I n) NoCarry = I n
+-- Recursion termination with carry bit
+type instance Add'    Z   Z      Carry = I Z
+type instance Add' (O n)  Z      Carry = I n
+type instance Add' (I n)  Z      Carry = Add' (I n) (I Z) NoCarry
+type instance Add'    Z  (O n)   Carry = I n
+type instance Add'    Z  (I n)   Carry = Add' (I n) (I Z) NoCarry
+-- Generic recursion (No carry)
+type instance Add' (O n) (O m) NoCarry = O (Add' n m NoCarry)
+type instance Add' (I n) (O m) NoCarry = I (Add' n m NoCarry)
+type instance Add' (O n) (I m) NoCarry = I (Add' n m NoCarry)
+type instance Add' (I n) (I m) NoCarry = O (Add' n m   Carry)
+-- Generic recursion (with carry)
+type instance Add' (O n) (O m)   Carry = I (Add' n m NoCarry)
+type instance Add' (I n) (O m)   Carry = O (Add' n m   Carry)
+type instance Add' (O n) (I m)   Carry = O (Add' n m   Carry)
+type instance Add' (I n) (I m)   Carry = I (Add' n m   Carry)
+
+-- Enumeration of all possible instances heads is required to avoid
+-- overlapping.
+type instance Add (O n) (O m) = Normalized (Add' (O n) (O m) NoCarry)
+type instance Add (I n) (O m) = Normalized (Add' (I n) (O m) NoCarry)
+type instance Add (O n) (I m) = Normalized (Add' (O n) (I m) NoCarry)
+type instance Add (I n) (I m) = Normalized (Add' (I n) (I m) NoCarry)
+type instance Add (O n)    Z  = Normalized (Add' (O n)    Z  NoCarry)
+type instance Add (I n)    Z  = Normalized (Add' (I n)    Z  NoCarry)
+type instance Add    Z  (O n) = Normalized (Add'    Z  (O n) NoCarry)
+type instance Add    Z  (I n) = Normalized (Add'    Z  (I n) NoCarry)
+type instance Add    Z     Z  = Normalized (Add'    Z     Z  NoCarry)
+
+----------------------------------------------------------------
+-- Subtraction
+data Borrow     -- Borrow bit
+data NoBorrow   -- Do not borrow bit
+
+-- Type class which actually implement addtition of natural numbers
+type family Sub' n m c :: *
+
+-- Recursion termination without carry bit. Full enumeration is
+-- required to avoid overlapping instances
+type instance Sub'    Z     Z  NoBorrow = Z
+type instance Sub' (O n)    Z  NoBorrow = O n
+type instance Sub' (I n)    Z  NoBorrow = I n
+-- Recursion termination with carry bit
+type instance Sub' (O n)  Z      Borrow = I (Sub' n Z Borrow)
+type instance Sub' (I n)  Z      Borrow = O n
+-- Generic recursion (No carry)
+type instance Sub' (O n) (O m) NoBorrow = O (Sub' n m NoBorrow)
+type instance Sub' (I n) (O m) NoBorrow = I (Sub' n m NoBorrow)
+type instance Sub' (O n) (I m) NoBorrow = I (Sub' n m   Borrow)
+type instance Sub' (I n) (I m) NoBorrow = O (Sub' n m NoBorrow)
+-- -- Generic recursion (with carry)
+type instance Sub' (O n) (O m)   Borrow = I (Sub' n m   Borrow)
+type instance Sub' (I n) (O m)   Borrow = O (Sub' n m NoBorrow)
+type instance Sub' (O n) (I m)   Borrow = O (Sub' n m   Borrow)
+type instance Sub' (I n) (I m)   Borrow = I (Sub' n m   Borrow)
+
+-- Enumeration of all possible instances heads is required to avoid
+-- overlapping.
+type instance Sub (O n) (O m) = Normalized (Sub' (O n) (O m) NoBorrow)
+type instance Sub (I n) (O m) = Normalized (Sub' (I n) (O m) NoBorrow)
+type instance Sub (O n) (I m) = Normalized (Sub' (O n) (I m) NoBorrow)
+type instance Sub (I n) (I m) = Normalized (Sub' (I n) (I m) NoBorrow)
+type instance Sub (O n)    Z  = Normalized (Sub' (O n)    Z  NoBorrow)
+type instance Sub (I n)    Z  = Normalized (Sub' (I n)    Z  NoBorrow)
+type instance Sub    Z     Z  = Normalized (Sub'    Z     Z  NoBorrow)
+
+----------------------------------------------------------------
+-- Multiplication
+----------------------------------------------------------------
+
+type instance Mul n    Z  = Z
+type instance Mul n (O m) = Normalized (O (Mul n m))
+type instance Mul n (I m) = Normalized (Add' n (O (Mul n m)) NoCarry)
diff --git a/TypeLevel/Number/Nat/Num.hs b/TypeLevel/Number/Nat/Num.hs
new file mode 100644
--- /dev/null
+++ b/TypeLevel/Number/Nat/Num.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE TemplateHaskell #-}
+module TypeLevel.Number.Nat.Num where
+
+import TypeLevel.Number.Nat
+
+type N0 = $(natT 0)
+type N1 = $(natT 1)
+type N2 = $(natT 2)
+type N3 = $(natT 3)
+type N4 = $(natT 4)
+type N5 = $(natT 5)
+type N6 = $(natT 6)
+type N7 = $(natT 7)
+type N8 = $(natT 8)
+type N9 = $(natT 9)
+
+n0 :: N0; n0 = undefined
+n1 :: N1; n1 = undefined
+n2 :: N2; n2 = undefined
+n3 :: N3; n3 = undefined
+n4 :: N4; n4 = undefined
+n5 :: N5; n5 = undefined
+n6 :: N6; n6 = undefined
+n7 :: N7; n7 = undefined
+n8 :: N8; n8 = undefined
+n9 :: N9; n9 = undefined
diff --git a/TypeLevel/Number/Nat/TH.hs b/TypeLevel/Number/Nat/TH.hs
new file mode 100644
--- /dev/null
+++ b/TypeLevel/Number/Nat/TH.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE TemplateHaskell #-}
+module TypeLevel.Number.Nat.TH ( nat
+                               , natT
+                               ) where
+
+
+import Language.Haskell.TH
+import TypeLevel.Number.Nat.Types
+
+splitToBits :: Integer -> [Int]
+splitToBits 0 = []
+splitToBits x | odd x     = 1 : splitToBits rest
+              | otherwise = 0 : splitToBits rest
+                where rest = x `div` 2
+
+
+-- | Create type for natural number.
+natT :: Integer -> TypeQ
+natT n | n >= 0    = foldr appT [t| Z |] . map con . splitToBits $ n
+       | otherwise = error "natT: negative number is supplied"
+  where
+    con 0 = [t| O |]
+    con 1 = [t| I |]
+    con _ = error "natT: Strange bit nor 0 nor 1"
+
+-- | Create value for type level natural. Value itself is undefined.
+nat :: Integer -> ExpQ
+nat n = sigE [|undefined|] (natT n)
diff --git a/TypeLevel/Number/Nat/Types.hs b/TypeLevel/Number/Nat/Types.hs
new file mode 100644
--- /dev/null
+++ b/TypeLevel/Number/Nat/Types.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE EmptyDataDecls #-}
+module TypeLevel.Number.Nat.Types ( I
+                                  , O
+                                  , Z
+                                  ) where
+
+-- | One bit.
+data I n
+-- | Zero bit.
+data O n
+-- | Bit stream terminator.
+data Z
diff --git a/TypeLevel/Reify.hs b/TypeLevel/Reify.hs
new file mode 100644
--- /dev/null
+++ b/TypeLevel/Reify.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+-- |
+-- Module      : TypeLevel.Reify
+-- Copyright   : Alexey Khudyakov
+-- License     : BSD3-style (see LICENSE)
+--
+-- Maintainer  : Alexey Khudyakov <alexey.skladnoy@gmail.com>
+-- Stability   : unstable
+-- Portability : unportable (GHC only)
+module TypeLevel.Reify ( Witness(..)
+                       , Reify(..)
+                       ) where
+
+
+data Witness t a = Witness { getValue :: a }
+                   deriving Show
+
+-- | Convert type level into value level using 
+class Reify t a where
+  witness :: Witness t a
+
+       
+       
diff --git a/TypeLevel/Util.hs b/TypeLevel/Util.hs
new file mode 100644
--- /dev/null
+++ b/TypeLevel/Util.hs
@@ -0,0 +1,5 @@
+module TypeLevel.Util ( cdr 
+                  ) where
+
+cdr :: t a -> a
+cdr _ = undefined
diff --git a/type-level-numbers.cabal b/type-level-numbers.cabal
new file mode 100644
--- /dev/null
+++ b/type-level-numbers.cabal
@@ -0,0 +1,49 @@
+Name:           type-level-numbers
+Version:        0.1
+Cabal-Version:  >= 1.6
+License:        BSD3
+License-File:   LICENSE
+Author:         Alexey Khudyakov <alexey.skladnoy@gmail.com>
+Maintainer:     Alexey Khudyakov <alexey.skladnoy@gmail.com>
+Homepage:       
+Category:       Type System
+Build-Type:     Simple
+Synopsis:       
+  Type level numbers implemented using type families.
+Description:
+  This is type level numbers implemented using type families. Natural
+  numbers use binary encoding. With default context stack numbers up
+  to 2^18-1 coudl be represented. Signed integer numbers use balanced ternary
+  encoding.
+  .
+  Package is structured as folows:
+  .
+  * [@TypeLevel.Number.Classes@] contain generic type families such as Add
+  .
+  * [@TypeLevel.Number.Nat@] natural numbers implemented using binary encoding
+  .
+  * [@TypeLevel.Number.Int@] signed integers implemented using balanced
+    ternary encoding
+  .
+  * [@TypeLevel.Boolean@] type level booleans
+  .
+  So far comparison of numbers, subtraction and multiplication of
+  numbers are supported.
+
+source-repository head
+  type:     hg
+  location: http://bitbucket.org/Shimuuar/type-numbers
+
+Library
+  Build-Depends:   base >=3 && <5,
+                   template-haskell > 2.0
+  Exposed-modules: TypeLevel.Number.Classes
+                   TypeLevel.Number.Nat
+                   TypeLevel.Number.Nat.Num
+                   TypeLevel.Number.Int
+                   TypeLevel.Boolean
+                   TypeLevel.Reify
+  Other-modules:   TypeLevel.Number.Nat.Types
+                   TypeLevel.Number.Nat.TH
+                   TypeLevel.Number.Int.Types
+                   TypeLevel.Util