fin-0: Nat and Fin

Data.Fin

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 # MethodsminBound :: Fin n #maxBound :: Fin n # SNatI n => Enum (Fin n) Source # Methodssucc :: 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. Methodsquot :: 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 # Ord (Fin n) Source # Methodscompare :: 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 # MethodstoRational :: Fin n -> Rational # Show (Fin n) Source # Fin is printed as Natural.To see explicit structure, use explicitShow or explicitShowsPrec MethodsshowsPrec :: Int -> Fin n -> ShowS #show :: Fin n -> String #showList :: [Fin n] -> ShowS # NFData (Fin n) Source # Methodsrnf :: Fin n -> () # Hashable (Fin n) Source # MethodshashWithSalt :: Int -> Fin n -> Int #hash :: Fin n -> Int #

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

Fold Fin.

# Showing

show displaying a structure of Fin.

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

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


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


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]


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.

Counting to one is boring.

>>> boring
0


# Aliases

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