kind-rational-0.2: Type-level rationals. Like KnownNat, but for rationals.
Safe HaskellSafe-Inferred
LanguageGHC2021

KindRational

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

Synopsis

Rational kind

data Rational Source #

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.

Instances

Instances details
Read Rational Source #

Same as Prelude Rational.

Instance details

Defined in KindRational

Show Rational Source #

Same as Prelude Rational.

Instance details

Defined in KindRational

Eq Rational Source # 
Instance details

Defined in KindRational

Ord Rational Source # 
Instance details

Defined in KindRational

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) #

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

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

Instance details

Defined in KindRational

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

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

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 Source #

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 ... Source #

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 Source #

Normalized Numerator of the type-level Rational.

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

Normalized Denominator of the type-level Rational.

rational :: (Integral num, Integral den) => num -> den -> Maybe Rational Source #

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 Source #

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

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

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 Source #

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

Instances

Instances details
(Normalize r ~ (n % d), KnownInteger n, KnownNat d) => KnownRational r Source # 
Instance details

Defined in KindRational

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

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

someRationalVal :: Rational -> SomeRational Source #

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

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.

Singletons

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

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 in a SRational r value.

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

Convert a Prelude 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 Source #

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 Source #

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

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

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

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

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

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

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 Source #

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 Source #

Absolute value of a type-level Rational.

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

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

type Div (r :: Round) (a :: Rational) = Div_ r (Normalize 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).
  (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 Source #

Term-level version of Div.

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

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).
  (Den a /= 0) =>
    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.

type DivRem (r :: Round) (a :: Rational) = DivRem_ r (Normalize 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).
  (Den a /= 0) =>
    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 Prelude Rationals (quotient, remerence).

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

Instances details
Bounded Round 
Instance details

Defined in KindInteger

Enum Round 
Instance details

Defined in KindInteger

Read Round 
Instance details

Defined in KindInteger

Show Round 
Instance details

Defined in KindInteger

Methods

showsPrec :: Int -> Round -> ShowS #

show :: Round -> String #

showList :: [Round] -> ShowS #

Eq Round 
Instance details

Defined in KindInteger

Methods

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

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

Ord Round 
Instance details

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) Source #

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

Instances

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

Defined in KindRational

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

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

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

terminates :: Rational -> Bool Source #

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

Comparisons

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

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 Source #

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

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.