HORIZON HASKELLDocslts/ghc-10.0.x77a86622026-10-31Search packagesCtrl K
Theme: |

GHC 10.0.0.20260917 · lts/ghc-10.0.x · 77a8662 · 2026-10-31

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
Contents
  1. Showing
  2. Conversions
  3. Interesting
  4. Plus
  5. Min and max
  6. Aliases
Synopsis
  • Packagefin-0.3.2
  • Exports34
  • LanguageHaskell2010
  • LicenceBSD-3-Clause
  • SourceFin.hs
datadata Fin (n :: Nat) where
Source#

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

Showing

valueexplicitShow :: Fin n -> String
Source#

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

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

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

valuemirror :: SNatI n => Fin n -> Fin n
Source#

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

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

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

Example1 expression
universe :: [Fin N.Nat3][0,1,2]

Plus

valueappend :: SNatI n => Either (Fin n) (Fin m) -> Fin (Plus n m)
Source#

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

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

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

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

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