fin-0.1.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 # (n ~ S m, SNatI m) => Function (Fin n) Source # Instance detailsDefined in Data.Fin Methodsfunction :: (Fin n -> b) -> Fin n :-> b # (n ~ S m, SNatI m) => Arbitrary (Fin n) Source # Instance detailsDefined in Data.Fin Methodsarbitrary :: Gen (Fin n) #shrink :: Fin n -> [Fin n] # Source # Instance detailsDefined in Data.Fin Methodscoarbitrary :: Fin n -> Gen b -> Gen b # 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

mirror :: forall n. InlineInduction n => Fin n -> Fin n Source #

Mirror the values, minBound becomes maxBound, etc.

>>> map mirror universe :: [Fin N.Nat4]
[3,2,1,0]
>>> reverse universe :: [Fin N.Nat4]
[3,2,1,0]

Since: 0.1.1

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 not inhabited.

Counting to one is boring.

>>> boring
0

# Plus

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

>>> map (weakenLeft (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])
[0,1,2]

weakenLeft1 :: InlineInduction n => Fin n -> Fin (S n) Source #

>>> map weakenLeft1 universe :: [Fin N.Nat5]
[0,1,2,3]

Since: 0.1.1

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

>>> map (weakenRight (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])
[2,3,4]

weakenRight1 :: Fin n -> Fin (S n) Source #

>>> map weakenRight1 universe :: [Fin N.Nat5]
[1,2,3,4]

Since: 0.1.1

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]

# Min and max

isMin :: Fin (S n) -> Maybe (Fin n) Source #

Return a one less.

>>> isMin (FZ :: Fin N.Nat1)
Nothing
>>> map isMin universe :: [Maybe (Fin N.Nat3)]
[Nothing,Just 0,Just 1,Just 2]

Since: 0.1.1

isMax :: forall n. InlineInduction n => Fin (S n) -> Maybe (Fin n) Source #

Return a one less.

>>> isMax (FZ :: Fin N.Nat1)
Nothing
>>> map isMax universe :: [Maybe (Fin N.Nat3)]
[Just 0,Just 1,Just 2,Nothing]

Since: 0.1.1