Safe Haskell	None
Language	Haskell2010

Data.Fin

Contents

Showing
Conversions
Interesting
Plus
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
inverse :: forall n. SNatI n => Fin n -> Fin n
universe :: SNatI n => [Fin n]
inlineUniverse :: InlineInduction n => [Fin n]
universe1 :: SNatI n => NonEmpty (Fin (S n))
inlineUniverse1 :: InlineInduction n => NonEmpty (Fin (S n))
absurd :: Fin Nat0 -> b
boring :: Fin Nat1
weakenLeft :: forall n m. InlineInduction n => Proxy m -> Fin n -> Fin (Plus n m)
weakenRight :: forall n m. InlineInduction n => Proxy n -> Fin m -> Fin (Plus n m)
append :: forall n m. InlineInduction n => Either (Fin n) (Fin m) -> Fin (Plus n m)
split :: forall n m. InlineInduction n => Fin (Plus n m) -> Either (Fin n) (Fin m)
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

(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 (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 #
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)
"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

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

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 #