Copyright	(C) 2015-2022 mniip
License	BSD3
Maintainer	mniip <mniip@mniip.com>
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Finite

Description

Synopsis

data Finite (n :: Nat )
packFinite :: KnownNat n => Integer -> Maybe ( Finite n)
packFiniteProxy :: KnownNat n => proxy n -> Integer -> Maybe ( Finite n)
finite :: KnownNat n => Integer -> Finite n
finiteProxy :: KnownNat n => proxy n -> Integer -> Finite n
getFinite :: Finite n -> Integer
finites :: KnownNat n => [ Finite n]
finitesProxy :: KnownNat n => proxy n -> [ Finite n]
modulo :: KnownNat n => Integer -> Finite n
moduloProxy :: KnownNat n => proxy n -> Integer -> Finite n
equals :: Finite n -> Finite m -> Bool
cmp :: Finite n -> Finite m -> Ordering
natToFinite :: ( KnownNat n, KnownNat m, (n + 1) <= m) => proxy n -> Finite m
weaken :: Finite n -> Finite (n + 1)
strengthen :: KnownNat n => Finite (n + 1) -> Maybe ( Finite n)
shift :: Finite n -> Finite (n + 1)
unshift :: Finite (n + 1) -> Maybe ( Finite n)
weakenN :: n <= m => Finite n -> Finite m
strengthenN :: KnownNat n => Finite m -> Maybe ( Finite n)
shiftN :: ( KnownNat n, KnownNat m, n <= m) => Finite n -> Finite m
unshiftN :: ( KnownNat n, KnownNat m) => Finite m -> Maybe ( Finite n)
weakenProxy :: proxy k -> Finite n -> Finite (n + k)
strengthenProxy :: KnownNat n => proxy k -> Finite (n + k) -> Maybe ( Finite n)
shiftProxy :: KnownNat k => proxy k -> Finite n -> Finite (n + k)
unshiftProxy :: KnownNat k => proxy k -> Finite (n + k) -> Maybe ( Finite n)
add :: Finite n -> Finite m -> Finite (n + m)
sub :: Finite n -> Finite m -> Either ( Finite m) ( Finite n)
multiply :: Finite n -> Finite m -> Finite (n * m)
combineSum :: KnownNat n => Either ( Finite n) ( Finite m) -> Finite (n + m)
combineProduct :: KnownNat n => ( Finite n, Finite m) -> Finite (n * m)
separateSum :: KnownNat n => Finite (n + m) -> Either ( Finite n) ( Finite m)
separateProduct :: KnownNat n => Finite (n * m) -> ( Finite n, Finite m)
isValidFinite :: KnownNat n => Finite n -> Bool

Documentation

data Finite (n :: Nat ) Source #

Finite number type. Finite n is inhabited by exactly n values the range [0, n) including 0 but excluding n . Invariants:

getFinite x < natVal x

getFinite x >= 0

Instances

Instances details

