Time.Rational

This module introduces Rat kind and all necessary functional.

Documentation

data Rat

Data structure represents the rational number. Rational number can be represented as a pair of natural numbers n and m where m is nor equal to zero.

Constructors

Nat ::% Nat

Instances

SeriesP ([] :: [Rat])

Defined in Time.Series

Methods

seriesP :: KnownRatName someUnit => String -> Maybe (Time someUnit)

SeriesF ([] :: [Rat])

Defined in Time.Series

Methods

seriesF :: KnownRatName someUnit => Time someUnit -> String

(KnownRatName unit, SeriesP (nextUnit ': units), DescendingConstraint (IsDescending (unit ': (nextUnit ': units)))) => SeriesP (unit ': (nextUnit ': units))

Defined in Time.Series

Methods

seriesP :: KnownRatName someUnit => String -> Maybe (Time someUnit)

KnownRatName unit => SeriesP (unit ': ([] :: [Rat]))

Defined in Time.Series

Methods

seriesP :: KnownRatName someUnit => String -> Maybe (Time someUnit)

(KnownRatName unit, SeriesF (nextUnit ': units), DescendingConstraint (IsDescending (unit ': (nextUnit ': units)))) => SeriesF (unit ': (nextUnit ': units))

Defined in Time.Series

Methods

seriesF :: KnownRatName someUnit => Time someUnit -> String

KnownRatName unit => SeriesF (unit ': ([] :: [Rat]))

Defined in Time.Series

Methods

seriesF :: KnownRatName someUnit => Time someUnit -> String

type DivK Nat Rat

Defined in Time.Rational

type DivK Nat Rat = Rat

type DivK Rat Nat

Defined in Time.Rational

type DivK Rat Nat = Rat

type DivK Rat Rat

Defined in Time.Rational

type DivK Rat Rat = Rat

type MulK Nat Rat

Defined in Time.Rational

type MulK Nat Rat = Rat

type MulK Rat Nat

Defined in Time.Rational

type MulK Rat Nat = Rat

type MulK Rat Rat

Defined in Time.Rational

type MulK Rat Rat = Rat

type (a :: Nat) / (b :: Rat)

Defined in Time.Rational

type (a :: Nat) / (b :: Rat) = DivRat (a :% 1) b

type (a :: Rat) / (b :: Nat)

Defined in Time.Rational

type (a :: Rat) / (b :: Nat)

type (a :: Rat) / (b :: Rat)

Defined in Time.Rational

type (a :: Rat) / (b :: Rat) = DivRat a b

type (a :: Nat) * (b :: Rat)

Defined in Time.Rational

type (a :: Nat) * (b :: Rat)

type (a :: Rat) * (b :: Nat)

Defined in Time.Rational

type (a :: Rat) * (b :: Nat)

type (a :: Rat) * (b :: Rat)

Defined in Time.Rational

type (a :: Rat) * (b :: Rat)

type (:%) = (::%)

More convenient name for promoted constructor of Rat.

type family (m :: Nat) % (n :: Nat) :: Rat where ... infixl 7

Type family for normalized pair of Nats — Rat.

Equations

a % b = Normalize (a :% b)

type family (a :: k1) * (b :: k2) :: MulK k1 k2

Overloaded multiplication.

Instances

type (a :: Nat) * (b :: Nat)

Defined in Time.Rational

type (a :: Nat) * (b :: Nat) = a * b

type (a :: Nat) * (b :: Rat)

Defined in Time.Rational

type (a :: Nat) * (b :: Rat)

type (a :: Rat) * (b :: Nat)

Defined in Time.Rational

type (a :: Rat) * (b :: Nat)

type (a :: Rat) * (b :: Rat)

Defined in Time.Rational

type (a :: Rat) * (b :: Rat)

type family (a :: k1) / (b :: k2) :: DivK k1 k2

Overloaded division.

Instances

type (a :: Nat) / (b :: Nat)

Defined in Time.Rational

type (a :: Nat) / (b :: Nat) = a % b

type (a :: Nat) / (b :: Rat)

Defined in Time.Rational

type (a :: Nat) / (b :: Rat) = DivRat (a :% 1) b

type (a :: Rat) / (b :: Nat)

Defined in Time.Rational

type (a :: Rat) / (b :: Nat)

type (a :: Rat) / (b :: Rat)

Defined in Time.Rational

type (a :: Rat) / (b :: Rat) = DivRat a b

type family MulK (k1 :: Type) (k2 :: Type) :: Type

The result kind of overloaded multiplication.

Instances

type MulK Nat Nat

Defined in Time.Rational

type MulK Nat Nat = Nat

type MulK Nat Rat

Defined in Time.Rational

type MulK Nat Rat = Rat

type MulK Rat Nat

Defined in Time.Rational

type MulK Rat Nat = Rat

type MulK Rat Rat

Defined in Time.Rational

type MulK Rat Rat = Rat

type family DivK (k1 :: Type) (k2 :: Type) :: Type

The result kind of overloaded division.

Instances

type DivK Nat Nat

Defined in Time.Rational

type DivK Nat Nat = Rat

type DivK Nat Rat

Defined in Time.Rational

type DivK Nat Rat = Rat

type DivK Rat Nat

Defined in Time.Rational

type DivK Rat Nat = Rat

type DivK Rat Rat

Defined in Time.Rational

type DivK Rat Rat = Rat

type family Gcd (m :: Nat) (n :: Nat) :: Nat where ...

Greatest common divisor for type-level naturals.

Example:

>>> :kind! Gcd 9 11
Gcd 9 11 :: Nat
= 1

>>> :kind! Gcd 9 12
Gcd 9 12 :: Nat
= 3

Equations

Gcd a 0 = a

Gcd a b = Gcd b (a `Mod` b)

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

Normalization of type-level rational.

Example:

>>> :kind! Normalize (9 % 11)
Normalize (9 % 11) :: Rat
= 9 :% 11

>>> :kind! Normalize (9 % 12)
Normalize (9 % 12) :: Rat
= 3 :% 4

Equations

Normalize (a :% b) = (a `Div` Gcd a b) :% (b `Div` Gcd a b)

type family DivRat (m :: Rat) (n :: Rat) :: Rat where ...

Division of type-level rationals.

If there are Rat with Nats a and b and another Rat with c d then the following formula should be applied: \[ \frac{a}{b} / \frac{c}{d} = \frac{a * d}{b * c} \]

Example:

>>> :kind! DivRat (9 % 11) (9 % 11)
DivRat (9 % 11) (9 % 11) :: Rat
= 1 :% 1

Equations

DivRat (a :% b) (c :% d) = (a * d) % (b * c)

type family (m :: Rat) >=% (n :: Rat) :: Bool where ... infix 4

Comparison of type-level rationals, as a function.

>>> :kind! (1 :% 42) >=% (5 :% 42)
(1 :% 42) >=% (5 :% 42) :: Bool
= 'False

>>> :kind! (5 :% 42) >=% (1 :% 42)
(5 :% 42) >=% (1 :% 42) :: Bool
= 'True

>>> :kind! (42 :% 1) >=% (42 :% 1)
(42 :% 1) >=% (42 :% 1) :: Bool
= 'True

Equations

(a :% b) >=% (c :% d) = (c * b) <=? (a * d)

type RatioNat = Ratio Natural

Rational numbers, with numerator and denominator of Natural type.

class KnownRat (r :: Rat) where

This class gives the integer associated with a type-level rational.

Minimal complete definition

ratVal

Methods

ratVal :: RatioNat

Instances

(KnownNat a, KnownNat b) => KnownRat (a :% b)

Defined in Time.Rational

Methods

ratVal :: RatioNat

withRuntimeDivRat :: forall (a :: Rat) (b :: Rat) r. (KnownRat a, KnownRat b) => (KnownRat (a / b) => r) -> r

Performs action with introduced DivRat constraint for rational numbers.

type KnownDivRat a b = (KnownRat a, KnownRat b, KnownRat (a / b))

Constraint alias for DivRat units.