KindRational

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 the same as the ones for type-level Naturals in GHC.TypeNats as of base-4.18, and it will continue to evolve together with base, trying to follow its core API as much as possible until the day base provides its own type-level rationals, making this module redundant.

Rational kind

data Rational

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 is also 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. Additionally, a KindRational's Rational can fully represent the internal structure of a type-level Rational. For these reasons, functions like fromSRational and withSomeSRational deal with it, rather than with Prelude's Rational.

Instances

Read Rational

Same as Prelude Rational.

Defined in KindRational

Methods

readsPrec :: Int -> ReadS Rational

readList :: ReadS [Rational]

readPrec :: ReadPrec Rational

readListPrec :: ReadPrec [Rational]

Show Rational

Same as Prelude Rational.

Defined in KindRational

Methods

showsPrec :: Int -> Rational -> ShowS

show :: Rational -> String

showList :: [Rational] -> ShowS

Eq Rational

Arithmethic equality. That is, \(\frac{1}{2} == \frac{2}{4}\).

Defined in KindRational

Methods

(==) :: Rational -> Rational -> Bool

(/=) :: Rational -> Rational -> Bool

Ord Rational

Defined in KindRational

Methods

compare :: Rational -> Rational -> Ordering

(<) :: Rational -> Rational -> Bool

(<=) :: Rational -> Rational -> Bool

(>) :: Rational -> Rational -> Bool

(>=) :: Rational -> Rational -> Bool

max :: Rational -> Rational -> Rational

min :: Rational -> Rational -> Rational

SingKind Rational

Demote refers to KindRational's Rational rather than Prelude's Rational so that the SRational's internal representation is preserved. Use toPrelude and fromPrelude as necessary.

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

Note that this checks for type equality, not arithmetic equality. That is, P 1 % 2 and P 2 % 4 are not equal types, even if they are arithmetically equal.

Defined in KindRational

Methods

(%~) :: forall (a :: Rational) (b :: Rational). Sing a -> Sing b -> Decision (a :~: b)

TestCoercion SRational

Note that this checks for type equality, not arithmetic equality. That is, P 1 % 2 and P 2 % 4 are not equal types, even if they are arithmetically equal.

Defined in KindRational

Methods

testCoercion :: forall (a :: k) (b :: k). SRational a -> SRational b -> Maybe (Coercion a b)

TestEquality SRational

Note that this checks for type equality, not arithmetic equality. That is, P 1 % 2 and P 2 % 4 are not equal types, even if they are arithmetically equal.

Defined in KindRational

Methods

testEquality :: forall (a :: k) (b :: k). SRational a -> SRational b -> Maybe (a :~: b)

KnownRational r => SingI (r :: Rational)

Defined in KindRational

Methods

sing :: Sing r

type Demote Rational

Defined in KindRational

type Demote Rational = Rational

type Sing

Defined in KindRational

type Sing = SRational

type Compare (a :: Rational) (b :: Rational)

Data.Type.Ord support for type-level Rationals.

Defined in KindRational

type Compare (a :: Rational) (b :: Rational) = CmpRational a b

type (%) (n :: Integer) (d :: Natural) = n :% d :: Rational

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.

type family n / d :: Rational where ... infixl 7

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.

Equations

(n :: Natural) / (d :: Natural) = Normalize (P n % d)

(n :: Natural) / (P d :: Integer) = Normalize (P n % d)

(n :: Natural) / (N d :: Integer) = Normalize (N n % d)

(n :: Natural) / (d :: Rational) = (P n % 1) * Recip d

(i :: Integer) / (d :: Natural) = Normalize (i % d)

(P n :: Integer) / (P d :: Integer) = Normalize (P n % d)

(N n :: Integer) / (N d :: Integer) = Normalize (P n % d)

(P n :: Integer) / (N d :: Integer) = Normalize (N n % d)

(N n :: Integer) / (P d :: Integer) = Normalize (N n % d)

(n :: Integer) / (d :: Rational) = (n % 1) * Recip d

(n :: Rational) / (d :: Natural) = n * Recip (P d % 1)

(n :: Rational) / (d :: Integer) = n * Recip (d % 1)

(n :: Rational) / (d :: Rational) = n * Recip d

type family Normalize (r :: Rational) :: Rational where ...

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.

Equations

