GHC.TypeLits.Extra

Additional type-level operations on Nat:

• Max: type-level max
• Min: type-level min
• Div: type-level div
• Mod: type-level mod
• FLog: type-level equivalent of integerLogBase# .i.e. the exact integer equivalent to "floor (logBase x y)"
• CLog: type-level equivalent of the ceiling of integerLogBase# .i.e. the exact integer equivalent to "ceiling (logBase x y)"
• Log: type-level equivalent of integerLogBase# where the operation only reduces when "floor (logBase b x) ~ ceiling (logBase b x)"
• GCD: a type-level gcd
• LCM: a type-level lcm

A custom solver for the above operations defined is defined in GHC.TypeLits.Extra.Solver as a GHC type-checker plugin. To use the plugin, add the

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}

pragma to the header of your file.

Type-level operations on Nat

Ord

type family Max (x :: Nat) (y :: Nat) :: Nat where ...

Type-level max

Equations

Max n n = n

Max x y = If (x <=? y) y x

type family Min (x :: Nat) (y :: Nat) :: Nat where ...

Type-level min

Equations

Min n n = n

Min x y = If (x <=? y) x y

Integral

type family Div (a :: Nat) (b :: Nat) :: Nat where ... infixl 7

Division (round down) of natural numbers. Div x 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

type family Mod (a :: Nat) (b :: Nat) :: Nat where ... infixl 7

Modulus of natural numbers. Mod x 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

type DivMod n d = '(Div n d, Mod n d)

Type-level divMod

Variants

type DivRU n d = Div (n + (d - 1)) d

A variant of Div that rounds up instead of down

Logarithm

type family FLog (x :: Nat) (y :: Nat) :: Nat where ...

Type-level equivalent of integerLogBase# .i.e. the exact integer equivalent to "floor (logBase x y)"

Note that additional equations are provided by the type-checker plugin solver GHC.TypeLits.Extra.Solver.

Equations

FLog 2 1 = 0

type family CLog (x :: Nat) (y :: Nat) :: Nat where ...

Type-level equivalent of the ceiling of integerLogBase# .i.e. the exact integer equivalent to "ceiling (logBase x y)"

Note that additional equations are provided by the type-checker plugin solver GHC.TypeLits.Extra.Solver.

Equations

CLog 2 1 = 0

Exact logarithm

type family Log (x :: Nat) (y :: Nat) :: Nat where ...

Type-level equivalent of integerLogBase# where the operation only reduces when:

FLog b x ~ CLog b x

Additionally, the following property holds for Log:

(b ^ (Log b x)) ~ x

Note that additional equations are provided by the type-checker plugin solver GHC.TypeLits.Extra.Solver.

Equations

Log 2 1 = 0

type family GCD (x :: Nat) (y :: Nat) :: Nat where ...

Type-level greatest common denominator (GCD).

Note that additional equations are provided by the type-checker plugin solver GHC.TypeLits.Extra.Solver.

Equations

GCD 0 x = x

GCD x 0 = x

GCD 1 x = 1

GCD x 1 = 1

GCD x x = x

type family LCM (x :: Nat) (y :: Nat) :: Nat where ...

Type-level least common multiple (LCM).

Note that additional equations are provided by the type-checker plugin solver GHC.TypeLits.Extra.Solver.

Equations

LCM 0 x = 0

LCM x 0 = 0

LCM 1 x = x

LCM x 1 = x

LCM x x = x

Orphan instances

(KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 "GHC.TypeLits.Extra.CLog" x y

Methods

natSing2 :: SNatKn "GHC.TypeLits.Extra.CLog"

(KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 "GHC.TypeLits.Extra.FLog" x y

Methods

natSing2 :: SNatKn "GHC.TypeLits.Extra.FLog"

(KnownNat x, KnownNat y) => KnownNat2 "GHC.TypeLits.Extra.GCD" x y

Methods

natSing2 :: SNatKn "GHC.TypeLits.Extra.GCD"

(KnownNat x, KnownNat y) => KnownNat2 "GHC.TypeLits.Extra.LCM" x y

Methods

natSing2 :: SNatKn "GHC.TypeLits.Extra.LCM"

(KnownNat x, KnownNat y, FLog x y ~ CLog x y) => KnownNat2 "GHC.TypeLits.Extra.Log" x y

Methods

natSing2 :: SNatKn "GHC.TypeLits.Extra.Log"

(KnownNat x, KnownNat y) => KnownNat2 "GHC.TypeLits.Extra.Max" x y

Methods

natSing2 :: SNatKn "GHC.TypeLits.Extra.Max"

(KnownNat x, KnownNat y) => KnownNat2 "GHC.TypeLits.Extra.Min" x y

Methods

natSing2 :: SNatKn "GHC.TypeLits.Extra.Min"