diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,31 @@
+Copyright (c) 2008-2012, Bjorn Buckwalter.
+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(s) nor the names of
+    contributors may be used to endorse or promote products derived
+    from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
+FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
+COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
+INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
+BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
diff --git a/Numeric/NumType/TF.lhs b/Numeric/NumType/TF.lhs
new file mode 100644
--- /dev/null
+++ b/Numeric/NumType/TF.lhs
@@ -0,0 +1,354 @@
+Numeric.NumType.TF -- Type-level (low cardinality) integers
+Bjorn Buckwalter, bjorn.buckwalter@gmail.com
+License: BSD3
+
+
+= Preliminaries =
+
+This module requires GHC 7.0 or later.
+
+> {-# LANGUAGE UndecidableInstances
+>            , TypeFamilies
+>            , EmptyDataDecls
+>            , FlexibleInstances
+>            , ScopedTypeVariables
+> #-}
+
+
+= Summary =
+
+> {- |
+>    Copyright  : Copyright (C) 2006-2012 Bjorn Buckwalter
+>    License    : BSD3
+>
+>    Maintainer : bjorn.buckwalter@gmail.com
+>    Stability  : Stable
+>    Portability: GHC only?
+>
+> This Module provides unary type-level representations, hereafter
+> referred to as 'NumType's, of the (positive and negative) integers
+> and basic operations (addition, subtraction, multiplication, division)
+> on these. While functions are provided for the operations 'NumType's
+> exist solely at the type level and their only value is 'undefined'.
+> 
+> There are similarities with the HNats of the HList library,
+> which was indeed a source of inspiration. Occasionally references
+> are made to the HNats. The main addition in this module is negative
+> numbers.
+> 
+> The practical size of the 'NumType's is limited by the type checker
+> stack. If the 'NumType's grow too large (which can happen quickly
+> with multiplication) an error message similar to the following will
+> be emitted:
+> 
+> @
+> Context reduction stack overflow; size = 20
+> Use -fcontext-stack=N to increase stack size to N
+> @
+>
+> This situation could concievably be mitigated significantly by using
+> e.g. a binary representation of integers rather than Peano numbers.
+> 
+> Please refer to the literate Haskell code for a narrative of 
+> the implementation.
+>
+> -}
+
+> module Numeric.NumType.TF (
+>   -- * Type level integers
+>     NumType
+>   -- * Data types
+>   -- | These are exported to avoid lengthy qualified types in complier
+>   -- error messages.
+>   , Z, S, N
+>   -- * Type level arithmetics
+>   , Pred, Succ, Negate, Add, Sub, Div, Mul
+>   -- * Type synonyms for convenience
+>   , Zero, Pos1, Pos2, Pos3, Pos4, Pos5, Neg1, Neg2, Neg3, Neg4, Neg5
+>   -- * Value level functions
+>   -- $functions
+>   , toNum, incr, decr, negate, (+), (-), (*), (/)
+>   -- * Values for convenience
+>   -- | For use with the value level functions.
+>   , zero, pos1, pos2, pos3, pos4, pos5, neg1, neg2, neg3, neg4, neg5
+>   ) where
+
+> import Prelude hiding ((*), (/), (+), (-), negate)
+> import qualified Prelude ((+), negate)
+
+Use the same fixity for operators as the Prelude.
+
+> infixl 7  *, /
+> infixl 6  +, -
+
+
+= NumTypes =
+
+We start by defining a class encompassing all integers with the
+class function 'toNum' that converts from the type-level to a
+value-level 'Num'.
+
+> class NumTypeI n where
+>   -- | Negation.
+>   type Negate n
+>   -- | Predecessor.
+>   type Pred n
+>   -- | Successor.
+>   type Succ n
+>   -- | Convert a type level integer to an instance of 'Prelude.Num'.
+>   toNum :: Num a => n -> a
+
+
+Now we use a trick from Oleg Kiselyov and Chung-chieh Shan [2]:
+
+    -- The well-formedness condition, the kind predicate
+    class Nat0 a where toInt :: a -> Int
+    class Nat0 a => Nat a           -- (positive) naturals
+
+    -- To prevent the user from adding new instances to Nat0 and especially
+    -- to Nat (e.g., to prevent the user from adding the instance |Nat B0|)
+    -- we do NOT export Nat0 and Nat. Rather, we export the following proxies.
+    -- The proxies entail Nat and Nat0 and so can be used to add Nat and Nat0
+    -- constraints in the signatures. However, all the constraints below
+    -- are expressed in terms of Nat0 and Nat 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.
+    class    Nat0 n => Nat0E n
+    instance Nat0 n => Nat0E n
+    class    Nat n => NatE n
+    instance Nat n => NatE n
+
+We apply this trick to our NumTypeI class. In our case we will elect to
+append an "I" to the internal (non-exported) classes rather than
+appending an "E" to the exported classes.
+
+> -- | Class encompassing all valid type level integers.
+> class    (NumTypeI n) => NumType n
+> instance (NumTypeI n) => NumType n
+
+Now we Define the data types used to represent integers. We begin
+with 'Zero', which we allow to be used as both a positive and a
+negative number in the sense of the previously defined type classes.
+'Z' corresponds to HList's 'HZero'.
+
+> -- | Type level zero.
+> data Z
+
+Next we define the "successor" type, here called 'S' (corresponding
+to HList's 'HSucc').
+
+> -- | Successor type for building type level natural numbers.
+> data S n
+
+Finally we define the "negation" type used to represent negative
+numbers.
+
+> -- | Negation type, used to represent negative numbers by negating
+> -- type level naturals.
+> data N n
+
+The 'NumTypeI' instances restrict how 'Z', 'S', and 'N' may be combined
+to assemble 'NumType's, and the type synonym declarations demonstrate
+some basic arithmetic.
+
+> instance NumTypeI Z where  -- Zero.
+>   type Negate Z = Z       -- Still zero.
+>   type Pred Z = N (S Z)   -- Negative one.
+>   type Succ Z = S Z       -- One.
+>   toNum _ = 0
+
+> instance NumTypeI (S Z) where   -- One.
+>   type Negate (S Z) = N (S Z)  -- Minus one.
+>   type Pred (S Z) = Z          -- Zero.
+>   type Succ (S Z) = S (S Z)    -- Two.
+>   toNum _ = 1
+
+> -- Naturals greater than one.
+> instance NumTypeI (S n) => NumTypeI (S (S n)) where  -- N.
+>   type Negate (S (S n)) = N (S (S n))              -- -N.
+>   type Pred (S (S n)) = S n                        -- N-1
+>   type Succ (S (S n)) = S (S (S n))                -- N+1
+>   toNum _ = 1 Prelude.+ toNum (undefined :: S n)
+
+> -- Negatives (minus one and below).
+> instance NumTypeI (S n) => NumTypeI (N (S n)) where  -- -N
+>   type Negate (N (S n)) = S n                      -- N
+>   type Pred (N (S n)) = N (S (S n))                -- -(N+1)
+>   type Succ (N (S n)) = Negate n                   -- -(N-1)
+>        -- NOTE: `N n` would be invalid for `Succ (N (S Z))`
+>   toNum _ = Prelude.negate $ toNum (undefined :: S n)
+
+
+= Show instances =
+
+For convenience we create show instances for the defined NumTypes.
+
+> instance Show Z where show = ("NumType " ++) . show . toNum
+> instance NumTypeI (S n) => Show (S n) where show = ("NumType " ++) . show . toNum
+> instance NumTypeI (N n) => Show (N n) where show = ("NumType " ++) . show . toNum
+
+
+= Addition and subtraction =
+
+Now let us move on towards more complex arithmetic operations. We
+define type families for addition and subtraction of NumTypes.
+
+> -- | Addition (@a + b@).
+> type family Add a b  -- a + b.
+> -- | Subtraction (@a - b@).
+> type family Sub a b  -- a - b.
+
+Adding anything to Zero gives "anything".
+
+> type instance Add Z n = n
+
+When adding to a non-Zero number our strategy is to "transfer" type
+constructors from the first type to the second type until the first
+type is Zero.
+
+> type instance Add (S n) n' = Add n (Succ n')
+> type instance Add (N n) n' = Add (Succ (N n)) (Pred n')
+
+Substitution is defined trivially with addition and negation.
+
+> type instance Sub a b = Add a (Negate b)
+
+
+= Multiplication =
+
+Type family for multiplication. Multiplication is limited by the
+type checker stack. If the result of multiplication is too large
+this error message will be emitted:
+
+    Context reduction stack overflow; size = 20
+    Use -fcontext-stack=N to increase stack size to N
+
+> -- | Multiplication (@a * b@).
+> type family Mul a b        -- a * b.
+> type instance Mul Z n = Z  -- Trivially.
+
+Multiplication is performed by recursive addition of one number
+to itself. The recursion is terminated by the `Mul Z n` instance.
+
+> type instance Mul (S n) n' = Add n' (Mul n n')  -- a*b = b+(a-1)*b
+> type instance Mul (N n) n' = Negate (Mul n n')  -- (-a)*b = -(a*b)
+
+
+= Division =
+
+Division is more complicated than multiplication. We start by
+defining division only for positive (natural) numbers. This is
+necessary to ensure bad division terminates with a proper error
+instead of overflowing the context stack (more confusing).
+
+> type family DivP n m            -- n / m.
+> type instance DivP Z (S n) = Z  -- Trivially.
+
+The recursive instance for division is quite complex and in fact I
+do not recall how I derived it. But it works (I promise!).
+
+> type instance DivP (S n) (S n') = S (DivP (Pred (Sub (S n) n')) (S n'))  -- Oh my!
+
+Now we can generalize division to negative numbers too, building on
+top of 'DivP'. A trivial but tedious exercise.
+
+> -- | Division (@a / b@).
+> type family Div a b            -- a / b.
+> type instance Div Z (N n) = Z  -- Mustn't allow “Div Z Z”!
+> type instance Div Z (S n) = Z
+> type instance Div (S n) (S n') = DivP (S n) (S n')
+> type instance Div (N n) (N n') = DivP n n'
+> type instance Div (N n) (S n') = N (DivP n (S n'))
+> type instance Div (S n) (N n') = N (DivP (S n) n')
+
+
+= Value level functions =
+
+> {- $functions
+> Using the above type families we define functions for various
+> arithmetic operations. All functions are undefined and only operate
+> on the type level. Their main contribution is that they facilitate
+> NumType arithmetic without explicit (and tedious) type declarations.
+> -}
+
+The main reason to collect all functions here is to keep the
+preceeding sections free from distraction.
+
+> -- | Negate a 'NumType'.
+> negate :: NumType a => a -> Negate a
+> negate _ = undefined
+
+> -- | Increment a 'NumType' by one.
+> incr :: NumType a => a -> Succ a
+> incr _ = undefined
+
+> -- | Decrement a 'NumType' by one.
+> decr :: NumType a => a -> Pred a
+> decr _ = undefined
+
+> -- | Add two 'NumType's.
+> (+) :: (NumType a, NumType b) => a -> b -> Add a b
+> _ + _ = undefined
+
+> -- | Subtract the second 'NumType' from the first.
+> (-) :: (NumType a, NumType b) => a -> b -> Sub a b
+> _ - _ = undefined
+
+> -- | Multiply two 'NumType's.
+> (*) :: (NumType a, NumType b) => a -> b -> Mul a b
+> _ * _ = undefined
+
+> -- | Divide the first 'NumType' by the second.
+> (/) :: (NumType a, NumType b) => a -> b -> Div a b
+> _ / _ = undefined
+
+
+= Convenince types and values =
+
+Finally we define some type synonyms for the convenience of clients
+of the library.
+
+> type Zero = Z
+> type Pos1 = S Z
+> type Pos2 = S Pos1
+> type Pos3 = S Pos2
+> type Pos4 = S Pos3
+> type Pos5 = S Pos4
+> type Neg1 = N Pos1
+> type Neg2 = N Pos2
+> type Neg3 = N Pos3
+> type Neg4 = N Pos4
+> type Neg5 = N Pos5
+
+Analogously we also define some convenience values (all 'undefined'
+but with the expected types).
+
+> zero :: Z  -- ~ hZero
+> zero = undefined
+> pos1 :: Pos1
+> pos1 = incr zero
+> pos2 :: Pos2
+> pos2 = incr pos1
+> pos3 :: Pos3
+> pos3 = incr pos2
+> pos4 :: Pos4
+> pos4 = incr pos3
+> pos5 :: Pos5
+> pos5 = incr pos4
+> neg1 :: Neg1
+> neg1 = decr zero
+> neg2 :: Neg2
+> neg2 = decr neg1
+> neg3 :: Neg3
+> neg3 = decr neg2
+> neg4 :: Neg4
+> neg4 = decr neg3
+> neg5 :: Neg5
+> neg5 = decr neg4
+
+
+= References =
+
+[1] http://homepages.cwi.nl/~ralf/HList/
+[2] http://okmij.org/ftp/Computation/resource-aware-prog/BinaryNumber.hs
diff --git a/Numeric/NumType/TFTests.hs b/Numeric/NumType/TFTests.hs
new file mode 100644
--- /dev/null
+++ b/Numeric/NumType/TFTests.hs
@@ -0,0 +1,111 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+
+module Numeric.NumType.TFTests where
+
+import Numeric.NumType.TF
+import Prelude hiding ((*), (/), (+), (-), negate)
+import qualified Prelude as P ((*), (/), (+), (-), negate)
+import Test.HUnit
+
+
+-- Compares a type level unary function with a value level unary function
+-- by converting 'NumType' to 'Integral'. This assumes that the 'toIntegral'
+-- function is solid.
+unaryTest :: (NumType n, NumType n', Num a)
+          => (n -> n') -> (a -> a) -> n -> Test
+unaryTest f f' x = TestCase $ assertEqual
+    "Unary function Integral equivalence"
+    (f' (toNum x)) (toNum (f x))
+
+-- Compares a type level binary function with a value level binary function
+-- by converting 'NumType' to 'Integral'. This assumes that the 'toIntegral'
+-- function is solid.
+binaryTest :: (NumType n, NumType n', NumType n'', Num a)
+           => (n -> n' -> n'') -> (a -> a -> a) -> n -> n' -> Test
+binaryTest f f' x y = TestCase $ assertEqual
+    "Binary function Integral equivalence"
+    (f' (toNum x) (toNum y)) (toNum (f x y))
+
+-- Test that conversion to 'Integral' works as expected. This is sort of a
+-- prerequisite for the other tests.
+testAsIntegral = TestLabel "Integral equivalence tests" $ TestList
+    [ TestCase $ -2 @=? toNum neg2
+    , TestCase $ -1 @=? toNum neg1
+    , TestCase $  0 @=? toNum zero
+    , TestCase $  1 @=? toNum pos1
+    , TestCase $  2 @=? toNum pos2
+    ] -- By induction all other NumTypes should be good if these are.
+
+-- Test increment and decrement for a bunch of 'NumTypes'.
+testIncrDecr = TestLabel "Increment and decrement tests" $ TestList
+    [ t neg2
+    , t neg1
+    , t zero
+    , t pos1
+    , t pos1
+    ] where
+        t x = TestList [ unaryTest incr (P.+ 1) x
+                       , unaryTest decr (P.- 1) x
+                       ]
+
+-- Test negation.
+testNegate = TestLabel "Negation tests" $ TestList
+    [ unaryTest negate P.negate neg2
+    , unaryTest negate P.negate neg1
+    , unaryTest negate P.negate zero
+    , unaryTest negate P.negate pos1
+    , unaryTest negate P.negate pos1
+    ]
+
+-- Test addition.
+testAddition = TestLabel "Addition tests" $ TestList
+    [ binaryTest (+) (P.+) pos2 pos3
+    , binaryTest (+) (P.+) neg2 pos3
+    , binaryTest (+) (P.+) pos2 neg3
+    , binaryTest (+) (P.+) neg2 neg3
+    ]
+
+-- Test subtraction.
+testSubtraction = TestLabel "Subtraction tests" $ TestList
+    [ binaryTest (-) (P.-) pos2 pos5
+    , binaryTest (-) (P.-) neg2 pos5
+    , binaryTest (-) (P.-) pos2 neg5
+    , binaryTest (-) (P.-) neg2 neg5
+    ]
+
+-- Test multiplication.
+testMultiplication = TestLabel "Multiplication tests" $ TestList
+    [ binaryTest (*) (P.*) pos2 pos5
+    , binaryTest (*) (P.*) neg2 pos5
+    , binaryTest (*) (P.*) pos2 neg5
+    , binaryTest (*) (P.*) neg2 neg5
+    , binaryTest (*) (P.*) pos2 zero
+    , binaryTest (*) (P.*) neg2 zero
+    , binaryTest (*) (P.*) zero pos5
+    , binaryTest (*) (P.*) zero neg5
+    ]
+
+-- Test division.
+testDivision = TestLabel "Division tests" $ TestList
+    [ binaryTest (/) (P./) pos4 pos2
+    , binaryTest (/) (P./) zero pos5
+    , binaryTest (/) (P./) zero neg3
+    , binaryTest (/) (P./) neg4 pos2
+    , binaryTest (/) (P./) pos4 neg2
+    , binaryTest (/) (P./) neg4 neg2
+    , binaryTest (/) (P./) pos5 pos5
+    ]
+
+
+-- Collect the test cases.
+tests = TestList
+    [ testAsIntegral
+    , testIncrDecr
+    , testNegate
+    , testAddition
+    , testSubtraction
+    , testMultiplication
+    , testDivision
+    ]
+
+main = runTestTT tests
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,10 @@
+For documentation see the literate haskell source code.
+
+For project information (issues, updates, wiki, examples) see:
+    http://code.google.com/p/dimensional/
+
+To install (requires GHC 6.6 or later):
+    runhaskell Setup.lhs configure
+    runhaskell Setup.lhs build
+    runhaskell Setup.lhs install
+
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,3 @@
+#!/usr/bin/env runhaskell
+> import Distribution.Simple
+> main = defaultMain
diff --git a/numtype-tf.cabal b/numtype-tf.cabal
new file mode 100644
--- /dev/null
+++ b/numtype-tf.cabal
@@ -0,0 +1,34 @@
+Name:                numtype-tf
+Version:             0.1
+License:             BSD3
+License-File:        LICENSE
+Copyright:           Bjorn Buckwalter 2012
+Author:              Bjorn Buckwalter
+Maintainer:          bjorn.buckwalter@gmail.com
+Stability:           stable
+Homepage:            http://dimensional.googlecode.com/
+Synopsis:            Type-level (low cardinality) integers, implemented
+                     using type families.
+Description:
+
+    This package provides unary type level representations of the
+    (positive and negative) integers and basic operations (addition,
+    subtraction, multiplication, division) on these.
+
+    Due to the unary implementation the practical size of the
+    NumTypes is severely limited making them unsuitable for
+    large-cardinality applications. If you will be working with
+    integers beyond (-20, 20) this package probably isn't for you.
+
+    The numtype-tf packade differs from the numtype package in that
+    the NumTypes are implemented using type families rather than
+    functional dependencies.
+
+    Requires GHC 7.0 or later.
+
+Category:            Math
+Build-Type:          Simple
+Build-Depends:       base < 5
+Exposed-Modules:     Numeric.NumType.TF
+Extra-source-files:  README,
+                     Numeric/NumType/TFTests.hs