Data.Fin

Finite numbers.

This module is designed to be imported qualified.

Documentation

data Fin (n :: Nat) where

Finite numbers: [0..n-1].

Constructors

Z :: Fin (S n)

S :: Fin n -> Fin (S n)

Instances

(n ~ S m, SNatI m) => Bounded (Fin n)

Defined in Data.Fin

Methods

minBound :: Fin n

maxBound :: Fin n

SNatI n => Enum (Fin n)

Defined in Data.Fin

Methods

succ :: Fin n -> Fin n

pred :: Fin n -> Fin n

toEnum :: Int -> Fin n

fromEnum :: Fin n -> Int

enumFrom :: Fin n -> [Fin n]

enumFromThen :: Fin n -> Fin n -> [Fin n]

enumFromTo :: Fin n -> Fin n -> [Fin n]

enumFromThenTo :: Fin n -> Fin n -> Fin n -> [Fin n]

Eq (Fin n)

Defined in Data.Fin

Methods

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

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

SNatI n => Integral (Fin n)

quot works only on Fin n where n is prime.

Defined in Data.Fin

Methods

quot :: Fin n -> Fin n -> Fin n

rem :: Fin n -> Fin n -> Fin n

div :: Fin n -> Fin n -> Fin n

mod :: Fin n -> Fin n -> Fin n

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

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

toInteger :: Fin n -> Integer

SNatI n => Num (Fin n)

Operations module n.

>>> map fromInteger [0, 1, 2, 3, 4, -5] :: [Fin N.Nat3]
[0,1,2,0,1,1]

>>> fromInteger 42 :: Fin N.Nat0
*** Exception: divide by zero
...

>>> signum (Z :: Fin N.Nat1)
0

>>> signum (3 :: Fin N.Nat4)
1

>>> 2 + 3 :: Fin N.Nat4
1

>>> 2 * 3 :: Fin N.Nat4
2

Defined in Data.Fin

Methods

(+) :: Fin n -> Fin n -> Fin n

(-) :: Fin n -> Fin n -> Fin n

(*) :: Fin n -> Fin n -> Fin n

negate :: Fin n -> Fin n

abs :: Fin n -> Fin n

signum :: Fin n -> Fin n

fromInteger :: Integer -> Fin n

Ord (Fin n)

Defined in Data.Fin

Methods

compare :: Fin n -> Fin n -> Ordering

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

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

(>) :: Fin n -> Fin n -> Bool

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

max :: Fin n -> Fin n -> Fin n

min :: Fin n -> Fin n -> Fin n

SNatI n => Real (Fin n)

Defined in Data.Fin

Methods

toRational :: Fin n -> Rational

Show (Fin n)

Fin is printed as Natural.

To see explicit structure, use explicitShow or explicitShowsPrec

Defined in Data.Fin

Methods

showsPrec :: Int -> Fin n -> ShowS

show :: Fin n -> String

showList :: [Fin n] -> ShowS

NFData (Fin n)

Defined in Data.Fin

Methods

rnf :: Fin n -> ()

Hashable (Fin n)

Defined in Data.Fin

Methods

hashWithSalt :: Int -> Fin n -> Int

hash :: Fin n -> Int

cata :: forall a n. a -> (a -> a) -> Fin n -> a

Fold Fin.

Showing

explicitShow :: Fin n -> String

show displaying a structure of Fin.

>>> explicitShow (0 :: Fin N.Nat1)
"Z"

>>> explicitShow (2 :: Fin N.Nat3)
"S (S Z)"

explicitShowsPrec :: Int -> Fin n -> ShowS

showsPrec displaying a structure of Fin.

Conversions

toNat :: Fin n -> Nat

Convert to Nat.

fromNat :: SNatI n => Nat -> Maybe (Fin n)

Convert from Nat.

>>> fromNat N.nat1 :: Maybe (Fin N.Nat2)
Just 1

>>> fromNat N.nat1 :: Maybe (Fin N.Nat1)
Nothing

toNatural :: Fin n -> Natural

Convert to Natural.

toInteger :: Integral a => a -> Integer

conversion to Integer

Interesting

inverse :: forall n. SNatI n => Fin n -> Fin n

Multiplicative inverse.

Works for Fin n where n is coprime with an argument, i.e. in general when n is prime.

>>> map inverse universe :: [Fin N.Nat5]
[0,1,3,2,4]

>>> zipWith (*) universe (map inverse universe) :: [Fin N.Nat5]
[0,1,1,1,1]

Adaptation of pseudo-code in Wikipedia

universe :: SNatI n => [Fin n]

All values. [minBound .. maxBound] won't work for Fin Nat0.

>>> universe :: [Fin N.Nat3]
[0,1,2]

inlineUniverse :: InlineInduction n => [Fin n]

universe which will be fully inlined, if n is known at compile time.

>>> inlineUniverse :: [Fin N.Nat3]
[0,1,2]

universe1 :: SNatI n => NonEmpty (Fin (S n))

Like universe but NonEmpty.

>>> universe1 :: NonEmpty (Fin N.Nat3)
0 :| [1,2]

inlineUniverse1 :: InlineInduction n => NonEmpty (Fin (S n))

>>> inlineUniverse1 :: NonEmpty (Fin N.Nat3)
0 :| [1,2]

absurd :: Fin Nat0 -> b

Fin Nat0 is inhabited.

boring :: Fin Nat1

Counting to one is boring.

>>> boring
0

Plus

weakenLeft :: forall n m. InlineInduction n => Proxy m -> Fin n -> Fin (Plus n m)

weakenRight :: forall n m. InlineInduction n => Proxy n -> Fin m -> Fin (Plus n m)

append :: forall n m. InlineInduction n => Either (Fin n) (Fin m) -> Fin (Plus n m)

Append two Fins together.

>>> append (Left fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))
2

>>> append (Right fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))
7

split :: forall n m. InlineInduction n => Fin (Plus n m) -> Either (Fin n) (Fin m)

Inverse of append.

>>> split fin2 :: Either (Fin N.Nat2) (Fin N.Nat3)
Right 0

>>> split fin1 :: Either (Fin N.Nat2) (Fin N.Nat3)
Left 1

>>> map split universe :: [Either (Fin N.Nat2) (Fin N.Nat3)]
[Left 0,Left 1,Right 0,Right 1,Right 2]

Aliases

fin0 :: Fin (Plus Nat0 (S n))

fin1 :: Fin (Plus Nat1 (S n))

fin2 :: Fin (Plus Nat2 (S n))

fin3 :: Fin (Plus Nat3 (S n))

fin4 :: Fin (Plus Nat4 (S n))

fin5 :: Fin (Plus Nat5 (S n))

fin6 :: Fin (Plus Nat6 (S n))

fin7 :: Fin (Plus Nat7 (S n))

fin8 :: Fin (Plus Nat8 (S n))

fin9 :: Fin (Plus Nat9 (S n))