fin-0.0.3: Nat and Fin: peano naturals and finite numbers

Safe HaskellNone
LanguageHaskell2010

Data.Fin

Contents

Description

Finite numbers.

This module is designed to be imported qualified.

Synopsis

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