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

Copyright | (C) 2015-2016 University of Twente 2017-2018 QBayLogic B.V.
License | BSD2 (see the file LICENSE)
Maintainer | Christiaan Baaij <christiaan.baaij@gmail.com>
Safe Haskell | Trustworthy
Language | Haskell2010

Extensions

- Cpp
- UndecidableInstances
- MonoLocalBinds
- TemplateHaskell
- TemplateHaskellQuotes
- ScopedTypeVariables
- TypeFamilies
- GADTs
- GADTSyntax
- DataKinds
- TypeSynonymInstances
- FlexibleInstances
- ConstrainedClassMethods
- MultiParamTypeClasses
- MagicHash
- KindSignatures
- TypeOperators
- ExplicitNamespaces
- ExplicitForAll
- TypeApplications

GHC.TypeLits.Extra

Contents

- Type-level operations on `Nat`
  - Ord
  - Integral
    - Variants
  - Logarithm
    - Exact logarithm
- Orphan instances

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

pragma to the header of your file.

Synopsis

- type family Max (x :: Nat) (y :: Nat) :: Nat where ...
- type family Min (x :: Nat) (y :: Nat) :: Nat where ...
- type family Div (a :: Natural) (b :: Natural) :: Natural where ...
- type family Mod (a :: Natural) (b :: Natural) :: Natural where ...
- type DivMod (n :: Natural) (d :: Natural) = '(Div n d, Mod n d)
- type DivRU (n :: Natural) (d :: Natural) = Div (n + (d - 1)) d
- type family FLog (base :: Nat) (value :: Nat) :: Nat where ...
- type family CLog (base :: Nat) (value :: Nat) :: Nat where ...
- type family Log (base :: Nat) (value :: Nat) :: Nat where ...
- type family GCD (x :: Nat) (y :: Nat) :: Nat where ...
- type family LCM (x :: Nat) (y :: Nat) :: Nat where ...

# 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 :: Natural) (b :: Natural) :: Natural where ... infixl 7 Source #

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 :: Natural) (b :: Natural) :: Natural where ... infixl 7 Source #

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

Since: base-4.11.0.0

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

Type-level `divMod`

### Variants

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

A variant of `Div` that rounds up instead of down

## Logarithm

type family FLog (base :: Nat) (value :: Nat) :: Nat where ... Source #

Type-level equivalent of integerLogBase# .i.e. the exact integer equivalent to "``floor` (`logBase` base value)`"

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

Equations

FLog 2 1 = 0 |

type family CLog (base :: Nat) (value :: Nat) :: Nat where ... Source #

Type-level equivalent of the ceiling of integerLogBase# .i.e. the exact integer equivalent to "``ceiling` (`logBase` base value)`"

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 (base :: Nat) (value :: Nat) :: Nat where ... Source #

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

    FLog base value ~ CLog base value

Additionally, the following property holds for `Log`:

    (base ^ (Log base value)) ~ value

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