Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
This module provides a type-level representation for term-level
Rational
s. 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 Natural
s
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
- 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
- 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
Instances
type FromNatural (n :: Natural) = FromNatural n :% 1 :: Rational Source #
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
.
class (SingKind kn, SingKind kd) => ToRational kn kd where Source #
enables constructing type-level ToRational
kn kdRational
s
from a numerator of kind kn
and a denominator of kind kd
.
type (n :: kn) % (d :: kd) :: Rational infixl 7 Source #
n
constructs and reduces a type-level %
dRational
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
. Instead, you must
pattern match on %
dx
, where :%
yx
.:%
y ~ n %
d
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
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 Rational
s satisfying KnownRational
can be converted to
SRational
s 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 Reduce
d 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 Rational
s can be reliably constrained for equality
using ~
. Only reduced Rational
s are KnownRational
s.
The type-level functions in the KindRational module
always produce reduced Rational
s.
rationalSing :: KnownRational r => SRational r Source #
Convert an implicit KnownRational
to an explicit SRational
.
rationalVal :: forall r proxy. KnownRational r => proxy r -> Rational Source #
withKnownRational :: forall r rep (x :: TYPE rep). SRational r -> (KnownRational r => x) -> x Source #
Convert an explicit
value into an implicit
SRational
r
constraint.KnownRational
r
data SomeRational Source #
This type represents unknown type-level Rational
.
forall n.KnownRational n => SomeRational (Proxy n) |
Instances
Read SomeRational Source # | |
Defined in KindRational readsPrec :: Int -> ReadS SomeRational # readList :: ReadS [SomeRational] # | |
Show SomeRational Source # | |
Defined in KindRational showsPrec :: Int -> SomeRational -> ShowS # show :: SomeRational -> String # showList :: [SomeRational] -> ShowS # | |
Eq SomeRational Source # | |
Defined in KindRational (==) :: SomeRational -> SomeRational -> Bool # (/=) :: SomeRational -> SomeRational -> Bool # | |
Ord SomeRational Source # | |
Defined in KindRational 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
.
data SRational (r :: Rational) Source #
Singleton type for a type-level Rational
r
.
Instances
TestCoercion SRational Source # | |
Defined in KindRational | |
TestEquality SRational Source # | |
Defined in KindRational | |
Show (SRational r) Source # | |
Eq (SRational r) Source # | |
Ord (SRational r) Source # | |
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
value from an
implicit SRational
r
constraint:KnownRational
r
SRational
@r ::KnownRational
r =>SRational
r
As a pattern: Matches on an explicit
value bringing
an implicit SRational
r
constraint into scope:KnownRational
r
f :: SRational
r -> ..
f SRational = {- SRational r in scope -}
fromSRational :: SRational r -> Rational Source #
withSomeSRational :: forall rep (x :: TYPE rep). Rational -> (forall r. SRational r -> x) -> x Source #
Proofs
Show
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
.
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
.
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
sRecip :: (Z :% 1) < Abs r => SRational r -> SRational (Recip r) Source #
Singleton version of Recip
. Type-checks only with a non-zero r
.
sDivRem :: SRound r -> SRational a -> (SInteger (Div r a), SRational (Rem r a)) Source #
Singleton version of DivRem
.
Rounding strategy.
RoundUp | Round up towards positive infinity. |
RoundDown | Round down towards negative infinity. Also known as Prelude's
|
RoundZero | Round towards zero. Also known as Prelude's |
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
|
RoundHalfOdd | Round towards the closest integer. If halfway between two integers, round towards the closest odd integer. |
Instances
Bounded Round | |
Enum Round | |
Read Round | |
Show Round | |
Eq Round | |
Ord Round | |
SingKind Round | |
SDecide Round | |
PEq Round | |
SEq Round | |
POrd Round | |
SOrd Round | |
Defined in KindInteger.Round 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 | |
Defined in KindInteger.Round | |
PEnum Round | |
Defined in KindInteger.Round | |
SBounded Round | |
Defined in KindInteger.Round | |
SEnum Round | |
Defined in KindInteger.Round 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 | |
SShow Round | |
Defined in KindInteger.Round 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 | |
Defined in KindInteger.Round | |
TestEquality SRound | |
Defined in KindInteger.Round | |
SingI 'RoundAway | |
Defined in KindInteger.Round | |
SingI 'RoundDown | |
Defined in KindInteger.Round | |
SingI 'RoundHalfAway | |
Defined in KindInteger.Round sing :: Sing 'RoundHalfAway # | |
SingI 'RoundHalfDown | |
Defined in KindInteger.Round sing :: Sing 'RoundHalfDown # | |
SingI 'RoundHalfEven | |
Defined in KindInteger.Round sing :: Sing 'RoundHalfEven # | |
SingI 'RoundHalfOdd | |
Defined in KindInteger.Round sing :: Sing 'RoundHalfOdd # | |
SingI 'RoundHalfUp | |
Defined in KindInteger.Round sing :: Sing 'RoundHalfUp # | |
SingI 'RoundHalfZero | |
Defined in KindInteger.Round sing :: Sing 'RoundHalfZero # | |
SingI 'RoundUp | |
Defined in KindInteger.Round | |
SingI 'RoundZero | |
Defined in KindInteger.Round | |
SuppressUnusedWarnings Compare_6989586621679052738Sym0 | |
Defined in KindInteger.Round suppressUnusedWarnings :: () # | |
SuppressUnusedWarnings TFHelper_6989586621679051564Sym0 | |
Defined in KindInteger.Round suppressUnusedWarnings :: () # | |
SuppressUnusedWarnings FromEnum_6989586621679050956Sym0 | |
Defined in KindInteger.Round suppressUnusedWarnings :: () # | |
SuppressUnusedWarnings ToEnum_6989586621679050919Sym0 | |
Defined in KindInteger.Round suppressUnusedWarnings :: () # | |
SuppressUnusedWarnings ShowsPrec_6989586621679055447Sym0 | |
Defined in KindInteger.Round suppressUnusedWarnings :: () # | |
SuppressUnusedWarnings (Compare_6989586621679052738Sym1 a6989586621679052743 :: TyFun Round Ordering -> Type) | |
Defined in KindInteger.Round suppressUnusedWarnings :: () # | |
SuppressUnusedWarnings (ShowsPrec_6989586621679055447Sym1 a6989586621679055473 :: TyFun Round (Symbol ~> Symbol) -> Type) | |
Defined in KindInteger.Round suppressUnusedWarnings :: () # | |
SuppressUnusedWarnings (TFHelper_6989586621679051564Sym1 a6989586621679051569 :: TyFun Round Bool -> Type) | |
Defined in KindInteger.Round suppressUnusedWarnings :: () # | |
type Demote Round | |
Defined in KindInteger.Round | |
type Sing | |
Defined in KindInteger.Round | |
type MaxBound | |
Defined in KindInteger.Round type MaxBound = MaxBound_6989586621679050419Sym0 | |
type MinBound | |
Defined in KindInteger.Round type MinBound = MinBound_6989586621679050416Sym0 | |
type FromEnum (a :: Round) | |
Defined in KindInteger.Round | |
type Pred (arg :: Round) | |
type Succ (arg :: Round) | |
type ToEnum a | |
Defined in KindInteger.Round | |
type Show_ (arg :: Round) | |
type (arg :: Round) /= (arg1 :: Round) | |
type (a1 :: Round) == (a2 :: Round) | |
type (arg :: Round) < (arg1 :: Round) | |
type (arg :: Round) <= (arg1 :: Round) | |
type (arg :: Round) > (arg1 :: Round) | |
type (arg :: Round) >= (arg1 :: Round) | |
type Compare (a1 :: Round) (a2 :: Round) | |
type Max (arg :: Round) (arg1 :: Round) | |
type Min (arg :: Round) (arg1 :: Round) | |
type EnumFromTo (arg :: Round) (arg1 :: Round) | |
type ShowList (arg :: [Round]) arg1 | |
type Apply FromEnum_6989586621679050956Sym0 (a6989586621679050960 :: Round) | |
Defined in KindInteger.Round | |
type Apply ToEnum_6989586621679050919Sym0 (a6989586621679050923 :: Natural) | |
Defined in KindInteger.Round | |
type EnumFromThenTo (arg :: Round) (arg1 :: Round) (arg2 :: Round) | |
type ShowsPrec a1 (a2 :: Round) a3 | |
type Apply (Compare_6989586621679052738Sym1 a6989586621679052743 :: TyFun Round Ordering -> Type) (a6989586621679052744 :: Round) | |
type Apply (TFHelper_6989586621679051564Sym1 a6989586621679051569 :: TyFun Round Bool -> Type) (a6989586621679051570 :: Round) | |
type Apply DivSym0 (r :: Round) | |
Defined in KindInteger | |
type Apply RemSym0 (r :: Round) | |
Defined in KindInteger | |
type Apply DivRemSym0 (r :: Round) | |
Defined in KindInteger | |
type Apply Compare_6989586621679052738Sym0 (a6989586621679052743 :: Round) | |
Defined in KindInteger.Round | |
type Apply TFHelper_6989586621679051564Sym0 (a6989586621679051569 :: Round) | |
Defined in KindInteger.Round | |
type Apply DivSym0 (a :: Round) Source # | |
Defined in KindRational | |
type Apply RemSym0 (a :: Round) Source # | |
Defined in KindRational | |
type Apply DivRemSym0 (a :: Round) Source # | |
Defined in KindRational | |
type Apply ShowsPrec_6989586621679055447Sym0 (a6989586621679055473 :: Natural) | |
Defined in KindInteger.Round | |
type Apply (ShowsPrec_6989586621679055447Sym1 a6989586621679055473 :: TyFun Round (Symbol ~> Symbol) -> Type) (a6989586621679055474 :: Round) | |
data SRound (a :: Round) where #
Instances
TestCoercion SRound | |
Defined in KindInteger.Round | |
TestEquality SRound | |
Defined in KindInteger.Round | |
Show (SRound z) | |
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.
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 (
,
except with a nicer error message when KnownRational
r, IsTerminating
r ~ True
)
.IsTerminating
r ~ False
type NonTerminating (r :: Rational) = NonTerminating_ r (IsTerminating r) :: Constraint Source #
This is essentially the same as (
,
except with a nicer error message when KnownRational
r, IsTerminating
r ~ False
)
.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 Rational
s 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 #
Defunctionalization
type (:%@#@$$$) b p = b :% p infixl 7 Source #
data FromNaturalSym0 :: Natural ~> Rational Source #
Instances
type Apply FromNaturalSym0 (i :: Natural) Source # | |
Defined in KindRational |
type FromNaturalSym1 i = FromNatural i Source #
data FromIntegerSym0 :: Integer ~> Rational Source #
Instances
type Apply FromIntegerSym0 (i :: Integer) Source # | |
Defined in KindRational |
type FromIntegerSym1 i = FromInteger i Source #
data ToRationalSym0 :: kkn ~> (kkd ~> Constraint) Source #
Instances
type Apply (ToRationalSym0 :: TyFun kkn (kkd ~> Constraint) -> Type) (kn :: kkn) Source # | |
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
type Apply (ToRationalSym1 kn :: TyFun Type Constraint -> Type) (kd :: Type) Source # | |
Defined in KindRational |
type ToRationalSym2 kn kd = ToRational kn kd Source #
data ReducedSym0 :: Rational ~> Rational Source #
Instances
type Apply ReducedSym0 (i :: Rational) Source # | |
Defined in KindRational |
type ReducedSym1 i = Reduced i Source #
data ShowLitSym0 :: Rational ~> Symbol Source #
Instances
type Apply ShowLitSym0 (i :: Rational) Source # | |
Defined in KindRational |
type ShowLitSym1 i = ShowLit i Source #
data ShowsLitSym0 :: Rational ~> (Symbol ~> Symbol) Source #
Instances
type Apply ShowsLitSym0 (i :: Rational) Source # | |
Defined in KindRational |
data ShowsLitSym1 :: Rational -> Symbol ~> Symbol Source #
Instances
type Apply (ShowsLitSym1 i :: TyFun Symbol Symbol -> Type) (s :: Symbol) Source # | |
Defined in KindRational |
type ShowsLitSym2 i s = ShowsLit i s Source #
data ShowsPrecLitSym0 :: Natural ~> (Rational ~> (Symbol ~> Symbol)) Source #
Instances
type Apply ShowsPrecLitSym0 (p :: Natural) Source # | |
Defined in KindRational |
data ShowsPrecLitSym2 :: Natural -> Rational -> Symbol ~> Symbol Source #
Instances
type Apply (ShowsPrecLitSym2 p i :: TyFun Symbol Symbol -> Type) (s :: Symbol) Source # | |
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
type Apply IsTerminatingSym0 (i :: Rational) Source # | |
Defined in KindRational |
type IsTerminatingSym1 i = IsTerminating i Source #
data TerminatingSym0 :: Rational ~> Constraint Source #
Instances
type Apply TerminatingSym0 (i :: Rational) Source # | |
Defined in KindRational |
type TerminatingSym1 i = Terminating i Source #
data NonTerminatingSym0 :: Rational ~> Constraint Source #
Instances
type Apply NonTerminatingSym0 (i :: Rational) Source # | |
Defined in KindRational |
type NonTerminatingSym1 i = NonTerminating i Source #
data SignumSym0 :: Rational ~> Integer Source #
Instances
type Apply SignumSym0 (i :: Rational) Source # | |
Defined in KindRational |
type SignumSym1 i = Signum i Source #
data DivRemSym0 :: Round ~> (Rational ~> (Integer, Rational)) Source #
Instances
type Apply DivRemSym0 (a :: Round) Source # | |
Defined in KindRational |
data DivRemSym1 :: Round -> Rational ~> (Integer, Rational) Source #
Instances
type Apply (DivRemSym1 a :: TyFun Rational (Integer, Rational) -> Type) (b :: Rational) Source # | |
Defined in KindRational type Apply (DivRemSym1 a :: TyFun Rational (Integer, Rational) -> Type) (b :: Rational) = DivRemSym2 a b |
type DivRemSym2 a b = DivRem a b Source #
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 ... #