Safe Haskell	Safe
Language	Haskell2010

Data.Fin

Contents

Showing
Conversions
Interesting
Plus
Min and max
Aliases

Description

Finite numbers.

This module is designed to be imported as

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

Synopsis

data Fin (n :: Nat) where
- FZ :: Fin ('S n)
- FS :: Fin n -> Fin ('S n)
cata :: forall a n. a -> (a -> a) -> Fin n -> a
explicitShow :: Fin n -> String
explicitShowsPrec :: Int -> Fin n -> ShowS
toNat :: Fin n -> Nat
fromNat :: SNatI n => Nat -> Maybe (Fin n)
toNatural :: Fin n -> Natural
toInteger :: Integral a => a -> Integer
mirror :: forall n. SNatI n => Fin n -> Fin n
inverse :: forall n. SNatI n => Fin n -> Fin n
universe :: SNatI n => [Fin n]
inlineUniverse :: SNatI n => [Fin n]
universe1 :: SNatI n => NonEmpty (Fin ('S n))
inlineUniverse1 :: SNatI n => NonEmpty (Fin ('S n))
absurd :: Fin Nat0 -> b
boring :: Fin Nat1
weakenLeft :: forall n m. SNatI n => Proxy m -> Fin n -> Fin (Plus n m)
weakenLeft1 :: SNatI n => Fin n -> Fin ('S n)
weakenRight :: forall n m. SNatI n => Proxy n -> Fin m -> Fin (Plus n m)
weakenRight1 :: Fin n -> Fin ('S n)
append :: forall n m. SNatI n => Either (Fin n) (Fin m) -> Fin (Plus n m)
split :: forall n m. SNatI n => Fin (Plus n m) -> Either (Fin n) (Fin m)
isMin :: Fin ('S n) -> Maybe (Fin n)
isMax :: forall n. SNatI n => Fin ('S n) -> Maybe (Fin n)
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))

Documentation

data Fin (n :: Nat) where Source #

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

Constructors

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

Instances

Instances details

EqP Fin Source #	`>>>` `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
Instance details Defined in Data.Fin Methods eqp :: forall (a :: k) (b :: k). Fin a -> Fin b -> Bool #
GShow Fin Source #	Since: 0.2.2
Instance details Defined in Data.Fin Methods gshowsPrec :: forall (a :: k). Int -> Fin a -> ShowS #
OrdP Fin Source #	`>>>` `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
Instance details Defined in Data.Fin Methods comparep :: forall (a :: k) (b :: k). Fin a -> Fin b -> Ordering #
(n ~ 'S m, SNatI m) => Arbitrary (Fin n) Source #
Instance details Defined in Data.Fin Methods arbitrary :: Gen (Fin n) # shrink :: Fin n -> [Fin n] #
CoArbitrary (Fin n) Source #
Instance details Defined in Data.Fin Methods coarbitrary :: Fin n -> Gen b -> Gen b #
(n ~ 'S m, SNatI m) => Function (Fin n) Source #
Instance details Defined in Data.Fin Methods function :: (Fin n -> b) -> Fin n :-> b #
(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] #
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 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 #
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 => 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 #
n ~ 'Z => Absurd (Fin n) Source #	Since: 0.2.1
Instance details Defined in Data.Fin Methods absurd :: Fin n -> b #
NFData (Fin n) Source #
Instance details Defined in Data.Fin Methods rnf :: Fin n -> () #
Eq (Fin n) Source #
Instance details Defined in Data.Fin Methods (==) :: Fin n -> Fin n -> Bool # (/=) :: Fin n -> Fin n -> Bool #
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 #
Hashable (Fin n) Source #
Instance details Defined in Data.Fin Methods hashWithSalt :: Int -> Fin n -> Int # hash :: Fin n -> Int #
SNatI n => Finite (Fin n) Source #	`>>>` `(U.cardinality :: U.Tagged (Fin N.Nat3) Natural) == U.Tagged (genericLength (U.universeF :: [Fin N.Nat3]))`True Since: 0.1.2
Instance details Defined in Data.Fin Methods universeF :: [Fin n] # cardinality :: Tagged (Fin n) Natural #
SNatI n => Universe (Fin n) Source #	Since: 0.1.2
Instance details Defined in Data.Fin Methods universe :: [Fin n] #

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

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

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

mirror :: forall n. SNatI 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]

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 :: SNatI 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 :: SNatI n => NonEmpty (Fin ('S n)) Source #

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

absurd :: Fin Nat0 -> b Source #

Fin Nat0 is not inhabited.

boring :: Fin Nat1 Source #

Counting to one is boring.

>>> boring
0

Plus

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

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

weakenLeft1 :: SNatI 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. SNatI 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. SNatI 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. SNatI 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. SNatI 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

Aliases

fin0 :: Fin (Plus Nat0 ('S n)) Source #

fin1 :: Fin (Plus Nat1 ('S n)) Source #

fin2 :: Fin (Plus Nat2 ('S n)) Source #

fin3 :: Fin (Plus Nat3 ('S n)) Source #

fin4 :: Fin (Plus Nat4 ('S n)) Source #

fin5 :: Fin (Plus Nat5 ('S n)) Source #

fin6 :: Fin (Plus Nat6 ('S n)) Source #

fin7 :: Fin (Plus Nat7 ('S n)) Source #

fin8 :: Fin (Plus Nat8 ('S n)) Source #

fin9 :: Fin (Plus Nat9 ('S n)) Source #