Data.TypeNums.Rats

Type level rational numbers expressed as a ratio between a type-level integer and a type-level natural. For example Neg 3 :% 2.

See also: Data.TypeInts

Documentation

data Rat

Type constructor for a rational

Constructors

k :% Nat

Instances

(KnownInt k n, KnownNat d, (/=) Nat d 0) => KnownRat Rat ((:%) k n d)

Methods

ratSing :: SRat ((k :% n) d) r

TypeError Constraint (Text "Denominator must not equal 0") => KnownRat Rat ((:%) k n 0)

Methods

ratSing :: SRat ((k :% n) 0) r

class KnownRat r

This class gives the (value-level) rational associated with a type-level rational. There are instances of this class for every combination of a concrete integer and concrete natural.

Minimal complete definition

ratSing

Instances

KnownInt k n => KnownRat k n

Methods

ratSing :: SRat n r

(KnownInt k n, KnownNat d, (/=) Nat d 0) => KnownRat Rat ((:%) k n d)

Methods

ratSing :: SRat ((k :% n) d) r

TypeError Constraint (Text "Denominator must not equal 0") => KnownRat Rat ((:%) k n 0)

Methods

ratSing :: SRat ((k :% n) 0) r

ratVal :: forall proxy r. KnownRat r => proxy r -> Rational

Get the value associated with a type-level rational

ratVal' :: forall r. KnownRat r => Proxy# r -> Rational

Get the value associated with a type-level rational. The difference between this function and ratVal is that it takes a Proxy# parameter, which has zero runtime representation and so is entirely free.