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

Copyright(C) 2015-2016 University of Twente
2017-2018 QBayLogic B.V.
LicenseBSD2 (see the file LICENSE)
MaintainerChristiaan Baaij <christiaan.baaij@gmail.com>
Safe HaskellTrustworthy
LanguageHaskell2010
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

Description

Additional type-level operations on Nat:

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

Type-level div

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

Equations

Div x 1 = x 

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

Type-level mod

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

Equations

Mod x 1 = 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 # 

Methods

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

(KnownNat x, KnownNat y, (<=) 1 y) => KnownNat2 "GHC.TypeLits.Extra.Div" x y Source # 

Methods

natSing2 :: SNatKn "GHC.TypeLits.Extra.Div" #

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

(KnownNat x, KnownNat y, (<=) 1 y) => KnownNat2 "GHC.TypeLits.Extra.Mod" x y Source # 

Methods

natSing2 :: SNatKn "GHC.TypeLits.Extra.Mod" #