type-level-tf-0.2.1: Type-level programming library (type families)

Portabilitynon-portable (MPTC, non-standard instances)
Stabilityexperimental
Maintaineralfonso.acosta@gmail.com

Data.TypeLevel.Num.Ops

Contents

Description

Type-level numerical operations and its value-level reflection functions.

Synopsis

Successor/Predecessor

type family Succ n Source

Successor type-level relation. Succ x y establishes that succ x = y. Assoc notes: Cannot avoid malformed types

succ :: x -> Succ xSource

value-level reflection function for the Succ type-level relation

type family Pred n Source

pred :: x -> Pred xSource

Addition/Subtraction

type family Add m n :: *Source

(+) :: x -> y -> Add x ySource

value-level reflection function for the Add type-level relation

type family Sub x y Source

(-) :: x -> y -> Sub x ySource

value-level reflection function for the Sub type-level relation

Multiplication/Division

type family Mul m n Source

(*) :: x -> y -> Mul x ySource

value-level reflection function for the multiplication type-level relation

type family Div x y Source

div :: x -> y -> Div x ySource

value-level reflection function for the Div type-level relation

type family Mod x y Source

mod :: x -> y -> Mod x ySource

value-level reflection function for the Mod type-level relation

class (Pos d, Nat x) => IsDivBy d x Source

Is-divisible-by type-level assertion. e.g IsDivBy d x establishes that x is divisible by d.

Instances

(Mod x d ~ D0, Pos d, Nat x) => IsDivBy d x 

isDivBy :: IsDivBy d x => d -> x -> ()Source

value-level reflection function for IsDivBy

Special efficiency cases

type family Mul10 n Source

Multiplication by 10 type-level relation (based on DivMod10). Mul10 x y establishes that 10 * x = y.

mul10 :: x -> Mul10 xSource

value-level reflection function for Mul10

type family Div10 m Source

div10 :: x -> Div10 xSource

type family DivMod10 n Source

divMod10 :: x -> (Div10 x, Mod10 x)Source

Exponientiation/Logarithm

type family ExpBase b e Source

(^) :: b -> e -> ExpBase b eSource

value-level reflection function for the ExpBase type-level relation

Special efficiency cases

type family Exp10 x Source

Assert that a number (x) can be expressed as the power of another one (b) (i.e. the fractional part of log_base_b x = 0, or, in a different way, exists y . b^y = x).

class (Pos b, b :>=: D2, Pos x) => IsPowOf b x instance (Trich x b cmp, IsPowOf' b x cmp) => IsPowOf b x class (Pos b, b :>=: D2, Pos x) => IsPowOf' b x cmp

exp10 :: x -> Exp10 xSource

value-level reflection function for Exp10

type family Log10 x Source

Base-10 logarithm type-level relation Note it is not relational (cannot be used to express Exponentation to 10) However, it works with any positive numeral (not just powers of 10)

log10 :: x -> Log10 xSource

value-level reflection function for Log10

Comparison assertions

General comparison assertion

type family Trich x y Source

Trichotomy type-level relation. 'Trich x y r' establishes the relation (r) between x and y. The obtained relation (r) Can be LT (if x is lower than y), EQ (if x equals y) or GT (if x is greater than y)

trich :: x -> y -> Trich x ySource

value-level reflection function for the comparison type-level assertion

Type-level values denoting comparison results

data LT Source

Lower than

data EQ Source

Equal

data GT Source

Greater than

type family OrderingEq o1 o2 Source

type family NatEq x y Source

Equality abbreviated type-level assertion

Abbreviated comparison assertions

type family x :>: y Source

Greater-than abbreviated type-level assertion

type family x :<: y Source

Lower-than abbreviated type-level assertion

type family x :>=: y Source

Greater-than or equal abbreviated type-level assertion

type family x :<=: y Source

Less-than or equal abbreviated type-level assertion

(>) :: x -> y -> x :>: ySource

value-level reflection function for >

(<) :: x -> y -> x :<: ySource

value-level reflection function for >

(>=) :: x -> y -> x :>=: ySource

value-level reflection function for >=

(<=) :: x -> y -> x :<=: ySource

value-level reflection function for >=

Maximum/Minimum

type family Max x y Source

max :: x -> y -> Max x ySource

value-level reflection function for the maximum type-level relation

type family Min x y Source

min :: x -> y -> Min x ySource

value-level reflection function for the minimum type-level relation

Greatest Common Divisor

type family GCD x y Source

Greatest Common Divisor type-level relation

gcd :: x -> y -> GCD x ySource

value-level reflection function for the GCD type-level relation