Type-level version of Rational. Use / to construct one, use % to pattern-match on it.

Rational is mostly used as a kind, with its types constructed using /. However, it might also be used as type, with its terms constructed using rational or fromPrelude. One reason why you may want a Rational at the term-level is so that you embed it in larger data-types (for example, this Rational embeds the Integer similarly offered by the KindInteger module). But perhaps more importantly, this Rational offers better safety than the Rational from Prelude, since it's not possible to construct one with a zero denominator, or so large that operating with it would exhaust system resources. Notwithstanding this, for ergonomic reasons, all of the functions exported by this module take Prelude Rationals as input and produce Prelude Rationals as outputs. Internally, however, the beforementioned checks are always performed, and fail with throw if necessary. If you want to be sure those errors never happen, just filter your Prelude Rationals with fromPrelude. In practice, it's very unlikely that you will be affected by this unless if you are unsafelly constructing Prelude Rationals.

Pattern-match on a type-level Rational.

NB: When constructing a Rational number, prefer to use /, which not only accepts more polymorphic inputs, but also Normalizes the type-level Rational. Also note that while n % 0 is a valid type, all tools in the KindRational will reject such input.

n/d constructs and Normalizes 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.

Normalize a type-level Rational so that a 0 denominator fails to type-check, and that the Numerator and denominator have no common factors.

Only Normalized Rationals can be reliably constrained for equality using ~.

All of the functions in the KindRational module accept both Normalized and non-Normalized inputs, but they always produce Normalized output.

Normalized Numerator of the type-level Rational.

Normalized Denominator of the type-level Rational.

Make a term-level KindRational Rational number, provided that the numerator is not 0, and that its numerator and denominator are not so large that they would exhaust system resources. The Rational is Normalized.

Try to obtain a term-level KindRational Rational from a term-level Prelude Rational. This can fail if the Prelude Rational is infinite, or if it is so big that it would exhaust system resources.

fromPrelude . toPrelude      == Just
fmap toPrelude . fromPrelude == Just

Convert a term-level KindRational Rational into a term-level Prelude Rational.

fromPrelude . toPrelude      == Just
fmap toPrelude . fromPrelude == Just

Shows the Rational as it appears literally at the type-level.

This is remerent from normal show for Rational, which shows the term-level value.

shows            0 (rationalVal (Proxy @(1/2))) "z" == "1 % 2z"
showsPrecTypeLit 0 (rationalVal (Proxy @(1/2))) "z" == "P 1 % 2z"

This class gives the rational associated with a type-level rational. There are instances of the class for every rational.

Term-level Prelude Rational representation of the type-level Rational r.

This type represents unknown type-level Rational.

Convert a term-level Prelude Rational into an unknown type-level Rational.

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

Singleton type for a type-level Rational r.

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

Return the term-level Prelude Rational number corresponding to r in a SRational r value.

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

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

a + b adds type-level Rationals a and b.

a * b multiplies type-level Rationals a and b.

a - b subtracts the type-level Rational b from the type-level Rational a.

Negate a type-level Rational. Also known as additive inverse.

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

• P 0 if zero.
• P 1 if positive.
• N 1 if negative.

Absolute value of a type-level Rational.

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

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).
  (Den a /= 0) =>
    Rem r a  ==  a - Div r a % 1

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

Term-level version of Div.

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

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

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

Term-level version of Rem.

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

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).
  (Den a /= 0) =>
    DivRem r a  ==  '(Div r a, Rem r a)

Term-level version of DivRem.

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

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

Constraint version of Terminates r. Satisfied by all type-level Rationals that can be represented as a finite decimal number.

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

Term-level version of the Terminates function. Takes a Prelude Rational as input.

Comparison of type-level Rationals, as a function.

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

This should be exported by Data.Type.Ord.

This should be exported by Data.Type.Ord.

This should be exported by Data.Type.Ord.

This should be exported by Data.Type.Ord.