(#2) Refactor Type-Level Arithmetic

* Move current Arithmetic module to Arithmetic.Internal
* Rename type families to Add/Mul, etc
* New Arithmetic module that just re-exports polykinded infix synonyms
  for the type families

NB. GHC 8.0.1 bug causes tests to fail to compile on -O1 or -O2

Closes #2

.travis.yml

@@ -206,7 +206,7 @@ script:
   set -ex
   case "$BUILD" in
     stack)
-      stack --stack-yaml $STACK_YAML --no-terminal $ARGS test --bench --no-run-benchmarks --haddock --no-haddock-deps
+      stack --stack-yaml $STACK_YAML --no-terminal $ARGS test --ghc-options=-O0 --bench --no-run-benchmarks --haddock --no-haddock-deps
       ;;
     cabal)
       cabal install --enable-tests --enable-benchmarks --force-reinstalls --ghc-options=-O0 --reorder-goals --max-backjumps=-1 $CABALARGS $PACKAGES

CHANGELOG.md

@@ -4,6 +4,12 @@ Change log
 typenums uses [PVP Versioning][1].
 The change log is available [on GitHub][2].
 
+0.1.2
+=====
+* ([#2](https://github.com/adituv/typenums/issues/2))
+  Refactored type-level arithmetic so that the type families are exposed from
+  an Internal module and are extensible.
+
 0.1.1.1
 =======
 * Add UndecidableInstances language extension to Data.TypeNums.Rats.  This

package.yaml

@@ -1,5 +1,5 @@
 name: typenums
-version: 0.1.1.1
+version: 0.1.2
 synopsis: Type level numbers using existing Nat functionality
 description: >
   Type level numbers using existing Nat functionality.

src/Data/TypeNums/Arithmetic.hs

@@ -1,103 +1,27 @@
-{-# LANGUAGE ConstraintKinds      #-}
-{-# LANGUAGE DataKinds            #-}
-{-# LANGUAGE ExplicitNamespaces   #-}
-{-# LANGUAGE PolyKinds            #-}
-{-# LANGUAGE Safe                 #-}
-{-# LANGUAGE TypeFamilies         #-}
-{-# LANGUAGE TypeInType           #-}
-{-# LANGUAGE TypeOperators        #-}
-{-# LANGUAGE UndecidableInstances #-}
-
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE PolyKinds          #-}
+{-# LANGUAGE Safe               #-}
+{-# LANGUAGE TypeOperators      #-}
+
+-- | This module provides operators for type-level arithmetic.  To
+--   extend this functionality, add new type instances to the underlying
+--   type families found in "Data.TypeNums.Arithmetic.Internal".
 module Data.TypeNums.Arithmetic
   ( type (+)
   , type (-)
   , type (*)
   ) where
 
-import Data.Type.Bool     (If)
-import Data.TypeNums.Ints
-import Data.TypeNums.Rats
-import GHC.TypeLits       (Nat)
-
-import qualified GHC.TypeLits as G
-
--- TODO: Reduce type-level rationals?  Probably not 100% necessary as the
--- user should only see them via ratVal which already handles reduction
--- at value level.
-
--- | The kind of the result of arithmetic
-type family ArithK k1 k2 where
-  ArithK Nat  Nat  = Nat
-  ArithK a    Rat  = Rat
-  ArithK Rat  a    = Rat
-  ArithK TInt a    = TInt
-  ArithK a    TInt = TInt
+import Data.TypeNums.Arithmetic.Internal
 
 infixl 6 +, -
 infixl 7 *
 
 -- | The sum of two type-level numbers
-type family (x :: k1) + (y :: k2) :: ArithK k1 k2 where
-  (x :: Nat)  + (y :: Nat)  = (G.+) x y
-
-  'Pos x      + 'Pos y      = 'Pos ((G.+) x y)
-  'Neg x      + 'Pos y      = If ((G.<=?) x y)
-                                ('Pos ((G.-) y x))
-                                ('Neg ((G.-) x y))
-  'Pos x      + 'Neg y      = If ((G.<=?) y x)
-                                ('Pos ((G.-) x y))
-                                ('Neg ((G.-) y x))
-  'Neg x      + 'Neg y      = 'Neg ((G.+) x y)
-
-  'Pos x      + (y :: Nat)  = 'Pos ((G.+) x y)
-  'Neg x      + (y :: Nat)  = If ((G.<=?) x y)
-                                ('Pos ((G.-) y x))
-                                ('Neg ((G.-) x y))
-  (x :: Nat)  + 'Pos y      = 'Pos ((G.+) x y)
-  (x :: Nat)  + 'Neg y      = If ((G.<=?) y x)
-                                ('Pos ((G.-) x y))
-                                ('Neg ((G.-) y x))
-
-  (n1 ':% d1) + (n2 ':% d2) = ((n1 * d2) + (n2 * d1)) ':% (d1 * d2)
-  (n ':% d)   + y           = ((d * y) + n) ':% d
-  x           + (n ':% d)   = ((d * x) + n) ':% d
-
-type family (x :: k1) - (y :: k2) :: ArithK k1 k2 where
-  (x :: Nat)  - (y :: Nat)  = (G.-) x y
-
-  'Pos x      - 'Pos y      = 'Pos x + 'Neg y
-  'Neg x      - 'Pos y      = 'Neg x + 'Neg y
-  'Pos x      - 'Neg y      = 'Pos x + 'Pos y
-  'Neg x      - 'Neg y      = 'Neg x + 'Pos y
-
-  'Pos x      - (y :: Nat)  = 'Pos x + 'Neg y
-  'Neg x      - (y :: Nat)  = 'Neg x + 'Neg y
-  (x :: Nat)  - 'Pos y      = 'Pos x + 'Neg y
-  (x :: Nat)  - 'Neg y      = 'Pos x + 'Pos y
-
-  -- Denominators are wrapped in Pos here to force the products to
-  -- evaluate as kind TInt instead of Nat.  Without this, it is possible
-  -- to end up with for example @(14 - 15) :: Nat@ which does not produce
-  -- a Nat and therefore causes typing to fail.
-  (n1 ':% d1) - (n2 ':% d2) = ((n1 * 'Pos d2) - (n2 * 'Pos d1)) ':% (d1 * d2)
-  (n ':% d)   - y           = (n - ('Pos d * y)) ':% d
-  x           - (n ':% d)   = (('Pos d * x) - n) ':% d
+type (+) a b = Add a b
 
+-- | The difference of two type-level numbers
+type (-) a b = Sub a b
 
 -- | The product of two type-level numbers
-type family (x :: k1) * (y :: k2) :: ArithK k1 k2 where
-  (x :: Nat)  * (y :: Nat)  = (G.*) x y
-
-  'Pos x      * 'Pos y      = 'Pos ((G.*) x y)
-  'Neg x      * 'Pos y      = 'Neg ((G.*) x y)
-  'Pos x      * 'Neg y      = 'Neg ((G.*) x y)
-  'Neg x      * 'Neg y      = 'Pos ((G.*) x y)
-
-  'Neg x      * (y :: Nat)  = 'Neg ((G.*) x y)
-  'Pos x      * (y :: Nat)  = 'Pos ((G.*) x y)
-  (x :: Nat)  * 'Neg y      = 'Neg ((G.*) x y)
-  (x :: Nat)  * 'Pos y      = 'Pos ((G.*) x y)
-
-  (n1 ':% d1) * (n2 ':% d2) = (n1 * n2) ':% (d1 * d2)
-  (n ':% d)   * y           = (n * y) ':% d
-  x           * (n ':% d)   = (x * n) ':% d
+type (*) a b = Mul a b

src/Data/TypeNums/Arithmetic/Internal.hs

@@ -0,0 +1,151 @@
+{-# LANGUAGE ConstraintKinds      #-}
+{-# LANGUAGE CPP                  #-}
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE ExplicitNamespaces   #-}
+{-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE Safe                 #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeInType           #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | This module exposes the inner workings of type-level arithmetic for
+--   further extensions.  The type families found within this module should
+--   not be used directly other than to add new  s; instead use
+--   the operators from "Data.TypeNums.Arithmetic".
+--
+--   Due to technical limitations, the type families are open for extension
+--   only in GHC 8.2 and onwards.
+-- @since 0.1.2
+module Data.TypeNums.Arithmetic.Internal where
+
+import Data.Type.Bool     (If)
+import Data.TypeNums.Ints
+import Data.TypeNums.Rats
+import GHC.TypeLits
+
+-- TODO: Reduce type-level rationals?  Probably not 100% necessary as the
+-- user should only see them via ratVal which already handles reduction
+-- at value level.
+
+-- | The kind of the result of addition.  If you add new cases to this
+--   type family, be aware that it could cause conflicts with other code
+--   that does the same.  Modify with caution.
+type family AddK k1 k2 where
+  AddK Nat  Nat  = Nat
+  AddK Nat  Rat  = Rat
+  AddK Nat  TInt = TInt
+  AddK Rat  Nat  = Rat
+  AddK Rat  Rat  = Rat
+  AddK Rat  TInt = Rat
+  AddK TInt Nat  = TInt
+  AddK TInt Rat  = Rat
+  AddK TInt TInt = TInt
+
+-- | The kind of the result of subtraction.  If you add new cases to this
+--   type family, be aware that it could cause conflicts with other code
+--   that does the same.  Modify with caution.
+type family SubK k1 k2 where
+  SubK Nat  Nat  = Nat
+  SubK Nat  Rat  = Rat
+  SubK Nat  TInt = TInt
+  SubK Rat  Nat  = Rat
+  SubK Rat  Rat  = Rat
+  SubK Rat  TInt = Rat
+  SubK TInt Nat  = TInt
+  SubK TInt Rat  = Rat
+  SubK TInt TInt = TInt
+
+-- | The kind of the result of multiplication.  If you add new cases to this
+--   type family, be aware that it could cause conflicts with other code
+--   that does the same.  Modify with caution.
+type family MulK k1 k2 where
+  MulK Nat  Nat  = Nat
+  MulK Nat  Rat  = Rat
+  MulK Nat  TInt = TInt
+  MulK Rat  Nat  = Rat
+  MulK Rat  Rat  = Rat
+  MulK Rat  TInt = Rat
+  MulK TInt Nat  = TInt
+  MulK TInt Rat  = Rat
+  MulK TInt TInt = TInt
+
+
+-- | The sum of two type-level numbers.
+type family Add (x :: k1) (y :: k2) :: AddK k1 k2 where
+  Add (x :: Nat) (y :: Nat)  = x + y
+
+  Add ('Pos x)   ('Pos y)   = 'Pos (x + y)
+  Add ('Neg x)   ('Pos y)   = If (x <=? y)
+                                            ('Pos (y - x))
+                                            ('Neg (x - y))
+  Add ('Pos x)   ('Neg y)   = If (y <=? x)
+                                            ('Pos (x - y))
+                                            ('Neg (y - x))
+  Add ('Neg x)   ('Neg y)   = 'Neg (x + y)
+
+  Add ('Pos x)   (y :: Nat) = 'Pos (x + y)
+  Add ('Neg x)   (y :: Nat) = If (x <=? y)
+                                            ('Pos (y - x))
+                                            ('Neg (x - y))
+  Add (x :: Nat)  ('Pos y)  = 'Pos (x + y)
+  Add (x :: Nat)  ('Neg y)  = If (y <=? x)
+                                            ('Pos (x - y))
+                                            ('Neg (y - x))
+
+  Add (n1 ':% d1) (n2 ':% d2) = (Add (Mul n1 d2) (Mul n2 d1))
+                                            ':% (Mul d1 d2)
+  Add (n ':% d)   (y :: Nat)  = (Add n (Mul d y)) ':% d
+  Add (n ':% d)   ('Pos y)    = (Add n (Mul d y)) ':% d
+  Add (n ':% d)   ('Neg y)    = (Add n (Mul d ('Neg y))) ':% d
+  Add (x :: Nat)  (n ':% d)   = (Add (Mul d x) n) ':% d
+  Add ('Pos x)    (n ':% d)   = (Add (Mul d x) n) ':% d
+  Add ('Neg x)    (n ':% d)   = (Add (Mul d ('Neg x)) n) ':% d
+
+-- | The difference of two type-level numbers
+type family Sub (x :: k1) (y :: k2) :: SubK k1 k2 where
+  Sub (x :: Nat) (y :: Nat)  = x - y
+
+  Sub ('Pos x)   ('Pos y)   = Add x ('Neg y)
+  Sub ('Neg x)   ('Pos y)   = Add ('Neg x) ('Neg y)
+  Sub ('Pos x)   ('Neg y)   = Add ('Pos x) ('Pos y)
+  Sub ('Neg x)   ('Neg y)   = Add ('Neg x) ('Pos y)
+
+  Sub ('Pos x)   (y :: Nat) = Add ('Pos x) ('Neg y)
+  Sub ('Neg x)   (y :: Nat) = Add ('Neg x) ('Neg y)
+  Sub (x :: Nat)  ('Pos y)  = Add x ('Neg y)
+  Sub (x :: Nat)  ('Neg y)  = Add x ('Pos y)
+
+-- Denominators are wrapped in Pos here to force the products to evaluate
+-- as kind TInt instead of Nat.  Without this, it is possible to end up with,
+-- for example, @(14-15) :: Nat@ which does not produce a Nat and therefore
+-- causes typing to fail.
+  Sub (n1 ':% d1) (n2 ':% d2) = (Sub (Mul n1 ('Pos d2)) (Mul n2 ('Pos d1))) ':% (Mul d1 d2)
+  Sub (n ':% d)   (y :: Nat)  = Sub (n ':% d) (y ':% 1)
+  Sub (n ':% d)   ('Pos y)    = Sub (n ':% d) ('Pos y ':% 1)
+  Sub (n ':% d)   ('Neg y)    = Sub (n ':% d) ('Neg y ':% 1)
+  Sub (x :: Nat)  (n ':% d)   = Sub (x ':% 1) (n ':% d)
+  Sub ('Pos x)    (n ':% d)   = Sub ('Pos x ':% 1) (n ':% d)
+  Sub ('Neg x)    (n ':% d)   = Sub ('Neg x ':% 1) (n ':% d)
+
+-- | The product of two type-level numbers
+type family Mul (x :: k1) (y :: k2) :: MulK k1 k2 where
+  Mul (x :: Nat) (y :: Nat) = x * y
+
+  Mul ('Pos x)   ('Pos y)   = 'Pos (x * y)
+  Mul ('Neg x)   ('Pos y)   = 'Neg (x * y)
+  Mul ('Pos x)   ('Neg y)   = 'Neg (x * y)
+  Mul ('Neg x)   ('Neg y)   = 'Pos (x * y)
+
+  Mul ('Pos x)   (y :: Nat) = 'Pos (x * y)
+  Mul ('Neg x)   (y :: Nat) = 'Neg (x * y)
+  Mul (x :: Nat)  ('Pos y)  = 'Pos (x * y)
+  Mul (x :: Nat)  ('Neg y)  = 'Neg (x * y)
+
+  Mul (n1 ':% d1) (n2 ':% d2) = (Mul n1 n2) ':% (Mul d1 d2)
+  Mul (n ':% d)   (y :: Nat)  = (Mul n y) ':% d
+  Mul (n ':% d)   ('Pos y)    = (Mul n ('Pos y)) ':% d
+  Mul (n ':% d)   ('Neg y)    = (Mul n ('Neg y)) ':% d
+  Mul (x :: Nat)  (n ':% d)   = (Mul x n) ':% d
+  Mul ('Pos x)    (n ':% d)   = (Mul ('Pos x) n) ':% d
+  Mul ('Neg x)    (n ':% d)   = (Mul ('Neg x) n) ':% d