KnownNat n => Bounded ( Finite n) Source #	Throws an error for `Finite 0`
Instance details Defined in Data.Finite.Internal Methods minBound :: Finite n Source # maxBound :: Finite n Source #
KnownNat n => Enum ( Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods succ :: Finite n -> Finite n Source # pred :: Finite n -> Finite n Source # toEnum :: Int -> Finite n Source # fromEnum :: Finite n -> Int Source # enumFrom :: Finite n -> [ Finite n] Source # enumFromThen :: Finite n -> Finite n -> [ Finite n] Source # enumFromTo :: Finite n -> Finite n -> [ Finite n] Source # enumFromThenTo :: Finite n -> Finite n -> Finite n -> [ Finite n] Source #
Eq ( Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods (==) :: Finite n -> Finite n -> Bool Source # (/=) :: Finite n -> Finite n -> Bool Source #
KnownNat n => Integral ( Finite n) Source #	`quot` and `rem` are the same as `div` and `mod` and they implement regular division of numbers in the range `[0, n)` , not modular arithmetic.
Instance details Defined in Data.Finite.Internal Methods quot :: Finite n -> Finite n -> Finite n Source # rem :: Finite n -> Finite n -> Finite n Source # div :: Finite n -> Finite n -> Finite n Source # mod :: Finite n -> Finite n -> Finite n Source # quotRem :: Finite n -> Finite n -> ( Finite n, Finite n) Source # divMod :: Finite n -> Finite n -> ( Finite n, Finite n) Source # toInteger :: Finite n -> Integer Source #
KnownNat n => Num ( Finite n) Source #	`+` , `-` , and `*` implement arithmetic modulo `n` . The `fromInteger` function raises an error for inputs outside of bounds.
Instance details Defined in Data.Finite.Internal Methods (+) :: Finite n -> Finite n -> Finite n Source # (-) :: Finite n -> Finite n -> Finite n Source # (*) :: Finite n -> Finite n -> Finite n Source # negate :: Finite n -> Finite n Source # abs :: Finite n -> Finite n Source # signum :: Finite n -> Finite n Source # fromInteger :: Integer -> Finite n Source #
Ord ( Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods compare :: Finite n -> Finite n -> Ordering Source # (<) :: Finite n -> Finite n -> Bool Source # (<=) :: Finite n -> Finite n -> Bool Source # (>) :: Finite n -> Finite n -> Bool Source # (>=) :: Finite n -> Finite n -> Bool Source # max :: Finite n -> Finite n -> Finite n Source # min :: Finite n -> Finite n -> Finite n Source #
KnownNat n => Read ( Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods readsPrec :: Int -> ReadS ( Finite n) Source # readList :: ReadS [ Finite n] Source # readPrec :: ReadPrec ( Finite n) Source # readListPrec :: ReadPrec [ Finite n] Source #
KnownNat n => Real ( Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods toRational :: Finite n -> Rational Source #
Show ( Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods showsPrec :: Int -> Finite n -> ShowS Source # show :: Finite n -> String Source # showList :: [ Finite n] -> ShowS Source #
Generic ( Finite n) Source #
Instance details Defined in Data.Finite.Internal Associated Types type Rep ( Finite n) :: Type -> Type Source # Methods from :: Finite n -> Rep ( Finite n) x Source # to :: Rep ( Finite n) x -> Finite n Source #
NFData ( Finite n) Source #
Instance details Defined in Data.Finite.Internal Methods rnf :: Finite n -> () Source #
type Rep ( Finite n) Source #
Instance details Defined in Data.Finite.Internal type Rep ( Finite n) = D1 (' MetaData "Finite" "Data.Finite.Internal" "finite-typelits-0.1.6.0-JWQ68Fc4Po0IMMqLp3mmi2" ' True ) ( C1 (' MetaCons "Finite" ' PrefixI ' False ) ( S1 (' MetaSel (' Nothing :: Maybe Symbol ) ' NoSourceUnpackedness ' NoSourceStrictness ' DecidedLazy ) ( Rec0 Integer )))

packFinite :: KnownNat n => Integer -> Maybe ( Finite n) Source #

Convert an Integer into a Finite , returning Nothing if the input is out of bounds.

packFiniteProxy :: KnownNat n => proxy n -> Integer -> Maybe ( Finite n) Source #

Same as packFinite but with a proxy argument to avoid type signatures.

finite :: KnownNat n => Integer -> Finite n Source #

Convert an Integer into a Finite , throwing an error if the input is out of bounds.

finiteProxy :: KnownNat n => proxy n -> Integer -> Finite n Source #

Same as finite but with a proxy argument to avoid type signatures.

getFinite :: Finite n -> Integer Source #

Convert a Finite into the corresponding Integer .

finites :: KnownNat n => [ Finite n] Source #

Generate a list of length n of all elements of Finite n .

finitesProxy :: KnownNat n => proxy n -> [ Finite n] Source #

Same as finites but with a proxy argument to avoid type signatures.

modulo :: KnownNat n => Integer -> Finite n Source #

Produce the Finite that is congruent to the given integer modulo n .

moduloProxy :: KnownNat n => proxy n -> Integer -> Finite n Source #

Same as modulo but with a proxy argument to avoid type signatures.

equals :: Finite n -> Finite m -> Bool infix 4 Source #

Test two different types of finite numbers for equality.

cmp :: Finite n -> Finite m -> Ordering Source #

Compare two different types of finite numbers.

natToFinite :: ( KnownNat n, KnownNat m, (n + 1) <= m) => proxy n -> Finite m Source #

Convert a type-level literal into a Finite .

weaken :: Finite n -> Finite (n + 1) Source #

Add one inhabitant in the end.

strengthen :: KnownNat n => Finite (n + 1) -> Maybe ( Finite n) Source #

Remove one inhabitant from the end. Returns Nothing if the input was the removed inhabitant.

shift :: Finite n -> Finite (n + 1) Source #

Add one inhabitant in the beginning, shifting everything up by one.

unshift :: Finite (n + 1) -> Maybe ( Finite n) Source #

Remove one inhabitant from the beginning, shifting everything down by one. Returns Nothing if the input was the removed inhabitant.

weakenN :: n <= m => Finite n -> Finite m Source #

Add multiple inhabitants in the end.

strengthenN :: KnownNat n => Finite m -> Maybe ( Finite n) Source #

Remove multiple inhabitants from the end. Returns Nothing if the input was one of the removed inhabitants.

shiftN :: ( KnownNat n, KnownNat m, n <= m) => Finite n -> Finite m Source #

Add multiple inhabitants in the beginning, shifting everything up by the amount of inhabitants added.

unshiftN :: ( KnownNat n, KnownNat m) => Finite m -> Maybe ( Finite n) Source #

Remove multiple inhabitants from the beginning, shifting everything down by the amount of inhabitants removed. Returns Nothing if the input was one of the removed inhabitants.

weakenProxy :: proxy k -> Finite n -> Finite (n + k) Source #

strengthenProxy :: KnownNat n => proxy k -> Finite (n + k) -> Maybe ( Finite n) Source #

shiftProxy :: KnownNat k => proxy k -> Finite n -> Finite (n + k) Source #

unshiftProxy :: KnownNat k => proxy k -> Finite (n + k) -> Maybe ( Finite n) Source #

add :: Finite n -> Finite m -> Finite (n + m) Source #

Add two Finite s.

sub :: Finite n -> Finite m -> Either ( Finite m) ( Finite n) Source #

Subtract two Finite s. Returns Left for negative results, and Right for positive results. Note that this function never returns Left 0 .

multiply :: Finite n -> Finite m -> Finite (n * m) Source #

Multiply two Finite s.

combineSum :: KnownNat n => Either ( Finite n) ( Finite m) -> Finite (n + m) Source #

Left -biased (left values come first) disjoint union of finite sets.

combineProduct :: KnownNat n => ( Finite n, Finite m) -> Finite (n * m) Source #

fst -biased (fst is the inner, and snd is the outer iteratee) product of finite sets.

separateSum :: KnownNat n => Finite (n + m) -> Either ( Finite n) ( Finite m) Source #

Take a Left -biased disjoint union apart.

separateProduct :: KnownNat n => Finite (n * m) -> ( Finite n, Finite m) Source #

Take a fst -biased product apart.

isValidFinite :: KnownNat n => Finite n -> Bool Source #

Verifies that a given Finite is valid. Should always return True unless you bring the Data.Finite.Internal.Finite constructor into the scope, or use unsafeCoerce or other nasty hacks.