Data.Finite

Documentation

data Finite (n :: Nat)

Finite number type. Finite n is inhabited by exactly n values. Invariants:

getFinite x < natVal x

getFinite x >= 0

Instances

KnownNat n => Bounded (Finite n)

Throws an error for Finite 0

Defined in Data.Finite.Internal

Methods

minBound :: Finite n

maxBound :: Finite n

KnownNat n => Enum (Finite n)

Defined in Data.Finite.Internal

Methods

succ :: Finite n -> Finite n

pred :: Finite n -> Finite n

toEnum :: Int -> Finite n

fromEnum :: Finite n -> Int

enumFrom :: Finite n -> [Finite n]

enumFromThen :: Finite n -> Finite n -> [Finite n]

enumFromTo :: Finite n -> Finite n -> [Finite n]

enumFromThenTo :: Finite n -> Finite n -> Finite n -> [Finite n]

Eq (Finite n)

Defined in Data.Finite.Internal

Methods

(==) :: Finite n -> Finite n -> Bool

(/=) :: Finite n -> Finite n -> Bool

KnownNat n => Integral (Finite n)

Not modular arithmetic.

Defined in Data.Finite.Internal

Methods

quot :: Finite n -> Finite n -> Finite n

rem :: Finite n -> Finite n -> Finite n

div :: Finite n -> Finite n -> Finite n

mod :: Finite n -> Finite n -> Finite n

quotRem :: Finite n -> Finite n -> (Finite n, Finite n)

divMod :: Finite n -> Finite n -> (Finite n, Finite n)

toInteger :: Finite n -> Integer

KnownNat n => Num (Finite n)

Modular arithmetic. Only the fromInteger function is supposed to be useful.

Defined in Data.Finite.Internal

Methods

(+) :: Finite n -> Finite n -> Finite n

(-) :: Finite n -> Finite n -> Finite n

(*) :: Finite n -> Finite n -> Finite n

negate :: Finite n -> Finite n

abs :: Finite n -> Finite n

signum :: Finite n -> Finite n

fromInteger :: Integer -> Finite n

Ord (Finite n)

Defined in Data.Finite.Internal

Methods

compare :: Finite n -> Finite n -> Ordering

(<) :: Finite n -> Finite n -> Bool

(<=) :: Finite n -> Finite n -> Bool

(>) :: Finite n -> Finite n -> Bool

(>=) :: Finite n -> Finite n -> Bool

max :: Finite n -> Finite n -> Finite n

min :: Finite n -> Finite n -> Finite n

KnownNat n => Read (Finite n)

Defined in Data.Finite.Internal

Methods

readsPrec :: Int -> ReadS (Finite n)

readList :: ReadS [Finite n]

readPrec :: ReadPrec (Finite n)

readListPrec :: ReadPrec [Finite n]

KnownNat n => Real (Finite n)

Defined in Data.Finite.Internal

Methods

toRational :: Finite n -> Rational

Show (Finite n)

Defined in Data.Finite.Internal

Methods

showsPrec :: Int -> Finite n -> ShowS

show :: Finite n -> String

showList :: [Finite n] -> ShowS

Generic (Finite n)

Defined in Data.Finite.Internal

Associated Types

type Rep (Finite n) :: * -> *

Methods

from :: Finite n -> Rep (Finite n) x

to :: Rep (Finite n) x -> Finite n

NFData (Finite n)

Defined in Data.Finite.Internal

Methods

rnf :: Finite n -> ()

type Rep (Finite n)

Defined in Data.Finite.Internal

type Rep (Finite n) = D1 (MetaData "Finite" "Data.Finite.Internal" "finite-typelits-0.1.4.2-LNt8ccQ3rb0a6MNjjNxeu" True) (C1 (MetaCons "Finite" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer)))

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

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

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

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

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

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

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

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

getFinite :: Finite n -> Integer

Convert a Finite into the corresponding Integer.

finites :: KnownNat n => [Finite n]

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

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

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

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

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

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

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

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

Test two different types of finite numbers for equality.

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

Compare two different types of finite numbers.

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

Convert a type-level literal into a Finite.

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

Add one inhabitant in the end.

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

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

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

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

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

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

Add multiple inhabitants in the end.

strengthenN :: (KnownNat n, n <= m) => Finite m -> Maybe (Finite n)

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

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

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

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)

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)

Add two Finites.

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

Subtract two Finites. 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)

Multiply two Finites.

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

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

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

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)

Take a Left-biased disjoint union apart.

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

Take a fst-biased product apart.

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

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