summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAdituV <>2018-06-13 03:01:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-06-13 03:01:00 (GMT)
commit811e0628c4d0c5fe6c35402a726b304002cf261e (patch)
tree3612c31d57609059d0d452384d3703b86323048e
version 0.1.0.00.1.0.0
-rw-r--r--CHANGELOG.md17
-rw-r--r--LICENSE29
-rw-r--r--README.md44
-rw-r--r--src/Data/TypeLits.hs81
-rw-r--r--src/Data/TypeNums.hs70
-rw-r--r--src/Data/TypeNums/Arithmetic.hs103
-rw-r--r--src/Data/TypeNums/Comparison.hs32
-rw-r--r--src/Data/TypeNums/Equality.hs26
-rw-r--r--src/Data/TypeNums/Ints.hs76
-rw-r--r--src/Data/TypeNums/Rats.hs81
-rw-r--r--test/Data/TypeNums/ArithmeticSpec.hs114
-rw-r--r--test/Data/TypeNums/IntsSpec.hs37
-rw-r--r--test/Data/TypeNums/RatsSpec.hs46
-rw-r--r--test/Spec.hs1
-rw-r--r--typenums.cabal62
15 files changed, 819 insertions, 0 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000..891d745
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,17 @@
+Change log
+==========
+
+typenums uses [PVP Versioning][1].
+The change log is available [on GitHub][2].
+
+0.1.0.0
+=======
+* Initial Haddock release
+* Defined type-level integers and rationals
+* Defined polykinded arithmetic over nats, ints and rats
+* Defined polykinded comparison over nats, ints and rats
+* Added Data.TypeLits module
+
+[1]: https://pvp.haskell.org
+[2]: https://github.com/adituv/typenums/releases
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..b1f8d69
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,29 @@
+BSD 3-Clause License
+
+Copyright (c) 2018, AdituV
+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 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 HOLDER 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/README.md b/README.md
new file mode 100644
index 0000000..a273ff1
--- /dev/null
+++ b/README.md
@@ -0,0 +1,44 @@
+# typenums
+
+[![Hackage](https://img.shields.io/hackage/v/typenums.svg)](https://hackage.haskell.org/package/typenums)
+[![Build status](https://secure.travis-ci.org/adituv/typenums.svg)](https://travis-ci.org/adituv/typenums)
+[![Windows build status](https://ci.appveyor.com/api/projects/status/github/adituv/typenums?branch=master&svg=true)](https://ci.appveyor.com/project/adituv/typenums)
+[![BSD3 license](https://img.shields.io/badge/license-BSD3-blue.svg)](https://github.com/adituv/typenums/blob/master/LICENSE)
+
+Type level numbers using existing Nat functionality. Uses kind-polymorphic
+typeclasses and type families to facilitate more general code compatible with
+existing code using type-level Naturals.
+
+## Usage
+Import either Data.TypeNums or Data.TypeLits instead of GHC.TypeLits. Some
+definitions conflict with GHC.TypeLits, so if you really must import it, use
+an explicit import list.
+
+This library is intended to be used in a kind-polymorphic way, such that
+a type-level integer parameter can be written as a natural, and a rational
+can be written as either of the other two. As an example:
+
+```haskell
+{-# LANGUAGE PolyKinds #-}
+
+data SomeType (n :: k) = SomeType
+
+useSomeType :: KnownInt n => SomeType n -> _
+useSomeType = -- ...
+```
+
+## Syntax
+* Positive integers are written as natural numbers, as before. Optionally
+ they can also be written as `Pos n`.
+* Negative integers are written as `Neg n`.
+* Ratios are written as `n :% d`, where `n` can be a natural number, `Pos n`,
+ or `Neg n`, and `d` is a natural number.
+
+Addition, subtraction and multiplication at type level are all given as infix
+operators with standard notation, and are compatible with any combination of
+the above types. Equality and comparison constraints are likewise available
+for any combination of the above types.
+
+N.B. The equality constraint conflicts with that in Data.Type.Equality. The
+(==) operator from Data.Type.Equality is re-exported as (==?) from both
+Data.TypeNums and Data.TypeLits.
diff --git a/src/Data/TypeLits.hs b/src/Data/TypeLits.hs
new file mode 100644
index 0000000..4f41051
--- /dev/null
+++ b/src/Data/TypeLits.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE Safe #-}
+
+{-|
+Module: Data.TypeLits
+Copyright: (c) 2018 Iris Ward
+License: BSD3
+Maintainer: aditu.venyhandottir@gmail.com
+Stability: experimental
+
+This module provides the same interface as "GHC.TypeLits", but with
+naming conflicts resolved in favour of this package. For example,
+'(<=)' resolves to the kind-polymorphic version from "Data.TypeNums".
+
+If you are only working with type-level numbers, import "Data.TypeNums"
+instead. This module is purely for convenience for those who want to
+use both functionality from "GHC.TypeLits" and functionality from
+"Data.TypeNums".
+-}
+
+module Data.TypeLits
+ (
+ -- * Type level numbers
+ -- ** Naturals
+ G.Nat
+ , G.KnownNat
+ , G.natVal
+ , G.natVal'
+ , G.SomeNat(..)
+ , G.someNatVal
+ , G.sameNat
+
+ -- ** Integers
+ , TInt(..)
+ , KnownInt
+ , intVal
+ , intVal'
+ -- ** Rationals
+ , Rat((:%))
+ , KnownRat
+ , ratVal
+ , ratVal'
+ -- * Type level numerical operations
+ -- ** Comparison
+ , type (==?)
+ , type (/=?)
+ , type (<=?)
+ , type (==)
+ , type (/=)
+ , type (<=)
+ , type (<)
+ , type (>=)
+ , type (>)
+ -- ** Arithmetic
+ , type (+)
+ , type (-)
+ , type (*)
+ , type (G.^)
+
+ -- * Symbols
+ , G.Symbol
+#if MIN_VERSION_base(4,10,0)
+ , G.AppendSymbol
+#endif
+ , G.CmpSymbol
+ , G.KnownSymbol
+ , G.symbolVal
+ , G.symbolVal'
+ , G.SomeSymbol(..)
+ , G.someSymbolVal
+ , G.sameSymbol
+
+ -- * User-defined type errors
+ , G.TypeError
+ , G.ErrorMessage(..)
+
+ ) where
+
+import Data.TypeNums
+import qualified GHC.TypeLits as G
diff --git a/src/Data/TypeNums.hs b/src/Data/TypeNums.hs
new file mode 100644
index 0000000..ec9d071
--- /dev/null
+++ b/src/Data/TypeNums.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE Safe #-}
+
+{-|
+Module: Data.TypeNums
+Copyright: (c) 2018 Iris Ward
+License: BSD3
+Maintainer: aditu.venyhandottir@gmail.com
+Stability: experimental
+
+This module provides a unified interface for natural numbers,
+signed integers, and rationals at the type level, in a way fully
+compatible with existing code using type-level naturals.
+
+Natural numbers are expressed as always, e.g. @5@. Negative integers
+are written as @Neg 3@. Ratios are written as @3 :% 2@.
+
+There are some naming conflicts between this module and "GHC.TypeLits",
+notably the comparison and arithmetic operators. This module reexports
+'Nat', 'KnownNat', 'natVal' and 'natVal'' so you may import just this
+module and not "GHC.TypeLits".
+
+If you wish to use other functionality from "GHC.TypeLits", this package
+also provides the module "Data.TypeLits" that includes (almost) full
+functionality from "GHC.TypeLits", but with the conflicts resolving in
+this packages favour.
+-}
+module Data.TypeNums
+ ( -- * Type level numbers
+ -- ** Naturals
+ G.Nat
+ , G.KnownNat
+ , G.natVal
+ , G.natVal'
+ , G.SomeNat(..)
+ , G.someNatVal
+ -- ** Integers
+ , TInt(..)
+ , KnownInt
+ , intVal
+ , intVal'
+ -- ** Rationals
+ , Rat((:%))
+ , KnownRat
+ , ratVal
+ , ratVal'
+ -- * Type level numerical operations
+ -- ** Comparisons
+ , type (==?)
+ , type (/=?)
+ , type (==)
+ , type (/=)
+ , type (<=?)
+ , type (<=)
+ , type (<)
+ , type (>=)
+ , type (>)
+ -- ** Arithmetic
+ , type (+)
+ , type (-)
+ , type (*)
+ ) where
+
+import Data.TypeNums.Arithmetic
+import Data.TypeNums.Comparison
+import Data.TypeNums.Equality
+import Data.TypeNums.Ints
+import Data.TypeNums.Rats
+
+import qualified GHC.TypeLits as G
diff --git a/src/Data/TypeNums/Arithmetic.hs b/src/Data/TypeNums/Arithmetic.hs
new file mode 100644
index 0000000..b45660e
--- /dev/null
+++ b/src/Data/TypeNums/Arithmetic.hs
@@ -0,0 +1,103 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+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
+
+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
+
+
+-- | 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
diff --git a/src/Data/TypeNums/Comparison.hs b/src/Data/TypeNums/Comparison.hs
new file mode 100644
index 0000000..8b91cd5
--- /dev/null
+++ b/src/Data/TypeNums/Comparison.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Data.TypeNums.Comparison where
+
+import Data.TypeNums.Arithmetic
+import Data.TypeNums.Ints
+import Data.TypeNums.Rats
+import GHC.TypeLits (Nat)
+
+import qualified GHC.TypeLits as G
+
+infix 4 <=?, <=, <, >=, >
+
+-- | Boolean comparison of two type-level numbers
+type family (a :: k1) <=? (b :: k2) :: Bool where
+ (a :: Nat) <=? (b :: Nat) = (G.<=?) a b
+ 0 <=? 'Neg 0 = 'True
+ 'Neg a <=? (b :: Nat) = 'True
+ 'Neg a <=? 'Neg b = (G.<=?) b a
+ (n1 ':% d1) <=? (n2 ':% d2) = (n1 * d1) <=? (n2 * d2)
+ a <=? (n ':% d) = (a * d) <=? n
+ (n ':% d) <=? b = n <=? (b * d)
+
+type (a :: k1) <= (b :: k2) = (a <=? b) ~ 'True
+type (a :: k1) < (b :: k2) = (b <=? a) ~ 'False
+type (a :: k1) >= (b :: k2) = (b <=? a) ~ 'True
+type (a :: k1) > (b :: k2) = (a <=? b) ~ 'False
diff --git a/src/Data/TypeNums/Equality.hs b/src/Data/TypeNums/Equality.hs
new file mode 100644
index 0000000..0f304e0
--- /dev/null
+++ b/src/Data/TypeNums/Equality.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.TypeNums.Equality where
+
+import Data.Type.Bool (Not)
+import qualified Data.Type.Equality as DTE
+
+infix 4 ==?, /=?, ==, /=
+
+-- | Boolean type-level equals. Useful for e.g.
+-- @'Data.Type.Bool.If' (x ==? 0)@
+type (a :: k) ==? (b :: k) = (DTE.==) a b
+
+-- | Boolean type-level not-equals.
+type (a :: k) /=? (b :: k) = Not ((DTE.==) a b)
+
+-- | Equality constraint, used as e.g. @(x == 3) => _@
+type (a :: k) == (b :: k) = ((DTE.==) a b) ~ 'True
+
+-- | Not-equal constraint
+type (a :: k) /= (b :: k) = ((DTE.==) a b) ~ 'False
diff --git a/src/Data/TypeNums/Ints.hs b/src/Data/TypeNums/Ints.hs
new file mode 100644
index 0000000..109fb40
--- /dev/null
+++ b/src/Data/TypeNums/Ints.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-|
+Module: Data.TypeNums.Ints
+Copyright: (c) 2018 Iris Ward
+License: BSD3
+Maintainer: aditu.venyhandottir@gmail.com
+Stability: experimental
+
+Type level integers can be used in the same way as type level naturals
+from "GHC.TypeLits", for example @3@. However, a minus sign is not
+recognised in this context, so a negative type-level integer is instead
+written as @'Neg' n@.
+-}
+module Data.TypeNums.Ints
+ ( -- * Construction
+ TInt(..)
+ -- * Linking type and value level
+ , KnownInt
+ , intVal
+ , intVal'
+ ) where
+
+import GHC.Exts (Proxy#, proxy#)
+import GHC.TypeLits (KnownNat, Nat, natVal')
+
+newtype SInt (n :: k) =
+ SInt Integer
+
+-- | (Kind) An integer that may be negative.
+data TInt = Pos Nat
+ | Neg Nat
+
+-- | This class gives the (value-level) integer associated with a type-level
+-- integer. There are instances of this class for every concrete natural:
+-- 0, 1, 2, etc. There are also instances of this class for every negated
+-- natural, such as @'Neg' 1@.
+class KnownInt (n :: k) where
+ intSing :: SInt n
+
+instance forall n. KnownNat n => KnownInt n where
+ intSing = SInt $! natVal' (proxy# @Nat @n)
+
+instance forall n. KnownNat n => KnownInt ('Pos n) where
+ intSing = SInt $! natVal' (proxy# @Nat @n)
+
+instance forall n. KnownNat n => KnownInt ('Neg n) where
+ intSing = SInt $! negate (natVal' (proxy# @Nat @n))
+
+-- | Get the value associated with a type-level integer
+intVal ::
+ forall n proxy. KnownInt n
+ => proxy n
+ -> Integer
+intVal _ =
+ case intSing :: SInt n of
+ SInt x -> x
+
+-- | Get the value associated with a type-level integer. The difference
+-- between this function and 'intVal' is that it takes a 'Proxy#' parameter,
+-- which has zero runtime representation and so is entirely free.
+intVal' ::
+ forall n. KnownInt n
+ => Proxy# n
+ -> Integer
+intVal' _ =
+ case intSing :: SInt n of
+ SInt x -> x
diff --git a/src/Data/TypeNums/Rats.hs b/src/Data/TypeNums/Rats.hs
new file mode 100644
index 0000000..c6212fd
--- /dev/null
+++ b/src/Data/TypeNums/Rats.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+{-|
+Module: Data.TypeNums.Rats
+Copyright: (c) 2018 Iris Ward
+License: BSD3
+Maintainer: aditu.venyhandottir@gmail.com
+Stability: experimental
+
+Type level rational numbers expressed as a ratio between a type-level integer
+and a type-level natural. For example @'Neg' 3 :% 2@.
+
+See also: "Data.TypeInts"
+-}
+module Data.TypeNums.Rats
+ ( Rat((:%))
+ , KnownRat
+ , ratVal
+ , ratVal'
+ ) where
+
+import Data.TypeNums.Equality (type (/=))
+import Data.TypeNums.Ints
+
+import Data.Ratio (Rational, (%))
+import GHC.Exts (Proxy#, proxy#)
+import GHC.TypeLits (ErrorMessage (..), KnownNat, Nat, TypeError, natVal')
+
+-- | Type constructor for a rational
+data Rat = forall k. k :% Nat
+
+newtype SRat r =
+ SRat Rational
+
+-- | This class gives the (value-level) rational associated with a type-level
+-- rational. There are instances of this class for every combination of a
+-- concrete integer and concrete natural.
+class KnownRat r where
+ ratSing :: SRat r
+
+instance {-# OVERLAPPING #-} (TypeError ('Text "Denominator must not equal 0")) =>
+ KnownRat (n ':% 0) where
+ ratSing = error "Unreachable"
+
+instance {-# OVERLAPS #-} forall (n :: k) d. (KnownInt n, KnownNat d, d /= 0) =>
+ KnownRat (n ':% d) where
+ ratSing = SRat $! intVal' (proxy# @k @n) % natVal' (proxy# @Nat @d)
+
+instance {-# OVERLAPPABLE #-} forall (n :: k). (KnownInt n) => KnownRat n where
+ ratSing = SRat $! intVal' (proxy# @k @n) % 1
+
+-- | Get the value associated with a type-level rational
+ratVal ::
+ forall proxy r. KnownRat r
+ => proxy r
+ -> Rational
+ratVal _ =
+ case ratSing :: SRat r of
+ SRat x -> x
+
+-- | Get the value associated with a type-level rational. The difference
+-- between this function and 'ratVal' is that it takes a 'Proxy#' parameter,
+-- which has zero runtime representation and so is entirely free.
+ratVal' ::
+ forall r. KnownRat r
+ => Proxy# r
+ -> Rational
+ratVal' _ =
+ case ratSing :: SRat r of
+ SRat x -> x
diff --git a/test/Data/TypeNums/ArithmeticSpec.hs b/test/Data/TypeNums/ArithmeticSpec.hs
new file mode 100644
index 0000000..0d4505c
--- /dev/null
+++ b/test/Data/TypeNums/ArithmeticSpec.hs
@@ -0,0 +1,114 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+module Data.TypeNums.ArithmeticSpec where
+
+import Data.TypeNums
+import Test.Hspec
+
+import Data.Proxy
+import Data.Ratio
+import GHC.Exts(Proxy#, proxy#)
+
+spec :: Spec
+spec = do
+ additionTests
+ subtractionTests
+ multiplicationTests
+
+additionTests :: Spec
+additionTests =
+ describe "addition" $ do
+ it "correctly adds two natural numbers" $
+ ratVal (Proxy @(3 + 5)) `shouldBe` 8
+ it "correctly adds a negative integer and a natural" $
+ ratVal (Proxy @((Neg 4) + 3)) `shouldBe` (-1)
+ it "correctly adds a natural and a negative integer" $
+ ratVal (Proxy @(8 + (Neg 7))) `shouldBe` 1
+ it "correctly adds two negative integers" $
+ ratVal (Proxy @((Neg 5) + (Neg 6))) `shouldBe` (-11)
+ it "correctly adds two positive integers" $
+ ratVal (Proxy @((Pos 5) + (Pos 6))) `shouldBe` 11
+ it "correctly adds a negative integer and a positive integer" $
+ ratVal (Proxy @((Neg 3) + (Pos 5))) `shouldBe` 2
+ it "correctly adds a positive integer and a negative integer" $
+ ratVal (Proxy @((Pos 7) + (Neg 8))) `shouldBe` (-1)
+ it "correctly adds two rationals" $
+ ratVal (Proxy @((2 ':% 3) + (5 ':% 7))) `shouldBe` (29 % 21)
+ it "correctly adds a rational with a natural" $
+ ratVal (Proxy @((2 ':% 3) + 2)) `shouldBe` (8 % 3)
+ it "correctly adds a natural with a rational" $
+ ratVal (Proxy @(2 + (2 ':% 3))) `shouldBe` (8 % 3)
+ it "correctly adds a rational with a negative integer" $
+ ratVal (Proxy @((2 ':% 3) + (Neg 2))) `shouldBe` ((-4) % 3)
+ it "correctly adds a negative integer with a rational" $
+ ratVal (Proxy @((Neg 2) + (2 ':% 3))) `shouldBe` ((-4) % 3)
+ it "correctly adds a rational with a positive integer" $
+ ratVal (Proxy @((2 ':% 3) + (Pos 2))) `shouldBe` 8 % 3
+ it "correctly adds a positive integer with a rational" $
+ ratVal (Proxy @((Pos 2) + (2 ':% 3))) `shouldBe` 8 % 3
+
+subtractionTests :: Spec
+subtractionTests =
+ describe "subtraction" $ do
+ it "correctly subtracts two natural numbers" $
+ ratVal (Proxy @(5 - 3)) `shouldBe` 2
+ it "correctly subtracts a negative integer and a natural" $
+ ratVal (Proxy @((Neg 4) - 3)) `shouldBe` (-7)
+ it "correctly subtracts a natural and a negative integer" $
+ ratVal (Proxy @(8 - (Neg 7))) `shouldBe` 15
+ it "correctly subtracts two negative integers" $
+ ratVal (Proxy @((Neg 5) - (Neg 6))) `shouldBe` 1
+ it "correctly subtracts two positive integers" $
+ ratVal (Proxy @((Pos 5) - (Pos 6))) `shouldBe` (-1)
+ it "correctly subtracts a negative integer and a positive integer" $
+ ratVal (Proxy @((Neg 3) - (Pos 5))) `shouldBe` (-8)
+ it "correctly subtracts a positive integer and a negative integer" $
+ ratVal (Proxy @((Pos 7) - (Neg 8))) `shouldBe` 15
+ it "correctly subtracts two rationals" $
+ ratVal (Proxy @((2 ':% 3) - (5 ':% 7))) `shouldBe` ((-1) % 21)
+ it "correctly subtracts a rational with a natural" $
+ ratVal (Proxy @((2 ':% 3) - 2)) `shouldBe` ((-4) % 3)
+ it "correctly subtracts a natural with a rational" $
+ ratVal (Proxy @(2 - (2 ':% 3))) `shouldBe` (4 % 3)
+ it "correctly subtracts a rational with a negative integer" $
+ ratVal (Proxy @((2 ':% 3) - (Neg 2))) `shouldBe` (8 % 3)
+ it "correctly subtracts a negative integer with a rational" $
+ ratVal (Proxy @((Neg 2) - (2 ':% 3))) `shouldBe` ((-8) % 3)
+ it "correctly subtracts a rational with a positive integer" $
+ ratVal (Proxy @((2 ':% 3) - (Pos 2))) `shouldBe` (-4) % 3
+ it "correctly subtracts a positive integer with a rational" $
+ ratVal (Proxy @((Pos 2) - (2 ':% 3))) `shouldBe` 4 % 3
+
+multiplicationTests :: Spec
+multiplicationTests =
+ describe "multiplication" $ do
+ it "correctly multiplies two natural numbers" $
+ ratVal (Proxy @(3 * 5)) `shouldBe` 15
+ it "correctly multiplies a negative integer and a natural" $
+ ratVal (Proxy @((Neg 4) * 3)) `shouldBe` (-12)
+ it "correctly multiplies a natural and a negative integer" $
+ ratVal (Proxy @(7 * (Neg 8))) `shouldBe` (-56)
+ it "correctly multiplies two negative integers" $
+ ratVal (Proxy @((Neg 5) * (Neg 6))) `shouldBe` 30
+ it "correctly multiplies two positive integers" $
+ ratVal (Proxy @((Pos 5) * (Pos 6))) `shouldBe` 30
+ it "correctly multiplies a negative integer and a positive integer" $
+ ratVal (Proxy @((Neg 4) * (Pos 3))) `shouldBe` (-12)
+ it "correctly multiplies a positive integer and a negative integer" $
+ ratVal (Proxy @((Pos 7) * (Neg 8))) `shouldBe` (-56)
+ it "correctly multiplies two rationals" $
+ ratVal (Proxy @((2 ':% 3) * (5 ':% 7))) `shouldBe` (10 % 21)
+ it "correctly multiplies a rational with a natural" $
+ ratVal (Proxy @((2 ':% 3) * 2)) `shouldBe` (4 % 3)
+ it "correctly multiplies a natural with a rational" $
+ ratVal (Proxy @(2 * (2 ':% 3))) `shouldBe` (4 % 3)
+ it "correctly multiplies a rational with a negative integer" $
+ ratVal (Proxy @((2 ':% 3) * (Neg 2))) `shouldBe` ((-4) % 3)
+ it "correctly multiplies a negative integer with a rational" $
+ ratVal (Proxy @((Neg 2) * (2 ':% 3))) `shouldBe` ((-4) % 3)
+ it "correctly multiplies a rational with a positive integer" $
+ ratVal (Proxy @((2 ':% 3) * (Pos 2))) `shouldBe` 4 % 3
+ it "correctly multiplies a positive integer with a rational" $
+ ratVal (Proxy @((Pos 2) * (2 ':% 3))) `shouldBe` 4 % 3
diff --git a/test/Data/TypeNums/IntsSpec.hs b/test/Data/TypeNums/IntsSpec.hs
new file mode 100644
index 0000000..5624ddd
--- /dev/null
+++ b/test/Data/TypeNums/IntsSpec.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+module Data.TypeNums.IntsSpec where
+
+import Data.TypeNums
+import Test.Hspec
+
+import Data.Proxy
+import Data.Ratio
+import GHC.Exts(Proxy#, proxy#)
+
+spec :: Spec
+spec = do
+ describe "intVal" $ do
+ it "correctly gets the value of a natural number" $
+ intVal (Proxy @3) `shouldBe` 3
+ it "correctly gets the value of zero" $
+ intVal (Proxy @0) `shouldBe` 0
+ it "correctly gets the value of Neg 0" $
+ intVal (Proxy @('Neg 0)) `shouldBe` 0
+ it "correctly gets the value of a negative integer" $
+ intVal (Proxy @('Neg 10)) `shouldBe` (-10)
+ it "correctly gets the value of a positive integer" $
+ intVal (Proxy @('Pos 53)) `shouldBe` 53
+ describe "intVal'" $ do
+ it "correctly gets the value of a natural number" $
+ intVal' (proxy# :: Proxy# 3) `shouldBe` 3
+ it "correctly gets the value of zero" $
+ intVal' (proxy# :: Proxy# 0) `shouldBe` 0
+ it "correctly gets the value of Neg 0" $
+ intVal' (proxy# :: Proxy# ('Neg 0)) `shouldBe` 0
+ it "correctly gets the value of a negative integer" $
+ intVal' (proxy# :: Proxy# ('Neg 10)) `shouldBe` (-10)
+ it "correctly gets the value of a positive integer" $
+ intVal' (proxy# :: Proxy# ('Pos 52)) `shouldBe` 52
diff --git a/test/Data/TypeNums/RatsSpec.hs b/test/Data/TypeNums/RatsSpec.hs
new file mode 100644
index 0000000..c34cac0
--- /dev/null
+++ b/test/Data/TypeNums/RatsSpec.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+module Data.TypeNums.RatsSpec where
+
+import Data.TypeNums
+import Test.Hspec
+
+import Data.Proxy
+import Data.Ratio
+import GHC.Exts(Proxy#, proxy#)
+
+spec :: Spec
+spec = do
+ describe "ratVal" $ do
+ it "correctly gets the value of a natural number" $
+ ratVal (Proxy @3) `shouldBe` 3
+ it "correctly gets the value of zero" $
+ ratVal (Proxy @0) `shouldBe` 0
+ it "correctly gets the value of Neg 0" $
+ ratVal (Proxy @('Neg 0)) `shouldBe` 0
+ it "correctly gets the value of a negative integer" $
+ ratVal (Proxy @('Neg 10)) `shouldBe` (-10)
+ it "correctly gets the value of a rational with natural numerator" $
+ ratVal (Proxy @(3 ':% 2)) `shouldBe` 3 % 2
+ it "correctly gets the value of a negative rational" $
+ ratVal (Proxy @('Neg 11 ':% 8)) `shouldBe` (-11) % 8
+ it "correctly gets the value of a positive rational" $
+ ratVal (Proxy @('Pos 16 ':% 25)) `shouldBe` 16 % 25
+ describe "ratVal'" $ do
+ it "correctly gets the value of a natural number" $
+ ratVal' (proxy# :: Proxy# 3) `shouldBe` 3
+ it "correctly gets the value of zero" $
+ ratVal' (proxy# :: Proxy# 0) `shouldBe` 0
+ it "correctly gets the value of Neg 0" $
+ ratVal' (proxy# :: Proxy# ('Neg 0)) `shouldBe` 0
+ it "correctly gets the value of a negative integer" $
+ ratVal' (proxy# :: Proxy# ('Neg 10)) `shouldBe` (-10)
+ it "correctly gets the value of a rational with natural numerator" $
+ ratVal' (proxy# :: Proxy# (3 ':% 2)) `shouldBe` 3 % 2
+ it "correctly gets the value of a negative rational" $
+ ratVal' (proxy# :: Proxy# ('Neg 11 ':% 8)) `shouldBe` (-11) % 8
+ it "correctly gets the value of a positive rational" $
+ ratVal' (proxy# :: Proxy# ('Pos 16 ':% 25)) `shouldBe` 16 % 25
+
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
index 0000000..a824f8c
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
diff --git a/typenums.cabal b/typenums.cabal
new file mode 100644
index 0000000..d4b72fb
--- /dev/null
+++ b/typenums.cabal
@@ -0,0 +1,62 @@
+-- This file has been generated from package.yaml by hpack version 0.28.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 630b28e361a7a94173b85febd9455330a3166fb13b165b22adc4709dc043b0b6
+
+name: typenums
+version: 0.1.0.0
+synopsis: Type level numbers using existing Nat functionality
+description: Type level numbers using existing Nat functionality. Uses kind-polymorphic typeclasses and type families to facilitate more general code compatible with existing code using type-level Naturals.
+category: Data
+homepage: https://github.com/adituv/typenums#readme
+bug-reports: https://github.com/adituv/typenums/issues
+author: AdituV
+maintainer: aditu.venyhandottir@gmail.com
+copyright: 2018 Iris Ward
+license: BSD3
+license-file: LICENSE
+tested-with: GHC == 8.0.1, GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3
+build-type: Simple
+cabal-version: 1.18
+extra-doc-files:
+ CHANGELOG.md
+ README.md
+
+source-repository head
+ type: git
+ location: https://github.com/adituv/typenums
+
+library
+ exposed-modules:
+ Data.TypeLits
+ Data.TypeNums
+ Data.TypeNums.Ints
+ Data.TypeNums.Rats
+ other-modules:
+ Data.TypeNums.Arithmetic
+ Data.TypeNums.Comparison
+ Data.TypeNums.Equality
+ hs-source-dirs:
+ src
+ ghc-options: -Wall
+ build-depends:
+ base >4.9 && <5.0
+ default-language: Haskell2010
+
+test-suite typenums-tests
+ type: exitcode-stdio-1.0
+ main-is: Spec.hs
+ other-modules:
+ Data.TypeNums.ArithmeticSpec
+ Data.TypeNums.IntsSpec
+ Data.TypeNums.RatsSpec
+ Paths_typenums
+ hs-source-dirs:
+ test
+ ghc-options: -Wall -Wno-all
+ build-depends:
+ base >4.9 && <5.0
+ , hspec
+ , typenums
+ default-language: Haskell2010