typenums-0.1.1: Type level numbers using existing Nat functionality

Copyright(c) 2018 Iris Ward
LicenseBSD3
Maintaineraditu.venyhandottir@gmail.com
Stabilityexperimental
Safe HaskellSafe
LanguageHaskell2010

Data.TypeNums

Contents

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

Type level numbers

Naturals

data Nat :: * #

(Kind) This is the kind of type-level natural numbers.

Instances

KnownNat n => KnownInt Nat n Source # 

Methods

intSing :: SInt n n

type (==) Nat a b 
type (==) Nat a b = EqNat a b

class KnownNat (n :: Nat) #

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: 4.7.0.0

Minimal complete definition

natSing

natVal :: KnownNat n => proxy n -> Integer #

Since: 4.7.0.0

natVal' :: KnownNat n => Proxy# Nat n -> Integer #

Since: 4.8.0.0

data SomeNat :: * where #

This type represents unknown type-level natural numbers.

Since: 4.10.0.0

Constructors

SomeNat :: SomeNat 

Instances

someNatVal :: Integer -> Maybe SomeNat #

Convert an integer into an unknown type-level natural.

Since: 4.7.0.0

Integers

data TInt Source #

(Kind) An integer that may be negative.

Constructors

Pos Nat 
Neg Nat 

Instances

KnownNat n => KnownInt TInt (Pos n) Source # 

Methods

intSing :: SInt (Pos n) n

KnownNat n => KnownInt TInt (Neg n) Source # 

Methods

intSing :: SInt (Neg n) n

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

Instances

KnownNat n => KnownInt Nat n Source # 

Methods

intSing :: SInt n n

KnownNat n => KnownInt TInt (Pos n) Source # 

Methods

intSing :: SInt (Pos n) n

KnownNat n => KnownInt TInt (Neg n) Source # 

Methods

intSing :: SInt (Neg n) n

intVal :: forall n proxy. KnownInt n => proxy n -> Integer Source #

Get the value associated with a type-level integer

intVal' :: forall n. KnownInt n => Proxy# n -> Integer Source #

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.

data SomeInt Source #

This type represents unknown type-level integers.

Since: 0.1.1

Constructors

KnownInt n => SomeInt (Proxy n) 

someIntVal :: Integer -> SomeInt Source #

Convert an integer into an unknown type-level integer.

Since: 0.1.1

Rationals

data Rat Source #

Type constructor for a rational

Constructors

k :% Nat 

Instances

(KnownInt k n, KnownNat d, (/=) Nat d 0) => KnownRat Rat ((:%) k n d) Source # 

Methods

ratSing :: SRat ((k :% n) d) r

TypeError Constraint (Text "Denominator must not equal 0") => KnownRat Rat ((:%) k n 0) Source # 

Methods

ratSing :: SRat ((k :% n) 0) r

class KnownRat r Source #

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 k n => KnownRat k n Source # 

Methods

ratSing :: SRat n r

(KnownInt k n, KnownNat d, (/=) Nat d 0) => KnownRat Rat ((:%) k n d) Source # 

Methods

ratSing :: SRat ((k :% n) d) r

TypeError Constraint (Text "Denominator must not equal 0") => KnownRat Rat ((:%) k n 0) Source # 

Methods

ratSing :: SRat ((k :% n) 0) r

ratVal :: forall proxy r. KnownRat r => proxy r -> Rational Source #

Get the value associated with a type-level rational

ratVal' :: forall r. KnownRat r => Proxy# r -> Rational Source #

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.

data SomeRat Source #

This type represents unknown type-level integers.

Since: 0.1.1

Constructors

KnownRat r => SomeRat (Proxy r) 

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) = Not ((==) a b) infix 4 Source #

Boolean type-level not-equals.

type (==) (a :: k) (b :: k) = (==) a b ~ True infix 4 Source #

Equality constraint, used as e.g. (x == 3) => _

type (/=) (a :: k) (b :: k) = (==) a b ~ False infix 4 Source #

Not-equal constraint

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 
0 <=? (Neg 0) = True 
(Neg a) <=? (b :: Nat) = True 
(Neg a) <=? (Neg b) = (<=?) 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 infix 4 Source #

type (<) (a :: k1) (b :: k2) = (b <=? a) ~ False infix 4 Source #

type (>=) (a :: k1) (b :: k2) = (b <=? a) ~ True infix 4 Source #

type (>) (a :: k1) (b :: k2) = (a <=? b) ~ False infix 4 Source #

Arithmetic

type family (x :: k1) + (y :: k2) :: ArithK k1 k2 where ... infixl 6 Source #

The sum of two type-level numbers

Equations

(x :: Nat) + (y :: Nat) = (+) x y 
(Pos x) + (Pos y) = Pos ((+) x y) 
(Neg x) + (Pos y) = If ((<=?) x y) (Pos ((-) y x)) (Neg ((-) x y)) 
(Pos x) + (Neg y) = If ((<=?) y x) (Pos ((-) x y)) (Neg ((-) y x)) 
(Neg x) + (Neg y) = Neg ((+) x y) 
(Pos x) + (y :: Nat) = Pos ((+) x y) 
(Neg x) + (y :: Nat) = If ((<=?) x y) (Pos ((-) y x)) (Neg ((-) x y)) 
(x :: Nat) + (Pos y) = Pos ((+) x y) 
(x :: Nat) + (Neg y) = If ((<=?) y x) (Pos ((-) x y)) (Neg ((-) 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 ... infixl 6 Source #

Equations

(x :: Nat) - (y :: Nat) = (-) 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 
(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 family (x :: k1) * (y :: k2) :: ArithK k1 k2 where ... infixl 7 Source #

The product of two type-level numbers

Equations

(x :: Nat) * (y :: Nat) = * x y 
(Pos x) * (Pos y) = Pos (* x y) 
(Neg x) * (Pos y) = Neg (* x y) 
(Pos x) * (Neg y) = Neg (* x y) 
(Neg x) * (Neg y) = Pos (* x y) 
(Neg x) * (y :: Nat) = Neg (* x y) 
(Pos x) * (y :: Nat) = Pos (* x y) 
(x :: Nat) * (Neg y) = Neg (* x y) 
(x :: Nat) * (Pos y) = Pos (* x y) 
(n1 :% d1) * (n2 :% d2) = (n1 * n2) :% (d1 * d2) 
(n :% d) * y = (n * y) :% d 
x * (n :% d) = (x * n) :% d