Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
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
- 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. SNatI n => Fin n -> Fin n
- inverse :: forall n. SNatI n => Fin n -> Fin n
- universe :: SNatI n => [Fin n]
- inlineUniverse :: SNatI n => [Fin n]
- universe1 :: SNatI n => NonEmpty (Fin ('S n))
- inlineUniverse1 :: SNatI n => NonEmpty (Fin ('S n))
- absurd :: Fin Nat0 -> b
- boring :: Fin Nat1
- weakenLeft :: forall n m. SNatI n => Proxy m -> Fin n -> Fin (Plus n m)
- weakenLeft1 :: SNatI n => Fin n -> Fin ('S n)
- weakenRight :: forall n m. SNatI n => Proxy n -> Fin m -> Fin (Plus n m)
- weakenRight1 :: Fin n -> Fin ('S n)
- append :: forall n m. SNatI n => Either (Fin n) (Fin m) -> Fin (Plus n m)
- split :: forall n m. SNatI n => Fin (Plus n m) -> Either (Fin n) (Fin m)
- isMin :: Fin ('S n) -> Maybe (Fin n)
- isMax :: forall n. SNatI 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]
.
Instances
EqP Fin Source # |
Since: 0.2.2 |
GShow Fin Source # | Since: 0.2.2 |
OrdP Fin Source # |
Since: 0.2.2 |
(n ~ 'S m, SNatI m) => Arbitrary (Fin n) Source # | |
CoArbitrary (Fin n) Source # | |
(n ~ 'S m, SNatI m) => Function (Fin n) Source # | |
(n ~ 'S m, SNatI m) => Bounded (Fin n) Source # | |
SNatI n => Enum (Fin n) Source # | |
SNatI n => Num (Fin n) Source # | Operations module
|
SNatI n => Integral (Fin n) Source # | |
SNatI n => Real (Fin n) Source # | |
Defined in Data.Fin toRational :: Fin n -> Rational # | |
Show (Fin n) Source # | To see explicit structure, use |
n ~ 'Z => Absurd (Fin n) Source # | Since: 0.2.1 |
NFData (Fin n) Source # | |
Eq (Fin n) Source # | |
Ord (Fin n) Source # | |
Hashable (Fin n) Source # | |
SNatI n => Finite (Fin n) Source # |
Since: 0.1.2 |
SNatI n => Universe (Fin n) Source # | Since: 0.1.2 |
Showing
explicitShow :: Fin n -> String Source #
Conversions
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
Interesting
inverse :: forall n. SNatI n => Fin n -> Fin n Source #
Multiplicative inverse.
Works for
where Fin
nn
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
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]
inlineUniverse1 :: SNatI n => NonEmpty (Fin ('S n)) Source #
>>>
inlineUniverse1 :: NonEmpty (Fin N.Nat3)
0 :| [1,2]
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 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. 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