Safe Haskell	Safe
Language	Haskell2010

Data.Fin

Contents

Showing
Conversions
Interesting
Aliases

Description

Finite numbers.

This module is designed to be imported qualified.

Synopsis

Documentation

data Fin n where Source #

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) Source #
Methods minBound :: Fin n # maxBound :: Fin n #
SNatI n => Enum (Fin n) Source #
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) Source #
Methods (==) :: Fin n -> Fin n -> Bool # (/=) :: Fin n -> Fin n -> Bool #
SNatI n => Integral (Fin n) Source #	`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) Source #	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) Source #
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) Source #
Methods toRational :: Fin n -> Rational #
Show (Fin n) Source #	`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) Source #
Methods rnf :: Fin n -> () #
Hashable (Fin n) Source #
Methods hashWithSalt :: Int -> Fin n -> Int # hash :: Fin n -> Int #

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

Fold Fin.

Showing

explicitShow :: Fin n -> String Source #

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 Source #

showsPrec displaying a structure of Fin.

Conversions

toNat :: Fin n -> Nat Source #

Convert to Nat.

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

Convert from Nat.

>>> fromNat N.one :: Maybe (Fin N.Two)
Just 1

>>> fromNat N.one :: Maybe (Fin N.One)
Nothing

toNatural :: Fin n -> Natural Source #

Convert to Natural.

toInteger :: Integral a => a -> Integer #

conversion to Integer

Interesting

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

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] Source #

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

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

inlineUniverse :: InlineInduction n => [Fin n] Source #

.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 Source #

Fin Zero is inhabited.

boring :: Fin One Source #

Counting to one is boring.

>>> boring
0

Aliases

zeroth :: Fin (S n) Source #

first :: Fin (S (S n)) Source #