Safe Haskell	None
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. InlineInduction n => Fin n -> Fin n
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)
weakenLeft1 :: InlineInduction n => Fin n -> Fin (' S n)
weakenRight :: forall n m. InlineInduction n => Proxy n -> Fin m -> Fin ( Plus n m)
weakenRight1 :: Fin n -> Fin (' S n)
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)
isMin :: Fin (' S n) -> Maybe ( Fin n)
isMax :: forall n. InlineInduction 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

(n ~ ' S m, SNatI m) => Bounded ( Fin n) Source #
Instance details Defined in Data.Fin Methods minBound :: Fin n Source # maxBound :: Fin n Source #
SNatI n => Enum ( Fin n) Source #
Instance details Defined in Data.Fin Methods succ :: Fin n -> Fin n Source # pred :: Fin n -> Fin n Source # toEnum :: Int -> Fin n Source # fromEnum :: Fin n -> Int Source # enumFrom :: Fin n -> [ Fin n] Source # enumFromThen :: Fin n -> Fin n -> [ Fin n] Source # enumFromTo :: Fin n -> Fin n -> [ Fin n] Source # enumFromThenTo :: Fin n -> Fin n -> Fin n -> [ Fin n] Source #
Eq ( Fin n) Source #
Instance details Defined in Data.Fin Methods (==) :: Fin n -> Fin n -> Bool Source # (/=) :: Fin n -> Fin n -> Bool Source #
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 Source # rem :: Fin n -> Fin n -> Fin n Source # div :: Fin n -> Fin n -> Fin n Source # mod :: Fin n -> Fin n -> Fin n Source # quotRem :: Fin n -> Fin n -> ( Fin n, Fin n) Source # divMod :: Fin n -> Fin n -> ( Fin n, Fin n) Source # toInteger :: Fin n -> Integer Source #
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 Source # (-) :: Fin n -> Fin n -> Fin n Source # (*) :: Fin n -> Fin n -> Fin n Source # negate :: Fin n -> Fin n Source # abs :: Fin n -> Fin n Source # signum :: Fin n -> Fin n Source # fromInteger :: Integer -> Fin n Source #
Ord ( Fin n) Source #
Instance details Defined in Data.Fin Methods compare :: Fin n -> Fin n -> Ordering Source # (<) :: Fin n -> Fin n -> Bool Source # (<=) :: Fin n -> Fin n -> Bool Source # (>) :: Fin n -> Fin n -> Bool Source # (>=) :: Fin n -> Fin n -> Bool Source # max :: Fin n -> Fin n -> Fin n Source # min :: Fin n -> Fin n -> Fin n Source #
SNatI n => Real ( Fin n) Source #
Instance details Defined in Data.Fin Methods toRational :: Fin n -> Rational Source #
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 Source # show :: Fin n -> String Source # showList :: [ Fin n] -> ShowS Source #
(n ~ ' S m, SNatI m) => Function ( Fin n) Source #
Instance details Defined in Data.Fin Methods function :: ( Fin n -> b) -> Fin n :-> b Source #
(n ~ ' S m, SNatI m) => Arbitrary ( Fin n) Source #
Instance details Defined in Data.Fin Methods arbitrary :: Gen ( Fin n) Source # shrink :: Fin n -> [ Fin n] Source #
CoArbitrary ( Fin n) Source #
Instance details Defined in Data.Fin Methods coarbitrary :: Fin n -> Gen b -> Gen b Source #
NFData ( Fin n) Source #
Instance details Defined in Data.Fin Methods rnf :: Fin n -> () Source #
Hashable ( Fin n) Source #
Instance details Defined in Data.Fin Methods hashWithSalt :: Int -> Fin n -> Int Source # hash :: Fin n -> Int Source #

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 Source #

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]

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 not 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 #

>>> 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 Fin s 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

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 #