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

Data.Fin

Description

Finite numbers.

This module is designed to be imported as

import Data.Fin (Fin (..))
import qualified Data.Fin as Fin

Synopsis

# Documentation

data Fin (n :: Nat) where Source #

Finite numbers: [0..n-1].

Constructors

 FZ :: Fin (S n) FS :: Fin n -> Fin (S n)
Instances
 (n ~ S m, SNatI m) => Bounded (Fin n) Source # Instance detailsDefined in Data.Fin MethodsminBound :: Fin n #maxBound :: Fin n # SNatI n => Enum (Fin n) Source # Instance detailsDefined in Data.Fin 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 # Instance detailsDefined 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 detailsDefined in Data.Fin 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.Nat3] [0,1,2,0,1,1] >>> fromInteger 42 :: Fin N.Nat0 *** Exception: divide by zero ... >>> signum (FZ :: Fin N.Nat1) 0 >>> signum (3 :: Fin N.Nat4) 1 >>> 2 + 3 :: Fin N.Nat4 1 >>> 2 * 3 :: Fin N.Nat4 2  Instance detailsDefined 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 # Ord (Fin n) Source # Instance detailsDefined in Data.Fin 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 # Instance detailsDefined in Data.Fin MethodstoRational :: Fin n -> Rational # Show (Fin n) Source # Fin is printed as Natural.To see explicit structure, use explicitShow or explicitShowsPrec Instance detailsDefined in Data.Fin MethodsshowsPrec :: Int -> Fin n -> ShowS #show :: Fin n -> String #showList :: [Fin n] -> ShowS # NFData (Fin n) Source # Instance detailsDefined in Data.Fin Methodsrnf :: Fin n -> () # Hashable (Fin n) Source # Instance detailsDefined in Data.Fin 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.Nat1)
"FZ"

>>> explicitShow (2 :: Fin N.Nat3)
"FS (FS FZ)"


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


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]


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 :: NonEmpty (Fin N.Nat3)
0 :| [1,2]


absurd :: Fin Nat0 -> b Source #

Fin Nat0 is inhabited.

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]