Data.Fin

Finite numbers.

This module is designed to be imported as

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

Documentation

data Fin (n :: Nat) where

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

Constructors

FZ :: Fin ('S n)

FS :: Fin n -> Fin ('S n)

Instances

EqP Fin

>>> eqp FZ FZ
True

>>> eqp FZ (FS FZ)
False

>>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ eqp x y | y <- ys ] | x <- xs ]
[True,False,False,False,False,False]
[False,True,False,False,False,False]
[False,False,True,False,False,False]
[False,False,False,True,False,False]

Since: 0.2.2

Defined in Data.Fin

Methods

eqp :: forall (a :: k) (b :: k). Fin a -> Fin b -> Bool

GShow Fin

Since: 0.2.2

Defined in Data.Fin

Methods

gshowsPrec :: forall (a :: k). Int -> Fin a -> ShowS

OrdP Fin

>>> let xs = universe @N.Nat4; ys = universe @N.Nat6 in traverse_ print [ [ comparep x y | y <- ys ] | x <- xs ]
[EQ,LT,LT,LT,LT,LT]
[GT,EQ,LT,LT,LT,LT]
[GT,GT,EQ,LT,LT,LT]
[GT,GT,GT,EQ,LT,LT]

Since: 0.2.2

Defined in Data.Fin

Methods

comparep :: forall (a :: k) (b :: k). Fin a -> Fin b -> Ordering

(n ~ 'S m, SNatI m) => Arbitrary (Fin n)

Defined in Data.Fin

Methods

arbitrary :: Gen (Fin n)

shrink :: Fin n -> [Fin n]

CoArbitrary (Fin n)

Defined in Data.Fin

Methods

coarbitrary :: Fin n -> Gen b -> Gen b

(n ~ 'S m, SNatI m) => Function (Fin n)

Defined in Data.Fin

Methods

function :: (Fin n -> b) -> Fin n :-> b

(n ~ 'S m, SNatI m) => Bounded (Fin n)

Defined in Data.Fin

Methods

minBound :: Fin n

maxBound :: Fin n

SNatI n => Enum (Fin n)

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]

SNatI n => Num (Fin n)

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

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

SNatI n => Integral (Fin n)

quot works only on Fin n where n is prime.

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 => Real (Fin n)

Defined in Data.Fin

Methods

toRational :: Fin n -> Rational

Show (Fin n)

Fin is printed as Natural.

To see explicit structure, use explicitShow or explicitShowsPrec

Defined in Data.Fin

Methods

showsPrec :: Int -> Fin n -> ShowS

show :: Fin n -> String

showList :: [Fin n] -> ShowS

n ~ 'Z => Absurd (Fin n)

Since: 0.2.1

Defined in Data.Fin

Methods

absurd :: Fin n -> b

NFData (Fin n)

Defined in Data.Fin

Methods

rnf :: Fin n -> ()

Eq (Fin n)

Defined in Data.Fin

Methods

(==) :: Fin n -> Fin n -> Bool

(/=) :: Fin n -> Fin n -> Bool

Ord (Fin n)

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

Hashable (Fin n)

Defined in Data.Fin

Methods

hashWithSalt :: Int -> Fin n -> Int

hash :: Fin n -> Int

SNatI n => Finite (Fin n)

>>> (U.cardinality :: U.Tagged (Fin N.Nat3) Natural) == U.Tagged (genericLength (U.universeF :: [Fin N.Nat3]))
True

Since: 0.1.2

Defined in Data.Fin

Methods

universeF :: [Fin n]

cardinality :: Tagged (Fin n) Natural

SNatI n => Universe (Fin n)

Since: 0.1.2

Defined in Data.Fin

Methods

universe :: [Fin n]

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

Fold Fin.

Showing

explicitShow :: Fin n -> String

show displaying a structure of Fin.

>>> explicitShow (0 :: Fin N.Nat1)
"FZ"

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

explicitShowsPrec :: Int -> Fin n -> ShowS

showsPrec displaying a structure of Fin.

Conversions

toNat :: Fin n -> Nat

Convert to Nat.

fromNat :: SNatI n => Nat -> Maybe (Fin n)

Convert from Nat.

>>> fromNat N.nat1 :: Maybe (Fin N.Nat2)
Just 1

>>> fromNat N.nat1 :: Maybe (Fin N.Nat1)
Nothing

toNatural :: Fin n -> Natural

Convert to Natural.

toInteger :: Integral a => a -> Integer

conversion to Integer

Interesting

mirror :: forall n. SNatI n => Fin n -> Fin n

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

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]

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

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

inlineUniverse :: SNatI n => [Fin n]

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

Like universe but NonEmpty.

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

inlineUniverse1 :: SNatI n => NonEmpty (Fin ('S n))

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

absurd :: Fin Nat0 -> b

Fin Nat0 is not inhabited.

boring :: Fin Nat1

Counting to one is boring.

>>> boring
0

Plus

weakenLeft :: forall n m. SNatI n => Proxy m -> Fin n -> Fin (Plus n m)

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

weakenLeft1 :: SNatI n => Fin n -> Fin ('S n)

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

Since: 0.1.1

weakenRight :: forall n m. SNatI n => Proxy n -> Fin m -> Fin (Plus n m)

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

weakenRight1 :: Fin n -> Fin ('S n)

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

Since: 0.1.1

append :: forall n m. SNatI n => Either (Fin n) (Fin m) -> Fin (Plus n m)

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. SNatI n => Fin (Plus n m) -> Either (Fin n) (Fin m)

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)

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. SNatI n => Fin ('S n) -> Maybe (Fin n)

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

Aliases

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