diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,26 @@
+Copyright (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch and
+ SAM Group at the School of Information and Communication  Technology,
+ (Royal Institute of Technology, Stockholm, Sweden)
+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 ForSyDe Team 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 HOLDERS ``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 HOLDERS TEAM BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,46 @@
+type-level: Type-level programming library
+
+DESCRIPTION
+
+
+ This library permits performing computations on the type-level. Type-level 
+ functions are implemented using functional dependencies of multi
+ parameter type classes. 
+
+ To date, Booleans and Numerals (Naturals and Positives) are
+ supported. With regard to Numerals, there is support for common
+ arithmetic operations (addition, substraction, multiplication,
+ division, exponientation, logarithm, maximum, comparison, GCD) 
+ over natural numbers (using a decimal representation to make 
+ compile-time errors friendlier).
+
+ Although making use of type-level computations might seem devious and
+ obfuscated at first sight, it is indeed useful in practice to implement 
+ lightweight dependent types such us number-parameterized types (e.g. an array 
+ type parameterized by the array's size or a modular group type Zn 
+ parameterized by the modulus).
+
+
+DEPENDENCIES
+ 
+ type-level depends on GHC (due to the use of Multiparameter Type Classes and 
+ infix type constructors) and Template Haskell
+
+INSTALLATION
+
+to install globally, for the whole system (requires admin permissions):
+
+$ ./Setup.hs configure
+$ ./Setup.hs build
+$ ./Setup.hs haddock # generate documentation, optional, 
+                     # requires Haddock > 2.0 due to the use of TH
+$ ./Setup.hs install
+
+to install locally and just for your own user:
+
+$ ./Setup.hs configure --prefix=The/selected/local/directory
+$ ./Setup.hs build
+$ ./Setup.hs haddock  # generate documentation, optional, 
+                      # requires Haddock > 2.0 due to the use of TH
+
+$ ./Setup.hs install --user
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,7 @@
+#! /usr/bin/env runhaskell
+module Main (main) where
+
+import Distribution.Simple
+
+main :: IO ()
+main = defaultMain
diff --git a/src/Data/TypeLevel.hs b/src/Data/TypeLevel.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel.hs
@@ -0,0 +1,20 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- This module is a wrapper for all the publicly usable types and functions
+-- of the type-level library.
+-- 
+-----------------------------------------------------------------------------
+module Data.TypeLevel (module Data.TypeLevel.Num, 
+                       module Data.TypeLevel.Bool) where
+
+import Data.TypeLevel.Num
+import Data.TypeLevel.Bool
diff --git a/src/Data/TypeLevel/Bool.hs b/src/Data/TypeLevel/Bool.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel/Bool.hs
@@ -0,0 +1,181 @@
+{-# LANGUAGE EmptyDataDecls, MultiParamTypeClasses, FunctionalDependencies,
+             Rank2Types, DeriveDataTypeable, FlexibleInstances,
+             UndecidableInstances, FlexibleContexts  #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel.Bool
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental (MPTC, non-standarad instances)
+-- Portability :  non-portable
+--
+-- Type-level Booleans.
+-- 
+----------------------------------------------------------------------------
+module Data.TypeLevel.Bool (
+    -- * Type-level boolean values
+    Bool,
+    False, false,
+    True, true,
+    reifyBool,
+    -- * Type-level boolean operations
+    Not, not,
+    And, (&&),
+    Or, (||),
+    Xor, xor,
+    Imp, imp,
+    Eq, eq
+
+) where
+
+import Data.Generics (Typeable)
+import Prelude hiding (Bool, not, (&&), (||), Eq)
+import qualified Prelude as P
+
+------------------------------------
+-- Definition of type-level Booleans
+------------------------------------
+
+-- | True type-level value
+data True deriving Typeable
+
+instance Show True where
+ show _ = "True"
+
+-- | True value-level reflecting function
+true :: True
+true = undefined
+
+-- | False type-level value
+data False deriving Typeable
+
+instance Show False where
+ show _ = "False"
+
+
+-- | False value-level reflecting function
+false :: False
+false = undefined
+
+
+-- | Booleans, internal version
+class BoolI b where
+ toBool :: b -> P.Bool
+
+
+-- To prevent the user from adding new instances to BoolI we do NOT export 
+-- BoolI itself. Rather, we export the following proxy (Bool). 
+-- The proxy entails BoolI and so can be used to add BoolI 
+-- constraints in the signatures. However, all the constraints below
+-- are expressed in terms of BoolI rather than the proxy. Thus, even if the 
+-- user adds new instances to the proxy, it would not matter. 
+-- Besides, because the following proxy instances are most general,
+-- one may not add further instances without the overlapping instances 
+-- extension.
+
+-- | Type-level Booleans
+class BoolI b => Bool b
+
+instance BoolI b => Bool b
+
+instance BoolI True where
+ toBool _ = True
+
+instance BoolI False where
+ toBool _ = False
+
+-- | Reification function. In CPS style (best possible solution)
+reifyBool :: P.Bool -> (forall b . Bool b => b -> r) -> r
+reifyBool True  f = f true
+reifyBool False f = f false
+
+-------------
+-- Operations
+-------------
+
+-- | Boolean negation type-level relation. @Not b1 b2@ establishes that
+-- @not b1 = b2@
+class (BoolI b1, BoolI b2) => Not b1 b2 | b1 -> b2, b2 -> b1
+instance Not False True
+instance Not True  False
+
+-- | value-level reflection function for the 'Not' type-level relation
+not :: Not b1 b2 => b1 -> b2
+not = undefined
+
+-- | 'And' type-level relation. @And b1 b2 b3@ establishes that
+--   @b1 && b2 = b3@
+class (BoolI b1, BoolI b2, BoolI b3) => And b1 b2 b3 | b1 b2 -> b3
+instance And False False False  
+instance And False True  False  
+instance And True  False False  
+instance And True  True  True
+
+
+-- | value-level reflection function for the 'And' type-level relation
+(&&) :: And b1 b2 b3 => b1 -> b2 -> b3
+(&&) = undefined
+
+  
+-- | Or type-level relation. @Or b1 b2 b3@ establishes that
+--   @b1 || b2 = b3@
+class (BoolI b1, BoolI b2, BoolI b3) => Or b1 b2 b3 | b1 b2 -> b3
+instance Or False False False  
+instance Or False True  True  
+instance Or True  False True  
+instance Or True  True  True
+
+
+-- | value-level reflection function for the 'Or' type-level relation
+(||) :: Or b1 b2 b3 => b1 -> b2 -> b3
+(||) = undefined
+
+-- | Exclusive or type-level relation. @Xor b1 b2 b3@ establishes that
+--   @xor b1 b2 = b3@
+class (BoolI b1, BoolI b2, BoolI b3) => Xor b1 b2 b3 | b1 b2 -> b3
+instance Xor False False False  
+instance Xor False True  True  
+instance Xor True  False True  
+instance Xor True  True  False
+
+-- | value-level reflection function for the 'Xor' type-level relation
+xor :: Xor b1 b2 b3 => b1 -> b2 -> b3
+xor = undefined
+
+
+-- | Implication type-level relation. @Imp b1 b2 b3@ establishes that
+-- @b1 =>b2 = b3@
+class (BoolI b1, BoolI b2, BoolI b3) => Imp b1 b2 b3 | b1 b2 -> b3
+instance Imp False False True  
+instance Imp False True  True  
+instance Imp True  False False  
+instance Imp True  True  True
+
+
+-- | value-level reflection function for the Imp type-level relation
+imp :: Imp b1 b2 b3 => b1 -> b2 -> b3
+imp = undefined
+
+
+-- Although equality can be defined as the composition of Xor and Not
+-- we define it specifically
+
+-- | Boolean equality type-level relation
+class (BoolI b1, BoolI b2, BoolI b3) => Eq b1 b2 b3 | b1 b2 -> b3
+instance Eq False False True  
+instance Eq False True  False  
+instance Eq True  False False  
+instance Eq True  True  True
+
+
+-- FIXME: eq should be named (==) but it clashes with the (==) defined
+--        in Data.TypeLevel.Num . The chosen (and ugly) workaround was 
+--        to rename it to eq.
+
+-- | value-level reflection function for the 'Eq' type-level relation
+eq :: Eq b1 b2 b3 => b1 -> b2 -> b3
+eq = undefined
+
diff --git a/src/Data/TypeLevel/Num.hs b/src/Data/TypeLevel/Num.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel/Num.hs
@@ -0,0 +1,25 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel.Num
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- This module is a wrapper for all the publicly usable numerical types and 
+-- functions of the type-level library.
+-- 
+----------------------------------------------------------------------------
+module Data.TypeLevel.Num 
+ (module Data.TypeLevel.Num.Reps,
+  module Data.TypeLevel.Num.Aliases,
+  module Data.TypeLevel.Num.Sets,
+  module Data.TypeLevel.Num.Ops) where
+
+import Data.TypeLevel.Num.Reps
+import Data.TypeLevel.Num.Aliases
+import Data.TypeLevel.Num.Sets
+import Data.TypeLevel.Num.Ops
diff --git a/src/Data/TypeLevel/Num/Aliases.hs b/src/Data/TypeLevel/Num/Aliases.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel/Num/Aliases.hs
@@ -0,0 +1,29 @@
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+{-# LANGUAGE TemplateHaskell #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel.Num.Aliases
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (Template Haskell)
+--
+-- Type synonym aliases of type-level numerals and 
+-- their value-level reflecting functions. Generated for user convenience.
+-- 
+-- Aliases are generated using binary, octal, decimal and hexadecimal bases.
+-- Available aliases cover binaries up to b10000000000, octals up to
+-- o10000, decimals up to d5000 and hexadecimals up to h1000 
+----------------------------------------------------------------------------
+module Data.TypeLevel.Num.Aliases where
+
+import Data.TypeLevel.Num.Reps
+import Data.TypeLevel.Num.Aliases.TH (genAliases)
+
+
+$(genAliases 1024 4096 5000 4096)
+
+
diff --git a/src/Data/TypeLevel/Num/Aliases/TH.hs b/src/Data/TypeLevel/Num/Aliases/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel/Num/Aliases/TH.hs
@@ -0,0 +1,130 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel.Num.Aliases
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (Template Haskell)
+--
+-- Internal template haskell functions to generate type-level numeral aliases
+-- 
+----------------------------------------------------------------------------
+module Data.TypeLevel.Num.Aliases.TH (genAliases, dec2TypeLevel) where
+
+import Language.Haskell.TH
+
+import Data.TypeLevel.Num.Reps
+
+data Base = Bin | Oct | Dec | Hex
+
+base2Int :: Base -> Int
+base2Int Bin = 2
+base2Int Oct = 8
+base2Int Dec = 10
+base2Int Hex = 16
+
+-- This module needs to be separated from Data.TypeLevel.Num.Aliases due to
+-- a limitation in Template Haskell implementation: 
+-- "You can only run a function at compile time if it is imported from another 
+-- module." 
+
+genAliases :: Int -- how many binary aliases 
+           -> Int -- how many octal aliases
+           -> Int -- how many dec aliases
+           -> Int -- how many hex aliases
+           -> Q [Dec]
+genAliases nb no nd nh = genAliases' nb no nd nh (maximum [nb,no,nd,nh])
+
+genAliases' :: Int -- how many binary aliases 
+            -> Int -- how many octal aliases
+            -> Int -- how many dec aliases
+            -> Int -- how many hex aliases
+            -> Int -- maximum alias
+            -> Q [Dec]
+-- FIXME: genAliases' is ugly!
+genAliases' nb no nd nh curr 
+ | curr < 0 = return []
+ | otherwise = 
+    do rest <- genAliases' nb no nd nh (curr-1)
+       -- binaries
+       restb <- addAliasBase (curr > nb) ('b' : bStr) ('B' : bStr) rest
+       -- octals
+       resto <- addAliasBase (curr > no) ('o' : oStr) ('O' : oStr) restb
+       -- decimals, we don't aliases of the decimal digits
+       -- (they are alredy defined in the representation module)
+       restd <- if curr > nd then return resto             
+                else do val <- genValAlias ('d' : dStr) decRep
+                        typ <- genTypeAlias ('D' : dStr) decRep
+                        if (curr < 10) then return $ val : resto
+                         else return $ val : typ : resto
+       -- hexadicimals
+       addAliasBase (curr > no) ('h' : hStr) ('H' : hStr) restd
+ 
+ where  -- Add aliases of certain base to the rest of aliases
+        addAliasBase cond vStr tStr rest =
+          if cond then return rest
+          else  do val <- genValAlias vStr decRep
+                   typ <- genTypeAlias tStr decRep
+                   return $ val : typ : rest
+
+        decRep = dec2TypeLevel curr        
+
+        bStr = toBase Bin curr
+        oStr = toBase Oct curr
+        dStr = toBase Dec curr
+        hStr = toBase Hex curr
+
+-- | Generate the type-level decimal representation for a value-level 
+--   natural number. 
+-- NOTE: This function could be useful by itself avoiding to generate 
+-- aliases. However, type-splicing is not yet supported by template haskell.
+dec2TypeLevel :: Int -> Q Type
+dec2TypeLevel n
+ | n <  0 = error "natural number expected"
+ | n < 10 = let name = case n of
+                  0 -> ''D0; 1 -> ''D1; 2 -> ''D2; 3 -> ''D3; 4 -> ''D4
+                  5 -> ''D5; 6 -> ''D6; 7 -> ''D7; 8 -> ''D8; 9 -> ''D9
+            in conT name          
+ | otherwise = let (quotient, reminder) = n `quotRem` 10 
+                   remType  = dec2TypeLevel reminder
+                   quotType = dec2TypeLevel quotient
+               in (conT ''(:*)) `appT` quotType `appT` remType
+
+
+-- | Generate a decimal type synonym alias
+genTypeAlias :: String -> Q Type -> Q Dec
+genTypeAlias str t = tySynD name [] t
+ where name = mkName $ str
+
+-- | Generate a decimal value-level reflected alias
+genValAlias :: String -> Q Type -> Q Dec
+genValAlias str t = body
+ where name = mkName $ str
+       body = valD (varP name) 
+                   (normalB (sigE [| undefined |] t)) []
+
+
+-- | Print an integer in certain base
+toBase :: Base  -- base 
+       -> Int  -- Number to print
+       -> String
+toBase Dec n = show n
+toBase b n
+  | n < 0 = '-' : toBase b (- n)
+  | n < bi = [int2Char n]
+  | otherwise = (toBase b rest) ++ [int2Char currDigit]
+   where bi = base2Int b 
+         (rest, currDigit) = n `quotRem` bi
+
+-- | print the corresponding character of a digit
+int2Char ::  Int  -- Number to print
+          -> Char
+int2Char i 
+ | i' < 10 = toEnum (i'+ 48)
+ | otherwise = toEnum (i' + 55)
+ where i' = abs i
diff --git a/src/Data/TypeLevel/Num/Ops.hs b/src/Data/TypeLevel/Num/Ops.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel/Num/Ops.hs
@@ -0,0 +1,766 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, TypeOperators,
+             FlexibleInstances, FlexibleContexts, UndecidableInstances,
+             EmptyDataDecls #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel.Num.Ops
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (MPTC, non-standard instances)
+--
+-- Type-level numerical operations and its value-level reflection functions.
+-- 
+----------------------------------------------------------------------------
+module Data.TypeLevel.Num.Ops 
+ (-- * Successor/Predecessor
+  Succ, succ,
+  Pred, pred,
+  -- * Addition/Subtraction
+  Add, (+),
+  Sub, (-),
+  -- * Multiplication/Division
+  Mul, (*),
+  Div, div,
+  Mod, mod,
+  DivMod, divMod,
+  IsDivBy, isDivBy,
+  -- ** Special efficiency cases
+  Mul10, mul10,
+  Div10, div10,
+  DivMod10, divMod10,
+  -- * Exponientiation/Logarithm
+  ExpBase, (^),
+  LogBase, logBase,
+  LogBaseF, logBaseF,
+  IsPowOf, isPowOf,
+  -- ** Special efficiency cases
+  Exp10, exp10,
+  Log10, log10,
+  -- * Comparison assertions
+  -- ** General comparison assertion
+  Trich, trich,
+  -- *** Type-level values denoting comparison results
+  LT, EQ, GT,
+  -- ** Abbreviated comparison assertions
+  (:==:), (:>:), (:<:), (:>=:), (:<=:),
+  (==)  , (>)  , (<)  , (>=)  , (<=), 
+  -- * Maximum/Minimum
+  Max, max,
+  Min, min,
+  -- * Greatest Common Divisor
+  GCD, gcd
+ ) where
+
+import Data.TypeLevel.Num.Reps
+import Data.TypeLevel.Num.Sets
+import Data.TypeLevel.Bool
+
+import Prelude hiding 
+ (succ, pred, (+), (-), (*), div, mod, divMod, (^), logBase,
+  (==), (>), (<), (<), (>=), (<=), max, min, gcd, Bool)
+
+-------------------------
+-- Successor, Predecessor
+-------------------------
+
+-- | Successor type-level relation. @Succ x y@ establishes
+--  that @succ x = y@.
+class (Nat x, Pos y) => Succ x y | x -> y, y -> x
+
+
+instance (Pos y, IsZero y yz, DivMod10 x xi xl, Succ' xi xl yi yl yz,
+         DivMod10 y yi yl)
+   => Succ x y
+
+class Succ' xh xl yh yl yz | xh xl -> yh yl yz, yh yl yz -> xh xl
+
+
+-- This intends to implement a user reporting operation when
+-- trying to calculate the predecesor of 0
+-- FIXME: however, the instance rule is never triggered!
+
+class Failure t
+-- No instances
+data PredecessorOfZeroError t
+ 
+instance Failure (PredecessorOfZeroError x) => Succ' (x,x) (x,x) D0 D0 True
+instance Succ' xi D0 xi D1 False
+instance Succ' xi D1 xi D2 False
+instance Succ' xi D2 xi D3 False
+instance Succ' xi D3 xi D4 False
+instance Succ' xi D4 xi D5 False
+instance Succ' xi D5 xi D6 False
+instance Succ' xi D6 xi D7 False
+instance Succ' xi D7 xi D8 False
+instance Succ' xi D8 xi D9 False
+instance Succ xi yi => Succ' xi D9 yi D0 False
+
+
+{-
+
+Nicer, but not relational implementation of Succ
+
+class (Nat x, Pos y) => Succ' x y | x -> y
+
+-- by structural induction on the first argument
+instance Succ' D0 D1
+instance Succ' D1 D2
+instance Succ' D2 D3
+instance Succ' D3 D4
+instance Succ' D4 D5
+instance Succ' D5 D6
+instance Succ' D6 D7
+instance Succ' D7 D8
+instance Succ' D8 D9
+instance Succ' D9 (D1 :* D0)
+instance Pos x => Succ' (x :* D0) (x :* D1)
+instance Pos x => Succ' (x :* D1) (x :* D2)
+instance Pos x => Succ' (x :* D2) (x :* D3)
+instance Pos x => Succ' (x :* D3) (x :* D4)
+instance Pos x => Succ' (x :* D4) (x :* D5)
+instance Pos x => Succ' (x :* D5) (x :* D6)
+instance Pos x => Succ' (x :* D6) (x :* D7)
+instance Pos x => Succ' (x :* D7) (x :* D8)
+instance Pos x => Succ' (x :* D8) (x :* D9)
+instance (Pos x, Succ' x y) => Succ' (x :* D9) (y  :* D0)
+
+
+class (Nat x, Pos y) => Succ x y | x -> y, y -> x
+instance Succ' x y => Succ x y
+-}
+
+-- | value-level reflection function for the 'Succ' type-level relation
+succ :: Succ x y => x -> y
+succ = undefined
+
+-- Note: maybe redundant 
+-- | Predecessor type-level relation. @Pred x y@ establishes
+--  that @pred x = y@.
+class (Pos x, Nat y) => Pred x y | x -> y, y -> x
+instance Succ x y => Pred y x
+
+-- | value-level reflection function for the 'Pred' type-level relation
+pred :: Pred x y => x -> y
+pred = undefined
+
+
+
+--------------------
+-- Add and Subtract
+--------------------
+
+
+class (Nat x, Nat y, Nat z) => Add' x y z | x y -> z, z x -> y
+
+-- by structural induction on the first argument
+instance Nat y   => Add' D0 y y
+instance Succ y z => Add' D1 y z
+instance (Succ z z', Add' D1 y z) => Add' D2 y z'
+instance (Succ z z', Add' D2 y z) => Add' D3 y z'
+instance (Succ z z', Add' D3 y z) => Add' D4 y z'
+instance (Succ z z', Add' D4 y z) => Add' D5 y z'
+instance (Succ z z', Add' D5 y z) => Add' D6 y z'
+instance (Succ z z', Add' D6 y z) => Add' D7 y z'
+instance (Succ z z', Add' D7 y z) => Add' D8 y z'
+instance (Succ z z', Add' D8 y z) => Add' D9 y z'
+-- multidigit addition
+-- TODO: explain
+instance (Pos (xi :* xl), Nat z,
+          Add' xi yi zi, DivMod10 y yi yl, Add' xl (zi :* yl) z)
+    => Add' (xi :* xl) y z
+
+-- | Addition type-level relation.  @Add x y z@ establishes
+--  that @x + y = z@.
+class (Add' x y z, Add' y x z) => Add x y z | x y -> z, z x -> y, z y -> x
+instance (Add' x y z, Add' y x z) => Add x y z
+
+
+-- | value-level reflection function for the 'Add' type-level relation 
+(+) :: (Add x y z) => x -> y -> z
+(+) = undefined
+
+-- | Subtraction type-level relation. @Sub x y z@ establishes
+--  that @x - y = z@ 
+class Sub x y z | x y -> z, z x -> y, z y -> x
+instance Add x y z => Sub z y x
+
+-- | value-level reflection function for the 'Sub' type-level relation 
+(-) :: (Sub x y z) => x -> y -> z
+(-) = undefined
+
+------------------------------
+-- Multiplication and Division
+------------------------------
+
+-----------------
+-- Multiplication
+-----------------
+
+-- | Multiplication type-level relation. @Mul x y z@ establishes
+--  that @x * y = z@.
+--   Note it isn't relational (i.e. its inverse cannot be used for division,
+--   however, even if it could, the resulting division would only
+--   work for zero-remainder divisions)
+class (Nat x, Nat y, Nat z) => Mul x y z | x y -> z
+
+-- By structural induction on the first argument
+instance Nat y => Mul D0 y D0
+instance Nat y => Mul D1 y y
+instance Add y y z => Mul D2 y z
+-- IMPORTANT: changing the line above by the commented line below
+--            would make multiplication relational. However, that would
+--            happen at the cost of performing a division by 2 in every 
+--            multiplication which doesn't pay off.
+--            Besides, the Division algortihm obtained out of the 
+--            inverse of Mul can only work when the remainder is zero, 
+--            which isn't really useful.
+-- instance (Add y y z, DivMod z D2 y D0) => Mul D2 y z
+instance (Add z y z', Mul D2 y z) => Mul D3 y z'
+instance (Add z y z', Mul D3 y z) => Mul D4 y z'
+instance (Add z y z', Mul D4 y z) => Mul D5 y z'
+instance (Add z y z', Mul D5 y z) => Mul D6 y z'
+instance (Add z y z', Mul D6 y z) => Mul D7 y z'
+instance (Add z y z', Mul D7 y z) => Mul D8 y z'
+instance (Add z y z', Mul D8 y z) => Mul D9 y z'
+-- TODO explain.
+instance (Pos (xi :* xl), Nat y, Mul xi y z, Mul10 z z10, Mul xl y dy, 
+          Add dy z10 z')  => Mul (xi :* xl) y z'
+
+
+-- | value-level reflection function for the multiplication type-level relation 
+(*) :: Mul x y z => x -> y -> z
+(*) = undefined
+
+
+-----------
+-- Division
+-----------
+
+-- | Division and Remainder type-level relation. @DivMod x y q r@ establishes
+--  that @x/y = q + r/y@
+--   Note it is not relational (i.e. its inverse cannot be used 
+--   for multiplication). 
+class (Nat x, Pos y) =>  DivMod x y q r | x y -> q r
+instance (Pos y, Trich x y cmp, DivMod' x y q r cmp) => DivMod x y q r
+
+class (Nat x, Pos y) => DivMod' x y q r cmp | x y cmp -> q r, 
+                                              q r cmp y -> x,
+                                              q r cmp x -> y 
+instance (Nat x, Pos y) => DivMod' x y D0 x  LT
+instance (Nat x, Pos y) => DivMod' x y D1 D0 EQ
+instance (Nat x, Pos y, Sub x y x', Pred q q', DivMod x' y q' r) 
+  => DivMod' x y q r GT
+
+-- | value-level reflection function for the 'DivMod' type-level relation
+divMod :: DivMod x y q r => x -> y -> (q,r)
+divMod _ _ = (undefined, undefined)
+
+-- | Division type-level relation. Remainder-discarding version of 'DivMod'. 
+--   Note it is not relational (due to DivMod not being relational)
+class Div x y z | x y -> z, x z -> y, y z -> x
+instance (DivMod x y q r) => Div x y q
+
+-- | value-level reflection function for the 'Div' type-level relation 
+div :: Div x y z => x -> y -> z
+div = undefined
+
+-- | Remainder of division, type-level relation. @Mod x y r@ establishes that
+--   @r@ is the reminder of dividing @x@ by @y@.
+class Mod x y r | x y -> r
+instance DivMod x y q r => Mod x y r
+
+-- | value-level reflection function for the 'Mod' type-level relation 
+mod :: Mod x y r => x -> y -> r
+mod = undefined
+
+
+----------------------------------------
+-- Multiplication/Division special cases
+----------------------------------------
+
+-- | Multiplication by 10 type-level relation (based on 'DivMod10').
+--   @Mul10 x y@ establishes that @10 * x = y@.
+class (Nat x, Nat q) => Mul10 x q | x -> q, q -> x
+instance DivMod10 x q D0 => Mul10 q x
+
+-- | value-level reflection function for 'Mul10' 
+mul10 :: Mul10 x q => x -> q
+mul10 = undefined
+
+-- | Division by 10 and Remainer type-level relation (similar to 'DivMod'). 
+--
+--   This operation is much faster than DivMod. Furthermore, it is 
+--   the general, non-structural, constructor/deconstructor since it
+--   splits a decimal numeral into its initial digits and last digit.
+--   Thus, it allows to inspect the structure of a number and is normally
+--   used to create type-level operations.
+--
+--   Note that contrary to 'DivMod', 'DivMod10' is relational (it can be used to
+--   multiply by 10)
+class (Nat i, Nat x) => DivMod10 x i l | i l -> x, x -> i l
+instance DivMod10 D0 D0 D0
+instance DivMod10 D1 D0 D1
+instance DivMod10 D2 D0 D2
+instance DivMod10 D3 D0 D3
+instance DivMod10 D4 D0 D4
+instance DivMod10 D5 D0 D5
+instance DivMod10 D6 D0 D6
+instance DivMod10 D7 D0 D7
+instance DivMod10 D8 D0 D8
+instance DivMod10 D9 D0 D9
+instance (Nat (D1 :* l)) => DivMod10 (D1 :* l) D1 l  
+instance (Nat (D2 :* l)) => DivMod10 (D2 :* l) D2 l  
+instance (Nat (D3 :* l)) => DivMod10 (D3 :* l) D3 l  
+instance (Nat (D4 :* l)) => DivMod10 (D4 :* l) D4 l  
+instance (Nat (D5 :* l)) => DivMod10 (D5 :* l) D5 l  
+instance (Nat (D6 :* l)) => DivMod10 (D6 :* l) D6 l 
+instance (Nat (D7 :* l)) => DivMod10 (D7 :* l) D7 l  
+instance (Nat (D8 :* l)) => DivMod10 (D8 :* l) D8 l  
+instance (Nat (D9 :* l)) => DivMod10 (D9 :* l) D9 l  
+instance (Nat (x :* l), Nat ((x :* l) :* l')) => 
+  DivMod10 ((x :* l) :* l') (x :* l) l' 
+
+-- | value-level reflection function for DivMod10 
+divMod10 :: DivMod10 x q r => x -> (q,r)
+divMod10 _ = (undefined, undefined)
+
+
+-- | Division by 10 type-level relation (based on DivMod10)
+class (Nat x, Nat q) => Div10 x q | x -> q, q -> x
+instance DivMod10 x q r => Div10 x q
+
+-- | value-level reflection function for Mul10 
+div10 :: Div10 x q => x -> q
+div10 = undefined
+
+----------------------------
+-- Is-Divisible-By assertion
+----------------------------
+
+-- | Is-divisible-by type-level assertion. e.g @IsDivBy d x@ establishes that
+--   @x@ is divisible by @d@.
+class (Pos d, Nat x) => IsDivBy d x
+instance (DivMod x d q D0) => IsDivBy d x
+
+-- | value-level reflection function for IsDivBy
+isDivBy :: IsDivBy d x => d -> x
+isDivBy = undefined
+
+---------------------------
+-- Exponentiation/Logarithm
+---------------------------
+
+-- | Exponentation type-level relation. @ExpBase b e r@ establishes
+--  that @b^e = r@
+--  Note it is not relational (i.e. it cannot be used to express logarithms)
+class (Nat b, Nat e, Nat r) => ExpBase b e r | b e -> r
+
+-- structural induction over the exponent
+instance Nat b => ExpBase b D0 D1
+instance Nat b => ExpBase b D1 b
+instance (Mul b b r) => ExpBase b D2 r
+instance (Mul r b r', ExpBase b D2 r) => ExpBase b D3 r'
+instance (Mul r b r', ExpBase b D3 r) => ExpBase b D4 r'
+instance (Mul r b r', ExpBase b D4 r) => ExpBase b D5 r'
+instance (Mul r b r', ExpBase b D5 r) => ExpBase b D6 r'
+instance (Mul r b r', ExpBase b D6 r) => ExpBase b D7 r'
+instance (Mul r b r', ExpBase b D7 r) => ExpBase b D8 r'
+instance (Mul r b r', ExpBase b D8 r) => ExpBase b D9 r'
+instance (Nat b, Pos (ei :* el), Nat r, 
+          Mul b r r', Pred (ei :* el) e', ExpBase b e' r) 
+           => ExpBase b (ei :* el) r'
+-- | value-level reflection function for the ExpBase type-level relation
+(^) :: ExpBase b e r => b -> e -> r
+(^) = undefined
+
+
+-- Logarithm type-level relation. @LogBase b x e@ establishes that 
+-- @log_base_b x = e@
+--  Note it is not relational (i.e. cannot be used to express exponentiation)
+class (Pos b, b :>=: D2, Pos x, Nat e) =>  LogBase b x e  | b x -> e 
+instance  LogBaseF b x e f => LogBase b x e
+
+
+-- | value-level reflection function for LogBase
+logBase :: LogBaseF b x e f => b -> x -> e
+logBase = undefined 
+
+
+-- | Version of LogBase which also outputs if the logarithm
+-- calculated was exact.
+-- f indicates if the resulting logarithm has no fractional part (i.e.
+-- tells if the result provided is exact)
+class (Pos b, b :>=: D2, Pos x, Nat e, Bool f) 
+     =>  LogBaseF b x e f | b x -> e f
+instance (Trich x b cmp, LogBaseF' b x e f cmp) => LogBaseF b x e f
+
+class (Pos b, b :>=: D2, Pos x, Nat e, Bool f)
+     => LogBaseF' b x e f cmp | b x cmp -> e f 
+instance (Pos b, b :>=: D2, Pos x) => LogBaseF' b x D0 False LT
+instance (Pos b, b :>=: D2) => LogBaseF' b b D1 True  EQ
+instance (Pos b, b :>=: D2, Pos x, DivMod x b q r, IsZero r rz, And rz f' f, 
+          Pred e e', LogBaseF b q e' f') => LogBaseF' b x e f GT
+
+-- | value-level reflection function for LogBaseF
+logBaseF :: LogBaseF b x e f => b -> x -> (e,f)
+logBaseF _ _ = (undefined, undefined) 
+
+
+-- We could reuse LogBaseF for IsPowOf but it would be inneficient.
+-- LogBaseF continues calculating the logarithm even if after knowing its
+-- not exact. Thus, it is desirable to include a custom definition of
+-- IsPowOf which can "abort" the calculation forcing the Divisions to be
+-- exact
+
+
+-- | Assert that a number (@x@) can be expressed as the power of another one
+--   (@b@) (i.e. the fractional part of @log_base_b x = 0@, or, 
+--   in a different way, @exists y . b\^y = x@). 
+class (Pos b, b :>=: D2, Pos x) =>  IsPowOf b x
+instance (Trich x b cmp, IsPowOf' b x cmp) => IsPowOf b x
+
+class (Pos b, b :>=: D2, Pos x) => IsPowOf' b x cmp
+-- If lower (x < b), then the logarithm is not exact  
+-- instance (Pos b, b :>=: D2, Pos x) => IsPowOf' b x LT
+instance (Pos b, b :>=: D2) => IsPowOf' b b EQ
+instance (Pos b, b :>=: D2, Pos x, DivMod x b q D0, IsPowOf b q) 
+         => IsPowOf' b x  GT
+-- | 
+isPowOf :: IsPowOf b x => b -> x -> ()
+isPowOf = undefined
+
+-----------------------------------
+-- Base-10 Exponentiation/Logarithm
+-----------------------------------
+
+-- | Base-10 Exponentiation type-level relation
+class (Nat x, Pos y) => Exp10 x y | x -> y, y -> x
+instance Exp10 D0 D1
+instance Exp10 D1 (D1 :* D0)
+instance Exp10 D2 (D1 :* D0 :* D0)
+instance Exp10 D3 (D1 :* D0 :* D0 :* D0)
+instance Exp10 D4 (D1 :* D0 :* D0 :* D0 :* D0)
+instance Exp10 D5 (D1 :* D0 :* D0 :* D0 :* D0 :* D0)
+instance Exp10 D6 (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
+instance Exp10 D7 (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
+instance Exp10 D8 (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
+instance Exp10 D9 (D1 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
+instance (Pred (xi :* xl) x', 
+          Exp10 x' (y :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0))
+      => Exp10 (xi :* xl) 
+               (y :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0 :* D0)
+
+-- | value-level reflection function for Exp10
+exp10 :: Exp10 x y => x -> y
+exp10 = undefined
+
+-- | Base-10 logarithm type-level relation
+--   Note it is not relational (cannot be used to express Exponentation to 10)
+--   However, it works with any positive numeral (not just powers of 10)
+class (Pos x, Nat y) => Log10 x y | x -> y
+instance Log10 D1 D0
+instance Log10 D2 D0
+instance Log10 D3 D0
+instance Log10 D4 D0
+instance Log10 D5 D0
+instance Log10 D6 D0
+instance Log10 D7 D0
+instance Log10 D8 D0
+instance Log10 D9 D0
+instance (Pos (xi :* xl), Pred y y', Log10 xi y') => Log10 (xi :* xl) y
+
+-- | value-level reflection function for 'Log10'
+log10 :: Log10 x y => x -> y
+log10 = undefined
+
+{- Log10': Alternative implementation of Log10
+
+Relational, but it only works for results of Exp10 (i.e. powers of 10).
+
+class (Pos x, Nat y) => Log10' x y | x -> y, y -> x
+instance Exp10 x y => Log10' y x
+-}
+
+
+-------------
+-- Comparison
+-------------
+
+-- type-level values denoting comparison results
+
+-- | Lower than 
+data LT
+-- | Equal
+data EQ
+-- | Greater than
+data GT
+
+-- | Trichotomy type-level relation. 'Trich x y r' establishes
+--   the relation (@r@) between @x@ and @y@. The obtained relation (@r@)
+--   Can be 'LT' (if @x@ is lower than @y@), 'EQ' (if @x@ equals @y@) or
+--   'GT' (if @x@ is greater than @y@)
+class (Nat x, Nat y) => Trich x y r | x y -> r
+
+-- | value-level reflection function for the comparison type-level assertion 
+trich :: Trich x y r => z -> x -> r
+trich = undefined
+
+-- by structural induction on the first, and then the second argument
+-- D0
+instance Trich D0 D0 EQ
+instance Trich D0 D1 LT
+instance Trich D0 D2 LT
+instance Trich D0 D3 LT
+instance Trich D0 D4 LT
+instance Trich D0 D5 LT
+instance Trich D0 D6 LT
+instance Trich D0 D7 LT
+instance Trich D0 D8 LT
+instance Trich D0 D9 LT
+instance Pos (yi :* yl) => Trich D0 (yi :* yl) LT
+instance Pos (yi :* yl) => Trich (yi :* yl) D0 GT
+-- D1
+instance Trich D1 D0 GT
+instance Trich D1 D1 EQ
+instance Trich D1 D2 LT
+instance Trich D1 D3 LT 
+instance Trich D1 D4 LT
+instance Trich D1 D5 LT 
+instance Trich D1 D6 LT
+instance Trich D1 D7 LT 
+instance Trich D1 D8 LT
+instance Trich D1 D9 LT
+instance Pos (yi :* yl) => Trich D1 (yi :* yl) LT
+instance Pos (yi :* yl) => Trich (yi :* yl) D1 GT
+-- D2
+instance Trich D2 D0 GT
+instance Trich D2 D1 GT
+instance Trich D2 D2 EQ
+instance Trich D2 D3 LT
+instance Trich D2 D4 LT
+instance Trich D2 D5 LT
+instance Trich D2 D6 LT
+instance Trich D2 D7 LT
+instance Trich D2 D8 LT
+instance Trich D2 D9 LT
+instance Pos (yi :* yl) => Trich D2 (yi :* yl) LT
+instance Pos (yi :* yl) => Trich (yi :* yl) D2 GT
+-- D3
+instance Trich D3 D0 GT
+instance Trich D3 D1 GT
+instance Trich D3 D2 GT
+instance Trich D3 D3 EQ
+instance Trich D3 D4 LT
+instance Trich D3 D5 LT
+instance Trich D3 D6 LT
+instance Trich D3 D7 LT
+instance Trich D3 D8 LT
+instance Trich D3 D9 LT
+instance Pos (yi :* yl) => Trich D3 (yi :* yl) LT
+instance Pos (yi :* yl) => Trich (yi :* yl) D3 GT
+-- D4
+instance Trich D4 D0 GT
+instance Trich D4 D1 GT
+instance Trich D4 D2 GT
+instance Trich D4 D3 GT
+instance Trich D4 D4 EQ
+instance Trich D4 D5 LT
+instance Trich D4 D6 LT
+instance Trich D4 D7 LT
+instance Trich D4 D8 LT
+instance Trich D4 D9 LT
+instance Pos (yi :* yl) => Trich D4 (yi :* yl) LT
+instance Pos (yi :* yl) => Trich (yi :* yl) D4 GT
+-- D5
+instance Trich D5 D0 GT
+instance Trich D5 D1 GT
+instance Trich D5 D2 GT
+instance Trich D5 D3 GT
+instance Trich D5 D4 GT
+instance Trich D5 D5 EQ
+instance Trich D5 D6 LT
+instance Trich D5 D7 LT
+instance Trich D5 D8 LT
+instance Trich D5 D9 LT
+instance Pos (yi :* yl) => Trich D5 (yi :* yl) LT
+instance Pos (yi :* yl) => Trich (yi :* yl) D5 GT
+-- D6
+instance Trich D6 D0 GT
+instance Trich D6 D1 GT
+instance Trich D6 D2 GT
+instance Trich D6 D3 GT
+instance Trich D6 D4 GT
+instance Trich D6 D5 GT
+instance Trich D6 D6 EQ
+instance Trich D6 D7 LT
+instance Trich D6 D8 LT
+instance Trich D6 D9 LT
+instance Pos (yi :* yl) => Trich D6 (yi :* yl) LT
+instance Pos (yi :* yl) => Trich (yi :* yl) D6 GT
+-- D7
+instance Trich D7 D0 GT
+instance Trich D7 D1 GT
+instance Trich D7 D2 GT
+instance Trich D7 D3 GT
+instance Trich D7 D4 GT
+instance Trich D7 D5 GT
+instance Trich D7 D6 GT
+instance Trich D7 D7 EQ
+instance Trich D7 D8 LT
+instance Trich D7 D9 LT
+instance Pos (yi :* yl) => Trich D7 (yi :* yl) LT
+instance Pos (yi :* yl) => Trich (yi :* yl) D7 GT
+-- D8
+instance Trich D8 D0 GT
+instance Trich D8 D1 GT
+instance Trich D8 D2 GT
+instance Trich D8 D3 GT
+instance Trich D8 D4 GT
+instance Trich D8 D5 GT
+instance Trich D8 D6 GT
+instance Trich D8 D7 GT
+instance Trich D8 D8 EQ
+instance Trich D8 D9 LT
+instance Pos (yi :* yl) => Trich D8 (yi :* yl) LT
+instance Pos (yi :* yl) => Trich (yi :* yl) D8 GT
+-- D9
+instance Trich D9 D0 GT
+instance Trich D9 D1 GT
+instance Trich D9 D2 GT
+instance Trich D9 D3 GT
+instance Trich D9 D4 GT
+instance Trich D9 D5 GT
+instance Trich D9 D6 GT
+instance Trich D9 D7 GT
+instance Trich D9 D8 GT
+instance Trich D9 D9 EQ
+instance Pos (yi :* yl) => Trich D9 (yi :* yl) LT
+instance Pos (yi :* yl) => Trich (yi :* yl) D9 GT
+
+
+-- multidigit comparison
+instance (Pos (xi :* xl), Pos (yi :* yl), Trich xl yl rl, Trich xi yi ri,
+	  CS ri rl r) => Trich (xi :* xl) (yi :* yl) r
+
+-- strengthen the comparison relation
+class CS r1 r2 r3 | r1 r2 -> r3
+instance CS EQ r r
+instance CS GT r GT
+instance CS LT r LT
+
+-- Abbreviated comparison assertions
+
+-- | Equality abbreviated type-level assertion
+class x :==: y
+instance (Trich x y EQ) => (:==:) x y -- ??? x :==: y fires an error 
+                                         -- with ghc 6.8.2 
+
+-- | value-level reflection function for the equality abbreviated 
+--   type-level assertion 
+(==) :: (x :==: y) => x -> y -> ()
+(==) = undefined
+
+-- | Greater-than abbreviated type-level assertion
+class x :>: y
+instance (Trich x y GT) => (:>:) x y 
+
+-- | value-level reflection function for the equality abbreviated 
+--   type-level assertion 
+(>) :: (x :>: y) => x -> y -> ()
+(>) = undefined
+
+-- | Lower-than abbreviated type-level assertion
+class x :<: y
+instance (Trich x y LT) => (:<:) x y 
+
+-- | value-level reflection function for the lower-than abbreviated 
+--   type-level assertion 
+(<) :: (x :<: y) => x -> y -> ()
+(<) = undefined
+
+-- | Greater-than or equal abbreviated type-level assertion
+class x :>=: y
+instance (Succ x x', Trich x' y GT) => (:>=:) x y 
+
+-- | value-level reflection function for the greater-than or equal abbreviated 
+--   type-level assertion 
+(>=) :: (x :>=: y) => x -> y -> ()
+(>=) = undefined
+
+-- | Lower-than or equal abbreviated type-level assertion
+class x :<=: y
+instance (Succ x' x, Trich x' y LT) => (:<=:) x y
+
+-- | value-level reflection function for the lower-than or equal abbreviated 
+--   type-level assertion 
+(<=) :: (x :<=: y) => x -> y -> ()
+(<=) = undefined
+
+------------------
+-- Maximum/Minimum
+------------------
+
+-- Choose the largest of x and y in the order b
+class Max' x y b r | x y b -> r
+instance Max' x y LT y
+instance Max' x y EQ y
+instance Max' x y GT x
+
+-- | Maximum type-level relation
+class Max x y z | x y -> z
+instance (Max' x y b z, Trich x y b) => Max x y z
+
+-- | value-level reflection function for the maximum type-level relation
+max :: Max x y z => x -> y -> z
+max = undefined
+
+-- | Minimum type-level relation
+class Min x y z | x y -> z
+instance (Max' y x b z, Trich x y b) => Min x y z
+
+
+-- | value-level reflection function for the minimum type-level relation
+min :: Min x y z => x -> y -> z
+min = undefined
+
+-------
+-- GCD
+-------
+
+-- | Greatest Common Divisor type-level relation
+class (Nat x, Nat y, Nat gcd) => GCD x y gcd | x y -> gcd
+instance (Nat x, Nat y, Trich x y cmp, IsZero y yz, GCD' x y yz cmp gcd)
+   => GCD x y gcd
+
+-- Euclidean algorithm 
+class (Nat x, Nat y, Nat gcd) => GCD' x y yz cmp gcd | x y yz cmp -> gcd
+instance Nat x => GCD' x D0 True cmp D0
+instance (Nat x, Nat y, GCD y x gcd) => GCD' x y False LT gcd
+instance Nat x => GCD' x x  False EQ x
+instance (Nat x, Nat y, Sub x y x', GCD x' y gcd) => GCD' x y False GT gcd
+
+-- | value-level reflection function for the GCD type-level relation
+gcd :: GCD x y z => x -> y -> z
+gcd = undefined
+
+---------------------
+-- Internal functions
+---------------------
+
+-- classify a natural as positive or zero
+class IsZero x r | x -> r
+instance IsZero D0 True
+instance IsZero D1 False
+instance IsZero D2 False
+instance IsZero D3 False
+instance IsZero D4 False
+instance IsZero D5 False
+instance IsZero D6 False
+instance IsZero D7 False
+instance IsZero D8 False
+instance IsZero D9 False
+instance Pos x => IsZero (x :* d) False
diff --git a/src/Data/TypeLevel/Num/Reps.hs b/src/Data/TypeLevel/Num/Reps.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel/Num/Reps.hs
@@ -0,0 +1,90 @@
+{-# LANGUAGE EmptyDataDecls, TypeOperators, DeriveDataTypeable,
+             ScopedTypeVariables, TemplateHaskell #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel.Num.Reps
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (TypeOperators)
+--
+-- Type-level numerical representations. Currently, only decimals are 
+-- supported.
+-- 
+----------------------------------------------------------------------------
+module Data.TypeLevel.Num.Reps (
+ -- * Decimal representation
+ --   $decdescription
+ --  ** Digits
+ D0, D1, D2, D3, D4, D5, D6, D7, D8, D9,
+ --  ** Connective
+ (:*)(..),
+ ) where
+
+import Data.Typeable (Typeable)
+import Language.Haskell.TH.Syntax (Lift(..)) 
+
+-------------------------
+-- Decimal Representation
+-------------------------
+
+-- $decdescription 
+-- Decimals are represented using a different type (@Dx@) for each digit and a 
+-- binary infix connective (@:*@) to enable forming arbitrary precision 
+-- multidigit numbers. For example @D0@ represents number 0, @D4 :* D2@ 
+-- represents number 42, @D1 :* D0 :* D0@ represents 100, etc ... Obviously, 
+-- negative numbers cannot be represented.
+
+-- | Decimal digit zero
+data D0 deriving Typeable
+instance Show D0 where show _ = "0"
+instance Lift D0 where lift _ = [| undefined :: D0 |]
+-- | Decimal digit one
+data D1 deriving Typeable
+instance Show D1 where show _ = "1"
+instance Lift D1 where lift _ = [| undefined :: D1 |]
+-- | Decimal digit two
+data D2 deriving Typeable
+instance Show D2 where show _ = "2"
+instance Lift D2 where lift _ = [| undefined :: D2 |]
+-- | Decimal digit three 
+data D3 deriving Typeable
+instance Show D3 where show _ = "3"
+instance Lift D3 where lift _ = [| undefined :: D3 |]
+-- | Decimal digit four 
+data D4 deriving Typeable
+instance Show D4 where show _ = "4"
+instance Lift D4 where lift _ = [| undefined :: D4 |]
+-- | Decimal digit five
+data D5 deriving Typeable
+instance Show D5 where show _ = "5"
+instance Lift D5 where lift _ = [| undefined :: D5 |]
+-- | Decimal digit six
+data D6 deriving Typeable
+instance Lift D6 where lift _ = [| undefined :: D6 |]
+instance Show D6 where show _ = "6"
+-- | Decimal digit seven
+data D7 deriving Typeable
+instance Show D7 where show _ = "7"
+instance Lift D7 where lift _ = [| undefined :: D7 |]
+-- | Decimal digit eight
+data D8 deriving Typeable
+instance Show D8 where show _ = "8"
+instance Lift D8 where lift _ = [| undefined :: D8 |]
+-- | Decimal digit nine
+data D9 deriving Typeable
+instance Show D9 where show _ = "9"
+instance Lift D9 where lift _ = [| undefined :: D9 |]
+
+-- | Connective to glue digits together.
+--   For example, @D1 :* D0 :* D0@ represents the decimal number 100
+data a :* b = a :* b deriving Typeable
+
+instance (Show a, Show b) => Show (a :* b) where
+  show _ = (show (undefined :: a)) ++ (show (undefined :: b))
+
+instance (Lift a, Lift b) => Lift (a :* b) where
+  lift _ = [| $(lift (undefined ::a)) :* $(lift (undefined :: b) ) |]
diff --git a/src/Data/TypeLevel/Num/Sets.hs b/src/Data/TypeLevel/Num/Sets.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeLevel/Num/Sets.hs
@@ -0,0 +1,172 @@
+{-# LANGUAGE TypeOperators, FlexibleInstances, FlexibleContexts,
+             UndecidableInstances, PatternSignatures, ScopedTypeVariables,
+             Rank2Types #-}
+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-name-shadowing #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.TypeLevel.Num.Sets
+-- Copyright   :  (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+--                    and KTH's SAM group 
+-- License     :  BSD-style (see the file LICENSE)
+-- 
+-- Maintainer  :  alfonso.acosta@gmail.com
+-- Stability   :  experimental
+-- Portability :  non-portable (non-standard instances)
+--
+-- Type-level numerical sets. Currently there is only support for Naturals and 
+-- Positives.
+-- 
+----------------------------------------------------------------------------
+module Data.TypeLevel.Num.Sets (Pos, Nat, toNum, toInt, reifyIntegral) where 
+
+import Data.TypeLevel.Num.Reps
+
+-----------
+-- Naturals
+-----------
+
+
+-- The well-formedness condition, the kind predicate.
+-- These classes are internal, denoted by the ending "I", which is removed in 
+-- the exported proxies (read below)
+
+-- | Naturals (Positives and zero), internal version
+class NatI n where 
+ -- | Reflecting function
+ toNum :: Num a => n -> a
+
+
+-- | Less generic reflecting function (Int)
+toInt :: Nat n => n -> Int
+toInt =  toNum
+
+
+
+-- | Positives (Naturals without zero), internal version
+class NatI n => PosI n
+
+-- To prevent the user from adding new instances to NatI and especially
+-- to PosI (e.g., to prevent the user from adding the instance |Pos D0|)
+-- we do NOT export NatI and PosI. Rather, we export the following proxies.
+-- The proxies entail PosI and NatI and so can be used to add PosI and NatI
+-- constraints in the signatures. However, all the constraints below
+-- are expressed in terms of NatI and PosI rather than proxies. Thus,
+-- even if the user adds new instances to proxies, it would not matter.
+-- Besides, because the following proxy instances are most general,
+-- one may not add further instances without overlapping instance extension.
+
+-- | Naturals (Positives and zero)
+class    NatI n => Nat n
+instance NatI n => Nat n
+
+-- | Positives (Naturals without zero)
+class    PosI n => Pos n
+instance PosI n => Pos n
+
+--------------------
+-- Natural Instances
+--------------------
+
+-- Note: TH would be helpful to sistematically define instances 
+--       (our type level operations)
+--       However, type-splicing is not yet implemented in GHC :S
+
+-- monodigit naturals
+instance NatI D0 where toNum _ = fromInteger 0
+instance NatI D1 where toNum _ = fromInteger 1
+instance NatI D2 where toNum _ = fromInteger 2
+instance NatI D3 where toNum _ = fromInteger 3
+instance NatI D4 where toNum _ = fromInteger 4
+instance NatI D5 where toNum _ = fromInteger 5
+instance NatI D6 where toNum _ = fromInteger 6
+instance NatI D7 where toNum _ = fromInteger 7
+instance NatI D8 where toNum _ = fromInteger 8
+instance NatI D9 where toNum _ = fromInteger 9
+
+-- multidigit naturals
+-- Note: The PosI constraint guarantees that all valid representations are 
+-- normalized (i.e. D0 :* D1 will lead to a compiler error)
+-- Note as well that ill-formed representations such as
+-- (D1 :* D2) :* (D3 :* D4) are not recognized as instances of
+-- naturals nor positives.
+instance PosI x => NatI (x :* D0) where toNum n = subLastDec n
+instance PosI x => NatI (x :* D1) where toNum n = subLastDec n + fromInteger 1
+instance PosI x => NatI (x :* D2) where toNum n = subLastDec n + fromInteger 2
+instance PosI x => NatI (x :* D3) where toNum n = subLastDec n + fromInteger 3
+instance PosI x => NatI (x :* D4) where toNum n = subLastDec n + fromInteger 4
+instance PosI x => NatI (x :* D5) where toNum n = subLastDec n + fromInteger 5
+instance PosI x => NatI (x :* D6) where toNum n = subLastDec n + fromInteger 6
+instance PosI x => NatI (x :* D7) where toNum n = subLastDec n + fromInteger 7
+instance PosI x => NatI (x :* D8) where toNum n = subLastDec n + fromInteger 8
+instance PosI x => NatI (x :* D9) where toNum n = subLastDec n + fromInteger 9
+
+-- monodigit positives
+instance PosI D1
+instance PosI D2
+instance PosI D3
+instance PosI D4
+instance PosI D5
+instance PosI D6
+instance PosI D7
+instance PosI D8
+instance PosI D9
+
+-- multidigit positives
+-- Note: The PosI constraint guarantees that all valid representations are 
+-- normalized (i.e. D0 :* D1 will lead to a compiler error)
+instance PosI x => PosI (x :* D0)
+instance PosI x => PosI (x :* D1)
+instance PosI x => PosI (x :* D2)
+instance PosI x => PosI (x :* D3)
+instance PosI x => PosI (x :* D4)
+instance PosI x => PosI (x :* D5)
+instance PosI x => PosI (x :* D6)
+instance PosI x => PosI (x :* D7)
+instance PosI x => PosI (x :* D8)
+instance PosI x => PosI (x :* D9)
+
+
+-- | Reification function. In CPS style (best possible solution)
+reifyIntegral :: Integral i => i -> (forall n . Nat n => n -> r) -> r
+reifyIntegral i f 
+ | i < 0     = error "reifyIntegral: integral < 0"
+ | i == 0    = f (undefined :: D0)
+ | otherwise = reifyIntegralp i f 
+       -- reifyIntegral for positives
+ where reifyIntegralp :: Integral i => i -> (forall n . Pos n => n -> r) -> r
+       reifyIntegralp i f 
+         | i < 10 = case i of
+                     1 -> f (undefined :: D1)
+                     2 -> f (undefined :: D2); 3 -> f (undefined :: D3)
+                     4 -> f (undefined :: D4); 5 -> f (undefined :: D5)
+                     6 -> f (undefined :: D6); 7 -> f (undefined :: D7)
+                     8 -> f (undefined :: D8); 9 -> f (undefined :: D9)
+         | otherwise =  
+            case m of
+              0 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D0)) 
+              1 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D1))
+              2 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D2))
+              3 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D3))
+              4 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D4))
+              5 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D5))
+              6 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D6))
+              7 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D7))
+              8 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D8))
+              9 -> reifyIntegralp d (\ (_::e) -> f (undefined :: e :* D9))      
+           where (d,m) = divMod i 10
+
+
+---------------------
+-- Internal functions
+---------------------
+
+-- substract the last digit of a decimal type-level numeral and obtain 
+-- the result's reflected value 
+{-# INLINE subLastDec #-}
+subLastDec :: (Num a, NatI (x :* d), NatI x) => x :* d -> a
+subLastDec = (10*).toNum.div10Dec
+
+-- Divide a decimal type-level numeral by 10 
+{-# INLINE div10Dec #-} 
+div10Dec :: NatI (x :* d) => x :* d -> x
+div10Dec _ = undefined
diff --git a/type-level.cabal b/type-level.cabal
new file mode 100644
--- /dev/null
+++ b/type-level.cabal
@@ -0,0 +1,51 @@
+name:           type-level
+version:        0.1
+cabal-version:  >= 1.2
+build-type:     Simple
+license:        BSD3
+license-file:   LICENSE
+copyright:      
+ Copyright (c) 2008 Alfonso Acosta, Oleg Kiselyov, Wolfgang Jeltsch
+                    and KTH's SAM group
+author:         Alfonso Acosta
+maintainer:     alfonso.acosta@gmail.com
+homepage:       http://code.haskell.org/type-level
+stability:      alpha
+package-url:    http://code.haskell.org/type-level
+synopsis:       Type-level programming library
+description:
+
+ This library permits performing computations on the type-level. Type-level 
+ functions are implemented using functional dependencies of multi
+ parameter type classes. 
+
+ To date, Booleans and Numerals (Naturals and Positives) are
+ supported. With regard to Numerals, there is support for common
+ arithmetic operations (addition, substraction, multiplication,
+ division, exponientation, logarithm, maximum, comparison, GCD) 
+ over natural numbers (using a decimal representation to make 
+ compile-time errors friendlier).
+
+ Although making use of type-level computations might seem devious and
+ obfuscated at first sight, it is indeed useful in practice to implement 
+ lightweight dependent types such us number-parameterized types (e.g. an array 
+ type parameterized by the array's size or a modular group type Zn 
+ parameterized by the modulus).
+
+category:       Data
+tested-with:    GHC==6.8.2
+
+
+-- depends on ghc due to the use of infix type constructors and template haskell
+Library
+  build-depends:   base, ghc, template-haskell > 2.0
+  hs-source-dirs:  src
+  exposed-modules: Data.TypeLevel,
+                   Data.TypeLevel.Bool,
+                   Data.TypeLevel.Num,
+                   Data.TypeLevel.Num.Reps,
+                   Data.TypeLevel.Num.Aliases,
+                   Data.TypeLevel.Num.Sets,
+                   Data.TypeLevel.Num.Ops,
+                   Data.TypeLevel.Num.Aliases.TH
+  ghc-options:	-Wall -O2