basement-0.0.16: Foundation scrap box of array & string
LicenseBSD-style
MaintainerHaskell Foundation
Safe HaskellSafe-Inferred
LanguageHaskell2010

Basement.Bounded

Description

Types to represent ℤ/nℤ.

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

Synopsis

Documentation

data Zn64 (n :: Nat) Source #

A type level bounded natural backed by a Word64

Instances

Instances details
(KnownNat n, NatWithinBound Word64 n) => Num (Zn64 n) Source # 
Instance details

Defined in Basement.Bounded

Methods

(+) :: Zn64 n -> Zn64 n -> Zn64 n #

(-) :: Zn64 n -> Zn64 n -> Zn64 n #

(*) :: Zn64 n -> Zn64 n -> Zn64 n #

negate :: Zn64 n -> Zn64 n #

abs :: Zn64 n -> Zn64 n #

signum :: Zn64 n -> Zn64 n #

fromInteger :: Integer -> Zn64 n #

Show (Zn64 n) Source # 
Instance details

Defined in Basement.Bounded

Methods

showsPrec :: Int -> Zn64 n -> ShowS #

show :: Zn64 n -> String #

showList :: [Zn64 n] -> ShowS #

(KnownNat n, NatWithinBound Word64 n) => Integral (Zn64 n) Source # 
Instance details

Defined in Basement.Bounded

NormalForm (Zn64 n) Source # 
Instance details

Defined in Basement.NormalForm

Methods

toNormalForm :: Zn64 n -> () Source #

(KnownNat n, NatWithinBound Word64 n) => Additive (Zn64 n) Source # 
Instance details

Defined in Basement.Numerical.Additive

Methods

azero :: Zn64 n Source #

(+) :: Zn64 n -> Zn64 n -> Zn64 n Source #

scale :: IsNatural n0 => n0 -> Zn64 n -> Zn64 n Source #

(KnownNat n, NatWithinBound Word64 n) => IsIntegral (Zn64 n) Source # 
Instance details

Defined in Basement.Bounded

Methods

toInteger :: Zn64 n -> Integer Source #

(KnownNat n, NatWithinBound Word64 n) => IsNatural (Zn64 n) Source # 
Instance details

Defined in Basement.Bounded

Methods

toNatural :: Zn64 n -> Natural Source #

(KnownNat n, NatWithinBound Word64 n) => Subtractive (Zn64 n) Source # 
Instance details

Defined in Basement.Numerical.Subtractive

Associated Types

type Difference (Zn64 n) Source #

Methods

(-) :: Zn64 n -> Zn64 n -> Difference (Zn64 n) Source #

Eq (Zn64 n) Source # 
Instance details

Defined in Basement.Bounded

Methods

(==) :: Zn64 n -> Zn64 n -> Bool #

(/=) :: Zn64 n -> Zn64 n -> Bool #

Ord (Zn64 n) Source # 
Instance details

Defined in Basement.Bounded

Methods

compare :: Zn64 n -> Zn64 n -> Ordering #

(<) :: Zn64 n -> Zn64 n -> Bool #

(<=) :: Zn64 n -> Zn64 n -> Bool #

(>) :: Zn64 n -> Zn64 n -> Bool #

(>=) :: Zn64 n -> Zn64 n -> Bool #

max :: Zn64 n -> Zn64 n -> Zn64 n #

min :: Zn64 n -> Zn64 n -> Zn64 n #

(KnownNat n, NatWithinBound Word16 n) => From (Zn64 n) Word16 Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn64 n -> Word16 Source #

(KnownNat n, NatWithinBound Word32 n) => From (Zn64 n) Word32 Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn64 n -> Word32 Source #

From (Zn64 n) Word64 Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn64 n -> Word64 Source #

(KnownNat n, NatWithinBound Word8 n) => From (Zn64 n) Word8 Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn64 n -> Word8 Source #

From (Zn64 n) Word128 Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn64 n -> Word128 Source #

From (Zn64 n) Word256 Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn64 n -> Word256 Source #

(KnownNat n, NatWithinBound Word64 n) => From (Zn n) (Zn64 n) Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn n -> Zn64 n Source #

KnownNat n => From (Zn64 n) (Zn n) Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn64 n -> Zn n Source #

type NatNumMaxBound (Zn64 n) Source # 
Instance details

Defined in Basement.Bounded

type NatNumMaxBound (Zn64 n) = n
type Difference (Zn64 n) Source # 
Instance details

Defined in Basement.Numerical.Subtractive

