Copyright | (C) 2015-2022 mniip |
---|---|
License | BSD3 |
Maintainer | mniip <mniip@mniip.com> |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
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.
is inhabited by exactly Finite
nn
values
the range [0, n)
including 0
but excluding n
. Invariants:
getFinite x < natVal x
getFinite x >= 0
Instances
KnownNat n => Bounded (Finite n) Source # | Throws an error for |
KnownNat n => Enum (Finite n) Source # | |
Eq (Finite n) Source # | |
KnownNat n => Integral (Finite n) Source # |
|
Defined in Data.Finite.Internal | |
KnownNat n => Num (Finite n) Source # |
|
Ord (Finite n) Source # | |
Defined in Data.Finite.Internal | |
KnownNat n => Read (Finite n) Source # | |
KnownNat n => Real (Finite n) Source # | |
Defined in Data.Finite.Internal toRational :: Finite n -> Rational # | |
Show (Finite n) Source # | |
Generic (Finite n) Source # | |
NFData (Finite n) Source # | |
Defined in Data.Finite.Internal | |
type Rep (Finite n) Source # | |
Defined in Data.Finite.Internal |
packFiniteProxy :: KnownNat n => proxy n -> Integer -> Maybe (Finite n) Source #
Same as packFinite
but with a proxy argument to avoid type signatures.
finiteProxy :: KnownNat n => proxy n -> Integer -> Finite n Source #
Same as finite
but with a proxy argument to avoid type signatures.
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.
natToFinite :: (KnownNat n, KnownNat m, (n + 1) <= m) => proxy n -> Finite m Source #
Convert a type-level literal into a Finite
.
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.
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.
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.