HORIZON HASKELLDocslts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

Modulefin-0.3.2Haskell2010

Data.Fin

Finite numbers.

This module is designed to be imported as

import Data.Fin (Fin (..))
import qualified Data.Fin as Fin
  • 1 type
  • 32 values
  • Packagefin-0.3.2
  • Exports34
  • LanguageHaskell2010
  • LicenceBSD-3-Clause
  • SourceFin.hs
datadata Fin (n :: Nat) where
#

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

Constructors

Instances19EqP, GShow, OrdP, Bounded, Enum, Eq, …
  • EqP FinDefined in fin-0.3.2 · Data.Fin
    Example1 expression
    eqp FZ FZTrue
    Example1 expression
    eqp FZ (FS FZ)False
    Example1 expression
    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]
  • GShow FinDefined in fin-0.3.2 · Data.Fin
  • OrdP FinDefined in fin-0.3.2 · Data.Fin
    Example1 expression
    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]
  • (n ~ 'S m, SNatI m) => Bounded (Fin n)Defined in fin-0.3.2 · Data.Fin
  • SNatI n => Enum (Fin n)Defined in fin-0.3.2 · Data.Fin
  • Eq (Fin n)Defined in fin-0.3.2 · Data.Fin
  • SNatI n => Integral (Fin n)Defined in fin-0.3.2 · Data.Fin

    quot works only on Fin n where n is prime.

  • SNatI n => Num (Fin n)Defined in fin-0.3.2 · Data.Fin

    Operations module n.

    Example1 expression
    map fromInteger [0, 1, 2, 3, 4, -5] :: [Fin N.Nat3][0,1,2,0,1,1]
    Example1 expression
    fromInteger 42 :: Fin N.Nat0*** Exception: divide by zero...
    Example1 expression
    signum (FZ :: Fin N.Nat1)0
    Example1 expression
    signum (3 :: Fin N.Nat4)1
    Example1 expression
    2 + 3 :: Fin N.Nat41
    Example1 expression
    2 * 3 :: Fin N.Nat42
  • Ord (Fin n)Defined in fin-0.3.2 · Data.Fin
  • SNatI n => Real (Fin n)Defined in fin-0.3.2 · Data.Fin
  • Show (Fin n)Defined in fin-0.3.2 · Data.Fin

    Fin is printed as Natural.

    To see explicit structure, use explicitShow or explicitShowsPrec

  • NFData (Fin n)Defined in fin-0.3.2 · Data.Fin
  • (n ~ 'S m, SNatI m) => Arbitrary (Fin n)Defined in fin-0.3.2 · Data.Fin
  • CoArbitrary (Fin n)Defined in fin-0.3.2 · Data.Fin
  • (n ~ 'S m, SNatI m) => Function (Fin n)Defined in fin-0.3.2 · Data.Fin
  • Hashable (Fin n)Defined in fin-0.3.2 · Data.Fin
  • n ~ 'Z => Absurd (Fin n)Defined in fin-0.3.2 · Data.Fin
  • SNatI n => Finite (Fin n)Defined in fin-0.3.2 · Data.Fin
    Example1 expression
    (U.cardinality :: U.Tagged (Fin N.Nat3) Natural) == U.Tagged (genericLength (U.universeF :: [Fin N.Nat3]))True
  • SNatI n => Universe (Fin n)Defined in fin-0.3.2 · Data.Fin
valuecata :: a -> (a -> a) -> Fin n -> a
#

Fold Fin.

Showing

2 declarations
valueexplicitShow :: Fin n -> String
#

show displaying a structure of Fin.

Example1 expression
explicitShow (0 :: Fin N.Nat1)"FZ"
Example1 expression
explicitShow (2 :: Fin N.Nat3)"FS (FS FZ)"

Conversions

4 declarations
valuefromNat :: SNatI n => Nat -> Maybe (Fin n)
#

Convert from Nat.

Example1 expression
fromNat N.nat1 :: Maybe (Fin N.Nat2)Just 1
Example1 expression
fromNat N.nat1 :: Maybe (Fin N.Nat1)Nothing

Interesting

8 declarations
valuemirror :: SNatI n => Fin n -> Fin n
#

Mirror the values, minBound becomes maxBound, etc.

Example1 expression
map mirror universe :: [Fin N.Nat4][3,2,1,0]
Example1 expression
reverse universe :: [Fin N.Nat4][3,2,1,0]
valueinverse :: SNatI n => Fin n -> Fin n
#

Multiplicative inverse.

Works for Fin n where n is coprime with an argument, i.e. in general when n is prime.

Example1 expression
map inverse universe :: [Fin N.Nat5][0,1,3,2,4]
Example1 expression
zipWith (*) universe (map inverse universe) :: [Fin N.Nat5][0,1,1,1,1]

Adaptation of pseudo-code in Wikipedia

valueuniverse :: SNatI n => [Fin n]
#

All values. [minBound .. maxBound] won't work for Fin Nat0.

Example1 expression
universe :: [Fin N.Nat3][0,1,2]
valueinlineUniverse :: SNatI n => [Fin n]
#

universe which will be fully inlined, if n is known at compile time.

Example1 expression
inlineUniverse :: [Fin N.Nat3][0,1,2]
valueboring :: Fin Nat1
#

Counting to one is boring.

Example1 expression
boring0

Plus

6 declarations
valueweakenLeft :: SNatI n => Proxy m -> Fin n -> Fin (Plus n m)
#
Example1 expression
map (weakenLeft (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])[0,1,2]
valueweakenLeft1 :: SNatI n => Fin n -> Fin ('S n)
#
Example1 expression
map weakenLeft1 universe :: [Fin N.Nat5][0,1,2,3]
valueweakenRight :: SNatI n => Proxy n -> Fin m -> Fin (Plus n m)
#
Example1 expression
map (weakenRight (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])[2,3,4]
valueweakenRight1 :: Fin n -> Fin ('S n)
#
Example1 expression
map weakenRight1 universe :: [Fin N.Nat5][1,2,3,4]
valueappend :: SNatI n => Either (Fin n) (Fin m) -> Fin (Plus n m)
#

Append two Fins together.

Example1 expression
append (Left fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))2
Example1 expression
append (Right fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))7
valuesplit :: SNatI n => Fin (Plus n m) -> Either (Fin n) (Fin m)
#

Inverse of append.

Example1 expression
split fin2 :: Either (Fin N.Nat2) (Fin N.Nat3)Right 0
Example1 expression
split fin1 :: Either (Fin N.Nat2) (Fin N.Nat3)Left 1
Example1 expression
map split universe :: [Either (Fin N.Nat2) (Fin N.Nat3)][Left 0,Left 1,Right 0,Right 1,Right 2]

Min and max

2 declarations
valueisMin :: Fin ('S n) -> Maybe (Fin n)
#

Return a one less.

Example1 expression
isMin (FZ :: Fin N.Nat1)Nothing
Example1 expression
map isMin universe :: [Maybe (Fin N.Nat3)][Nothing,Just 0,Just 1,Just 2]
valueisMax :: SNatI n => Fin ('S n) -> Maybe (Fin n)
#

Return a one less.

Example1 expression
isMax (FZ :: Fin N.Nat1)Nothing
Example1 expression
map isMax universe :: [Maybe (Fin N.Nat3)][Just 0,Just 1,Just 2,Nothing]

Aliases

10 declarations