Safe Haskell	None
Language	Haskell2010

Data.Fin

Contents

Showing
Conversions
Interesting
Plus
Aliases

Description

Finite numbers.

This module is designed to be imported qualified.

Synopsis

data Fin (n :: Nat) where
- Z :: Fin (S n)
- S :: Fin n -> Fin (S n)
cata :: forall a n. a -> (a -> a) -> Fin n -> a
explicitShow :: Fin n -> String
explicitShowsPrec :: Int -> Fin n -> ShowS
toNat :: Fin n -> Nat
fromNat :: SNatI n => Nat -> Maybe (Fin n)
toNatural :: Fin n -> Natural
toInteger :: Integral a => a -> Integer
inverse :: forall n. SNatI n => Fin n -> Fin n
universe :: SNatI n => [Fin n]
inlineUniverse :: InlineInduction n => [Fin n]
universe1 :: SNatI n => NonEmpty (Fin (S n))
inlineUniverse1 :: InlineInduction n => NonEmpty (Fin (S n))
absurd :: Fin Nat0 -> b
boring :: Fin Nat1
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)
split :: forall n m. InlineInduction n => Fin (Plus n m) -> Either (Fin n) (Fin m)
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))

Documentation

data Fin (n :: Nat) where Source #

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) Source #
Instance details Defined in Data.Fin Methods minBound :: Fin n # maxBound :: Fin n #
SNatI n => Enum (Fin n) Source #
Instance details 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) Source #
Instance details Defined in Data.Fin 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.
Instance details 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) Source #	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
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Data.Fin Methods toRational :: Fin n -> Rational #
Show (Fin n) Source #	`Fin` is printed as `Natural`. To see explicit structure, use `explicitShow` or `explicitShowsPrec`
Instance details Defined in Data.Fin Methods showsPrec :: Int -> Fin n -> ShowS # show :: Fin n -> String # showList :: [Fin n] -> ShowS #
NFData (Fin n) Source #
Instance details Defined in Data.Fin Methods rnf :: Fin n -> () #
Hashable (Fin n) Source #
Instance details Defined in Data.Fin 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.Nat1)
"Z"

>>> explicitShow (2 :: Fin N.Nat3)
"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.nat1 :: Maybe (Fin N.Nat2)
Just 1

>>> fromNat N.nat1 :: Maybe (Fin N.Nat1)
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.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] Source #

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

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

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

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

Like universe but NonEmpty.

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

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

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

absurd :: Fin Nat0 -> b Source #

Fin Nat0 is inhabited.

boring :: Fin Nat1 Source #

Counting to one is boring.

>>> boring
0

Plus

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

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

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

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

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

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

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

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

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

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

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

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

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

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