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

Copyright(C) 2015-2016 University of Twente
LicenseBSD2 (see the file LICENSE)
MaintainerChristiaan Baaij <christiaan.baaij@gmail.com>
Safe HaskellTrustworthy
LanguageHaskell2010
Extensions
  • 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 0 y = y 
Max x 0 = x 
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 0 y = 0 
Min x 0 = 0 
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 

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 

Orphan instances

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

Associated Types

type KnownNatF2 ("GHC.TypeLits.Extra.CLog" :: Symbol) :: (~>) Nat ((~>) Nat Nat) #

Methods

natSing2 :: SNatKn ((Nat @@ Nat) ((Nat @@ (Nat ~> Nat)) (KnownNatF2 "GHC.TypeLits.Extra.CLog") x) y) #

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

Associated Types

type KnownNatF2 ("GHC.TypeLits.Extra.Div" :: Symbol) :: (~>) Nat ((~>) Nat Nat) #

Methods

natSing2 :: SNatKn ((Nat @@ Nat) ((Nat @@ (Nat ~> Nat)) (KnownNatF2 "GHC.TypeLits.Extra.Div") x) y) #

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

Associated Types

type KnownNatF2 ("GHC.TypeLits.Extra.FLog" :: Symbol) :: (~>) Nat ((~>) Nat Nat) #

Methods

natSing2 :: SNatKn ((Nat @@ Nat) ((Nat @@ (Nat ~> Nat)) (KnownNatF2 "GHC.TypeLits.Extra.FLog") x) y) #

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

Associated Types

type KnownNatF2 ("GHC.TypeLits.Extra.GCD" :: Symbol) :: (~>) Nat ((~>) Nat Nat) #

Methods

natSing2 :: SNatKn ((Nat @@ Nat) ((Nat @@ (Nat ~> Nat)) (KnownNatF2 "GHC.TypeLits.Extra.GCD") x) y) #

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

Associated Types

type KnownNatF2 ("GHC.TypeLits.Extra.LCM" :: Symbol) :: (~>) Nat ((~>) Nat Nat) #

Methods

natSing2 :: SNatKn ((Nat @@ Nat) ((Nat @@ (Nat ~> Nat)) (KnownNatF2 "GHC.TypeLits.Extra.LCM") x) y) #

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

Associated Types

type KnownNatF2 ("GHC.TypeLits.Extra.Log" :: Symbol) :: (~>) Nat ((~>) Nat Nat) #

Methods

natSing2 :: SNatKn ((Nat @@ Nat) ((Nat @@ (Nat ~> Nat)) (KnownNatF2 "GHC.TypeLits.Extra.Log") x) y) #

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

Associated Types

type KnownNatF2 ("GHC.TypeLits.Extra.Max" :: Symbol) :: (~>) Nat ((~>) Nat Nat) #

Methods

natSing2 :: SNatKn ((Nat @@ Nat) ((Nat @@ (Nat ~> Nat)) (KnownNatF2 "GHC.TypeLits.Extra.Max") x) y) #

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

Associated Types

type KnownNatF2 ("GHC.TypeLits.Extra.Min" :: Symbol) :: (~>) Nat ((~>) Nat Nat) #

Methods

natSing2 :: SNatKn ((Nat @@ Nat) ((Nat @@ (Nat ~> Nat)) (KnownNatF2 "GHC.TypeLits.Extra.Min") x) y) #

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

Associated Types

type KnownNatF2 ("GHC.TypeLits.Extra.Mod" :: Symbol) :: (~>) Nat ((~>) Nat Nat) #

Methods

natSing2 :: SNatKn ((Nat @@ Nat) ((Nat @@ (Nat ~> Nat)) (KnownNatF2 "GHC.TypeLits.Extra.Mod") x) y) #