diff --git a/Data/SizedInt.hs b/Data/SizedInt.hs
new file mode 100644
--- /dev/null
+++ b/Data/SizedInt.hs
@@ -0,0 +1,157 @@
+module Data.SizedInt
+    ( SizedInt ) where
+
+import Data.Bits
+import Types
+
+newtype (NaturalT nT) => SizedInt nT = SizedInt Integer
+
+sizeT :: SizedInt nT
+      -> nT
+sizeT _ = undefined
+
+mask :: forall nT . NaturalT nT
+     => nT
+     -> Integer
+mask _ = bit (fromIntegerT (undefined :: nT)) - 1
+
+signBit :: forall nT . NaturalT nT
+        => nT
+        -> Int
+signBit _ = fromIntegerT (undefined :: nT) - 1
+
+isNegative :: forall nT . NaturalT nT
+           => SizedInt nT
+           -> Bool
+isNegative (SizedInt x) =
+    testBit x $ signBit (undefined :: nT)
+
+instance NaturalT nT => Eq (SizedInt nT) where
+    (SizedInt x) == (SizedInt y) = x == y
+    (SizedInt x) /= (SizedInt y) = x /= y
+
+instance NaturalT nT => Show (SizedInt nT) where
+    showsPrec prec n =
+        showsPrec prec $ toInteger n
+
+instance NaturalT nT => Read (SizedInt nT) where
+    readsPrec prec str =
+        [ (fromInteger n, str)
+        | (n, str) <- readsPrec prec str ]
+
+instance NaturalT nT => Ord (SizedInt nT) where
+    a `compare` b = toInteger a `compare` toInteger b
+
+instance NaturalT nT => Bounded (SizedInt nT) where
+    minBound = SizedInt $ negate $ 1 `shiftL` (fromIntegerT (undefined :: nT) - 1)
+    maxBound = SizedInt $ (1 `shiftL` (fromIntegerT (undefined :: nT) - 1)) - 1
+
+instance NaturalT nT => Enum (SizedInt nT) where
+    succ x
+       | x == maxBound  = error $ "Enum.succ{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `succ' of maxBound"
+       | otherwise      = x + 1
+    pred x
+       | x == minBound  = error $ "Enum.succ{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `pred' of minBound"
+       | otherwise      = x - 1
+    
+    fromEnum (SizedInt x)
+        | x > toInteger (maxBound :: Int) =
+            error $ "Enum.fromEnum{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedInt greater than maxBound :: Int"
+        | x < toInteger (minBound :: Int) =
+            error $ "Enum.fromEnum{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedInt smaller than minBound :: Int"
+        | otherwise =
+            fromInteger x
+    toEnum x
+        | x' > toInteger (maxBound :: SizedInt nT) =
+            error $ "Enum.fromEnum{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedInt greater than maxBound :: SizedInt " ++ show (fromIntegerT (undefined :: nT))
+        | x' < toInteger (minBound :: SizedInt nT) =
+            error $ "Enum.fromEnum{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedInt smaller than minBound :: SizedInt " ++ show (fromIntegerT (undefined :: nT))
+        | otherwise =
+            fromInteger x'
+            where x' = toInteger x
+
+instance NaturalT nT => Num (SizedInt nT) where
+    (SizedInt a) + (SizedInt b) =
+        fromInteger $ a + b
+    (SizedInt a) * (SizedInt b) =
+        fromInteger $ a * b
+    negate (SizedInt n) =
+        fromInteger $ (n `xor` mask (undefined :: nT)) + 1
+    a - b =
+        a + (negate b)
+    
+    fromInteger n
+      | n > 0 =
+        SizedInt $ n .&. mask (undefined :: nT)
+    fromInteger n
+      | n < 0 =
+        negate $ fromInteger $ negate n
+    fromInteger _ =
+        SizedInt 0
+    
+    abs s
+      | isNegative s =
+          negate s
+      | otherwise =
+          s
+    signum s
+      | isNegative s =
+          -1
+      | s == 0 =
+          0
+      | otherwise =
+          1
+
+instance NaturalT nT => Real (SizedInt nT) where
+    toRational n = toRational $ toInteger n
+
+instance NaturalT nT => Integral (SizedInt nT) where
+    a `quot` b =
+        fromInteger $ toInteger a `quot` toInteger b
+    a `rem` b =
+        fromInteger $ toInteger a `rem` toInteger b
+    a `div` b =
+        fromInteger $ toInteger a `div` toInteger b
+    a `mod` b =
+        fromInteger $ toInteger a `mod` toInteger b
+    a `quotRem` b =
+        let (quot, rem) = toInteger a `quotRem` toInteger b
+        in (fromInteger quot, fromInteger rem)
+    a `divMod` b =
+        let (div, mod) = toInteger a `divMod` toInteger b
+        in (fromInteger div, fromInteger mod)
+    toInteger s@(SizedInt x) =
+        if isNegative s
+           then let SizedInt x' = negate s in negate x'
+           else x
+
+instance NaturalT nT => Bits (SizedInt nT) where
+    (SizedInt a) .&. (SizedInt b) = SizedInt $ a .&. b
+    (SizedInt a) .|. (SizedInt b) = SizedInt $ a .|. b
+    (SizedInt a) `xor` SizedInt b = SizedInt $ a `xor` b
+    complement (SizedInt x) = SizedInt $ x `xor` mask (undefined :: nT)
+    (SizedInt x) `shiftL` b
+      | b < 0 = error $ "Bits.shiftL{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to shift by negative amount"
+      | otherwise =
+        SizedInt $ mask (undefined :: nT) .&. (x `shiftL` b)
+    s@(SizedInt x) `shiftR` b
+      | b < 0 = error $ "Bits.shiftR{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to shift by negative amount"
+      | isNegative s =
+        SizedInt $ mask (undefined :: nT) .&.
+            ((x `shiftR` b) .|. (mask (undefined :: nT) `shiftL` (fromIntegerT (undefined :: nT) - b)))
+      | otherwise =
+        SizedInt $ (mask (undefined :: nT)) .&. (x `shiftR` b)
+    (SizedInt a) `rotateL` b
+      | b < 0 =
+        error $ "Bits.rotateL{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to rotate by negative amount"
+      | otherwise =
+        SizedInt $ mask (undefined :: nT) .&.
+            ((a `shiftL` b) .|. (a `shiftR` (fromIntegerT (undefined :: nT) - b)))
+    (SizedInt a) `rotateR` b
+      | b < 0 =
+        error $ "Bits.rotateR{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to rotate by negative amount"
+      | otherwise =
+        SizedInt $ mask (undefined :: nT) .&.
+            ((a `shiftR` b) .|. (a `shiftL` (fromIntegerT (undefined :: nT) - b)))
+    bitSize _ = fromIntegerT (undefined :: nT)
+    isSigned _ = True
diff --git a/Data/SizedWord.hs b/Data/SizedWord.hs
new file mode 100644
--- /dev/null
+++ b/Data/SizedWord.hs
@@ -0,0 +1,133 @@
+module Data.SizedWord
+    ( SizedWord ) where
+
+import Data.Bits
+import Types
+
+newtype (NaturalT nT) => SizedWord nT = SizedWord Integer
+
+sizeT :: SizedWord nT
+      -> nT
+sizeT _ = undefined
+
+mask :: forall nT . NaturalT nT
+     => nT
+     -> Integer
+mask _ = bit (fromIntegerT (undefined :: nT)) - 1
+
+instance NaturalT nT => Eq (SizedWord nT) where
+    (SizedWord x) == (SizedWord y) = x == y
+    (SizedWord x) /= (SizedWord y) = x /= y
+
+instance NaturalT nT => Show (SizedWord nT) where
+    showsPrec prec n =
+        showsPrec prec $ toInteger n
+
+instance NaturalT nT => Read (SizedWord nT) where
+    readsPrec prec str =
+        [ (fromInteger n, str)
+        | (n, str) <- readsPrec prec str ]
+
+instance NaturalT nT => Ord (SizedWord nT) where
+    a `compare` b = toInteger a `compare` toInteger b
+
+instance NaturalT nT => Bounded (SizedWord nT) where
+    minBound = 0
+    maxBound = SizedWord $ (1 `shiftL` (fromIntegerT (undefined :: nT))) - 1
+
+instance NaturalT nT => Enum (SizedWord nT) where
+    succ x
+       | x == maxBound  = error $ "Enum.succ{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `succ' of maxBound"
+       | otherwise      = x + 1
+    pred x
+       | x == minBound  = error $ "Enum.succ{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `pred' of minBound"
+       | otherwise      = x - 1
+    
+    fromEnum (SizedWord x)
+        | x > toInteger (maxBound :: Int) =
+            error $ "Enum.fromEnum{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedWord greater than maxBound :: Int"
+        | x < toInteger (minBound :: Int) =
+            error $ "Enum.fromEnum{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedWord smaller than minBound :: Int"
+        | otherwise =
+            fromInteger x
+    toEnum x
+        | x > fromIntegral (maxBound :: SizedWord nT) =
+            error $ "Enum.fromEnum{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedWord greater than maxBound :: SizedWord " ++ show (fromIntegerT (undefined :: nT))
+        | x < fromIntegral (minBound :: SizedWord nT) =
+            error $ "Enum.fromEnum{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedWord smaller than minBound :: SizedWord " ++ show (fromIntegerT (undefined :: nT))
+        | otherwise =
+            fromInteger $ toInteger x
+
+instance NaturalT nT => Num (SizedWord nT) where
+    (SizedWord a) + (SizedWord b) =
+        fromInteger $ a + b
+    (SizedWord a) * (SizedWord b) =
+        fromInteger $ a * b
+    negate s@(SizedWord n) =
+        fromInteger $ (n `xor` mask (sizeT s)) + 1
+    a - b =
+        a + (negate b)
+    
+    fromInteger n
+      | n > 0 =
+        SizedWord $ n .&. mask (undefined :: nT)
+    fromInteger n
+      | n < 0 =
+        negate $ fromInteger $ negate n
+    fromInteger _ =
+        SizedWord 0
+    
+    abs s = s
+    signum s
+      | s == 0 =
+          0
+      | otherwise =
+          1
+
+instance NaturalT nT => Real (SizedWord nT) where
+    toRational n = toRational $ toInteger n
+
+instance NaturalT nT => Integral (SizedWord nT) where
+    a `quot` b =
+        fromInteger $ toInteger a `quot` toInteger b
+    a `rem` b =
+        fromInteger $ toInteger a `rem` toInteger b
+    a `div` b =
+        fromInteger $ toInteger a `div` toInteger b
+    a `mod` b =
+        fromInteger $ toInteger a `mod` toInteger b
+    a `quotRem` b =
+        let (quot, rem) = toInteger a `quotRem` toInteger b
+        in (fromInteger quot, fromInteger rem)
+    a `divMod` b =
+        let (div, mod) = toInteger a `divMod` toInteger b
+        in (fromInteger div, fromInteger mod)
+    toInteger s@(SizedWord x) = x
+
+instance NaturalT nT => Bits (SizedWord nT) where
+    (SizedWord a) .&. (SizedWord b) = SizedWord $ a .&. b
+    (SizedWord a) .|. (SizedWord b) = SizedWord $ a .|. b
+    (SizedWord a) `xor` SizedWord b = SizedWord $ a `xor` b
+    complement (SizedWord x) = SizedWord $ x `xor` mask (undefined :: nT)
+    s@(SizedWord x) `shiftL` b
+      | b < 0 = error $ "Bits.shiftL{SizedWord " ++ show (bitSize s) ++ "}: tried to shift by negative amount"
+      | otherwise =
+        SizedWord $ mask (undefined :: nT) .&. (x `shiftL` b)
+    s@(SizedWord x) `shiftR` b
+      | b < 0 = error $ "Bits.shiftR{SizedWord " ++ show (bitSize s) ++ "}: tried to shift by negative amount"
+      | otherwise =
+        SizedWord $ (x `shiftR` b)
+    s@(SizedWord x) `rotateL` b
+      | b < 0 =
+        error $ "Bits.rotateL{SizedWord " ++ show (bitSize s) ++ "}: tried to rotate by negative amount"
+      | otherwise =
+        SizedWord $ mask (undefined :: nT) .&.
+            ((x `shiftL` b) .|. (x `shiftR` (bitSize s - b)))
+    s@(SizedWord x) `rotateR` b
+      | b < 0 =
+        error $ "Bits.rotateR{SizedWord " ++ show (bitSize s) ++ "}: tried to rotate by negative amount"
+      | otherwise =
+        SizedWord $ mask (undefined :: nT) .&.
+            ((x `shiftR` b) .|. (x `shiftL` (bitSize s - b)))
+    bitSize _ = fromIntegerT (undefined :: nT)
+    isSigned _ = False
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,25 @@
+Copyright (c) 2008 Peter Gavin
+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 the copyright holder nor the
+      names of its 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 HOLDER ``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 HOLDER 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/Test.hs b/Test.hs
new file mode 100644
--- /dev/null
+++ b/Test.hs
@@ -0,0 +1,155 @@
+module Main where
+
+import qualified Prelude
+
+import Types.Data.Ord
+import Types.Data.Num
+import Types.Data.Num.Decimal.Literals.TH
+import Types.Data.Bool
+import Data.SizedWord
+
+testIsPositive1 :: IsPositive D1 -> True
+testIsPositive1 = Prelude.id
+testIsPositive2 :: IsPositive D0 -> False
+testIsPositive2 = Prelude.id
+testIsPositive3 :: IsPositive DN1 -> False
+testIsPositive3 = Prelude.id
+testIsPositive4 :: IsPositive D10 -> True
+testIsPositive4 = Prelude.id
+testIsPositive5 :: IsPositive DN10 -> False
+testIsPositive5 = Prelude.id
+
+testIsNegative1 :: IsNegative D1 -> False
+testIsNegative1 = Prelude.id
+testIsNegative2 :: IsNegative D0 -> False
+testIsNegative2 = Prelude.id
+testIsNegative3 :: IsNegative DN1 -> True
+testIsNegative3 = Prelude.id
+testIsNegative4 :: IsNegative D10 -> False
+testIsNegative4 = Prelude.id
+testIsNegative5 :: IsNegative DN10 -> True
+testIsNegative5 = Prelude.id
+
+testIsZero1 :: IsZero D1 -> False
+testIsZero1 = Prelude.id
+testIsZero2 :: IsZero D0 -> True
+testIsZero2 = Prelude.id
+testIsZero3 :: IsZero DN1 -> False
+testIsZero3 = Prelude.id
+testIsZero4 :: IsZero D10 -> False
+testIsZero4 = Prelude.id
+testIsZero5 :: IsZero DN10 -> False
+testIsZero5 = Prelude.id
+
+testSucc1 :: Succ D0 -> D1
+testSucc1 = Prelude.id
+testSucc2 :: Succ D9 -> D10
+testSucc2 = Prelude.id
+testSucc3 :: Succ DN1 -> D0
+testSucc3 = Prelude.id
+testSucc4 :: Succ D99 -> D100
+testSucc4 = Prelude.id
+testSucc5 :: Succ DN100 -> DN99
+testSucc5 = Prelude.id
+testSucc6 :: Succ D100 -> D101
+testSucc6 = Prelude.id
+testSucc7 :: Succ DN101 -> DN100
+testSucc7 = Prelude.id
+
+testPred1 :: Pred D1 -> D0
+testPred1 = Prelude.id
+testPred2 :: Pred D0 -> DN1
+testPred2 = Prelude.id
+testPred3 :: Pred DN1 -> DN2
+testPred3 = Prelude.id
+testPred4 :: Pred DN9 -> DN10
+testPred4 = Prelude.id
+testPred5 :: Pred D10 -> D9
+testPred5 = Prelude.id
+testPred6 :: Pred DN99 -> DN100
+testPred6 = Prelude.id
+testPred7 :: Pred D100 -> D99
+testPred7 = Prelude.id
+
+testAdd1 :: D0 :+: D0 -> D0
+testAdd1 = Prelude.id
+testAdd2 :: DN1 :+: D1 -> D0
+testAdd2 = Prelude.id
+testAdd3 :: D1 :+: DN1 -> D0
+testAdd3 = Prelude.id
+testAdd4 :: D1 :+: D1 -> D2
+testAdd4 = Prelude.id
+testAdd5 :: D9 :+: D1 -> D10
+testAdd5 = Prelude.id
+testAdd6 :: D10 :+: DN1 -> D9
+testAdd6 = Prelude.id
+testAdd7 :: D100 :+: DN1 -> D99
+testAdd7 = Prelude.id
+testAdd8 :: D100 :+: DN10 -> D90
+testAdd8 = Prelude.id
+
+testSub1 :: D0 :-: D0 -> D0
+testSub1 = Prelude.id
+testSub2 :: D1 :-: D0 -> D1
+testSub2 = Prelude.id
+testSub3 :: D0 :-: D1 -> DN1
+testSub3 = Prelude.id
+testSub4 :: DN1 :-: D0 -> DN1
+testSub4 = Prelude.id
+testSub5 :: D0 :-: DN1 -> D1
+testSub5 = Prelude.id
+testSub6 :: D100 :-: D1 -> D99
+testSub6 = Prelude.id
+testSub7 :: DN100 :-: D1 -> DN101
+testSub7 = Prelude.id
+testSub8 :: D100 :-: DN1 -> D101
+testSub8 = Prelude.id
+testSub9 :: DN100 :-: DN1 -> DN99
+testSub9 = Prelude.id
+testSub10 :: D1 :-: D100 -> DN99
+testSub10 = Prelude.id
+testSub11 :: DN1 :-: D100 -> DN101
+testSub11 = Prelude.id
+testSub12 :: D1 :-: DN100 -> D101
+testSub12 = Prelude.id
+testSub13 :: DN1 :-: DN100 -> D99
+testSub13 = Prelude.id
+testSub14 :: D57 :-: D58 -> DN1
+testSub14 = Prelude.id
+testSub15 :: D1000 :-: D11 -> D989
+testSub15 = Prelude.id
+
+testMul1 :: D0 :*: D0 -> D0
+testMul1 = Prelude.id
+testMul2 :: D1 :*: D1 -> D1
+testMul2 = Prelude.id
+testMul3 :: D0 :*: D1 -> D0
+testMul3 = Prelude.id
+testMul4 :: D1 :*: D0 -> D0
+testMul4 = Prelude.id
+testMul5 :: D1 :*: DN1 -> DN1
+testMul5 = Prelude.id
+testMul6 :: DN1 :*: D1 -> DN1
+testMul6 = Prelude.id
+testMul7 :: DN1 :*: DN1 -> D1
+testMul7 = Prelude.id
+testMul8 :: D100 :*: D100 -> D10000
+testMul8 = Prelude.id
+testMul9 :: D17 :*: D31 -> D527
+testMul9 = Prelude.id
+
+testFac1 :: Fac D0 -> D1
+testFac1 = Prelude.id
+testFac2 :: Fac D1 -> D1
+testFac2 = Prelude.id
+testFac3 :: Fac D6 -> D720
+testFac3 = Prelude.id
+$( decLiteralD "D" "d" 3628800 )
+testFac4 :: Fac D10 -> D3628800
+testFac4 = Prelude.id
+
+f :: n -> (n :+: D5)
+f _ = Prelude.undefined
+
+main :: Prelude.IO ()
+main = Prelude.return ()
diff --git a/Types.hs b/Types.hs
new file mode 100644
--- /dev/null
+++ b/Types.hs
@@ -0,0 +1,13 @@
+module Types
+    ( module Types.Base
+    , module Types.Data.Bool
+    , module Types.Data.Num
+    , module Types.Data.List
+    , module Types.Data.Ord
+    ) where
+
+import Types.Base
+import Types.Data.Bool
+import Types.Data.Num
+import Types.Data.List
+import Types.Data.Ord
diff --git a/Types/Base.hs b/Types/Base.hs
new file mode 100644
--- /dev/null
+++ b/Types/Base.hs
@@ -0,0 +1,24 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Types.Data.Decimal.Ops
+-- Copyright   :  (c) 2008 Peter Gavin
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  pgavin@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (type families, requires ghc >= 6.9)
+--
+-- Type-level numerical operations using type families.
+-- 
+----------------------------------------------------------------------------
+
+module Types.Base
+    where
+
+import qualified Prelude
+
+type family Id x
+type instance Id x = x
+
+_T :: a
+_T = Prelude.undefined
diff --git a/Types/Data/Bool.hs b/Types/Data/Bool.hs
new file mode 100644
--- /dev/null
+++ b/Types/Data/Bool.hs
@@ -0,0 +1,70 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Types.Data.Bool
+-- Copyright   :  (c) 2008 Peter Gavin
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  pgavin@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (type families, requires ghc >= 6.9)
+--
+-- Type-level numerical operations using type families.
+-- 
+----------------------------------------------------------------------------
+
+module Types.Data.Bool
+    ( True
+    , trueT
+    , False
+    , falseT
+    , Not
+    , notT
+    , (:&&:)
+    , andT
+    , (:||:)
+    , orT
+    , IfT(..)
+    ) where
+
+import Data.Typeable
+
+import qualified Prelude
+
+data True deriving (Typeable)
+trueT :: True
+trueT = Prelude.undefined
+instance Prelude.Show True where
+    show _ = "True"
+data False deriving (Typeable)
+falseT :: False
+falseT = Prelude.undefined
+instance Prelude.Show False where
+    show _ = "False"
+
+type family Not x
+type instance Not False = True
+type instance Not True  = False
+notT :: x -> Not x
+notT _ = Prelude.undefined
+
+type family x :&&: y
+type instance False :&&: x = False
+type instance True  :&&: x = x
+andT :: x -> y -> x :&&: x
+andT _ _ = Prelude.undefined
+
+type family x :||: y
+type instance True  :||: x = True
+type instance False :||: x = x
+orT :: x -> y -> x :||: x
+orT _ _ = Prelude.undefined
+
+class IfT x y z where
+    type If x y z
+    ifT :: x -> y -> z -> If x y z
+instance IfT True y z where
+    type If True y z = y
+    ifT _ y _ = y
+instance IfT False y z where
+    type If False y z = z
+    ifT _ _ z = z
diff --git a/Types/Data/List.hs b/Types/Data/List.hs
new file mode 100644
--- /dev/null
+++ b/Types/Data/List.hs
@@ -0,0 +1,47 @@
+module Types.Data.List
+    ( Cons
+    , Null
+    , IsNull
+    , Head
+    , Tail
+    , Reverse
+    , Append
+    ) where
+
+import qualified Prelude
+
+import Data.Typeable
+
+import Types.Data.Bool
+
+data Cons car cdr deriving (Typeable)
+instance (Prelude.Show car, Prelude.Show cdr) => Prelude.Show (Cons car cdr) where
+    show = showCons
+
+showCons :: forall car cdr . (Prelude.Show car, Prelude.Show cdr) => Cons car cdr -> Prelude.String
+showCons _ = "Cons (" Prelude.++ Prelude.show (Prelude.undefined :: car) Prelude.++ ") (" Prelude.++ Prelude.show (Prelude.undefined :: cdr) Prelude.++ ")"
+
+data Null deriving (Typeable)
+instance Prelude.Show Null where
+    show _ = ""
+
+type family IsNull l
+type instance IsNull (Cons car cdr) = False
+type instance IsNull Null = True
+
+type family Head l
+type instance Head (Cons car cdr) = car
+
+type family Tail l
+type instance Tail (Cons car cdr) = cdr
+
+type family Reverse l
+type instance Reverse l = Reverse' l Null
+
+type family Reverse' l a
+type instance Reverse' Null a = a
+type instance Reverse' (Cons car cdr) a = Reverse' cdr (Cons car a)
+
+type family Append l1 l2
+type instance Append Null l2 = l2
+type instance Append (Cons car1 cdr2) l2 = Cons car1 (Append cdr2 l2)
diff --git a/Types/Data/Num.hs b/Types/Data/Num.hs
new file mode 100644
--- /dev/null
+++ b/Types/Data/Num.hs
@@ -0,0 +1,21 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Types.Data.Num
+-- Copyright   :  (c) 2008 Peter Gavin
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  pgavin@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (type families, requires ghc >= 6.9)
+--
+-- Type-level numerical operations using type families.
+-- 
+----------------------------------------------------------------------------
+
+module Types.Data.Num
+    ( module Types.Data.Num.Ops
+    , module Types.Data.Num.Decimal
+    ) where
+
+import Types.Data.Num.Ops
+import Types.Data.Num.Decimal
diff --git a/Types/Data/Num/Decimal.hs b/Types/Data/Num/Decimal.hs
new file mode 100644
--- /dev/null
+++ b/Types/Data/Num/Decimal.hs
@@ -0,0 +1,9 @@
+module Types.Data.Num.Decimal
+    ( module Types.Data.Num.Decimal.Digits
+    , module Types.Data.Num.Decimal.Literals
+    , module Types.Data.Num.Decimal.Ops
+    ) where
+
+import Types.Data.Num.Decimal.Digits
+import Types.Data.Num.Decimal.Literals
+import Types.Data.Num.Decimal.Ops ()
diff --git a/Types/Data/Num/Decimal/Digits.hs b/Types/Data/Num/Decimal/Digits.hs
new file mode 100644
--- /dev/null
+++ b/Types/Data/Num/Decimal/Digits.hs
@@ -0,0 +1,61 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Types.Data.Num.Decimal.Digits
+-- Copyright   :  (c) 2008 Peter Gavin
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  pgavin@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (type families, requires ghc >= 6.9)
+--
+-- Type-level numerical operations using type families.
+-- 
+----------------------------------------------------------------------------
+
+module Types.Data.Num.Decimal.Digits
+    where
+
+import Data.Typeable
+
+import Types.Data.List
+import Types.Data.Num.Ops
+
+-- | The wrapper type for decimal type level numbers.
+data Dec x
+data Neg' x
+
+-- | The terminator type for decimal digit lists.
+data DecN
+instance Show DecN where
+    show _ = ""
+
+data Dec0 deriving (Typeable)
+instance Show Dec0 where
+    show _ = "0"
+data Dec1 deriving (Typeable)
+instance Show Dec1 where
+    show _ = "1"
+data Dec2 deriving (Typeable)
+instance Show Dec2 where
+    show _ = "2"
+data Dec3 deriving (Typeable)
+instance Show Dec3 where
+    show _ = "3"
+data Dec4 deriving (Typeable)
+instance Show Dec4 where
+    show _ = "4"
+data Dec5 deriving (Typeable)
+instance Show Dec5 where
+    show _ = "5"
+data Dec6 deriving (Typeable)
+instance Show Dec6 where
+    show _ = "6"
+data Dec7 deriving (Typeable)
+instance Show Dec7 where
+    show _ = "7"
+data Dec8 deriving (Typeable)
+instance Show Dec8 where
+    show _ = "8"
+data Dec9 deriving (Typeable)
+instance Show Dec9 where
+    show _ = "9"
diff --git a/Types/Data/Num/Decimal/Literals.hs b/Types/Data/Num/Decimal/Literals.hs
new file mode 100644
--- /dev/null
+++ b/Types/Data/Num/Decimal/Literals.hs
@@ -0,0 +1,8 @@
+module Types.Data.Num.Decimal.Literals where
+
+import Types.Data.Num.Decimal.Literals.TH
+
+import Types.Data.Num.Decimal.Digits
+import Types.Data.Num.Ops
+
+$( decLiteralsD "D" "d" (-10000) (10000) )
diff --git a/Types/Data/Num/Decimal/Literals/TH.hs b/Types/Data/Num/Decimal/Literals/TH.hs
new file mode 100644
--- /dev/null
+++ b/Types/Data/Num/Decimal/Literals/TH.hs
@@ -0,0 +1,30 @@
+module Types.Data.Num.Decimal.Literals.TH where
+
+import Language.Haskell.TH
+
+decLiteralT :: Integer -> Q Type
+decLiteralT n = appT (conT (mkName "Dec")) (decLiteralT' n)
+    where decLiteralT' n | n < 0     = appT (conT (mkName "Neg'")) (decLiteralT' (-n))
+                         | n == 0    = conT (mkName "DecN")
+                         | otherwise = appT (appT (conT (mkName ":.")) (decLiteralT' (n `div` 10))) (conT (mkName ("Dec" ++ show (n `mod` 10))))
+
+decLiteralD :: String
+            -> String
+            -> Integer
+            -> Q [Dec]
+decLiteralD typePrefix valPrefix n =
+    do let suffix = if n < 0 then "N" ++ show (-n) else show n
+           typeName = mkName $ typePrefix ++ suffix
+           valName = mkName $ valPrefix ++ suffix
+       tySyn <- tySynD typeName [] (decLiteralT n)
+       sig   <- sigD valName (conT typeName)
+       val   <- valD (varP valName) (normalB [| undefined |]) []
+       return [ tySyn, sig, val ]
+
+decLiteralsD :: String
+             -> String
+             -> Integer
+             -> Integer
+             -> Q [Dec]
+decLiteralsD typePrefix valPrefix from to =
+    fmap concat $ sequence $ [ decLiteralD typePrefix valPrefix n | n <- [from..to] ]
diff --git a/Types/Data/Num/Decimal/Ops.hs b/Types/Data/Num/Decimal/Ops.hs
new file mode 100644
--- /dev/null
+++ b/Types/Data/Num/Decimal/Ops.hs
@@ -0,0 +1,886 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Types.Data.Num.Decimal.Ops
+-- Copyright   :  (c) 2008 Peter Gavin
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  pgavin@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (type families, requires ghc >= 6.9)
+--
+-- Type-level numerical operations using type families.
+-- 
+----------------------------------------------------------------------------
+
+module Types.Data.Num.Decimal.Ops ()
+    where
+
+import Types.Base
+import Types.Data.Bool
+import Types.Data.Ord
+import Types.Data.Num.Ops
+import Types.Data.Num.Decimal.Literals
+import Types.Data.Num.Decimal.Digits
+
+instance IntegerT' x => IntegerT (Dec x) where
+    fromIntegerT _ = fromIntegerT' (undefined :: x)
+
+class IntegerT' x where
+    fromIntegerT' :: Num y => x -> y
+instance IntegerT' DecN where
+    fromIntegerT' _ = 0
+instance IntegerT' x => IntegerT' (Neg' x) where
+    fromIntegerT' _ = negate (fromIntegerT' (undefined :: x))
+instance IntegerT' xh => IntegerT' (xh :. Dec0) where
+    fromIntegerT' _ = 0 + 10 * fromIntegerT' (undefined :: xh)
+instance IntegerT' xh => IntegerT' (xh :. Dec1) where
+    fromIntegerT' _ = 1 + 10 * fromIntegerT' (undefined :: xh)
+instance IntegerT' xh => IntegerT' (xh :. Dec2) where
+    fromIntegerT' _ = 2 + 10 * fromIntegerT' (undefined :: xh)
+instance IntegerT' xh => IntegerT' (xh :. Dec3) where
+    fromIntegerT' _ = 3 + 10 * fromIntegerT' (undefined :: xh)
+instance IntegerT' xh => IntegerT' (xh :. Dec4) where
+    fromIntegerT' _ = 4 + 10 * fromIntegerT' (undefined :: xh)
+instance IntegerT' xh => IntegerT' (xh :. Dec5) where
+    fromIntegerT' _ = 5 + 10 * fromIntegerT' (undefined :: xh)
+instance IntegerT' xh => IntegerT' (xh :. Dec6) where
+    fromIntegerT' _ = 6 + 10 * fromIntegerT' (undefined :: xh)
+instance IntegerT' xh => IntegerT' (xh :. Dec7) where
+    fromIntegerT' _ = 7 + 10 * fromIntegerT' (undefined :: xh)
+instance IntegerT' xh => IntegerT' (xh :. Dec8) where
+    fromIntegerT' _ = 8 + 10 * fromIntegerT' (undefined :: xh)
+instance IntegerT' xh => IntegerT' (xh :. Dec9) where
+    fromIntegerT' _ = 9 + 10 * fromIntegerT' (undefined :: xh)
+
+type family Normalize x
+type instance Normalize (Dec x) = Dec (Normalize' x)
+
+type family Normalize' x
+type instance Normalize' DecN       = DecN
+type instance Normalize' (xh :. xl) = NormalizePos (xh :. xl)
+type instance Normalize' (Neg' x)   = NormalizeNeg x
+
+type family NormalizePos x
+type instance NormalizePos x = NormalizePos' (ReverseDigits x)
+type family NormalizePos' x
+type instance NormalizePos' DecN         = DecN
+type instance NormalizePos' (xh :. Dec0) = NormalizePos' xh
+type instance NormalizePos' (xh :. Dec1) = ReverseDigits (xh :. Dec1)
+type instance NormalizePos' (xh :. Dec2) = ReverseDigits (xh :. Dec2)
+type instance NormalizePos' (xh :. Dec3) = ReverseDigits (xh :. Dec3)
+type instance NormalizePos' (xh :. Dec4) = ReverseDigits (xh :. Dec4)
+type instance NormalizePos' (xh :. Dec5) = ReverseDigits (xh :. Dec5)
+type instance NormalizePos' (xh :. Dec6) = ReverseDigits (xh :. Dec6)
+type instance NormalizePos' (xh :. Dec7) = ReverseDigits (xh :. Dec7)
+type instance NormalizePos' (xh :. Dec8) = ReverseDigits (xh :. Dec8)
+type instance NormalizePos' (xh :. Dec9) = ReverseDigits (xh :. Dec9)
+
+type family ReverseDigits x
+type instance ReverseDigits DecN       = DecN
+type instance ReverseDigits (xh :. xl) = ReverseDigits' (xh :. xl) DecN
+
+type family ReverseDigits' x y
+type instance ReverseDigits' DecN y = y
+type instance ReverseDigits' (xh :. xl) y = ReverseDigits' xh (y :. xl)
+
+type family NormalizeNeg x
+type instance NormalizeNeg (Neg' x)   = Normalize' x -- negate . negate == id
+type instance NormalizeNeg DecN       = DecN         -- negate 0 = 0
+type instance NormalizeNeg (xh :. xl) = NormalizeNeg' (NormalizePos (xh :. xl))
+
+type family NormalizeNeg' x
+type instance NormalizeNeg' DecN = DecN
+type instance NormalizeNeg' (xh :. xl) = Neg' (xh :. xl)
+
+-- type family IsPositive x
+type instance IsPositive (Dec x) = IsPositive' x
+type family IsPositive' x
+type instance IsPositive' (Neg' x)   = False
+type instance IsPositive' DecN       = False
+type instance IsPositive' (xh :. xl) = True
+
+-- type family IsZero x
+type instance IsZero (Dec x) = IsZero' x
+type family IsZero' x
+type instance IsZero' (Neg' x)   = False
+type instance IsZero' DecN       = True
+type instance IsZero' (xh :. xl) = False
+
+-- type family IsNegative x
+type instance IsNegative (Dec x) = IsNegative' x
+type family IsNegative' x
+type instance IsNegative' (Neg' x)   = True
+type instance IsNegative' DecN       = False
+type instance IsNegative' (xh :. xl) = False
+
+-- type family Neg x
+type instance Neg (Dec DecN)     = Dec DecN
+type instance Neg (Dec (Neg' x)) = Dec x
+type instance Neg (Dec (xh :. xl)) = Dec (Neg' (xh :. xl))
+
+-- type family Succ x
+type instance Succ (Dec x) = Dec (Succ' x)
+
+type family Succ' x
+type instance Succ' (Neg' x   ) = Normalize' (Neg' (Pred'' x))
+type instance Succ' (DecN     ) = DecN :. Dec1
+type instance Succ' (x :. Dec0) = x :. Dec1
+type instance Succ' (x :. Dec1) = x :. Dec2
+type instance Succ' (x :. Dec2) = x :. Dec3
+type instance Succ' (x :. Dec3) = x :. Dec4
+type instance Succ' (x :. Dec4) = x :. Dec5
+type instance Succ' (x :. Dec5) = x :. Dec6
+type instance Succ' (x :. Dec6) = x :. Dec7
+type instance Succ' (x :. Dec7) = x :. Dec8
+type instance Succ' (x :. Dec8) = x :. Dec9
+type instance Succ' (x :. Dec9) = Succ' x :. Dec0
+
+-- type family Pred x
+type instance Pred (Dec x)     = Dec (Pred' x)
+
+type family Pred' x
+type instance Pred' x = Normalize' (Pred'' x)
+type family Pred'' x
+type instance Pred'' (Neg' x   ) = Neg' (Succ' x)
+type instance Pred'' (DecN     ) = Neg' (DecN :. Dec1)
+type instance Pred'' (x :. Dec0) = Pred'' x :. Dec9
+type instance Pred'' (x :. Dec1) = x :. Dec0
+type instance Pred'' (x :. Dec2) = x :. Dec1
+type instance Pred'' (x :. Dec3) = x :. Dec2
+type instance Pred'' (x :. Dec4) = x :. Dec3
+type instance Pred'' (x :. Dec5) = x :. Dec4
+type instance Pred'' (x :. Dec6) = x :. Dec5
+type instance Pred'' (x :. Dec7) = x :. Dec6
+type instance Pred'' (x :. Dec8) = x :. Dec7
+type instance Pred'' (x :. Dec9) = x :. Dec8
+
+--------------------
+-- Addition
+
+type family AddDigit x y
+-- putStr $ unlines $ concat $ [ [ "type instance AddDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = Dec" ++ show ((x+y) `mod` 10) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
+type instance AddDigit Dec0 Dec0 = Dec0
+type instance AddDigit Dec0 Dec1 = Dec1
+type instance AddDigit Dec0 Dec2 = Dec2
+type instance AddDigit Dec0 Dec3 = Dec3
+type instance AddDigit Dec0 Dec4 = Dec4
+type instance AddDigit Dec0 Dec5 = Dec5
+type instance AddDigit Dec0 Dec6 = Dec6
+type instance AddDigit Dec0 Dec7 = Dec7
+type instance AddDigit Dec0 Dec8 = Dec8
+type instance AddDigit Dec0 Dec9 = Dec9
+
+type instance AddDigit Dec1 Dec0 = Dec1
+type instance AddDigit Dec1 Dec1 = Dec2
+type instance AddDigit Dec1 Dec2 = Dec3
+type instance AddDigit Dec1 Dec3 = Dec4
+type instance AddDigit Dec1 Dec4 = Dec5
+type instance AddDigit Dec1 Dec5 = Dec6
+type instance AddDigit Dec1 Dec6 = Dec7
+type instance AddDigit Dec1 Dec7 = Dec8
+type instance AddDigit Dec1 Dec8 = Dec9
+type instance AddDigit Dec1 Dec9 = Dec0
+
+type instance AddDigit Dec2 Dec0 = Dec2
+type instance AddDigit Dec2 Dec1 = Dec3
+type instance AddDigit Dec2 Dec2 = Dec4
+type instance AddDigit Dec2 Dec3 = Dec5
+type instance AddDigit Dec2 Dec4 = Dec6
+type instance AddDigit Dec2 Dec5 = Dec7
+type instance AddDigit Dec2 Dec6 = Dec8
+type instance AddDigit Dec2 Dec7 = Dec9
+type instance AddDigit Dec2 Dec8 = Dec0
+type instance AddDigit Dec2 Dec9 = Dec1
+
+type instance AddDigit Dec3 Dec0 = Dec3
+type instance AddDigit Dec3 Dec1 = Dec4
+type instance AddDigit Dec3 Dec2 = Dec5
+type instance AddDigit Dec3 Dec3 = Dec6
+type instance AddDigit Dec3 Dec4 = Dec7
+type instance AddDigit Dec3 Dec5 = Dec8
+type instance AddDigit Dec3 Dec6 = Dec9
+type instance AddDigit Dec3 Dec7 = Dec0
+type instance AddDigit Dec3 Dec8 = Dec1
+type instance AddDigit Dec3 Dec9 = Dec2
+
+type instance AddDigit Dec4 Dec0 = Dec4
+type instance AddDigit Dec4 Dec1 = Dec5
+type instance AddDigit Dec4 Dec2 = Dec6
+type instance AddDigit Dec4 Dec3 = Dec7
+type instance AddDigit Dec4 Dec4 = Dec8
+type instance AddDigit Dec4 Dec5 = Dec9
+type instance AddDigit Dec4 Dec6 = Dec0
+type instance AddDigit Dec4 Dec7 = Dec1
+type instance AddDigit Dec4 Dec8 = Dec2
+type instance AddDigit Dec4 Dec9 = Dec3
+
+type instance AddDigit Dec5 Dec0 = Dec5
+type instance AddDigit Dec5 Dec1 = Dec6
+type instance AddDigit Dec5 Dec2 = Dec7
+type instance AddDigit Dec5 Dec3 = Dec8
+type instance AddDigit Dec5 Dec4 = Dec9
+type instance AddDigit Dec5 Dec5 = Dec0
+type instance AddDigit Dec5 Dec6 = Dec1
+type instance AddDigit Dec5 Dec7 = Dec2
+type instance AddDigit Dec5 Dec8 = Dec3
+type instance AddDigit Dec5 Dec9 = Dec4
+
+type instance AddDigit Dec6 Dec0 = Dec6
+type instance AddDigit Dec6 Dec1 = Dec7
+type instance AddDigit Dec6 Dec2 = Dec8
+type instance AddDigit Dec6 Dec3 = Dec9
+type instance AddDigit Dec6 Dec4 = Dec0
+type instance AddDigit Dec6 Dec5 = Dec1
+type instance AddDigit Dec6 Dec6 = Dec2
+type instance AddDigit Dec6 Dec7 = Dec3
+type instance AddDigit Dec6 Dec8 = Dec4
+type instance AddDigit Dec6 Dec9 = Dec5
+
+type instance AddDigit Dec7 Dec0 = Dec7
+type instance AddDigit Dec7 Dec1 = Dec8
+type instance AddDigit Dec7 Dec2 = Dec9
+type instance AddDigit Dec7 Dec3 = Dec0
+type instance AddDigit Dec7 Dec4 = Dec1
+type instance AddDigit Dec7 Dec5 = Dec2
+type instance AddDigit Dec7 Dec6 = Dec3
+type instance AddDigit Dec7 Dec7 = Dec4
+type instance AddDigit Dec7 Dec8 = Dec5
+type instance AddDigit Dec7 Dec9 = Dec6
+
+type instance AddDigit Dec8 Dec0 = Dec8
+type instance AddDigit Dec8 Dec1 = Dec9
+type instance AddDigit Dec8 Dec2 = Dec0
+type instance AddDigit Dec8 Dec3 = Dec1
+type instance AddDigit Dec8 Dec4 = Dec2
+type instance AddDigit Dec8 Dec5 = Dec3
+type instance AddDigit Dec8 Dec6 = Dec4
+type instance AddDigit Dec8 Dec7 = Dec5
+type instance AddDigit Dec8 Dec8 = Dec6
+type instance AddDigit Dec8 Dec9 = Dec7
+
+type instance AddDigit Dec9 Dec0 = Dec9
+type instance AddDigit Dec9 Dec1 = Dec0
+type instance AddDigit Dec9 Dec2 = Dec1
+type instance AddDigit Dec9 Dec3 = Dec2
+type instance AddDigit Dec9 Dec4 = Dec3
+type instance AddDigit Dec9 Dec5 = Dec4
+type instance AddDigit Dec9 Dec6 = Dec5
+type instance AddDigit Dec9 Dec7 = Dec6
+type instance AddDigit Dec9 Dec8 = Dec7
+type instance AddDigit Dec9 Dec9 = Dec8
+
+-- | If adding @x@ and @y@ would not carry, then
+--   @AddCarry x y z@ evaluates to @z@.  Otherwise,
+--   @AddCarry x y z@ evaluates to @Succ' z@
+type family AddCarry x y z
+-- putStr $ unlines $ concat $ [ [ "type instance AddCarry Dec" ++ show x ++ " Dec" ++ show y ++ " x = " ++ (if x + y >= 10 then "Succ'" else "Id") ++ " x" | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
+type instance AddCarry Dec0 Dec0 x = Id x
+type instance AddCarry Dec0 Dec1 x = Id x
+type instance AddCarry Dec0 Dec2 x = Id x
+type instance AddCarry Dec0 Dec3 x = Id x
+type instance AddCarry Dec0 Dec4 x = Id x
+type instance AddCarry Dec0 Dec5 x = Id x
+type instance AddCarry Dec0 Dec6 x = Id x
+type instance AddCarry Dec0 Dec7 x = Id x
+type instance AddCarry Dec0 Dec8 x = Id x
+type instance AddCarry Dec0 Dec9 x = Id x
+
+type instance AddCarry Dec1 Dec0 x = Id x
+type instance AddCarry Dec1 Dec1 x = Id x
+type instance AddCarry Dec1 Dec2 x = Id x
+type instance AddCarry Dec1 Dec3 x = Id x
+type instance AddCarry Dec1 Dec4 x = Id x
+type instance AddCarry Dec1 Dec5 x = Id x
+type instance AddCarry Dec1 Dec6 x = Id x
+type instance AddCarry Dec1 Dec7 x = Id x
+type instance AddCarry Dec1 Dec8 x = Id x
+type instance AddCarry Dec1 Dec9 x = Succ' x
+
+type instance AddCarry Dec2 Dec0 x = Id x
+type instance AddCarry Dec2 Dec1 x = Id x
+type instance AddCarry Dec2 Dec2 x = Id x
+type instance AddCarry Dec2 Dec3 x = Id x
+type instance AddCarry Dec2 Dec4 x = Id x
+type instance AddCarry Dec2 Dec5 x = Id x
+type instance AddCarry Dec2 Dec6 x = Id x
+type instance AddCarry Dec2 Dec7 x = Id x
+type instance AddCarry Dec2 Dec8 x = Succ' x
+type instance AddCarry Dec2 Dec9 x = Succ' x
+
+type instance AddCarry Dec3 Dec0 x = Id x
+type instance AddCarry Dec3 Dec1 x = Id x
+type instance AddCarry Dec3 Dec2 x = Id x
+type instance AddCarry Dec3 Dec3 x = Id x
+type instance AddCarry Dec3 Dec4 x = Id x
+type instance AddCarry Dec3 Dec5 x = Id x
+type instance AddCarry Dec3 Dec6 x = Id x
+type instance AddCarry Dec3 Dec7 x = Succ' x
+type instance AddCarry Dec3 Dec8 x = Succ' x
+type instance AddCarry Dec3 Dec9 x = Succ' x
+
+type instance AddCarry Dec4 Dec0 x = Id x
+type instance AddCarry Dec4 Dec1 x = Id x
+type instance AddCarry Dec4 Dec2 x = Id x
+type instance AddCarry Dec4 Dec3 x = Id x
+type instance AddCarry Dec4 Dec4 x = Id x
+type instance AddCarry Dec4 Dec5 x = Id x
+type instance AddCarry Dec4 Dec6 x = Succ' x
+type instance AddCarry Dec4 Dec7 x = Succ' x
+type instance AddCarry Dec4 Dec8 x = Succ' x
+type instance AddCarry Dec4 Dec9 x = Succ' x
+
+type instance AddCarry Dec5 Dec0 x = Id x
+type instance AddCarry Dec5 Dec1 x = Id x
+type instance AddCarry Dec5 Dec2 x = Id x
+type instance AddCarry Dec5 Dec3 x = Id x
+type instance AddCarry Dec5 Dec4 x = Id x
+type instance AddCarry Dec5 Dec5 x = Succ' x
+type instance AddCarry Dec5 Dec6 x = Succ' x
+type instance AddCarry Dec5 Dec7 x = Succ' x
+type instance AddCarry Dec5 Dec8 x = Succ' x
+type instance AddCarry Dec5 Dec9 x = Succ' x
+
+type instance AddCarry Dec6 Dec0 x = Id x
+type instance AddCarry Dec6 Dec1 x = Id x
+type instance AddCarry Dec6 Dec2 x = Id x
+type instance AddCarry Dec6 Dec3 x = Id x
+type instance AddCarry Dec6 Dec4 x = Succ' x
+type instance AddCarry Dec6 Dec5 x = Succ' x
+type instance AddCarry Dec6 Dec6 x = Succ' x
+type instance AddCarry Dec6 Dec7 x = Succ' x
+type instance AddCarry Dec6 Dec8 x = Succ' x
+type instance AddCarry Dec6 Dec9 x = Succ' x
+
+type instance AddCarry Dec7 Dec0 x = Id x
+type instance AddCarry Dec7 Dec1 x = Id x
+type instance AddCarry Dec7 Dec2 x = Id x
+type instance AddCarry Dec7 Dec3 x = Succ' x
+type instance AddCarry Dec7 Dec4 x = Succ' x
+type instance AddCarry Dec7 Dec5 x = Succ' x
+type instance AddCarry Dec7 Dec6 x = Succ' x
+type instance AddCarry Dec7 Dec7 x = Succ' x
+type instance AddCarry Dec7 Dec8 x = Succ' x
+type instance AddCarry Dec7 Dec9 x = Succ' x
+
+type instance AddCarry Dec8 Dec0 x = Id x
+type instance AddCarry Dec8 Dec1 x = Id x
+type instance AddCarry Dec8 Dec2 x = Succ' x
+type instance AddCarry Dec8 Dec3 x = Succ' x
+type instance AddCarry Dec8 Dec4 x = Succ' x
+type instance AddCarry Dec8 Dec5 x = Succ' x
+type instance AddCarry Dec8 Dec6 x = Succ' x
+type instance AddCarry Dec8 Dec7 x = Succ' x
+type instance AddCarry Dec8 Dec8 x = Succ' x
+type instance AddCarry Dec8 Dec9 x = Succ' x
+
+type instance AddCarry Dec9 Dec0 x = Id x
+type instance AddCarry Dec9 Dec1 x = Succ' x
+type instance AddCarry Dec9 Dec2 x = Succ' x
+type instance AddCarry Dec9 Dec3 x = Succ' x
+type instance AddCarry Dec9 Dec4 x = Succ' x
+type instance AddCarry Dec9 Dec5 x = Succ' x
+type instance AddCarry Dec9 Dec6 x = Succ' x
+type instance AddCarry Dec9 Dec7 x = Succ' x
+type instance AddCarry Dec9 Dec8 x = Succ' x
+type instance AddCarry Dec9 Dec9 x = Succ' x
+
+-- type family x :+: y
+type instance Dec x :+: Dec y = Dec (Add x y)
+
+type family Add x y
+type instance Add (DecN    ) (DecN    ) = DecN
+type instance Add (xh :. xl) (DecN    ) = (xh :. xl)
+type instance Add (DecN    ) (yh :. yl) = (yh :. yl)
+type instance Add (Neg' x  ) (Neg' y  ) = Neg' (Add x y)
+type instance Add (xh :. xl) (Neg' y  ) = Sub (xh :. xl) y
+type instance Add (Neg' x  ) (yh :. yl) = Sub (yh :. yl) x
+type instance Add (xh :. xl) (yh :. yl) = (AddCarry xl yl (Add xh yh)) :. (AddDigit xl yl)
+
+--------------------
+-- Subtraction
+
+type family SubDigit x y
+-- putStr $ unlines $ concat $ [ [ "type instance SubDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = Dec" ++ show ((x-y) `mod` 10) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
+type instance SubDigit Dec0 Dec0 = Dec0
+type instance SubDigit Dec0 Dec1 = Dec9
+type instance SubDigit Dec0 Dec2 = Dec8
+type instance SubDigit Dec0 Dec3 = Dec7
+type instance SubDigit Dec0 Dec4 = Dec6
+type instance SubDigit Dec0 Dec5 = Dec5
+type instance SubDigit Dec0 Dec6 = Dec4
+type instance SubDigit Dec0 Dec7 = Dec3
+type instance SubDigit Dec0 Dec8 = Dec2
+type instance SubDigit Dec0 Dec9 = Dec1
+
+type instance SubDigit Dec1 Dec0 = Dec1
+type instance SubDigit Dec1 Dec1 = Dec0
+type instance SubDigit Dec1 Dec2 = Dec9
+type instance SubDigit Dec1 Dec3 = Dec8
+type instance SubDigit Dec1 Dec4 = Dec7
+type instance SubDigit Dec1 Dec5 = Dec6
+type instance SubDigit Dec1 Dec6 = Dec5
+type instance SubDigit Dec1 Dec7 = Dec4
+type instance SubDigit Dec1 Dec8 = Dec3
+type instance SubDigit Dec1 Dec9 = Dec2
+
+type instance SubDigit Dec2 Dec0 = Dec2
+type instance SubDigit Dec2 Dec1 = Dec1
+type instance SubDigit Dec2 Dec2 = Dec0
+type instance SubDigit Dec2 Dec3 = Dec9
+type instance SubDigit Dec2 Dec4 = Dec8
+type instance SubDigit Dec2 Dec5 = Dec7
+type instance SubDigit Dec2 Dec6 = Dec6
+type instance SubDigit Dec2 Dec7 = Dec5
+type instance SubDigit Dec2 Dec8 = Dec4
+type instance SubDigit Dec2 Dec9 = Dec3
+
+type instance SubDigit Dec3 Dec0 = Dec3
+type instance SubDigit Dec3 Dec1 = Dec2
+type instance SubDigit Dec3 Dec2 = Dec1
+type instance SubDigit Dec3 Dec3 = Dec0
+type instance SubDigit Dec3 Dec4 = Dec9
+type instance SubDigit Dec3 Dec5 = Dec8
+type instance SubDigit Dec3 Dec6 = Dec7
+type instance SubDigit Dec3 Dec7 = Dec6
+type instance SubDigit Dec3 Dec8 = Dec5
+type instance SubDigit Dec3 Dec9 = Dec4
+
+type instance SubDigit Dec4 Dec0 = Dec4
+type instance SubDigit Dec4 Dec1 = Dec3
+type instance SubDigit Dec4 Dec2 = Dec2
+type instance SubDigit Dec4 Dec3 = Dec1
+type instance SubDigit Dec4 Dec4 = Dec0
+type instance SubDigit Dec4 Dec5 = Dec9
+type instance SubDigit Dec4 Dec6 = Dec8
+type instance SubDigit Dec4 Dec7 = Dec7
+type instance SubDigit Dec4 Dec8 = Dec6
+type instance SubDigit Dec4 Dec9 = Dec5
+
+type instance SubDigit Dec5 Dec0 = Dec5
+type instance SubDigit Dec5 Dec1 = Dec4
+type instance SubDigit Dec5 Dec2 = Dec3
+type instance SubDigit Dec5 Dec3 = Dec2
+type instance SubDigit Dec5 Dec4 = Dec1
+type instance SubDigit Dec5 Dec5 = Dec0
+type instance SubDigit Dec5 Dec6 = Dec9
+type instance SubDigit Dec5 Dec7 = Dec8
+type instance SubDigit Dec5 Dec8 = Dec7
+type instance SubDigit Dec5 Dec9 = Dec6
+
+type instance SubDigit Dec6 Dec0 = Dec6
+type instance SubDigit Dec6 Dec1 = Dec5
+type instance SubDigit Dec6 Dec2 = Dec4
+type instance SubDigit Dec6 Dec3 = Dec3
+type instance SubDigit Dec6 Dec4 = Dec2
+type instance SubDigit Dec6 Dec5 = Dec1
+type instance SubDigit Dec6 Dec6 = Dec0
+type instance SubDigit Dec6 Dec7 = Dec9
+type instance SubDigit Dec6 Dec8 = Dec8
+type instance SubDigit Dec6 Dec9 = Dec7
+
+type instance SubDigit Dec7 Dec0 = Dec7
+type instance SubDigit Dec7 Dec1 = Dec6
+type instance SubDigit Dec7 Dec2 = Dec5
+type instance SubDigit Dec7 Dec3 = Dec4
+type instance SubDigit Dec7 Dec4 = Dec3
+type instance SubDigit Dec7 Dec5 = Dec2
+type instance SubDigit Dec7 Dec6 = Dec1
+type instance SubDigit Dec7 Dec7 = Dec0
+type instance SubDigit Dec7 Dec8 = Dec9
+type instance SubDigit Dec7 Dec9 = Dec8
+
+type instance SubDigit Dec8 Dec0 = Dec8
+type instance SubDigit Dec8 Dec1 = Dec7
+type instance SubDigit Dec8 Dec2 = Dec6
+type instance SubDigit Dec8 Dec3 = Dec5
+type instance SubDigit Dec8 Dec4 = Dec4
+type instance SubDigit Dec8 Dec5 = Dec3
+type instance SubDigit Dec8 Dec6 = Dec2
+type instance SubDigit Dec8 Dec7 = Dec1
+type instance SubDigit Dec8 Dec8 = Dec0
+type instance SubDigit Dec8 Dec9 = Dec9
+
+type instance SubDigit Dec9 Dec0 = Dec9
+type instance SubDigit Dec9 Dec1 = Dec8
+type instance SubDigit Dec9 Dec2 = Dec7
+type instance SubDigit Dec9 Dec3 = Dec6
+type instance SubDigit Dec9 Dec4 = Dec5
+type instance SubDigit Dec9 Dec5 = Dec4
+type instance SubDigit Dec9 Dec6 = Dec3
+type instance SubDigit Dec9 Dec7 = Dec2
+type instance SubDigit Dec9 Dec8 = Dec1
+type instance SubDigit Dec9 Dec9 = Dec0
+
+-- | If subtracting @y@ from @x@ would not borrow, then
+--   @Borrow x y z@ evaluates to @z@.  Otherwise,
+--   @Borrow x y z@ evaluates to @Pred' z@
+type family Borrow x y z
+-- putStr $ unlines $ concat $ [ [ "type instance Borrow Dec" ++ show x ++ " Dec" ++ show y ++ " x = " ++ (if x < y then "Pred'" else "Id") ++ " x" | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
+type instance Borrow Dec0 Dec0 x = Id x
+type instance Borrow Dec0 Dec1 x = Pred' x
+type instance Borrow Dec0 Dec2 x = Pred' x
+type instance Borrow Dec0 Dec3 x = Pred' x
+type instance Borrow Dec0 Dec4 x = Pred' x
+type instance Borrow Dec0 Dec5 x = Pred' x
+type instance Borrow Dec0 Dec6 x = Pred' x
+type instance Borrow Dec0 Dec7 x = Pred' x
+type instance Borrow Dec0 Dec8 x = Pred' x
+type instance Borrow Dec0 Dec9 x = Pred' x
+
+type instance Borrow Dec1 Dec0 x = Id x
+type instance Borrow Dec1 Dec1 x = Id x
+type instance Borrow Dec1 Dec2 x = Pred' x
+type instance Borrow Dec1 Dec3 x = Pred' x
+type instance Borrow Dec1 Dec4 x = Pred' x
+type instance Borrow Dec1 Dec5 x = Pred' x
+type instance Borrow Dec1 Dec6 x = Pred' x
+type instance Borrow Dec1 Dec7 x = Pred' x
+type instance Borrow Dec1 Dec8 x = Pred' x
+type instance Borrow Dec1 Dec9 x = Pred' x
+
+type instance Borrow Dec2 Dec0 x = Id x
+type instance Borrow Dec2 Dec1 x = Id x
+type instance Borrow Dec2 Dec2 x = Id x
+type instance Borrow Dec2 Dec3 x = Pred' x
+type instance Borrow Dec2 Dec4 x = Pred' x
+type instance Borrow Dec2 Dec5 x = Pred' x
+type instance Borrow Dec2 Dec6 x = Pred' x
+type instance Borrow Dec2 Dec7 x = Pred' x
+type instance Borrow Dec2 Dec8 x = Pred' x
+type instance Borrow Dec2 Dec9 x = Pred' x
+
+type instance Borrow Dec3 Dec0 x = Id x
+type instance Borrow Dec3 Dec1 x = Id x
+type instance Borrow Dec3 Dec2 x = Id x
+type instance Borrow Dec3 Dec3 x = Id x
+type instance Borrow Dec3 Dec4 x = Pred' x
+type instance Borrow Dec3 Dec5 x = Pred' x
+type instance Borrow Dec3 Dec6 x = Pred' x
+type instance Borrow Dec3 Dec7 x = Pred' x
+type instance Borrow Dec3 Dec8 x = Pred' x
+type instance Borrow Dec3 Dec9 x = Pred' x
+
+type instance Borrow Dec4 Dec0 x = Id x
+type instance Borrow Dec4 Dec1 x = Id x
+type instance Borrow Dec4 Dec2 x = Id x
+type instance Borrow Dec4 Dec3 x = Id x
+type instance Borrow Dec4 Dec4 x = Id x
+type instance Borrow Dec4 Dec5 x = Pred' x
+type instance Borrow Dec4 Dec6 x = Pred' x
+type instance Borrow Dec4 Dec7 x = Pred' x
+type instance Borrow Dec4 Dec8 x = Pred' x
+type instance Borrow Dec4 Dec9 x = Pred' x
+
+type instance Borrow Dec5 Dec0 x = Id x
+type instance Borrow Dec5 Dec1 x = Id x
+type instance Borrow Dec5 Dec2 x = Id x
+type instance Borrow Dec5 Dec3 x = Id x
+type instance Borrow Dec5 Dec4 x = Id x
+type instance Borrow Dec5 Dec5 x = Id x
+type instance Borrow Dec5 Dec6 x = Pred' x
+type instance Borrow Dec5 Dec7 x = Pred' x
+type instance Borrow Dec5 Dec8 x = Pred' x
+type instance Borrow Dec5 Dec9 x = Pred' x
+
+type instance Borrow Dec6 Dec0 x = Id x
+type instance Borrow Dec6 Dec1 x = Id x
+type instance Borrow Dec6 Dec2 x = Id x
+type instance Borrow Dec6 Dec3 x = Id x
+type instance Borrow Dec6 Dec4 x = Id x
+type instance Borrow Dec6 Dec5 x = Id x
+type instance Borrow Dec6 Dec6 x = Id x
+type instance Borrow Dec6 Dec7 x = Pred' x
+type instance Borrow Dec6 Dec8 x = Pred' x
+type instance Borrow Dec6 Dec9 x = Pred' x
+
+type instance Borrow Dec7 Dec0 x = Id x
+type instance Borrow Dec7 Dec1 x = Id x
+type instance Borrow Dec7 Dec2 x = Id x
+type instance Borrow Dec7 Dec3 x = Id x
+type instance Borrow Dec7 Dec4 x = Id x
+type instance Borrow Dec7 Dec5 x = Id x
+type instance Borrow Dec7 Dec6 x = Id x
+type instance Borrow Dec7 Dec7 x = Id x
+type instance Borrow Dec7 Dec8 x = Pred' x
+type instance Borrow Dec7 Dec9 x = Pred' x
+
+type instance Borrow Dec8 Dec0 x = Id x
+type instance Borrow Dec8 Dec1 x = Id x
+type instance Borrow Dec8 Dec2 x = Id x
+type instance Borrow Dec8 Dec3 x = Id x
+type instance Borrow Dec8 Dec4 x = Id x
+type instance Borrow Dec8 Dec5 x = Id x
+type instance Borrow Dec8 Dec6 x = Id x
+type instance Borrow Dec8 Dec7 x = Id x
+type instance Borrow Dec8 Dec8 x = Id x
+type instance Borrow Dec8 Dec9 x = Pred' x
+
+type instance Borrow Dec9 Dec0 x = Id x
+type instance Borrow Dec9 Dec1 x = Id x
+type instance Borrow Dec9 Dec2 x = Id x
+type instance Borrow Dec9 Dec3 x = Id x
+type instance Borrow Dec9 Dec4 x = Id x
+type instance Borrow Dec9 Dec5 x = Id x
+type instance Borrow Dec9 Dec6 x = Id x
+type instance Borrow Dec9 Dec7 x = Id x
+type instance Borrow Dec9 Dec8 x = Id x
+type instance Borrow Dec9 Dec9 x = Id x
+
+-- type family x :-: y
+type instance Dec x :-: Dec y = Dec (Sub x y)
+
+type family Sub x y
+type instance Sub x y = Normalize' (Sub' x y)
+
+type family Sub' x y
+type instance Sub' (Neg' x  ) (Neg' y  ) = Sub' y x
+type instance Sub' (Neg' x  ) (DecN    ) = Neg' x
+type instance Sub' (Neg' x  ) (yh :. yl) = Neg' (Add x (yh :. yl))
+type instance Sub' (DecN    ) (Neg' x  ) = x
+type instance Sub' (DecN    ) (DecN    ) = DecN
+type instance Sub' (DecN    ) (yh :. yl) = Neg' (yh :. yl)
+type instance Sub' (xh :. xl) (Neg' y  ) = Add (xh :. xl) y
+type instance Sub' (xh :. xl) (DecN    ) = xh :. xl
+type instance Sub' (xh :. xl) (yh :. yl) = Sub'' (xh :. xl) (yh :. yl) (Compare' (xh :. xl) (yh :. yl))
+
+type family Sub'' x y c
+type instance Sub'' x y GT = SubPos x y DecN
+type instance Sub'' x y EQ = DecN
+type instance Sub'' x y LT = Neg' (SubPos y x DecN)
+
+type family SubPos x y z
+type instance SubPos (xh :. xl) (yh :. yl) z = SubPos (Borrow xl yl xh) yh (z :. SubDigit xl yl)
+type instance SubPos (xh :. xl) DecN       z = SubPos xh DecN (z :. xl)
+type instance SubPos DecN       DecN       z = ReverseDigits z
+
+--------------------
+-- Multiplication
+
+-- type family Mul2 x
+type instance Mul2 (Dec x) = Mul2' x
+type family Mul2' x
+type instance Mul2' x = Add x x
+
+-- type family x :*: y
+type instance (Dec x) :*: (Dec y) = Dec (Mul x y)
+
+-- Peasant style
+type family Mul x y
+type instance Mul DecN       DecN       = DecN            -- 0 * 0 = 0
+type instance Mul (xh :. xl) DecN       = DecN            -- x * 0 = 0
+type instance Mul DecN       (yh :. yl) = DecN            -- 0 * x = 0
+type instance Mul (Neg' x)   (Neg' y)   = Mul x y        -- -x * -y = x*y
+type instance Mul (xh :. xl) (Neg' y)   = Neg' (Mul (xh :. xl) y)  -- x * -y = -(x*y)
+type instance Mul (Neg' x)   (yh :. yl) = Neg' (Mul x (yh :. yl))  -- -x * y = -(x*y)
+type instance Mul (xh :. xl) (yh :. yl) = Mul' (xh :. xl) (yh :. yl) DecN -- x & y positive
+
+type family Mul' x y z
+type instance Mul' x DecN       z = z
+type instance Mul' x (yh :. yl) z = Mul' (Mul2' x) (Div2' (yh :. yl)) (If (IsEven' (yh :. yl)) z (Add z x))
+
+-- type family Fac x
+type instance Fac x = Fac' x (IsZero x)
+type family Fac' x is0
+type instance Fac' x True = D1
+type instance Fac' x False = x :*: Fac (Pred x)
+
+-----------
+-- Division / Modulus
+
+-- type family IsEven x
+type instance IsEven (Dec x) = IsEven' x
+type family IsEven' x
+type instance IsEven' DecN = True
+type instance IsEven' (Neg' x) = IsEven' x
+type instance IsEven' (xh :. Dec0) = True
+type instance IsEven' (xh :. Dec1) = False
+type instance IsEven' (xh :. Dec2) = True
+type instance IsEven' (xh :. Dec3) = False
+type instance IsEven' (xh :. Dec4) = True
+type instance IsEven' (xh :. Dec5) = False
+type instance IsEven' (xh :. Dec6) = True
+type instance IsEven' (xh :. Dec7) = False
+type instance IsEven' (xh :. Dec8) = True
+type instance IsEven' (xh :. Dec9) = False
+
+-- type family Div2 x
+type instance Div2 (Dec x) = Dec (Div2' x)
+
+type family Div2Digit x
+type instance Div2Digit Dec0 = Dec0
+type instance Div2Digit Dec1 = Dec0
+type instance Div2Digit Dec2 = Dec1
+type instance Div2Digit Dec3 = Dec1
+type instance Div2Digit Dec4 = Dec2
+type instance Div2Digit Dec5 = Dec2
+type instance Div2Digit Dec6 = Dec3
+type instance Div2Digit Dec7 = Dec3
+type instance Div2Digit Dec8 = Dec4
+type instance Div2Digit Dec9 = Dec4
+
+type family Div2' x
+type instance Div2' DecN       = DecN
+type instance Div2' (Neg' x)   = Neg' (Div2Pos x)
+type instance Div2' (xh :. xl) = Div2Pos (xh :. xl)
+
+type family Div2Pos x
+type instance Div2Pos (xh :. xl) = Normalize' (Div2Pos' xh (Div2Digit xl) (If (IsEven' xh) Dec0 Dec5))
+
+type family Div2Pos' xh xl' rem
+type instance Div2Pos' xh xl' rem =
+    (AddCarry xl' rem (Div2' xh)) :. (AddDigit xl' rem)
+
+---------------
+-- Exponentiation
+
+type instance Pow2 (Dec x) = Dec (Pow2' x (DecN :. Dec1))
+
+type family Pow2' x y
+type instance Pow2' (Neg' x)   y = DecN
+type instance Pow2' DecN       y = y
+type instance Pow2' (xh :. xl) y = Pow2' (Pred' (xh :. xl)) (Mul2' y)
+
+---------------
+-- Compare
+
+type family CompareDigit x y
+-- putStr $ unlines $ concat $ [ [ "type instance CompareDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = " ++ (if x < y then "LT" else (if x > y then "GT" else "EQ")) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]
+type instance CompareDigit Dec0 Dec0 = EQ
+type instance CompareDigit Dec0 Dec1 = LT
+type instance CompareDigit Dec0 Dec2 = LT
+type instance CompareDigit Dec0 Dec3 = LT
+type instance CompareDigit Dec0 Dec4 = LT
+type instance CompareDigit Dec0 Dec5 = LT
+type instance CompareDigit Dec0 Dec6 = LT
+type instance CompareDigit Dec0 Dec7 = LT
+type instance CompareDigit Dec0 Dec8 = LT
+type instance CompareDigit Dec0 Dec9 = LT
+
+type instance CompareDigit Dec1 Dec0 = GT
+type instance CompareDigit Dec1 Dec1 = EQ
+type instance CompareDigit Dec1 Dec2 = LT
+type instance CompareDigit Dec1 Dec3 = LT
+type instance CompareDigit Dec1 Dec4 = LT
+type instance CompareDigit Dec1 Dec5 = LT
+type instance CompareDigit Dec1 Dec6 = LT
+type instance CompareDigit Dec1 Dec7 = LT
+type instance CompareDigit Dec1 Dec8 = LT
+type instance CompareDigit Dec1 Dec9 = LT
+
+type instance CompareDigit Dec2 Dec0 = GT
+type instance CompareDigit Dec2 Dec1 = GT
+type instance CompareDigit Dec2 Dec2 = EQ
+type instance CompareDigit Dec2 Dec3 = LT
+type instance CompareDigit Dec2 Dec4 = LT
+type instance CompareDigit Dec2 Dec5 = LT
+type instance CompareDigit Dec2 Dec6 = LT
+type instance CompareDigit Dec2 Dec7 = LT
+type instance CompareDigit Dec2 Dec8 = LT
+type instance CompareDigit Dec2 Dec9 = LT
+
+type instance CompareDigit Dec3 Dec0 = GT
+type instance CompareDigit Dec3 Dec1 = GT
+type instance CompareDigit Dec3 Dec2 = GT
+type instance CompareDigit Dec3 Dec3 = EQ
+type instance CompareDigit Dec3 Dec4 = LT
+type instance CompareDigit Dec3 Dec5 = LT
+type instance CompareDigit Dec3 Dec6 = LT
+type instance CompareDigit Dec3 Dec7 = LT
+type instance CompareDigit Dec3 Dec8 = LT
+type instance CompareDigit Dec3 Dec9 = LT
+
+type instance CompareDigit Dec4 Dec0 = GT
+type instance CompareDigit Dec4 Dec1 = GT
+type instance CompareDigit Dec4 Dec2 = GT
+type instance CompareDigit Dec4 Dec3 = GT
+type instance CompareDigit Dec4 Dec4 = EQ
+type instance CompareDigit Dec4 Dec5 = LT
+type instance CompareDigit Dec4 Dec6 = LT
+type instance CompareDigit Dec4 Dec7 = LT
+type instance CompareDigit Dec4 Dec8 = LT
+type instance CompareDigit Dec4 Dec9 = LT
+
+type instance CompareDigit Dec5 Dec0 = GT
+type instance CompareDigit Dec5 Dec1 = GT
+type instance CompareDigit Dec5 Dec2 = GT
+type instance CompareDigit Dec5 Dec3 = GT
+type instance CompareDigit Dec5 Dec4 = GT
+type instance CompareDigit Dec5 Dec5 = EQ
+type instance CompareDigit Dec5 Dec6 = LT
+type instance CompareDigit Dec5 Dec7 = LT
+type instance CompareDigit Dec5 Dec8 = LT
+type instance CompareDigit Dec5 Dec9 = LT
+
+type instance CompareDigit Dec6 Dec0 = GT
+type instance CompareDigit Dec6 Dec1 = GT
+type instance CompareDigit Dec6 Dec2 = GT
+type instance CompareDigit Dec6 Dec3 = GT
+type instance CompareDigit Dec6 Dec4 = GT
+type instance CompareDigit Dec6 Dec5 = GT
+type instance CompareDigit Dec6 Dec6 = EQ
+type instance CompareDigit Dec6 Dec7 = LT
+type instance CompareDigit Dec6 Dec8 = LT
+type instance CompareDigit Dec6 Dec9 = LT
+
+type instance CompareDigit Dec7 Dec0 = GT
+type instance CompareDigit Dec7 Dec1 = GT
+type instance CompareDigit Dec7 Dec2 = GT
+type instance CompareDigit Dec7 Dec3 = GT
+type instance CompareDigit Dec7 Dec4 = GT
+type instance CompareDigit Dec7 Dec5 = GT
+type instance CompareDigit Dec7 Dec6 = GT
+type instance CompareDigit Dec7 Dec7 = EQ
+type instance CompareDigit Dec7 Dec8 = LT
+type instance CompareDigit Dec7 Dec9 = LT
+
+type instance CompareDigit Dec8 Dec0 = GT
+type instance CompareDigit Dec8 Dec1 = GT
+type instance CompareDigit Dec8 Dec2 = GT
+type instance CompareDigit Dec8 Dec3 = GT
+type instance CompareDigit Dec8 Dec4 = GT
+type instance CompareDigit Dec8 Dec5 = GT
+type instance CompareDigit Dec8 Dec6 = GT
+type instance CompareDigit Dec8 Dec7 = GT
+type instance CompareDigit Dec8 Dec8 = EQ
+type instance CompareDigit Dec8 Dec9 = LT
+
+type instance CompareDigit Dec9 Dec0 = GT
+type instance CompareDigit Dec9 Dec1 = GT
+type instance CompareDigit Dec9 Dec2 = GT
+type instance CompareDigit Dec9 Dec3 = GT
+type instance CompareDigit Dec9 Dec4 = GT
+type instance CompareDigit Dec9 Dec5 = GT
+type instance CompareDigit Dec9 Dec6 = GT
+type instance CompareDigit Dec9 Dec7 = GT
+type instance CompareDigit Dec9 Dec8 = GT
+type instance CompareDigit Dec9 Dec9 = EQ
+
+type instance Compare (Dec x) (Dec y) = Compare' x y
+type family Compare' x y
+type instance Compare' (Neg' x)   (Neg' y)   = CompareNeg (ComparePos x y EQ)
+type instance Compare' (Neg' x)   DecN       = LT
+type instance Compare' (Neg' x)   (yh :. yl) = LT
+type instance Compare' DecN       (Neg' y)   = GT
+type instance Compare' DecN       DecN       = EQ
+type instance Compare' DecN       (yh :. yl) = LT
+type instance Compare' (xh :. xl) (Neg' y)   = GT
+type instance Compare' (xh :. xl) DecN       = GT
+type instance Compare' (xh :. xl) (yh :. yl) = ComparePos (xh :. xl) (yh :. yl) EQ
+
+type family ComparePos x y c
+type instance ComparePos DecN       DecN       c = c
+type instance ComparePos DecN       (yh :. yl) c = LT
+type instance ComparePos (xh :. xl) DecN       c = GT
+type instance ComparePos (xh :. xl) (yh :. yl) GT = ComparePos' xh yh (CompareDigit xl yl) GT
+type instance ComparePos (xh :. xl) (yh :. yl) EQ = ComparePos xh yh (CompareDigit xl yl)
+type instance ComparePos (xh :. xl) (yh :. yl) LT = ComparePos' xh yh (CompareDigit xl yl) LT
+
+type family ComparePos' x y c l
+type instance ComparePos' x y LT c = ComparePos x y LT
+type instance ComparePos' x y EQ c = ComparePos x y c
+type instance ComparePos' x y GT c = ComparePos x y GT
+
+type family CompareNeg c
+type instance CompareNeg LT = GT
+type instance CompareNeg EQ = EQ
+type instance CompareNeg GT = LT
diff --git a/Types/Data/Num/Ops.hs b/Types/Data/Num/Ops.hs
new file mode 100644
--- /dev/null
+++ b/Types/Data/Num/Ops.hs
@@ -0,0 +1,148 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Types.Data.Decimal.Ops
+-- Copyright   :  (c) 2008 Peter Gavin
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  pgavin@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (type families, requires ghc >= 6.9)
+--
+-- Type-level numerical operations using type families.
+-- 
+----------------------------------------------------------------------------
+
+module Types.Data.Num.Ops
+    ( (:.)
+    , Neg
+    , negT
+    , IsPositive
+    , isPositiveT
+    , IsZero
+    , isZeroT
+    , IsNegative
+    , isNegativeT
+    , Succ
+    , succT
+    , Pred
+    , predT
+    , IsEven
+    , isEvenT
+    , IsOdd
+    , isOddT
+    , (:+:)
+    , addT
+    , (:-:)
+    , subT
+    , (:*:)
+    , mulT
+    , Mul2
+    , mul2T
+    , Pow2
+    , pow2T
+    , DivMod
+    , divModT
+    , Div
+    , divT
+    , Mod
+    , modT
+    , Div2
+    , div2T
+    , Fac
+    , facT
+    , IntegerT (..)
+    , NaturalT
+    , PositiveT
+    , NegativeT
+    ) where
+
+import Types.Data.Bool
+
+data ds :. d
+instance (Show ds, Show d) => Show (ds :. d) where
+    show _ = show (undefined :: ds) ++ show (undefined :: d)
+
+-- | @Neg x@ evaluates to the additive inverse of (i.e., minus) @x@.
+type family Neg x
+negT :: x -> Neg x
+negT _ = undefined
+
+type family IsPositive x
+isPositiveT :: x -> IsPositive x
+isPositiveT _ = undefined
+
+type family IsZero x
+isZeroT :: x -> IsZero x
+isZeroT _ = undefined
+
+type family IsNegative x
+isNegativeT :: x -> IsNegative x
+isNegativeT _ = undefined
+
+type family Succ x
+succT :: x -> Succ x
+succT _ = undefined
+
+type family Pred x
+predT :: x -> Pred x
+predT _ = undefined
+
+type family IsEven x
+isEvenT :: x -> IsEven x
+isEvenT _ = undefined
+
+type family IsOdd x
+type instance IsOdd x = Not (IsEven x)
+isOddT :: x -> IsOdd x
+isOddT _ = undefined
+
+type family x :+: y
+addT :: x -> y -> x :+: y
+addT _ _ = undefined
+
+type family x :-: y
+subT :: x -> y -> x :-: y
+subT _ _ = undefined
+
+type family x :*: y
+mulT :: x -> y -> x :*: y
+mulT _ _ = undefined
+
+type family Mul2 x
+mul2T :: x -> Mul2 x
+mul2T _ = undefined
+
+type family DivMod x y
+divModT :: x -> y -> DivMod x y
+divModT _ _ = undefined
+
+type family Div x y
+divT :: x -> y -> Div x y
+divT _ _ = undefined
+
+type family Mod x y
+modT :: x -> y -> Mod x y
+modT _ _ = undefined
+
+type family Div2 x
+div2T :: x -> Div2 x
+div2T _ = undefined
+
+type family Fac x
+facT :: x -> Fac x
+facT _ = undefined
+
+type family Pow2 x
+pow2T :: x -> Pow2 x
+pow2T _ = undefined
+
+class IntegerT x => NaturalT x
+instance (IntegerT x, IsNegative x ~ False) => NaturalT x
+
+class IntegerT x => PositiveT x
+instance (IntegerT x, IsPositive x ~ True) => PositiveT x
+class IntegerT x => NegativeT x
+instance (IntegerT x, IsNegative x ~ True) => NegativeT x
+
+class IntegerT x where
+    fromIntegerT :: Num y => x -> y
diff --git a/Types/Data/Ord.hs b/Types/Data/Ord.hs
new file mode 100644
--- /dev/null
+++ b/Types/Data/Ord.hs
@@ -0,0 +1,114 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Types.Data.Decimal.Digits
+-- Copyright   :  (c) 2008 Peter Gavin
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  pgavin@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (type families, requires ghc >= 6.9)
+--
+-- Type-level numerical operations using type families.
+-- 
+----------------------------------------------------------------------------
+
+module Types.Data.Ord
+    ( Compare
+    , compareT
+    , LT
+    , EQ
+    , GT
+    , IsLT
+    , isLTT
+    , IsEQ
+    , isEQT
+    , IsGT
+    , isGTT
+    , (:<:)
+    , ltT
+    , (:<=:)
+    , leT
+    , (:==:)
+    , eqT
+    , (:>=:)
+    , geT
+    , (:>:)
+    , gtT
+    ) where
+
+import qualified Prelude
+
+import Types.Data.Bool
+
+type family Compare x y
+data LT
+data EQ
+data GT
+compareT :: x -> y -> Compare x y
+compareT _ _ = Prelude.undefined
+
+type family IsLT c
+type instance IsLT LT = True
+type instance IsLT EQ = False
+type instance IsLT GT = False
+isLTT :: c -> IsLT c
+isLTT _ = Prelude.undefined
+
+type family IsEQ c
+type instance IsEQ LT = False
+type instance IsEQ EQ = True
+type instance IsEQ GT = False
+isEQT :: c -> IsEQ c
+isEQT _ = Prelude.undefined
+
+type family IsGT c
+type instance IsGT LT = False
+type instance IsGT EQ = False
+type instance IsGT GT = True
+isGTT :: c -> IsGT c
+isGTT _ = Prelude.undefined
+
+type instance Compare LT LT = EQ
+type instance Compare LT EQ = LT
+type instance Compare LT GT = LT
+type instance Compare EQ LT = GT
+type instance Compare EQ EQ = EQ
+type instance Compare EQ GT = LT
+type instance Compare GT LT = GT
+type instance Compare GT EQ = GT
+type instance Compare GT GT = EQ
+
+type family x :<: y
+type instance x :<: y = IsLT (Compare x y)
+ltT :: x -> y -> x :<: y
+ltT _ _ = Prelude.undefined
+
+type family x :<=: y
+type instance x :<=: y = Not (x :>: y)
+leT :: x -> y -> x :<=: y
+leT _ _ = Prelude.undefined
+
+type family x :==: y
+type instance x :==: y = IsEQ (Compare x y)
+eqT :: x -> y -> x :==: y
+eqT _ _ = Prelude.undefined
+
+type family x :/=: y
+type instance x :/=: y = Not (x :==: y)
+neT :: x -> y -> x :/=: y
+neT _ _ = Prelude.undefined
+
+type family x :>=: y
+type instance x :>=: y = Not (x :<: y)
+geT :: x -> y -> x :>=: y
+geT _ _ = Prelude.undefined
+
+type family x :>: y
+type instance x :>: y = IsGT (Compare x y)
+gtT :: x -> y -> x :>: y
+gtT _ _ = Prelude.undefined
+
+type instance Compare False False = EQ
+type instance Compare False True  = LT
+type instance Compare True  False = GT
+type instance Compare True  True  = EQ
diff --git a/tfp.cabal b/tfp.cabal
new file mode 100644
--- /dev/null
+++ b/tfp.cabal
@@ -0,0 +1,61 @@
+name:           tfp
+version:        0.1
+cabal-version:  >= 1.2
+build-type:     Simple
+license:        BSD3
+license-file:   LICENSE
+copyright:      Copyright (c) 2008 Peter Gavin
+author:         Peter Gavin
+maintainer:     pgavin@gmail.com
+homepage:       http://code.haskell.org/~pgavin/tfp
+stability:      alpha
+package-url:    http://code.haskell.org/~pgavin/tfp
+synopsis:       Type-level programming library using type families
+description:	TFP (short for Type Family Programming) provides implementations of type-level integers and booleans,
+		and (eventually) simple type-level data structures. It uses type families as functions to produce new types,
+		which provides an intuitive way to parameterize data types and functions on numerical values at compile time.
+category:       Data
+tested-with:    GHC == 6.9.0
+
+flag build-test
+  description: Build the tfp-test test program
+  default: False
+
+library {
+  extensions:     TypeFamilies, UndecidableInstances, TypeOperators,
+                  EmptyDataDecls, DeriveDataTypeable, ScopedTypeVariables,
+                  FlexibleInstances, TemplateHaskell, TypeSynonymInstances,
+                  MultiParamTypeClasses, GeneralizedNewtypeDeriving
+  build-depends:  base >= 3.0, template-haskell >= 2.0
+  exposed-modules:
+    Data.SizedInt,
+    Data.SizedWord,
+    Types,
+    Types.Base,
+    Types.Data.Bool,
+    Types.Data.Num
+    Types.Data.Num.Ops
+    Types.Data.Num.Decimal,
+    Types.Data.Num.Decimal.Literals
+    Types.Data.Num.Decimal.Literals.TH
+    Types.Data.Num.Decimal.Digits
+    Types.Data.List,
+    Types.Data.Ord
+  other-modules:
+    Types.Data.Num.Decimal.Ops
+}
+
+
+executable tfp-test {
+  if flag(build-test) {
+    buildable: True
+  } else {
+    buildable: False
+  }
+  extensions:     TypeFamilies, UndecidableInstances, TypeOperators,
+                  EmptyDataDecls, DeriveDataTypeable, ScopedTypeVariables,
+                  FlexibleInstances, TemplateHaskell, TypeSynonymInstances,
+                  MultiParamTypeClasses, GeneralizedNewtypeDeriving
+  main-is: Test.hs
+  build-depends:  base >= 3.0, template-haskell >= 2.0
+}