type Difference (Zn64 n) = Zn64 n

data Zn (n :: Nat) Source #

A type level bounded natural

Instances

Instances details
KnownNat n => Num (Zn n) Source # 
Instance details

Defined in Basement.Bounded

Methods

(+) :: Zn n -> Zn n -> Zn n #

(-) :: Zn n -> Zn n -> Zn n #

(*) :: Zn n -> Zn n -> Zn n #

negate :: Zn n -> Zn n #

abs :: Zn n -> Zn n #

signum :: Zn n -> Zn n #

fromInteger :: Integer -> Zn n #

Show (Zn n) Source # 
Instance details

Defined in Basement.Bounded

Methods

showsPrec :: Int -> Zn n -> ShowS #

show :: Zn n -> String #

showList :: [Zn n] -> ShowS #

KnownNat n => Integral (Zn n) Source # 
Instance details

Defined in Basement.Bounded

Methods

fromInteger :: Integer -> Zn n Source #

NormalForm (Zn n) Source # 
Instance details

Defined in Basement.NormalForm

Methods

toNormalForm :: Zn n -> () Source #

KnownNat n => Additive (Zn n) Source # 
Instance details

Defined in Basement.Numerical.Additive

Methods

azero :: Zn n Source #

(+) :: Zn n -> Zn n -> Zn n Source #

scale :: IsNatural n0 => n0 -> Zn n -> Zn n Source #

KnownNat n => IsIntegral (Zn n) Source # 
Instance details

Defined in Basement.Bounded

Methods

toInteger :: Zn n -> Integer Source #

KnownNat n => IsNatural (Zn n) Source # 
Instance details

Defined in Basement.Bounded

Methods

toNatural :: Zn n -> Natural Source #

KnownNat n => Subtractive (Zn n) Source # 
Instance details

Defined in Basement.Numerical.Subtractive

Associated Types

type Difference (Zn n) Source #

Methods

(-) :: Zn n -> Zn n -> Difference (Zn n) Source #

Eq (Zn n) Source # 
Instance details

Defined in Basement.Bounded

Methods

(==) :: Zn n -> Zn n -> Bool #

(/=) :: Zn n -> Zn n -> Bool #

Ord (Zn n) Source # 
Instance details

Defined in Basement.Bounded

Methods

compare :: Zn n -> Zn n -> Ordering #

(<) :: Zn n -> Zn n -> Bool #

(<=) :: Zn n -> Zn n -> Bool #

(>) :: Zn n -> Zn n -> Bool #

(>=) :: Zn n -> Zn n -> Bool #

max :: Zn n -> Zn n -> Zn n #

min :: Zn n -> Zn n -> Zn n #

(KnownNat n, NatWithinBound Word16 n) => From (Zn n) Word16 Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn n -> Word16 Source #

(KnownNat n, NatWithinBound Word32 n) => From (Zn n) Word32 Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn n -> Word32 Source #

(KnownNat n, NatWithinBound Word64 n) => From (Zn n) Word64 Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn n -> Word64 Source #

(KnownNat n, NatWithinBound Word8 n) => From (Zn n) Word8 Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn n -> Word8 Source #

(KnownNat n, NatWithinBound Word128 n) => From (Zn n) Word128 Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn n -> Word128 Source #

(KnownNat n, NatWithinBound Word256 n) => From (Zn n) Word256 Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn n -> Word256 Source #

(KnownNat n, NatWithinBound Word64 n) => From (Zn n) (Zn64 n) Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn n -> Zn64 n Source #

KnownNat n => From (Zn64 n) (Zn n) Source # 
Instance details

Defined in Basement.From

Methods

from :: Zn64 n -> Zn n Source #

type NatNumMaxBound (Zn n) Source # 
Instance details

Defined in Basement.Bounded

type NatNumMaxBound (Zn n) = n
type Difference (Zn n) Source # 
Instance details

Defined in Basement.Numerical.Subtractive

type Difference (Zn n) = Zn n

zn64 :: forall n. (KnownNat n, NatWithinBound Word64 n) => Word64 -> Zn64 n Source #

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

zn :: forall n. KnownNat n => Natural -> Zn n Source #

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

zn64Nat :: forall m n. (KnownNat m, KnownNat n, NatWithinBound Word64 m, NatWithinBound Word64 n, CmpNat m n ~ 'LT) => Proxy m -> Zn64 n Source #

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

znNat :: forall m n. (KnownNat m, KnownNat n, CmpNat m n ~ 'LT) => Proxy m -> Zn n Source #

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