Normalize (_ % 0) = TypeError ('Text "KindRational: Denominator is zero")

Normalize (P 0 % _) = P 0 % 1

Normalize (N 0 % _) = P 0 % 1

Normalize (P n % d) = P (Div n (GCD n d)) % Div d (GCD n d)

Normalize (N n % d) = N (Div n (GCD n d)) % Div d (GCD n d)

type Num (r :: Rational) = Num_ (Normalize r) :: Integer

Normalized Numerator of the type-level Rational.

type Den (r :: Rational) = Den_ (Normalize r) :: Natural

Normalized Denominator of the type-level Rational.

rational :: (Integral num, Integral den) => num -> den -> Maybe 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.

fromPrelude :: Rational -> Maybe Rational

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

toPrelude :: Rational -> Rational

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

fromPrelude . toPrelude == Just

showsPrecTypeLit :: Int -> Rational -> ShowS

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"

Types ⇔ Terms

class KnownRational (r :: Rational) where

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

Methods

rationalSing :: SRational r

Instances

(Normalize r ~ (n % d), KnownInteger (Num_ r), KnownNat (Den_ r)) => KnownRational r

This instance checks that r Normalizes, but the obtained SRational is not normalized. This is so that SDecide, TestEquality and TestCoercion behave as expected. If you want a Normalized SRational, then use rationalSing @(Normalize r).

Defined in KindRational

Methods

rationalSing :: SRational r

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

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

data SomeRational

This type represents unknown type-level Rational.

Constructors

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

Instances

Read SomeRational

Defined in KindRational

Methods

readsPrec :: Int -> ReadS SomeRational

readList :: ReadS [SomeRational]

readPrec :: ReadPrec SomeRational

readListPrec :: ReadPrec [SomeRational]

Show SomeRational

Defined in KindRational

Methods

showsPrec :: Int -> SomeRational -> ShowS

show :: SomeRational -> String

showList :: [SomeRational] -> ShowS

Eq SomeRational

Arithmethic equality. That is, \(\frac{1}{2} == \frac{2}{4}\).

Defined in KindRational

Methods

(==) :: SomeRational -> SomeRational -> Bool

(/=) :: SomeRational -> SomeRational -> Bool

Ord SomeRational

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

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

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

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

Singletons

data SRational (r :: Rational)

Singleton type for a type-level Rational r.

Instances

TestCoercion SRational

Note that this checks for type equality, not arithmetic equality. That is, P 1 % 2 and P 2 % 4 are not equal types, even if they are arithmetically equal.

Defined in KindRational

Methods

testCoercion :: forall (a :: k) (b :: k). SRational a -> SRational b -> Maybe (Coercion a b)

TestEquality SRational

Note that this checks for type equality, not arithmetic equality. That is, P 1 % 2 and P 2 % 4 are not equal types, even if they are arithmetically equal.

Defined in KindRational

Methods

testEquality :: forall (a :: k) (b :: k). SRational a -> SRational b -> Maybe (a :~: b)

Show (SRational r)

Defined in KindRational

Methods

showsPrec :: Int -> SRational r -> ShowS

show :: SRational r -> String

showList :: [SRational r] -> ShowS

pattern SRational :: forall r. () => KnownRational r => SRational 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 -}

fromSRational :: SRational r -> Rational

Return the term-level KindRational Rational number corresponding to r in a SRational r value. This Rational is not Normalized.

withSomeSRational :: forall rep (a :: TYPE rep). Rational -> (forall r. SRational r -> a) -> a

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

withKnownRational :: forall r rep (a :: TYPE rep). SRational r -> (KnownRational r => a) -> a

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

Arithmethic

type (+) (a :: Rational) (b :: Rational) = Add_ (Normalize a) (Normalize b) :: Rational infixl 6

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

type * (a :: Rational) (b :: Rational) = Mul_ (Normalize a) (Normalize b) :: Rational infixl 7

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

type (-) (a :: Rational) (b :: Rational) = a + Negate b :: Rational infixl 6

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

type family Negate (r :: Rational) :: Rational where ...

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

Equations

Negate (P n % d) = Normalize (N n % d)

Negate (N n % d) = Normalize (P n % d)

type Sign (r :: Rational) = Sign (Num r) :: Integer

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

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

type Abs (r :: Rational) = Normalize (P (Abs (Num_ r)) % Den_ r) :: Rational

Absolute value of a type-level Rational.

type Recip (a :: Rational) = Recip_ (Normalize a) :: Rational

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

type Div (r :: Round) (a :: Rational) = Div_ r (Normalize a) :: Integer

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.

div :: Round -> Rational -> Integer

Term-level version of Div.

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

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

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

rem :: Round -> Rational -> Rational

Term-level version of Rem.

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

type DivRem (r :: Round) (a :: Rational) = DivRem_ r (Normalize a) :: (Integer, 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)

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

Term-level version of DivRem.

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

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

data Round

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

Bounded Round

Defined in KindInteger

Methods

minBound :: Round

maxBound :: Round

Enum Round

Defined in KindInteger

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

Defined in KindInteger

Methods

readsPrec :: Int -> ReadS Round

readList :: ReadS [Round]

readPrec :: ReadPrec Round

readListPrec :: ReadPrec [Round]

Show Round

Defined in KindInteger

Methods

showsPrec :: Int -> Round -> ShowS

show :: Round -> String

showList :: [Round] -> ShowS

Eq Round

Defined in KindInteger

Methods

(==) :: Round -> Round -> Bool

(/=) :: Round -> Round -> Bool

Ord Round

Defined in KindInteger

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

Decimals

class (KnownRational r, Terminates r ~ True) => Terminating (r :: Rational)

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

Instances

(KnownRational r, Terminates r ~ 'True, If (Terminates r) () (TypeError ((('Text "\8216" ':<>: 'ShowType r) ':<>: 'Text "\8217 is not a terminating ") ':<>: 'ShowType Rational) :: Constraint)) => Terminating r

Defined in KindRational

withTerminating :: forall r a. KnownRational r => (Terminating r => a) -> Maybe a

type Terminates (r :: Rational) = Terminates_ (Den r) :: Bool

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

terminates :: Rational -> Bool

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

Comparisons

type CmpRational (a :: Rational) (b :: Rational) = CmpRational_ (Normalize a) (Normalize b) :: Ordering

Comparison of type-level Rationals, as a function.

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

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

eqRationalRep :: Rational -> Rational -> Bool

Whether the internal representation of the Rationals are equal.

Note that this is not the same as (==). Use (==) unless you know what you are doing.

Extra

This stuff should be exported by the Data.Type.Ord module.

type (==?) (a :: k) (b :: k) = OrdCond (Compare a b) 'False 'True 'False infixr 4

This should be exported by Data.Type.Ord.

type (==) (a :: k) (b :: k) = (a ==? b) ~ 'True infixr 4

This should be exported by Data.Type.Ord.

type (/=?) (a :: k) (b :: k) = OrdCond (Compare a b) 'True 'False 'True infixr 4

This should be exported by Data.Type.Ord.

type (/=) (a :: k) (b :: k) = (a /=? b) ~ 'True infixr 4

This should be exported by Data.Type.Ord.