| Copyright | (c) 2018-2021 Iris Ward |
|---|---|
| License | BSD3 |
| Maintainer | aditu.venyhandottir@gmail.com |
| Stability | experimental |
| Safe Haskell | Safe |
| Language | Haskell2010 |
Data.TypeNums
Description
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.
Synopsis
- data Nat
- class KnownNat (n :: Nat)
- natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Integer
- natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Integer
- data SomeNat = KnownNat n => SomeNat (Proxy n)
- someNatVal :: Integer -> Maybe SomeNat
- data TInt
- class KnownInt (n :: k)
- intVal :: forall n proxy. KnownInt n => proxy n -> Integer
- intVal' :: forall n. KnownInt n => Proxy# n -> Integer
- data SomeInt = forall n.KnownInt n => SomeInt (Proxy n)
- someIntVal :: Integer -> SomeInt
- data Rat = forall k. k :% Nat
- class KnownRat r
- ratVal :: forall proxy r. KnownRat r => proxy r -> Rational
- ratVal' :: forall r. KnownRat r => Proxy# r -> Rational
- data SomeRat = forall r.KnownRat r => SomeRat (Proxy r)
- someRatVal :: Rational -> SomeRat
- type (==?) (a :: k) (b :: k) = (==) a b
- type (/=?) (a :: k) (b :: k) = Not ((==) a b)
- type (==) (a :: k) (b :: k) = (==) a b ~ 'True
- type (/=) (a :: k) (b :: k) = (==) a b ~ 'False
- type family (a :: k1) <=? (b :: k2) :: Bool where ...
- 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
- type (+) a b = Add a b
- type (-) a b = Sub a b
- type * a b = Mul a b
Type level numbers
Naturals
(Kind) This is the kind of type-level natural numbers.
This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.
Since: base-4.7.0.0
Minimal complete definition
natSing
This type represents unknown type-level natural numbers.
Since: base-4.10.0.0
someNatVal :: Integer -> Maybe SomeNat #
Convert an integer into an unknown type-level natural.
Since: base-4.7.0.0
Integers
(Kind) An integer that may be negative.
class KnownInt (n :: k) Source #
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
Minimal complete definition
intSing
intVal :: forall n proxy. KnownInt n => proxy n -> Integer Source #
Get the value associated with a type-level integer
This type represents unknown type-level integers.
Since: 0.1.1
someIntVal :: Integer -> SomeInt Source #
Convert an integer into an unknown type-level integer.
Since: 0.1.1
Rationals
Type constructor for a rational
Instances
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.
Minimal complete definition
ratSing
Instances
| KnownInt n => KnownRat (n :: k) Source # | |
Defined in Data.TypeNums.Rats Methods ratSing :: SRat n | |
| (KnownInt n, KnownNat d, d /= 0) => KnownRat (n :% d :: Rat) Source # | |
Defined in Data.TypeNums.Rats | |
| (TypeError ('Text "Denominator must not equal 0") :: Constraint) => KnownRat (n :% 0 :: Rat) Source # | |
Defined in Data.TypeNums.Rats | |
ratVal :: forall proxy r. KnownRat r => proxy r -> Rational Source #
Get the value associated with a type-level rational
This type represents unknown type-level integers.
Since: 0.1.1
someRatVal :: Rational -> SomeRat Source #
Convert a rational into an unknown type-level rational.
Since: 0.1.1
Type level numerical operations
Comparisons
type (==?) (a :: k) (b :: k) = (==) a b infix 4 Source #
Boolean type-level equals. Useful for e.g.
If (x ==? 0)
type (==) (a :: k) (b :: k) = (==) a b ~ 'True infix 4 Source #
Equality constraint, used as e.g. (x == 3) => _
type family (a :: k1) <=? (b :: k2) :: Bool where ... infix 4 Source #
Boolean comparison of two type-level numbers
Equations
| (a :: Nat) <=? (b :: Nat) = (<=?) a b | |
| ('Pos a) <=? ('Pos b) = (<=?) a b | |
| ('Neg _) <=? ('Pos _) = 'True | |
| ('Pos 0) <=? ('Neg 0) = 'True | |
| ('Pos _) <=? ('Neg _) = 'False | |
| ('Pos a) <=? b = a <=? b | |
| a <=? ('Pos b) = a <=? b | |
| 0 <=? ('Neg 0) = 'True | |
| (a :: Nat) <=? ('Neg _) = 'False | |
| ('Neg a) <=? (b :: Nat) = 'True | |
| ('Neg a) <=? ('Neg b) = (<=?) b a | |
| (n :% 0) <=? _ = TypeError ('Text "Denominator must not equal 0") | |
| _ <=? (n :% 0) = TypeError ('Text "Denominator must not equal 0") | |
| (n1 :% d1) <=? (n2 :% d2) = (n1 * d2) <=? (n2 * d1) | |
| a <=? (n :% d) = (a * d) <=? n | |
| (n :% d) <=? b = n <=? (b * d) |
Arithmetic
type * a b = Mul a b infixl 7 Source #
The product of two type-level numbers.
Due to changes in GHC 8.6, using this operator infix and unqualified requires the NoStarIsType language extension to be active. See the GHC 8.6.x migration guide for details: https://ghc.haskell.org/trac/ghc/wiki/Migration/8.6