Safe Haskell	Safe-Inferred
Language	GHC2021

KindRational

Contents

Rational
SRational
Proofs
Show
Arithmethic
Decimals
Comparisons
Defunctionalization

Description

This module provides a type-level representation for term-level Rationals. This type-level representation is also named Rational, So import this module qualified to avoid name conflicts.

import KindRational qualified as KR

The implementation details are similar to the ones for type-level Naturals as of base-4.18 and singletons-base-3.1.1, and they will continue to evolve together with base and singletons-base, trying to more or less follow their API.

Synopsis

data Rational
type (:%) (n :: Integer) (d :: Natural) = n ':% d :: Rational
type FromNatural (n :: Natural) = FromNatural n :% 1 :: Rational
fromNatural :: Natural -> Rational
sFromNatural :: Sing (n :: Natural) -> SRational (FromNatural n)
type FromInteger (i :: Integer) = Normalized i :% 1 :: Rational
fromInteger :: Integer -> Rational
sFromInteger :: SInteger n -> SRational (FromInteger n)
type Num (r :: Rational) = Num_ (Reduced r) :: Integer
sNum :: SRational r -> SInteger (Num r)
type Den (r :: Rational) = Den_ (Reduced r) :: Natural
sDen :: SRational r -> Sing (Den r :: Natural)
class (SingKind kn, SingKind kd) => ToRational kn kd where
- type (n :: kn) % (d :: kd) :: Rational
- mkRational :: Demote kn -> Demote kd -> Maybe Rational
sMkRational :: forall kn kd n d. ToRational kn kd => Sing (n :: kn) -> Sing (d :: kd) -> Maybe (SRational (n % d))
(%%) :: forall kn kd n d. (ToRational kn kd, KnownRational (n % d)) => Sing (n :: kn) -> Sing (d :: kd) -> SRational (n % d)
(%) :: forall kn kd. (ToRational kn kd, HasCallStack) => Demote kn -> Demote kd -> Rational
type KnownRational (r :: Rational) = (KnownRational_ r, Reduced r ~ r, KnownInteger (Num r), KnownNat (Den r))
type Reduced (r :: Rational) = Reduced_ r (Reduce r) :: Rational
rationalSing :: KnownRational r => SRational r
rationalVal :: forall r proxy. KnownRational r => proxy r -> Rational
withKnownRational :: forall r rep (x :: TYPE rep). SRational r -> (KnownRational r => x) -> x
data SomeRational = forall n.KnownRational n => SomeRational (Proxy n)
someRationalVal :: Rational -> SomeRational
data SRational (r :: Rational)
pattern SRational :: forall r. () => KnownRational r => SRational r
fromSRational :: SRational r -> Rational
withSomeSRational :: forall rep (x :: TYPE rep). Rational -> (forall r. SRational r -> x) -> x
sNegateRefl :: Sing (r :: Rational) -> r :~: Negate (Negate r)
type ShowLit (r :: Rational) = ShowsLit r "" :: Symbol
showLit :: Rational -> String
sShowLit :: SRational r -> Sing (ShowLit r)
type ShowsLit (r :: Rational) (s :: Symbol) = ShowsPrecLit 0 r s :: Symbol
showsLit :: Rational -> ShowS
sShowsLit :: SRational r -> Sing (s :: Symbol) -> Sing (ShowsLit r s)
type ShowsPrecLit (p :: Natural) (r :: Rational) (s :: Symbol) = ShowParen (p >= AppPrec1) (ShowsLitSym1 (Num r) .@#@$$$ (ShowStringSym1 " :% " .@#@$$$ ShowsSym1 (Den r))) s :: Symbol
showsPrecLit :: Int -> Rational -> ShowS
sShowsPrecLit :: Sing (p :: Natural) -> SRational r -> Sing (s :: Symbol) -> Sing (ShowsPrecLit p r s)
readPrecLit :: ReadPrec Rational
type Signum (r :: Rational) = Signum (Num r) :: Integer
sSignum :: Sing (r :: Rational) -> SInteger (Signum r)
sSignumRefl :: SRational r -> (Signum r :~: Signum (Num r), Signum r :~: Num (Signum r))
type Recip (a :: Rational) = Den a % Num a :: Rational
sRecip :: (Z :% 1) < Abs r => SRational r -> SRational (Recip r)
sRecip' :: forall r. SRational r -> Maybe (SRational (Recip r))
type Div (r :: Round) (a :: Rational) = Div_ r (Reduce a) :: Integer
sDiv :: SRound r -> SRational a -> SInteger (Div r a)
div :: Round -> Rational -> Integer
type Rem (r :: Round) (a :: Rational) = Snd (DivRem r a) :: Rational
rem :: Round -> Rational -> Rational
sRem :: SRound r -> SRational a -> SRational (Rem r a)
type DivRem (r :: Round) (a :: Rational) = DivRem_ r (Reduce a) :: (Integer, Rational)
divRem :: Round -> Rational -> (Integer, Rational)
sDivRem :: SRound r -> SRational a -> (SInteger (Div r a), SRational (Rem r a))
data Round
- = RoundUp
- | RoundDown
- | RoundZero
- | RoundAway
- | RoundHalfUp
- | RoundHalfDown
- | RoundHalfZero
- | RoundHalfAway
- | RoundHalfEven
- | RoundHalfOdd
data SRound (a :: Round) where
- SRoundUp :: SRound 'RoundUp
- SRoundDown :: SRound 'RoundDown
- SRoundZero :: SRound 'RoundZero
- SRoundAway :: SRound 'RoundAway
- SRoundHalfUp :: SRound 'RoundHalfUp
- SRoundHalfDown :: SRound 'RoundHalfDown
- SRoundHalfZero :: SRound 'RoundHalfZero
- SRoundHalfAway :: SRound 'RoundHalfAway
- SRoundHalfEven :: SRound 'RoundHalfEven
- SRoundHalfOdd :: SRound 'RoundHalfOdd
type IsTerminating (r :: Rational) = IsTerminating_ (Den r) :: Bool
isTerminating :: Rational -> Bool
termination :: forall r a. (NonTerminating r => a) -> (Terminating r => a) -> SRational r -> a
type Terminating (r :: Rational) = Terminating_ r (IsTerminating r) :: Constraint
type NonTerminating (r :: Rational) = NonTerminating_ r (IsTerminating r) :: Constraint
pattern SRationalTerminating :: forall r. () => Terminating r => SRational r
pattern SRationalNonTerminating :: forall r. () => NonTerminating r => SRational r
cmpRational :: forall a b proxy1 proxy2. (KnownRational a, KnownRational b) => proxy1 a -> proxy2 b -> OrderingI a b
sameRational :: forall a b proxy1 proxy2. (KnownRational a, KnownRational b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)
data (%@#@$) :: kn ~> (kd ~> Rational)
data (%@#@$$) :: kn -> kd ~> Rational
type (%@#@$$$) b p = b % p
data (:%@#@$) :: Integer ~> (Natural ~> Rational)
data (:%@#@$$) :: Integer -> Natural ~> Rational
type (:%@#@$$$) b p = b :% p
data FromNaturalSym0 :: Natural ~> Rational
type FromNaturalSym1 i = FromNatural i
data FromIntegerSym0 :: Integer ~> Rational
type FromIntegerSym1 i = FromInteger i
data NumSym0 :: Rational ~> Integer
type NumSym1 i = Num i
data DenSym0 :: Rational ~> Natural
type DenSym1 i = Den i
data ToRationalSym0 :: kkn ~> (kkd ~> Constraint)
data ToRationalSym1 :: kkn -> kkd ~> Constraint
type ToRationalSym2 kn kd = ToRational kn kd
data ReducedSym0 :: Rational ~> Rational
type ReducedSym1 i = Reduced i
data ShowLitSym0 :: Rational ~> Symbol
type ShowLitSym1 i = ShowLit i
data ShowsLitSym0 :: Rational ~> (Symbol ~> Symbol)
data ShowsLitSym1 :: Rational -> Symbol ~> Symbol
type ShowsLitSym2 i s = ShowsLit i s
data ShowsPrecLitSym0 :: Natural ~> (Rational ~> (Symbol ~> Symbol))
data ShowsPrecLitSym1 :: Natural -> Rational ~> (Symbol ~> Symbol)
data ShowsPrecLitSym2 :: Natural -> Rational -> Symbol ~> Symbol
type ShowsPrecLitSym3 p i s = ShowsPrecLit p i s
data IsTerminatingSym0 :: Rational ~> Bool
type IsTerminatingSym1 i = IsTerminating i
data TerminatingSym0 :: Rational ~> Constraint
type TerminatingSym1 i = Terminating i
data NonTerminatingSym0 :: Rational ~> Constraint
type NonTerminatingSym1 i = NonTerminating i
data SignumSym0 :: Rational ~> Integer
type SignumSym1 i = Signum i
data RecipSym0 :: Rational ~> Rational
type RecipSym1 i = Recip i
data DivSym0 :: Round ~> (Rational ~> Integer)
data DivSym1 :: Round -> Rational ~> Integer
type DivSym2 a b = Div a b
data RemSym0 :: Round ~> (Rational ~> Rational)
data RemSym1 :: Round -> Rational ~> Rational
type RemSym2 a b = Rem a b
data DivRemSym0 :: Round ~> (Rational ~> (Integer, Rational))
data DivRemSym1 :: Round -> Rational ~> (Integer, Rational)
type DivRemSym2 a b = DivRem a b
type family RoundUpSym0 :: Round where ...
type family RoundDownSym0 :: Round where ...
type family RoundZeroSym0 :: Round where ...
type family RoundAwaySym0 :: Round where ...
type family RoundHalfUpSym0 :: Round where ...
type family RoundHalfDownSym0 :: Round where ...
type family RoundHalfZeroSym0 :: Round where ...
type family RoundHalfAwaySym0 :: Round where ...
type family RoundHalfEvenSym0 :: Round where ...
type family RoundHalfOddSym0 :: Round where ...

Rational

data Rational Source #

Type-level version of Prelude.Rational, used only as a kind.

Use % to construct one, use :% to pattern-match on it.

Instances

Instances details

SingKind Rational Source #
Instance details Defined in KindRational Associated Types type Demote Rational = (r :: Type) # Methods fromSing :: forall (a :: Rational). Sing a -> Demote Rational # toSing :: Demote Rational -> SomeSing Rational #
SDecide Rational Source #
Instance details Defined in KindRational Methods (%~) :: forall (a :: Rational) (b :: Rational). Sing a -> Sing b -> Decision (a :~: b) #
PEq Rational Source #
Instance details Defined in KindRational Associated Types type arg == arg1 :: Bool # type arg /= arg1 :: Bool #
SEq Rational Source #
Instance details Defined in KindRational Methods (%==) :: forall (t1 :: Rational) (t2 :: Rational). Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2) # (%/=) :: forall (t1 :: Rational) (t2 :: Rational). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) t1) t2) #
POrd Rational Source #
Instance details Defined in KindRational Associated Types type Compare arg arg1 :: Ordering # type arg < arg1 :: Bool # type arg <= arg1 :: Bool # type arg > arg1 :: Bool # type arg >= arg1 :: Bool # type Max arg arg1 :: a # type Min arg arg1 :: a #
SOrd Rational Source #
Instance details Defined in KindRational Methods sCompare :: forall (t1 :: Rational) (t2 :: Rational). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) # (%<) :: forall (t1 :: Rational) (t2 :: Rational). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) # (%<=) :: forall (t1 :: Rational) (t2 :: Rational). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) # (%>) :: forall (t1 :: Rational) (t2 :: Rational). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) # (%>=) :: forall (t1 :: Rational) (t2 :: Rational). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) # sMax :: forall (t1 :: Rational) (t2 :: Rational). Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) # sMin :: forall (t1 :: Rational) (t2 :: Rational). Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #
PNum Rational Source #
Instance details Defined in KindRational Associated Types type arg + arg1 :: a # type arg - arg1 :: a # type arg * arg1 :: a # type Negate arg :: a # type Abs arg :: a # type Signum arg :: a # type FromInteger arg :: a #
SNum Rational Source #
Instance details Defined in KindRational Methods (%+) :: forall (t1 :: Rational) (t2 :: Rational). Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: forall (t1 :: Rational) (t2 :: Rational). Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%) :: forall (t1 :: Rational) (t2 :: Rational). Sing t1 -> Sing t2 -> Sing (Apply (Apply (@#@$) t1) t2) # sNegate :: forall (t :: Rational). Sing t -> Sing (Apply NegateSym0 t) # sAbs :: forall (t :: Rational). Sing t -> Sing (Apply AbsSym0 t) # sSignum :: forall (t :: Rational). Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: forall (t :: Natural). Sing t -> Sing (Apply FromIntegerSym0 t) #
PShow Rational Source #	Shows just as a term-level Prelude.`Rational`. `ShowsPrec` type-checks only if the type-level `Rational` is `Reduced`.
Instance details Defined in KindRational Associated Types type ShowsPrec arg arg1 arg2 :: Symbol # type Show_ arg :: Symbol # type ShowList arg arg1 :: Symbol #
SShow Rational Source #	Shows just as a term-level Prelude.`Rational`.
Instance details Defined in KindRational Methods sShowsPrec :: forall (t1 :: Natural) (t2 :: Rational) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) # sShow_ :: forall (t :: Rational). Sing t -> Sing (Apply Show_Sym0 t) # sShowList :: forall (t1 :: [Rational]) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) #
TestCoercion SRational Source #
Instance details Defined in KindRational Methods testCoercion :: forall (a :: k) (b :: k). SRational a -> SRational b -> Maybe (Coercion a b) #
TestEquality SRational Source #
Instance details Defined in KindRational Methods testEquality :: forall (a :: k) (b :: k). SRational a -> SRational b -> Maybe (a :~: b) #
ToRational Integer Rational Source #
Instance details Defined in KindRational Associated Types type n % d :: Rational Source # Methods mkRational :: Demote Integer -> Demote Rational -> Maybe Rational0 Source #
ToRational Rational Integer Source #
Instance details Defined in KindRational Associated Types type n % d :: Rational Source # Methods mkRational :: Demote Rational -> Demote Integer -> Maybe Rational0 Source #
ToRational Rational Rational Source #
Instance details Defined in KindRational Associated Types type n % d :: Rational Source # Methods mkRational :: Demote Rational -> Demote Rational -> Maybe Rational0 Source #
ToRational Rational Natural Source #
Instance details Defined in KindRational Associated Types type n % d :: Rational Source # Methods mkRational :: Demote Rational -> Demote Natural -> Maybe Rational0 Source #
ToRational Natural Rational Source #
Instance details Defined in KindRational Associated Types type n % d :: Rational Source # Methods mkRational :: Demote Natural -> Demote Rational -> Maybe Rational0 Source #
KnownRational r => SingI (r :: Rational) Source #
Instance details Defined in KindRational Methods sing :: Sing r #
type Demote Rational Source #
Instance details Defined in KindRational type Demote Rational = Rational
type Sing Source #
Instance details Defined in KindRational type Sing = SRational
type Abs (r :: Rational) Source #
Instance details Defined in KindRational type Abs (r :: Rational)
type FromInteger n Source #
Instance details Defined in KindRational type FromInteger n = FromNatural n
type Negate (r :: Rational) Source #
Instance details Defined in KindRational type Negate (r :: Rational)
type Signum (r :: Rational) Source #
Instance details Defined in KindRational type Signum (r :: Rational) = Signum (Num r) :% 1
type Show_ (arg :: Rational) Source #
Instance details Defined in KindRational type Show_ (arg :: Rational) = Apply (Show__6989586621680028698Sym0 :: TyFun Rational Symbol -> Type) arg
type Compare (a :: Rational) (b :: Rational) Source #	Data.Type.Ord support for type-level `Rational`s.
Instance details Defined in KindRational type Compare (a :: Rational) (b :: Rational)
type (arg :: Rational) /= (arg1 :: Rational) Source #
Instance details Defined in KindRational type (arg :: Rational) /= (arg1 :: Rational) = Apply (Apply (TFHelper_6989586621679140582Sym0 :: TyFun Rational (Rational ~> Bool) -> Type) arg) arg1
type (a :: Rational) == (b :: Rational) Source #
Instance details Defined in KindRational type (a :: Rational) == (b :: Rational)
type (arg :: Rational) < (arg1 :: Rational) Source #
Instance details Defined in KindRational type (arg :: Rational) < (arg1 :: Rational) = Apply (Apply (TFHelper_6989586621679338501Sym0 :: TyFun Rational (Rational ~> Bool) -> Type) arg) arg1
type (arg :: Rational) <= (arg1 :: Rational) Source #
Instance details Defined in KindRational type (arg :: Rational) <= (arg1 :: Rational) = Apply (Apply (TFHelper_6989586621679338543Sym0 :: TyFun Rational (Rational ~> Bool) -> Type) arg) arg1
type (arg :: Rational) > (arg1 :: Rational) Source #
Instance details Defined in KindRational type (arg :: Rational) > (arg1 :: Rational) = Apply (Apply (TFHelper_6989586621679338562Sym0 :: TyFun Rational (Rational ~> Bool) -> Type) arg) arg1
type (arg :: Rational) >= (arg1 :: Rational) Source #
Instance details Defined in KindRational type (arg :: Rational) >= (arg1 :: Rational) = Apply (Apply (TFHelper_6989586621679338578Sym0 :: TyFun Rational (Rational ~> Bool) -> Type) arg) arg1
type Compare (a :: Rational) (b :: Rational) Source #
Instance details Defined in KindRational type Compare (a :: Rational) (b :: Rational)
type Max (arg :: Rational) (arg1 :: Rational) Source #
Instance details Defined in KindRational type Max (arg :: Rational) (arg1 :: Rational) = Apply (Apply (Max_6989586621679338594Sym0 :: TyFun Rational (Rational ~> Rational) -> Type) arg) arg1
type Min (arg :: Rational) (arg1 :: Rational) Source #
Instance details Defined in KindRational type Min (arg :: Rational) (arg1 :: Rational) = Apply (Apply (Min_6989586621679338610Sym0 :: TyFun Rational (Rational ~> Rational) -> Type) arg) arg1
type (l :: Rational) * (r :: Rational) Source #
Instance details Defined in KindRational type (l :: Rational) * (r :: Rational)
type (l :: Rational) + (r :: Rational) Source #
Instance details Defined in KindRational type (l :: Rational) + (r :: Rational)
type (l :: Rational) - (r :: Rational) Source #
Instance details Defined in KindRational type (l :: Rational) - (r :: Rational)
type ShowList (arg :: [Rational]) arg1 Source #
Instance details Defined in KindRational type ShowList (arg :: [Rational]) arg1 = Apply (Apply (ShowList_6989586621680028706Sym0 :: TyFun [Rational] (Symbol ~> Symbol) -> Type) arg) arg1
type (n :: Integer) % (d :: Rational) Source #
Instance details Defined in KindRational type (n :: Integer) % (d :: Rational) = FromInteger n * Recip d
type (n :: Rational) % (d :: Integer) Source #
Instance details Defined in KindRational type (n :: Rational) % (d :: Integer) = n * Recip (FromInteger d)
type (n :: Rational) % (d :: Rational) Source #
Instance details Defined in KindRational type (n :: Rational) % (d :: Rational) = n * Recip d
type (n :: Rational) % (d :: Natural) Source #
Instance details Defined in KindRational type (n :: Rational) % (d :: Natural) = n * Recip (FromNatural d)
type (n :: Natural) % (d :: Rational) Source #
Instance details Defined in KindRational type (n :: Natural) % (d :: Rational) = FromNatural n * Recip d
type Apply FromIntegerSym0 (i :: Integer) Source #
Instance details Defined in KindRational type Apply FromIntegerSym0 (i :: Integer) = FromInteger i
type Apply NumSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply NumSym0 (i :: Rational) = Num i
type Apply SignumSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply SignumSym0 (i :: Rational) = Signum i
type Apply RecipSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply RecipSym0 (i :: Rational) = Recip i
type Apply ReducedSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply ReducedSym0 (i :: Rational) = Reduced i
type Apply DenSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply DenSym0 (i :: Rational) = Den i
type Apply IsTerminatingSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply IsTerminatingSym0 (i :: Rational) = IsTerminating i
type Apply NonTerminatingSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply NonTerminatingSym0 (i :: Rational) = NonTerminating i
type Apply TerminatingSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply TerminatingSym0 (i :: Rational) = Terminating i
type Apply ShowLitSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply ShowLitSym0 (i :: Rational) = ShowLitSym1 i
type Apply FromNaturalSym0 (i :: Natural) Source #
Instance details Defined in KindRational type Apply FromNaturalSym0 (i :: Natural) = FromNatural i
type ShowsPrec p (r :: Rational) s Source #
Instance details Defined in KindRational type ShowsPrec p (r :: Rational) s = ShowParen (p >= AppPrec1) (ShowsPrecSym2 AppPrec1 (Num r) .@#@$$$ (ShowStringSym1 " % " .@#@$$$ ShowsSym1 (Den r))) s
type Apply (DivSym1 a :: TyFun Rational Integer -> Type) (b :: Rational) Source #
Instance details Defined in KindRational type Apply (DivSym1 a :: TyFun Rational Integer -> Type) (b :: Rational) = DivSym2 a b
type Apply (RemSym1 a :: TyFun Rational Rational -> Type) (b :: Rational) Source #
Instance details Defined in KindRational type Apply (RemSym1 a :: TyFun Rational Rational -> Type) (b :: Rational) = RemSym2 a b
type Apply ((:%@#@$$) b :: TyFun Natural Rational -> Type) (p :: Natural) Source #
Instance details Defined in KindRational type Apply ((:%@#@$$) b :: TyFun Natural Rational -> Type) (p :: Natural) = b :%@#@$$$ p
type Apply ((%@#@$$) b :: TyFun kd Rational -> Type) (p :: kd) Source #
Instance details Defined in KindRational type Apply ((%@#@$$) b :: TyFun kd Rational -> Type) (p :: kd) = b %@#@$$$ p
type Apply (:%@#@$) (b :: Integer) Source #
Instance details Defined in KindRational type Apply (:%@#@$) (b :: Integer) = (:%@#@$$) b
type Apply DivSym0 (a :: Round) Source #
Instance details Defined in KindRational type Apply DivSym0 (a :: Round) = DivSym1 a
type Apply RemSym0 (a :: Round) Source #
Instance details Defined in KindRational type Apply RemSym0 (a :: Round) = RemSym1 a
type Apply DivRemSym0 (a :: Round) Source #
Instance details Defined in KindRational type Apply DivRemSym0 (a :: Round) = DivRemSym1 a
type Apply ShowsLitSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply ShowsLitSym0 (i :: Rational) = ShowsLitSym1 i
type Apply ShowsPrecLitSym0 (p :: Natural) Source #
Instance details Defined in KindRational type Apply ShowsPrecLitSym0 (p :: Natural) = ShowsPrecLitSym1 p
type Apply (ShowsPrecLitSym1 p :: TyFun Rational (Symbol ~> Symbol) -> Type) (i :: Rational) Source #
Instance details Defined in KindRational type Apply (ShowsPrecLitSym1 p :: TyFun Rational (Symbol ~> Symbol) -> Type) (i :: Rational) = ShowsPrecLitSym2 p i
type Apply (DivRemSym1 a :: TyFun Rational (Integer, Rational) -> Type) (b :: Rational) Source #
Instance details Defined in KindRational type Apply (DivRemSym1 a :: TyFun Rational (Integer, Rational) -> Type) (b :: Rational) = DivRemSym2 a b
type Apply ((%@#@$) :: TyFun kn (kd ~> Rational) -> Type) (b :: kn) Source #
Instance details Defined in KindRational type Apply ((%@#@$) :: TyFun kn (kd ~> Rational) -> Type) (b :: kn) = (%@#@$$) b :: TyFun kd Rational -> Type

type (:%) (n :: Integer) (d :: Natural) = n ':% d :: Rational infixl 7 Source #

Pattern-match on a type-level Rational.

Note that :% doesn't check that the Rational be Reduced nor have a non-zero denominator.

When constructing Rationals, use % instead, which not only accepts more polymorphic inputs, but also returns a Reduced result with denominator known to be non-zero.

type FromNatural (n :: Natural) = FromNatural n :% 1 :: Rational Source #

Construct a type-level Rational from a type-level Natural.

fromNatural :: Natural -> Rational Source #

Demoted version of FromNatural.

sFromNatural :: Sing (n :: Natural) -> SRational (FromNatural n) Source #

Singleton version of FromNatural.

type FromInteger (i :: Integer) = Normalized i :% 1 :: Rational Source #

Construct a type-level Rational from a type-level Integer. It fails to type-check if the Integer isn't Normalized.

fromInteger :: Integer -> Rational Source #

Demoted version of FromInteger.

sFromInteger :: SInteger n -> SRational (FromInteger n) Source #

Singleton version of FromInteger.

type Num (r :: Rational) = Num_ (Reduced r) :: Integer Source #

Literal Numerator of a type-level Rational. It fails to type-check if the Rational is not Reduced.

sNum :: SRational r -> SInteger (Num r) Source #

Singleton version of Num.

type Den (r :: Rational) = Den_ (Reduced r) :: Natural Source #

Literal Denominator of a type-level Rational. It fails to type-check if the Rational is not Reduced.

sDen :: SRational r -> Sing (Den r :: Natural) Source #

Singleton version of Den.

class (SingKind kn, SingKind kd) => ToRational kn kd where Source #

ToRational kn kd enables constructing type-level Rationals from a numerator of kind kn and a denominator of kind kd.

Associated Types

type (n :: kn) % (d :: kd) :: Rational infixl 7 Source #

n % d constructs and reduces a type-level Rational with numerator n and denominator d.

This type-family accepts any combination of Natural, Integer and Rational as input.

( %) :: Natural  -> Natural  -> Rational
( %) :: Natural  -> Integer  -> Rational
( %) :: Natural  -> Rational -> Rational

( %) :: Integer  -> Natural  -> Rational
( %) :: Integer  -> Integer  -> Rational
( %) :: Integer  -> Rational -> Rational

( %) :: Rational -> Natural  -> Rational
( %) :: Rational -> Integer  -> Rational
( %) :: Rational -> Rational -> Rational

It's not possible to pattern-match on n % d. Instead, you must pattern match on x :% y, where x :% y ~ n % d.

Methods

mkRational :: Demote kn -> Demote kd -> Maybe Rational Source #

Demoted version of %. Returns Nothing where % would fail to type-check (that is, denominator is 0). See ToRational for an unsafe version of this.

Instances

Instances details

ToRational Integer Integer Source #
Instance details Defined in KindRational Associated Types type n % d :: Rational Source # Methods mkRational :: Demote Integer -> Demote Integer -> Maybe Rational Source #
ToRational Integer Rational Source #
Instance details Defined in KindRational Associated Types type n % d :: Rational Source # Methods mkRational :: Demote Integer -> Demote Rational -> Maybe Rational0 Source #
ToRational Integer Natural Source #
Instance details Defined in KindRational Associated Types type n % d :: Rational Source # Methods mkRational :: Demote Integer -> Demote Natural -> Maybe Rational Source #
ToRational Rational Integer Source #
Instance details Defined in KindRational Associated Types type n % d :: Rational Source # Methods mkRational :: Demote Rational -> Demote Integer -> Maybe Rational0 Source #
ToRational Rational Rational Source #
Instance details Defined in KindRational Associated Types type n % d :: Rational Source # Methods mkRational :: Demote Rational -> Demote Rational -> Maybe Rational0 Source #
ToRational Rational Natural Source #
Instance details Defined in KindRational Associated Types type n % d :: Rational Source # Methods mkRational :: Demote Rational -> Demote Natural -> Maybe Rational0 Source #
ToRational Natural Integer Source #
Instance details Defined in KindRational Associated Types type n % d :: Rational Source # Methods mkRational :: Demote Natural -> Demote Integer -> Maybe Rational Source #
ToRational Natural Rational Source #
Instance details Defined in KindRational Associated Types type n % d :: Rational Source # Methods mkRational :: Demote Natural -> Demote Rational -> Maybe Rational0 Source #
ToRational Natural Natural Source #
Instance details Defined in KindRational Associated Types type n % d :: Rational Source # Methods mkRational :: Demote Natural -> Demote Natural -> Maybe Rational Source #

sMkRational :: forall kn kd n d. ToRational kn kd => Sing (n :: kn) -> Sing (d :: kd) -> Maybe (SRational (n % d)) Source #

Singleton version of mkRational.

(%%) :: forall kn kd n d. (ToRational kn kd, KnownRational (n % d)) => Sing (n :: kn) -> Sing (d :: kd) -> SRational (n % d) infixl 7 Source #

Like sMkRational, but never fails, thanks to a KnownRational constraint.

(%) :: forall kn kd. (ToRational kn kd, HasCallStack) => Demote kn -> Demote kd -> Rational infixl 7 Source #

Like mkRational, but fails with error where mkRational would fail with Nothing.

SRational

type KnownRational (r :: Rational) = (KnownRational_ r, Reduced r ~ r, KnownInteger (Num r), KnownNat (Den r)) Source #

Type-level Rationals satisfying KnownRational can be converted to SRationals using rationalSing. Moreover, KnownRational implies that the numerator is a KnownInteger, and that the denominator is a KnownNat.

type Reduced (r :: Rational) = Reduced_ r (Reduce r) :: Rational Source #

A Reduced rational number is one in which the numerator and denominator have no common denominators. Reduced fails to type-check if the given type-level Rational is not reduced, otherwise it returns the given Rational, unmodified. It also fails to type-check if the Integer numerator isn't Normalized, or if the denominator is zero.

Only reduced Rationals can be reliably constrained for equality using ~. Only reduced Rationals are KnownRationals.

The type-level functions in the KindRational module always produce reduced Rationals.

rationalSing :: KnownRational r => SRational r Source #

Convert an implicit KnownRational to an explicit SRational.

rationalVal :: forall r proxy. KnownRational r => proxy r -> Rational Source #

Normalized term-level Prelude Rational representation of the type-level Rational r.

withKnownRational :: forall r rep (x :: TYPE rep). SRational r -> (KnownRational r => x) -> x Source #

Convert an explicit SRational r value into an implicit KnownRational r constraint.

data SomeRational Source #

This type represents unknown type-level Rational.

Constructors

forall n.KnownRational n => SomeRational (Proxy n)

Instances

Instances details

Read SomeRational Source #	As for Prelude.`Rational`.
Instance details Defined in KindRational Methods readsPrec :: Int -> ReadS SomeRational # readList :: ReadS [SomeRational] # readPrec :: ReadPrec SomeRational # readListPrec :: ReadPrec [SomeRational] #
Show SomeRational Source #	As for Prelude.`Rational`.
Instance details Defined in KindRational Methods showsPrec :: Int -> SomeRational -> ShowS # show :: SomeRational -> String # showList :: [SomeRational] -> ShowS #
Eq SomeRational Source #
Instance details Defined in KindRational Methods (==) :: SomeRational -> SomeRational -> Bool # (/=) :: SomeRational -> SomeRational -> Bool #
Ord SomeRational Source #
Instance details Defined in KindRational Methods compare :: SomeRational -> SomeRational -> Ordering # (<) :: SomeRational -> SomeRational -> Bool # (<=) :: SomeRational -> SomeRational -> Bool # (>) :: SomeRational -> SomeRational -> Bool # (>=) :: SomeRational -> SomeRational -> Bool # max :: SomeRational -> SomeRational -> SomeRational # min :: SomeRational -> SomeRational -> SomeRational #

someRationalVal :: Rational -> SomeRational Source #

Convert a term-level Prelude.Rational into an extistentialized KnownRational wrapped in SomeRational.

NB: errors if a non-Reduced Rational is given.

data SRational (r :: Rational) Source #

Singleton type for a type-level Rational r.

Instances

Instances details

TestCoercion SRational Source #
Instance details Defined in KindRational Methods testCoercion :: forall (a :: k) (b :: k). SRational a -> SRational b -> Maybe (Coercion a b) #
TestEquality SRational Source #
Instance details Defined in KindRational Methods testEquality :: forall (a :: k) (b :: k). SRational a -> SRational b -> Maybe (a :~: b) #
Show (SRational r) Source #
Instance details Defined in KindRational Methods showsPrec :: Int -> SRational r -> ShowS # show :: SRational r -> String # showList :: [SRational r] -> ShowS #
Eq (SRational r) Source #
Instance details Defined in KindRational Methods (==) :: SRational r -> SRational r -> Bool # (/=) :: SRational r -> SRational r -> Bool #
Ord (SRational r) Source #
Instance details Defined in KindRational Methods compare :: SRational r -> SRational r -> Ordering # (<) :: SRational r -> SRational r -> Bool # (<=) :: SRational r -> SRational r -> Bool # (>) :: SRational r -> SRational r -> Bool # (>=) :: SRational r -> SRational r -> Bool # max :: SRational r -> SRational r -> SRational r # min :: SRational r -> SRational r -> SRational r #

pattern SRational :: forall r. () => KnownRational r => SRational r Source #

A explicitly bidirectional pattern synonym relating an SRational to a KnownRational constraint.

As an expression: Constructs an explicit SRational r value from an implicit KnownRational r constraint:

SRational @r :: KnownRational r => SRational r

As a pattern: Matches on an explicit SRational r value bringing an implicit KnownRational r constraint into scope:

f :: SRational r -> ..
f SRational = {- SRational r in scope -}

fromSRational :: SRational r -> Rational Source #

Return the term-level Prelude.Rational number corresponding to r.

withSomeSRational :: forall rep (x :: TYPE rep). Rational -> (forall r. SRational r -> x) -> x Source #

Convert a Prelude.Rational number into an SRational n value, where n is a fresh type-level Rational.

Proofs

sNegateRefl :: Sing (r :: Rational) -> r :~: Negate (Negate r) Source #

Show

Besides the following *Lit tools, PShow and SShow can be used to display as Prelude.Rational does.

type ShowLit (r :: Rational) = ShowsLit r "" :: Symbol Source #

Shows as a type-level KindRational.Rational apears literally at the type-level. Type-checks only if the type-level Rational is Reduced.

showLit :: Rational -> String Source #

Demoted version of ShowLit.

sShowLit :: SRational r -> Sing (ShowLit r) Source #

Singleton version of ShowLit.

type ShowsLit (r :: Rational) (s :: Symbol) = ShowsPrecLit 0 r s :: Symbol Source #

Shows as a type-level KindRational.Rational apears literally at the type-level. Type-checks only if the type-level Rational is Reduced.

showsLit :: Rational -> ShowS Source #

Demoted version of ShowsLit.

sShowsLit :: SRational r -> Sing (s :: Symbol) -> Sing (ShowsLit r s) Source #

Singleton version of ShowsLit.

type ShowsPrecLit (p :: Natural) (r :: Rational) (s :: Symbol) = ShowParen (p >= AppPrec1) (ShowsLitSym1 (Num r) .@#@$$$ (ShowStringSym1 " :% " .@#@$$$ ShowsSym1 (Den r))) s :: Symbol Source #

Shows as a type-level KindRational.Rational apears literally at the type-level. Type-checks only if the type-level Rational is Reduced.

showsPrecLit :: Int -> Rational -> ShowS Source #

Demoted version of ShowsPrecLit.

sShowsPrecLit :: Sing (p :: Natural) -> SRational r -> Sing (s :: Symbol) -> Sing (ShowsPrecLit p r s) Source #

Singleton version of ShowsPrecLit.

readPrecLit :: ReadPrec Rational Source #

Inverse of showsPrecLit.

Arithmethic

type Signum (r :: Rational) = Signum (Num r) :: Integer Source #

Sign of type-level Rationals, as a type-level Integer.

Z if zero.
P 1 if positive.
N 1 if negative.

sSignum :: Sing (r :: Rational) -> SInteger (Signum r) Source #

Singleton version of Signum.

sSignumRefl :: SRational r -> (Signum r :~: Signum (Num r), Signum r :~: Num (Signum r)) Source #

The Signum of a Rational equals the PNum Signum of its Numerator, as well as the Numerator of its PNum Signum.

type Recip (a :: Rational) = Den a % Num a :: Rational Source #

Reciprocal of the type-level Rational. Also known as multiplicative inverse.

sRecip :: (Z :% 1) < Abs r => SRational r -> SRational (Recip r) Source #

Singleton version of Recip. Type-checks only with a non-zero r.

sRecip' :: forall r. SRational r -> Maybe (SRational (Recip r)) Source #

Like sRecip, except it fails with Nothing when r is zero, rather than requiring to satisfy this as a type-level constraint.

type Div (r :: Round) (a :: Rational) = Div_ r (Reduce a) :: Integer Source #

Quotient of the Division of the Numerator of type-level Rational a by its Denominator, using the specified Rounding r.

forall (r :: Round) (a :: Rational).
  (KnownRational a) =>
    Rem r a  ==  a - Div r a % 1

Use this to approximate a type-level Rational to an Integer.

sDiv :: SRound r -> SRational a -> SInteger (Div r a) Source #

Singleton version of Div.

div :: Round -> Rational -> Integer Source #

Term-level version of Div.

Takes a KindRational.Rational as input, returns a Prelude Integer.

NB: errors if the Rational denominator is 0.

type Rem (r :: Round) (a :: Rational) = Snd (DivRem r a) :: Rational Source #

Remainder from Dividing the Numerator of the type-level Rational a by its Denominator, using the specified Rounding r.

forall (r :: Round) (a :: Rational).
  (KnownRational a) =>
    Rem r a  ==  a - Div r a % 1

rem :: Round -> Rational -> Rational Source #

Term-level version of Rem.

Takes a Prelude.Rational as input, returns a Prelude.Rational.

NB: errors if the Rational denominator is 0.

sRem :: SRound r -> SRational a -> SRational (Rem r a) Source #

Singleton version of Rem.

type DivRem (r :: Round) (a :: Rational) = DivRem_ r (Reduce a) :: (Integer, Rational) Source #

Get both the quotient and the Remainder of the Division of the Numerator of type-level Rational a by its Denominator, using the specified Rounding r.

forall (r :: Round) (a :: Rational).
  (KnownRational a) =>
    DivRem r a  ==  '(Div r a, Rem r a)

divRem :: Round -> Rational -> (Integer, Rational) Source #

Term-level version of DivRem.

Takes a Prelude.Rational as input, returns a pair of (quotient, reminder).

forall (r :: Round) (a :: Rational).
  (denominator a PEq 0) =>
    divRem r a  PEq  (div r a, rem r a)

NB: errors if the Rational denominator is 0.

sDivRem :: SRound r -> SRational a -> (SInteger (Div r a), SRational (Rem r a)) Source #

Singleton version of DivRem.

data Round #

Rounding strategy.

Constructors

RoundUp	Round up towards positive infinity.
RoundDown	Round down towards negative infinity. Also known as Prelude's `floor`. This is the type of rounding used by Prelude's `div`, `mod`, `divMod`, `Div`, `Mod`.
RoundZero	Round towards zero. Also known as Prelude's `truncate`. This is the type of rounding used by Prelude's `quot`, `rem`, `quotRem`.
RoundAway	Round away from zero.
RoundHalfUp	Round towards the closest integer. If halfway between two integers, round up towards positive infinity.
RoundHalfDown	Round towards the closest integer. If halfway between two integers, round down towards negative infinity.
RoundHalfZero	Round towards the closest integer. If halfway between two integers, round towards zero.
RoundHalfAway	Round towards the closest integer. If halfway between two integers, round away from zero.
RoundHalfEven	Round towards the closest integer. If halfway between two integers, round towards the closest even integer. Also known as Prelude's `round`.
RoundHalfOdd	Round towards the closest integer. If halfway between two integers, round towards the closest odd integer.

Instances

Instances details

Bounded Round
Instance details Defined in KindInteger.Round Methods minBound :: Round # maxBound :: Round #
Enum Round
Instance details Defined in KindInteger.Round Methods succ :: Round -> Round # pred :: Round -> Round # toEnum :: Int -> Round # fromEnum :: Round -> Int # enumFrom :: Round -> [Round] # enumFromThen :: Round -> Round -> [Round] # enumFromTo :: Round -> Round -> [Round] # enumFromThenTo :: Round -> Round -> Round -> [Round] #
Read Round
Instance details Defined in KindInteger.Round Methods readsPrec :: Int -> ReadS Round # readList :: ReadS [Round] # readPrec :: ReadPrec Round # readListPrec :: ReadPrec [Round] #
Show Round
Instance details Defined in KindInteger.Round Methods showsPrec :: Int -> Round -> ShowS # show :: Round -> String # showList :: [Round] -> ShowS #
Eq Round
Instance details Defined in KindInteger.Round Methods (==) :: Round -> Round -> Bool # (/=) :: Round -> Round -> Bool #
Ord Round
Instance details Defined in KindInteger.Round Methods compare :: Round -> Round -> Ordering # (<) :: Round -> Round -> Bool # (<=) :: Round -> Round -> Bool # (>) :: Round -> Round -> Bool # (>=) :: Round -> Round -> Bool # max :: Round -> Round -> Round # min :: Round -> Round -> Round #
SingKind Round
Instance details Defined in KindInteger.Round Associated Types type Demote Round = (r :: Type) # Methods fromSing :: forall (a :: Round). Sing a -> Demote Round # toSing :: Demote Round -> SomeSing Round #
SDecide Round
Instance details Defined in KindInteger.Round Methods (%~) :: forall (a :: Round) (b :: Round). Sing a -> Sing b -> Decision (a :~: b) #
PEq Round
Instance details Defined in KindInteger.Round Associated Types type arg == arg1 :: Bool # type arg /= arg1 :: Bool #
SEq Round
Instance details Defined in KindInteger.Round Methods (%==) :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply (==@#@$) t1) t2) # (%/=) :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) t1) t2) #
POrd Round
Instance details Defined in KindInteger.Round Associated Types type Compare arg arg1 :: Ordering # type arg < arg1 :: Bool # type arg <= arg1 :: Bool # type arg > arg1 :: Bool # type arg >= arg1 :: Bool # type Max arg arg1 :: a # type Min arg arg1 :: a #
SOrd Round
Instance details Defined in KindInteger.Round Methods sCompare :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) # (%<) :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) # (%<=) :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) # (%>) :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) # (%>=) :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) # sMax :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) # sMin :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) #
PBounded Round
Instance details Defined in KindInteger.Round Associated Types type MinBound :: a # type MaxBound :: a #
PEnum Round
Instance details Defined in KindInteger.Round Associated Types type Succ arg :: a # type Pred arg :: a # type ToEnum arg :: a # type FromEnum arg :: Natural # type EnumFromTo arg arg1 :: [a] # type EnumFromThenTo arg arg1 arg2 :: [a] #
SBounded Round
Instance details Defined in KindInteger.Round Methods sMinBound :: Sing MinBoundSym0 # sMaxBound :: Sing MaxBoundSym0 #
SEnum Round
Instance details Defined in KindInteger.Round Methods sSucc :: forall (t :: Round). Sing t -> Sing (Apply SuccSym0 t) # sPred :: forall (t :: Round). Sing t -> Sing (Apply PredSym0 t) # sToEnum :: forall (t :: Natural). Sing t -> Sing (Apply ToEnumSym0 t) # sFromEnum :: forall (t :: Round). Sing t -> Sing (Apply FromEnumSym0 t) # sEnumFromTo :: forall (t1 :: Round) (t2 :: Round). Sing t1 -> Sing t2 -> Sing (Apply (Apply EnumFromToSym0 t1) t2) # sEnumFromThenTo :: forall (t1 :: Round) (t2 :: Round) (t3 :: Round). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t1) t2) t3) #
PShow Round
Instance details Defined in KindInteger.Round Associated Types type ShowsPrec arg arg1 arg2 :: Symbol # type Show_ arg :: Symbol # type ShowList arg arg1 :: Symbol #
SShow Round
Instance details Defined in KindInteger.Round Methods sShowsPrec :: forall (t1 :: Natural) (t2 :: Round) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) # sShow_ :: forall (t :: Round). Sing t -> Sing (Apply Show_Sym0 t) # sShowList :: forall (t1 :: [Round]) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) #
TestCoercion SRound
Instance details Defined in KindInteger.Round Methods testCoercion :: forall (a :: k) (b :: k). SRound a -> SRound b -> Maybe (Coercion a b) #
TestEquality SRound
Instance details Defined in KindInteger.Round Methods testEquality :: forall (a :: k) (b :: k). SRound a -> SRound b -> Maybe (a :~: b) #
SingI 'RoundAway
Instance details Defined in KindInteger.Round Methods sing :: Sing 'RoundAway #
SingI 'RoundDown
Instance details Defined in KindInteger.Round Methods sing :: Sing 'RoundDown #
SingI 'RoundHalfAway
Instance details Defined in KindInteger.Round Methods sing :: Sing 'RoundHalfAway #
SingI 'RoundHalfDown
Instance details Defined in KindInteger.Round Methods sing :: Sing 'RoundHalfDown #
SingI 'RoundHalfEven
Instance details Defined in KindInteger.Round Methods sing :: Sing 'RoundHalfEven #
SingI 'RoundHalfOdd
Instance details Defined in KindInteger.Round Methods sing :: Sing 'RoundHalfOdd #
SingI 'RoundHalfUp
Instance details Defined in KindInteger.Round Methods sing :: Sing 'RoundHalfUp #
SingI 'RoundHalfZero
Instance details Defined in KindInteger.Round Methods sing :: Sing 'RoundHalfZero #
SingI 'RoundUp
Instance details Defined in KindInteger.Round Methods sing :: Sing 'RoundUp #
SingI 'RoundZero
Instance details Defined in KindInteger.Round Methods sing :: Sing 'RoundZero #
SuppressUnusedWarnings Compare_6989586621679052738Sym0
Instance details Defined in KindInteger.Round Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings TFHelper_6989586621679051564Sym0
Instance details Defined in KindInteger.Round Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings FromEnum_6989586621679050956Sym0
Instance details Defined in KindInteger.Round Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ToEnum_6989586621679050919Sym0
Instance details Defined in KindInteger.Round Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings ShowsPrec_6989586621679055447Sym0
Instance details Defined in KindInteger.Round Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (Compare_6989586621679052738Sym1 a6989586621679052743 :: TyFun Round Ordering -> Type)
Instance details Defined in KindInteger.Round Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (ShowsPrec_6989586621679055447Sym1 a6989586621679055473 :: TyFun Round (Symbol ~> Symbol) -> Type)
Instance details Defined in KindInteger.Round Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings (TFHelper_6989586621679051564Sym1 a6989586621679051569 :: TyFun Round Bool -> Type)
Instance details Defined in KindInteger.Round Methods suppressUnusedWarnings :: () #
type Demote Round
Instance details Defined in KindInteger.Round type Demote Round = Round
type Sing
Instance details Defined in KindInteger.Round type Sing = SRound
type MaxBound
Instance details Defined in KindInteger.Round type MaxBound = MaxBound_6989586621679050419Sym0
type MinBound
Instance details Defined in KindInteger.Round type MinBound = MinBound_6989586621679050416Sym0
type FromEnum (a :: Round)
Instance details Defined in KindInteger.Round type FromEnum (a :: Round) = Apply FromEnum_6989586621679050956Sym0 a
type Pred (arg :: Round)
Instance details Defined in KindInteger.Round type Pred (arg :: Round) = Apply (Pred_6989586621679523156Sym0 :: TyFun Round Round -> Type) arg
type Succ (arg :: Round)
Instance details Defined in KindInteger.Round type Succ (arg :: Round) = Apply (Succ_6989586621679523121Sym0 :: TyFun Round Round -> Type) arg
type ToEnum a
Instance details Defined in KindInteger.Round type ToEnum a = Apply ToEnum_6989586621679050919Sym0 a
type Show_ (arg :: Round)
Instance details Defined in KindInteger.Round type Show_ (arg :: Round) = Apply (Show__6989586621680028698Sym0 :: TyFun Round Symbol -> Type) arg
type (arg :: Round) /= (arg1 :: Round)
Instance details Defined in KindInteger.Round type (arg :: Round) /= (arg1 :: Round) = Apply (Apply (TFHelper_6989586621679140582Sym0 :: TyFun Round (Round ~> Bool) -> Type) arg) arg1
type (a1 :: Round) == (a2 :: Round)
Instance details Defined in KindInteger.Round type (a1 :: Round) == (a2 :: Round) = Apply (Apply TFHelper_6989586621679051564Sym0 a1) a2
type (arg :: Round) < (arg1 :: Round)
Instance details Defined in KindInteger.Round type (arg :: Round) < (arg1 :: Round) = Apply (Apply (TFHelper_6989586621679338501Sym0 :: TyFun Round (Round ~> Bool) -> Type) arg) arg1
type (arg :: Round) <= (arg1 :: Round)
Instance details Defined in KindInteger.Round type (arg :: Round) <= (arg1 :: Round) = Apply (Apply (TFHelper_6989586621679338543Sym0 :: TyFun Round (Round ~> Bool) -> Type) arg) arg1
type (arg :: Round) > (arg1 :: Round)
Instance details Defined in KindInteger.Round type (arg :: Round) > (arg1 :: Round) = Apply (Apply (TFHelper_6989586621679338562Sym0 :: TyFun Round (Round ~> Bool) -> Type) arg) arg1
type (arg :: Round) >= (arg1 :: Round)
Instance details Defined in KindInteger.Round type (arg :: Round) >= (arg1 :: Round) = Apply (Apply (TFHelper_6989586621679338578Sym0 :: TyFun Round (Round ~> Bool) -> Type) arg) arg1
type Compare (a1 :: Round) (a2 :: Round)
Instance details Defined in KindInteger.Round type Compare (a1 :: Round) (a2 :: Round) = Apply (Apply Compare_6989586621679052738Sym0 a1) a2
type Max (arg :: Round) (arg1 :: Round)
Instance details Defined in KindInteger.Round type Max (arg :: Round) (arg1 :: Round) = Apply (Apply (Max_6989586621679338594Sym0 :: TyFun Round (Round ~> Round) -> Type) arg) arg1
type Min (arg :: Round) (arg1 :: Round)
Instance details Defined in KindInteger.Round type Min (arg :: Round) (arg1 :: Round) = Apply (Apply (Min_6989586621679338610Sym0 :: TyFun Round (Round ~> Round) -> Type) arg) arg1
type EnumFromTo (arg :: Round) (arg1 :: Round)
Instance details Defined in KindInteger.Round type EnumFromTo (arg :: Round) (arg1 :: Round) = Apply (Apply (EnumFromTo_6989586621679523181Sym0 :: TyFun Round (Round ~> [Round]) -> Type) arg) arg1
type ShowList (arg :: [Round]) arg1
Instance details Defined in KindInteger.Round type ShowList (arg :: [Round]) arg1 = Apply (Apply (ShowList_6989586621680028706Sym0 :: TyFun [Round] (Symbol ~> Symbol) -> Type) arg) arg1
type Apply FromEnum_6989586621679050956Sym0 (a6989586621679050960 :: Round)
Instance details Defined in KindInteger.Round type Apply FromEnum_6989586621679050956Sym0 (a6989586621679050960 :: Round) = FromEnum_6989586621679050956 a6989586621679050960
type Apply ToEnum_6989586621679050919Sym0 (a6989586621679050923 :: Natural)
Instance details Defined in KindInteger.Round type Apply ToEnum_6989586621679050919Sym0 (a6989586621679050923 :: Natural) = ToEnum_6989586621679050919 a6989586621679050923
type EnumFromThenTo (arg :: Round) (arg1 :: Round) (arg2 :: Round)
Instance details Defined in KindInteger.Round type EnumFromThenTo (arg :: Round) (arg1 :: Round) (arg2 :: Round) = Apply (Apply (Apply (EnumFromThenTo_6989586621679523214Sym0 :: TyFun Round (Round ~> (Round ~> [Round])) -> Type) arg) arg1) arg2
type ShowsPrec a1 (a2 :: Round) a3
Instance details Defined in KindInteger.Round type ShowsPrec a1 (a2 :: Round) a3 = Apply (Apply (Apply ShowsPrec_6989586621679055447Sym0 a1) a2) a3
type Apply (Compare_6989586621679052738Sym1 a6989586621679052743 :: TyFun Round Ordering -> Type) (a6989586621679052744 :: Round)
Instance details Defined in KindInteger.Round type Apply (Compare_6989586621679052738Sym1 a6989586621679052743 :: TyFun Round Ordering -> Type) (a6989586621679052744 :: Round) = Compare_6989586621679052738 a6989586621679052743 a6989586621679052744
type Apply (TFHelper_6989586621679051564Sym1 a6989586621679051569 :: TyFun Round Bool -> Type) (a6989586621679051570 :: Round)
Instance details Defined in KindInteger.Round type Apply (TFHelper_6989586621679051564Sym1 a6989586621679051569 :: TyFun Round Bool -> Type) (a6989586621679051570 :: Round) = TFHelper_6989586621679051564 a6989586621679051569 a6989586621679051570
type Apply DivSym0 (r :: Round)
Instance details Defined in KindInteger type Apply DivSym0 (r :: Round) = DivSym1 r
type Apply RemSym0 (r :: Round)
Instance details Defined in KindInteger type Apply RemSym0 (r :: Round) = RemSym1 r
type Apply DivRemSym0 (r :: Round)
Instance details Defined in KindInteger type Apply DivRemSym0 (r :: Round) = DivRemSym1 r
type Apply Compare_6989586621679052738Sym0 (a6989586621679052743 :: Round)
Instance details Defined in KindInteger.Round type Apply Compare_6989586621679052738Sym0 (a6989586621679052743 :: Round) = Compare_6989586621679052738Sym1 a6989586621679052743
type Apply TFHelper_6989586621679051564Sym0 (a6989586621679051569 :: Round)
Instance details Defined in KindInteger.Round type Apply TFHelper_6989586621679051564Sym0 (a6989586621679051569 :: Round) = TFHelper_6989586621679051564Sym1 a6989586621679051569
type Apply DivSym0 (a :: Round) Source #
Instance details Defined in KindRational type Apply DivSym0 (a :: Round) = DivSym1 a
type Apply RemSym0 (a :: Round) Source #
Instance details Defined in KindRational type Apply RemSym0 (a :: Round) = RemSym1 a
type Apply DivRemSym0 (a :: Round) Source #
Instance details Defined in KindRational type Apply DivRemSym0 (a :: Round) = DivRemSym1 a
type Apply ShowsPrec_6989586621679055447Sym0 (a6989586621679055473 :: Natural)
Instance details Defined in KindInteger.Round type Apply ShowsPrec_6989586621679055447Sym0 (a6989586621679055473 :: Natural) = ShowsPrec_6989586621679055447Sym1 a6989586621679055473
type Apply (ShowsPrec_6989586621679055447Sym1 a6989586621679055473 :: TyFun Round (Symbol ~> Symbol) -> Type) (a6989586621679055474 :: Round)
Instance details Defined in KindInteger.Round type Apply (ShowsPrec_6989586621679055447Sym1 a6989586621679055473 :: TyFun Round (Symbol ~> Symbol) -> Type) (a6989586621679055474 :: Round) = ShowsPrec_6989586621679055447Sym2 a6989586621679055473 a6989586621679055474

data SRound (a :: Round) where #

Constructors

SRoundUp :: SRound 'RoundUp
SRoundDown :: SRound 'RoundDown
SRoundZero :: SRound 'RoundZero
SRoundAway :: SRound 'RoundAway
SRoundHalfUp :: SRound 'RoundHalfUp
SRoundHalfDown :: SRound 'RoundHalfDown
SRoundHalfZero :: SRound 'RoundHalfZero
SRoundHalfAway :: SRound 'RoundHalfAway
SRoundHalfEven :: SRound 'RoundHalfEven
SRoundHalfOdd :: SRound 'RoundHalfOdd

Instances

Instances details

TestCoercion SRound
Instance details Defined in KindInteger.Round Methods testCoercion :: forall (a :: k) (b :: k). SRound a -> SRound b -> Maybe (Coercion a b) #
TestEquality SRound
Instance details Defined in KindInteger.Round Methods testEquality :: forall (a :: k) (b :: k). SRound a -> SRound b -> Maybe (a :~: b) #
Show (SRound z)
Instance details Defined in KindInteger.Round Methods showsPrec :: Int -> SRound z -> ShowS # show :: SRound z -> String # showList :: [SRound z] -> ShowS #

Decimals

type IsTerminating (r :: Rational) = IsTerminating_ (Den r) :: Bool Source #

Whether the type-level Rational is terminating. That is, whether it can be fully represented as a finite decimal number.

isTerminating :: Rational -> Bool Source #

Term-level version of the IsTerminating function.

NB: errors if the Rational denominator is 0.

termination :: forall r a. (NonTerminating r => a) -> (Terminating r => a) -> SRational r -> a Source #

Determine whether r is Terminating or NonTerminating at the term-level, and create the corresponding type-level proof.

type Terminating (r :: Rational) = Terminating_ r (IsTerminating r) :: Constraint Source #

This is essentially the same as (KnownRational r, IsTerminating r ~ True), except with a nicer error message when IsTerminating r ~ False.

type NonTerminating (r :: Rational) = NonTerminating_ r (IsTerminating r) :: Constraint Source #

This is essentially the same as (KnownRational r, IsTerminating r ~ False), except with a nicer error message when IsTerminating r ~ False.

pattern SRationalTerminating :: forall r. () => Terminating r => SRational r Source #

Matches a SRational that is Terminating.

pattern SRationalNonTerminating :: forall r. () => NonTerminating r => SRational r Source #

Matches a SRational that is NonTerminating.

Comparisons

Additional comparison tools are available at SDdecide, TestEquality, TestCoercion, PEq, SEq, POrd, SOrd and Compare.

cmpRational :: forall a b proxy1 proxy2. (KnownRational a, KnownRational b) => proxy1 a -> proxy2 b -> OrderingI a b Source #

Like sameRational, but if the type-level Rationals aren't equal, this additionally provides proof of LT or GT.

sameRational :: forall a b proxy1 proxy2. (KnownRational a, KnownRational b) => proxy1 a -> proxy2 b -> Maybe (a :~: b) Source #

We either get evidence that this function was instantiated with the same type-level Rationals, or Nothing.

Defunctionalization

data (%@#@$) :: kn ~> (kd ~> Rational) Source #

Instances

Instances details

type Apply ((%@#@$) :: TyFun kn (kd ~> Rational) -> Type) (b :: kn) Source #
Instance details Defined in KindRational type Apply ((%@#@$) :: TyFun kn (kd ~> Rational) -> Type) (b :: kn) = (%@#@$$) b :: TyFun kd Rational -> Type

data (%@#@$$) :: kn -> kd ~> Rational Source #

Instances

Instances details

type Apply ((%@#@$$) b :: TyFun kd Rational -> Type) (p :: kd) Source #
Instance details Defined in KindRational type Apply ((%@#@$$) b :: TyFun kd Rational -> Type) (p :: kd) = b %@#@$$$ p

type (%@#@$$$) b p = b % p infixl 7 Source #

data (:%@#@$) :: Integer ~> (Natural ~> Rational) Source #

Instances

Instances details

type Apply (:%@#@$) (b :: Integer) Source #
Instance details Defined in KindRational type Apply (:%@#@$) (b :: Integer) = (:%@#@$$) b

data (:%@#@$$) :: Integer -> Natural ~> Rational Source #

Instances

Instances details

type Apply ((:%@#@$$) b :: TyFun Natural Rational -> Type) (p :: Natural) Source #
Instance details Defined in KindRational type Apply ((:%@#@$$) b :: TyFun Natural Rational -> Type) (p :: Natural) = b :%@#@$$$ p

type (:%@#@$$$) b p = b :% p infixl 7 Source #

data FromNaturalSym0 :: Natural ~> Rational Source #

Instances

Instances details

type Apply FromNaturalSym0 (i :: Natural) Source #
Instance details Defined in KindRational type Apply FromNaturalSym0 (i :: Natural) = FromNatural i

type FromNaturalSym1 i = FromNatural i Source #

data FromIntegerSym0 :: Integer ~> Rational Source #

Instances

Instances details

type Apply FromIntegerSym0 (i :: Integer) Source #
Instance details Defined in KindRational type Apply FromIntegerSym0 (i :: Integer) = FromInteger i

type FromIntegerSym1 i = FromInteger i Source #

data NumSym0 :: Rational ~> Integer Source #

Instances

Instances details

type Apply NumSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply NumSym0 (i :: Rational) = Num i

type NumSym1 i = Num i Source #

data DenSym0 :: Rational ~> Natural Source #

Instances

Instances details

type Apply DenSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply DenSym0 (i :: Rational) = Den i

type DenSym1 i = Den i Source #

data ToRationalSym0 :: kkn ~> (kkd ~> Constraint) Source #

Instances

Instances details

type Apply (ToRationalSym0 :: TyFun kkn (kkd ~> Constraint) -> Type) (kn :: kkn) Source #
Instance details Defined in KindRational type Apply (ToRationalSym0 :: TyFun kkn (kkd ~> Constraint) -> Type) (kn :: kkn) = ToRationalSym1 kn :: TyFun kkd Constraint -> Type

data ToRationalSym1 :: kkn -> kkd ~> Constraint Source #

Instances

Instances details

type Apply (ToRationalSym1 kn :: TyFun Type Constraint -> Type) (kd :: Type) Source #
Instance details Defined in KindRational type Apply (ToRationalSym1 kn :: TyFun Type Constraint -> Type) (kd :: Type) = ToRationalSym2 kn kd

type ToRationalSym2 kn kd = ToRational kn kd Source #

data ReducedSym0 :: Rational ~> Rational Source #

Instances

Instances details

type Apply ReducedSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply ReducedSym0 (i :: Rational) = Reduced i

type ReducedSym1 i = Reduced i Source #

data ShowLitSym0 :: Rational ~> Symbol Source #

Instances

Instances details

type Apply ShowLitSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply ShowLitSym0 (i :: Rational) = ShowLitSym1 i

type ShowLitSym1 i = ShowLit i Source #

data ShowsLitSym0 :: Rational ~> (Symbol ~> Symbol) Source #

Instances

Instances details

type Apply ShowsLitSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply ShowsLitSym0 (i :: Rational) = ShowsLitSym1 i

data ShowsLitSym1 :: Rational -> Symbol ~> Symbol Source #

Instances

Instances details

type Apply (ShowsLitSym1 i :: TyFun Symbol Symbol -> Type) (s :: Symbol) Source #
Instance details Defined in KindRational type Apply (ShowsLitSym1 i :: TyFun Symbol Symbol -> Type) (s :: Symbol) = ShowsLitSym2 i s

type ShowsLitSym2 i s = ShowsLit i s Source #

data ShowsPrecLitSym0 :: Natural ~> (Rational ~> (Symbol ~> Symbol)) Source #

Instances

Instances details

type Apply ShowsPrecLitSym0 (p :: Natural) Source #
Instance details Defined in KindRational type Apply ShowsPrecLitSym0 (p :: Natural) = ShowsPrecLitSym1 p

data ShowsPrecLitSym1 :: Natural -> Rational ~> (Symbol ~> Symbol) Source #

Instances

Instances details

type Apply (ShowsPrecLitSym1 p :: TyFun Rational (Symbol ~> Symbol) -> Type) (i :: Rational) Source #
Instance details Defined in KindRational type Apply (ShowsPrecLitSym1 p :: TyFun Rational (Symbol ~> Symbol) -> Type) (i :: Rational) = ShowsPrecLitSym2 p i

data ShowsPrecLitSym2 :: Natural -> Rational -> Symbol ~> Symbol Source #

Instances

Instances details

type Apply (ShowsPrecLitSym2 p i :: TyFun Symbol Symbol -> Type) (s :: Symbol) Source #
Instance details Defined in KindRational type Apply (ShowsPrecLitSym2 p i :: TyFun Symbol Symbol -> Type) (s :: Symbol) = ShowsPrecLitSym3 p i s

type ShowsPrecLitSym3 p i s = ShowsPrecLit p i s Source #

data IsTerminatingSym0 :: Rational ~> Bool Source #

Instances

Instances details

type Apply IsTerminatingSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply IsTerminatingSym0 (i :: Rational) = IsTerminating i

type IsTerminatingSym1 i = IsTerminating i Source #

data TerminatingSym0 :: Rational ~> Constraint Source #

Instances

Instances details

type Apply TerminatingSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply TerminatingSym0 (i :: Rational) = Terminating i

type TerminatingSym1 i = Terminating i Source #

data NonTerminatingSym0 :: Rational ~> Constraint Source #

Instances

Instances details

type Apply NonTerminatingSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply NonTerminatingSym0 (i :: Rational) = NonTerminating i

type NonTerminatingSym1 i = NonTerminating i Source #

data SignumSym0 :: Rational ~> Integer Source #

Instances

Instances details

type Apply SignumSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply SignumSym0 (i :: Rational) = Signum i

type SignumSym1 i = Signum i Source #

data RecipSym0 :: Rational ~> Rational Source #

Instances

Instances details

type Apply RecipSym0 (i :: Rational) Source #
Instance details Defined in KindRational type Apply RecipSym0 (i :: Rational) = Recip i

type RecipSym1 i = Recip i Source #

data DivSym0 :: Round ~> (Rational ~> Integer) Source #

Instances

Instances details

type Apply DivSym0 (a :: Round) Source #
Instance details Defined in KindRational type Apply DivSym0 (a :: Round) = DivSym1 a

data DivSym1 :: Round -> Rational ~> Integer Source #

Instances

Instances details

type Apply (DivSym1 a :: TyFun Rational Integer -> Type) (b :: Rational) Source #
Instance details Defined in KindRational type Apply (DivSym1 a :: TyFun Rational Integer -> Type) (b :: Rational) = DivSym2 a b

type DivSym2 a b = Div a b Source #

data RemSym0 :: Round ~> (Rational ~> Rational) Source #

Instances

Instances details

type Apply RemSym0 (a :: Round) Source #
Instance details Defined in KindRational type Apply RemSym0 (a :: Round) = RemSym1 a

data RemSym1 :: Round -> Rational ~> Rational Source #

Instances

Instances details

type Apply (RemSym1 a :: TyFun Rational Rational -> Type) (b :: Rational) Source #
Instance details Defined in KindRational type Apply (RemSym1 a :: TyFun Rational Rational -> Type) (b :: Rational) = RemSym2 a b

type RemSym2 a b = Rem a b Source #

data DivRemSym0 :: Round ~> (Rational ~> (Integer, Rational)) Source #

Instances

Instances details

type Apply DivRemSym0 (a :: Round) Source #
Instance details Defined in KindRational type Apply DivRemSym0 (a :: Round) = DivRemSym1 a

data DivRemSym1 :: Round -> Rational ~> (Integer, Rational) Source #

Instances

Instances details

type Apply (DivRemSym1 a :: TyFun Rational (Integer, Rational) -> Type) (b :: Rational) Source #
Instance details Defined in KindRational type Apply (DivRemSym1 a :: TyFun Rational (Integer, Rational) -> Type) (b :: Rational) = DivRemSym2 a b