fin-0.2: Nat and Fin: peano naturals and finite numbers
Safe HaskellSafe
LanguageHaskell2010

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

Instances details
(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 #

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

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 #

SNatI n => Universe (Fin n) Source #

Since: 0.1.2

Instance details

Defined in Data.Fin

Methods

universe :: [Fin n] #

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

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 #