ghc-typelits-extra-0.2.5: Additional type-level operations on GHC.TypeLits.Nat

GHC.TypeLits.Extra

Description

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 #-}


Synopsis

Type-level operations on Nat

Ord

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

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 ... Source #

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

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

Type-level divMod

Variants

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

A variant of Div that rounds up instead of down

Logarithm

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

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 Source # Instance detailsMethodsnatSing2 :: SNatKn "GHC.TypeLits.Extra.CLog" (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 "GHC.TypeLits.Extra.FLog" x y Source # Instance detailsMethodsnatSing2 :: SNatKn "GHC.TypeLits.Extra.FLog" (KnownNat x, KnownNat y) => KnownNat2 "GHC.TypeLits.Extra.GCD" x y Source # Instance detailsMethodsnatSing2 :: SNatKn "GHC.TypeLits.Extra.GCD" (KnownNat x, KnownNat y) => KnownNat2 "GHC.TypeLits.Extra.LCM" x y Source # Instance detailsMethodsnatSing2 :: SNatKn "GHC.TypeLits.Extra.LCM" (KnownNat x, KnownNat y, FLog x y ~ CLog x y) => KnownNat2 "GHC.TypeLits.Extra.Log" x y Source # Instance detailsMethodsnatSing2 :: SNatKn "GHC.TypeLits.Extra.Log" (KnownNat x, KnownNat y) => KnownNat2 "GHC.TypeLits.Extra.Max" x y Source # Instance detailsMethodsnatSing2 :: SNatKn "GHC.TypeLits.Extra.Max" (KnownNat x, KnownNat y) => KnownNat2 "GHC.TypeLits.Extra.Min" x y Source # Instance detailsMethodsnatSing2 :: SNatKn "GHC.TypeLits.Extra.Min" (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 "GHC.TypeNats.Div" x y Source # Instance detailsMethodsnatSing2 :: SNatKn "GHC.TypeNats.Div" (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 "GHC.TypeNats.Mod" x y Source # Instance detailsMethodsnatSing2 :: SNatKn "GHC.TypeNats.Mod"