Data.Fin

Finite numbers.

This module is designed to be imported qualified.

Documentation

data Fin n where

Finite Numbers up to n.

Constructors

Z :: Fin (S n)

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

Instances

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

Methods

minBound :: Fin n

maxBound :: Fin n

SNatI n => Enum (Fin n)

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)

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.

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.Three]
[0,1,2,0,1,1]

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

>>> signum (Z :: Fin N.One)
*** Exception: signum @(Fin n): not implemented
...

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

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

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)

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)

Methods

toRational :: Fin n -> Rational

Show (Fin n)

Fin is printed as Natural.

To see explicit structure, use explicitShow or explicitShowsPrec

Methods

showsPrec :: Int -> Fin n -> ShowS

show :: Fin n -> String

showList :: [Fin n] -> ShowS

NFData (Fin n)

Methods

rnf :: Fin n -> ()

Hashable (Fin n)

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.One)
"Z"

>>> explicitShow (2 :: Fin N.Three)
"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.one :: Maybe (Fin N.Two)
Just 1

>>> fromNat N.one :: Maybe (Fin N.One)
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.Five]
[0,1,3,2,4]

>>> zipWith (*) universe (map inverse universe) :: [Fin N.Five]
[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 Zero.

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

inlineUniverse :: InlineInduction n => [Fin n]

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

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

absurd :: Fin Zero -> b

Fin Zero is inhabited.

boring :: Fin One

Counting to one is boring.

>>> boring
0

Aliases

zeroth :: Fin (S n)

first :: Fin (S (S n))