Modulebasement-0.0.16Haskell2010

Basement.Bounded

Types to represent ℤ/nℤ.

ℤ/nℤ is a finite field and is defined as the set of natural number: {0, 1, ..., n − 1}.

2 types
6 values

Packagebasement-0.0.16
Exports8
LanguageHaskell2010
LicenceBSD-3-Clause
SourceBounded.hs

newtypenewtype Zn64 (n :: Nat)

A type level bounded natural backed by a Word64

Instances20Eq, Num, Ord, Show, Additive, Subtractive, …

Eq (Zn64 n)Defined in basement-0.0.16 · Basement.Bounded
(KnownNat n, NatWithinBound Word64 n) => Num (Zn64 n)Defined in basement-0.0.16 · Basement.Bounded
Ord (Zn64 n)Defined in basement-0.0.16 · Basement.Bounded
Show (Zn64 n)Defined in basement-0.0.16 · Basement.Bounded
(KnownNat n, NatWithinBound Word64 n) => Additive (Zn64 n)Defined in basement-0.0.16 · Basement.Numerical.Additive
(KnownNat n, NatWithinBound Word64 n) => Subtractive (Zn64 n)Defined in basement-0.0.16 · Basement.Numerical.Subtractive
(KnownNat n, NatWithinBound Word64 n) => Integral (Zn64 n)Defined in basement-0.0.16 · Basement.Bounded
(KnownNat n, NatWithinBound Word64 n) => IsNatural (Zn64 n)Defined in basement-0.0.16 · Basement.Bounded
(KnownNat n, NatWithinBound Word64 n) => IsIntegral (Zn64 n)Defined in basement-0.0.16 · Basement.Bounded
NormalForm (Zn64 n)Defined in basement-0.0.16 · Basement.NormalForm
From (Zn64 n) Word128Defined in basement-0.0.16 · Basement.From
From (Zn64 n) Word256Defined in basement-0.0.16 · Basement.From
From (Zn64 n) Word64Defined in basement-0.0.16 · Basement.From
(KnownNat n, NatWithinBound Word16 n) => From (Zn64 n) Word16Defined in basement-0.0.16 · Basement.From
(KnownNat n, NatWithinBound Word32 n) => From (Zn64 n) Word32Defined in basement-0.0.16 · Basement.From
(KnownNat n, NatWithinBound Word8 n) => From (Zn64 n) Word8Defined in basement-0.0.16 · Basement.From
KnownNat n => From (Zn64 n) (Zn n)Defined in basement-0.0.16 · Basement.From
(KnownNat n, NatWithinBound Word64 n) => From (Zn n) (Zn64 n)Defined in basement-0.0.16 · Basement.From
type Difference (Zn64 n) = Zn64 nDefined in basement-0.0.16 · Basement.Numerical.Subtractive
type NatNumMaxBound (Zn64 n) = nDefined in basement-0.0.16 · Basement.Bounded

valueunZn64 :: Zn64 n -> Word64

newtypenewtype Zn (n :: Nat)

A type level bounded natural

Instances20Eq, Num, Ord, Show, Additive, Subtractive, …

Eq (Zn n)Defined in basement-0.0.16 · Basement.Bounded
KnownNat n => Num (Zn n)Defined in basement-0.0.16 · Basement.Bounded
Ord (Zn n)Defined in basement-0.0.16 · Basement.Bounded
Show (Zn n)Defined in basement-0.0.16 · Basement.Bounded
KnownNat n => Additive (Zn n)Defined in basement-0.0.16 · Basement.Numerical.Additive
KnownNat n => Subtractive (Zn n)Defined in basement-0.0.16 · Basement.Numerical.Subtractive
KnownNat n => Integral (Zn n)Defined in basement-0.0.16 · Basement.Bounded
KnownNat n => IsNatural (Zn n)Defined in basement-0.0.16 · Basement.Bounded
KnownNat n => IsIntegral (Zn n)Defined in basement-0.0.16 · Basement.Bounded
NormalForm (Zn n)Defined in basement-0.0.16 · Basement.NormalForm
(KnownNat n, NatWithinBound Word128 n) => From (Zn n) Word128Defined in basement-0.0.16 · Basement.From
(KnownNat n, NatWithinBound Word256 n) => From (Zn n) Word256Defined in basement-0.0.16 · Basement.From
(KnownNat n, NatWithinBound Word16 n) => From (Zn n) Word16Defined in basement-0.0.16 · Basement.From
(KnownNat n, NatWithinBound Word32 n) => From (Zn n) Word32Defined in basement-0.0.16 · Basement.From
(KnownNat n, NatWithinBound Word64 n) => From (Zn n) Word64Defined in basement-0.0.16 · Basement.From
(KnownNat n, NatWithinBound Word8 n) => From (Zn n) Word8Defined in basement-0.0.16 · Basement.From
KnownNat n => From (Zn64 n) (Zn n)Defined in basement-0.0.16 · Basement.From
(KnownNat n, NatWithinBound Word64 n) => From (Zn n) (Zn64 n)Defined in basement-0.0.16 · Basement.From
type Difference (Zn n) = Zn nDefined in basement-0.0.16 · Basement.Numerical.Subtractive
type NatNumMaxBound (Zn n) = nDefined in basement-0.0.16 · Basement.Bounded

valueunZn :: Zn n -> Natural

valuezn64 :: (KnownNat n, NatWithinBound Word64 n) => Word64 -> Zn64 n

Create an element of ℤ/nℤ from a Word64

If the value is greater than n, then the value is normalized by using the integer modulus n

valuezn :: KnownNat n => Natural -> Zn n

Create an element of ℤ/nℤ from a Natural.

If the value is greater than n, then the value is normalized by using the integer modulus n

valuezn64Nat

:: (KnownNat m, KnownNat n, NatWithinBound Word64 m, NatWithinBound Word64 n, CmpNat m n ~ 'LT)
=> Proxy m
-> Zn64 n

Create an element of ℤ/nℤ from a type level Nat

valueznNat :: (KnownNat m, KnownNat n, CmpNat m n ~ 'LT) => Proxy m -> Zn n

Create an element of ℤ/nℤ from a type level Nat