fin-0.1: Nat and Fin: peano naturals and finite numbers

Safe HaskellNone
LanguageHaskell2010

Data.Fin

Contents

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