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.Type.Nat

Nat numbers. DataKinds stuff.

This module re-exports Data.Nat, and adds type-level things.

Contents
  1. Natural, Nat numbers
  2. Showing
  3. Singleton
  4. Implicit
  5. Equality
  6. Induction
  7. Example: unfoldedFix
  8. Arithmetic
  9. Conversion to GHC Nat
  10. Aliases
  11. Nat
  12. promoted Nat
  13. Proofs
Synopsis
  • Packagefin-0.3.2
  • Exports54
  • LanguageHaskell2010
  • LicenceBSD-3-Clause
  • SourceNat.hs

Natural, Nat numbers

datadata Nat
Source#

Nat natural numbers.

Better than GHC's built-in Nat for some use cases.

Constructors

Instances25Enum, Eq, Integral, Data, Num, Ord, …
  • Enum NatDefined in fin-0.3.2 · Data.Nat
  • Eq NatDefined in fin-0.3.2 · Data.Nat
  • Integral NatDefined in fin-0.3.2 · Data.Nat
  • Data NatDefined in fin-0.3.2 · Data.Nat
  • Num NatDefined in fin-0.3.2 · Data.Nat
  • Ord NatDefined in fin-0.3.2 · Data.Nat
  • Real NatDefined in fin-0.3.2 · Data.Nat
  • Show NatDefined in fin-0.3.2 · Data.Nat

    Nat is printed as Natural.

    To see explicit structure, use explicitShow or explicitShowsPrec

  • NFData NatDefined in fin-0.3.2 · Data.Nat
  • Arbitrary NatDefined in fin-0.3.2 · Data.Nat
  • CoArbitrary NatDefined in fin-0.3.2 · Data.Nat
  • Function NatDefined in fin-0.3.2 · Data.Nat
  • Hashable NatDefined in fin-0.3.2 · Data.Nat
  • Universe NatDefined in fin-0.3.2 · Data.Nat
    Example2 expressions
    import qualified Data.Universe.Class as Utake 10 (U.universe :: [Nat])[0,1,2,3,4,5,6,7,8,9]
  • Category LEProofDefined in fin-0.3.2 · Data.Type.Nat.LE.ReflStep

    The other variant (Data.Type.Nat.LE.LEPRoof) isn't Category, because leRefl requires SNat evidence.

  • TestEquality SNatDefined in fin-0.3.2 · Data.Type.Nat
  • 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]
  • EqP SNatDefined in fin-0.3.2 · Data.Type.Nat
  • GCompare SNatDefined in fin-0.3.2 · Data.Type.Nat
  • GEq SNatDefined in fin-0.3.2 · Data.Type.Nat
  • GNFData SNatDefined in fin-0.3.2 · Data.Type.Nat
  • GShow FinDefined in fin-0.3.2 · Data.Fin
  • GShow SNatDefined in fin-0.3.2 · Data.Type.Nat
  • 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]
  • OrdP SNatDefined in fin-0.3.2 · Data.Type.Nat
valuetoNatural :: Nat -> Natural
Source#

Convert Nat to Natural

Example1 expression
toNatural 00
Example1 expression
toNatural 22
Example1 expression
toNatural $ S $ S $ Z2
valuecata :: a -> (a -> a) -> Nat -> a
Source#

Fold Nat.

Example1 expression
cata [] ('x' :) 2"xx"

Showing

Singleton

datadata SNat (n :: Nat) where
Source#

Singleton of Nat.

Constructors

Instances12TestEquality, EqP, GCompare, GEq, GNFData, GShow, …
  • TestEquality SNatDefined in fin-0.3.2 · Data.Type.Nat
  • EqP SNatDefined in fin-0.3.2 · Data.Type.Nat
  • GCompare SNatDefined in fin-0.3.2 · Data.Type.Nat
  • GEq SNatDefined in fin-0.3.2 · Data.Type.Nat
  • GNFData SNatDefined in fin-0.3.2 · Data.Type.Nat
  • GShow SNatDefined in fin-0.3.2 · Data.Type.Nat
  • OrdP SNatDefined in fin-0.3.2 · Data.Type.Nat
  • Eq (SNat a)Defined in fin-0.3.2 · Data.Type.Nat
  • Ord (SNat a)Defined in fin-0.3.2 · Data.Type.Nat
  • Show (SNat p)Defined in fin-0.3.2 · Data.Type.Nat
  • NFData (SNat n)Defined in fin-0.3.2 · Data.Type.Nat
  • SNatI n => Boring (SNat n)Defined in fin-0.3.2 · Data.Type.Nat
patternpattern SS' :: () => m ~ 'S n => SNat n -> SNat m
Source#

A pattern with explicit argument

Example2 expressions
let predSNat :: SNat (S n) -> SNat n; predSNat (SS' n) = npredSNat (SS' (SS' SZ))SS
Example1 expression
reflect $ predSNat (SS' (SS' SZ))1

Implicit

classclass SNatI (n :: Nat) where
Source#

Implicit SNat.

In an unorthodox singleton way, it actually provides an induction function.

The induction should often be fully inlined. See test/Inspection.hs.

Example3 expressions
:set -XPolyKindsnewtype Const a b = Const a deriving (Show)induction (Const 0) (coerce ((+2) :: Int -> Int)) :: Const Int Nat3Const 6

Methods

Instances2SNatI
  • SNatI 'ZDefined in fin-0.3.2 · Data.Type.Nat
  • SNatI n => SNatI ('S n)Defined in fin-0.3.2 · Data.Type.Nat

Equality

valueeqNat :: (SNatI n, SNatI m) => Maybe (n :~: m)
Source#

Decide equality of type-level numbers.

Example1 expression
eqNat :: Maybe (Nat3 :~: Plus Nat1 Nat2)Just Refl
Example1 expression
eqNat :: Maybe (Nat3 :~: Mult Nat2 Nat2)Nothing
valuediscreteNat :: (SNatI n, SNatI m) => Dec (n :~: m)
Source#

Decide equality of type-level numbers.

Example1 expression
decShow (discreteNat :: Dec (Nat3 :~: Plus Nat1 Nat2))"Yes Refl"
valuecmpNat :: (SNatI n, SNatI m) => GOrdering n m
Source#

Decide equality of type-level numbers.

Example1 expression
cmpNat :: GOrdering Nat3 (Plus Nat1 Nat2)GEQ
Example1 expression
cmpNat :: GOrdering Nat3 (Mult Nat2 Nat2)GLT
Example1 expression
cmpNat :: GOrdering Nat5 (Mult Nat2 Nat2)GGT

Induction

valueinduction1
  1. :: SNatI n
  2. => f 'Z a

    zero case

  3. -> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a)

    induction step

  4. -> f n a
Source#

Induction on Nat, functor form. Useful for computation.

Example: unfoldedFix

valueunfoldedFix :: SNatI n => proxy n -> (a -> a) -> a
Source#

Unfold n steps of a general recursion.

Note: Always benchmark. This function may give you both bad properties: a lot of code (increased binary size), and worse performance.

For known n unfoldedFix will unfold recursion, for example

unfoldedFix (Proxy :: Proxy Nat3) f = f (f (f (fix f)))

Arithmetic

familytype family Plus (n :: Nat) (m :: Nat) :: Nat where
Source#

Addition.

Example1 expression
reflect (snat :: SNat (Plus Nat1 Nat2))3

Equations

familytype family Mult (n :: Nat) (m :: Nat) :: Nat where
Source#

Multiplication.

Example1 expression
reflect (snat :: SNat (Mult Nat2 Nat3))6

Equations

familytype family Mult2 (n :: Nat) :: Nat where
Source#

Multiplication by two. Doubling.

Example1 expression
reflect (snat :: SNat (Mult2 Nat4))8

Equations

familytype family DivMod2 (n :: Nat) :: (Nat, Bool) where
Source#

Division by two. False is 0 and True is 1 as a remainder.

Example1 expression
:kind! DivMod2 Nat7 == '(Nat3, True)DivMod2 Nat7 == '(Nat3, True) :: Bool= 'True
Example1 expression
:kind! DivMod2 Nat4 == '(Nat2, False)DivMod2 Nat4 == '(Nat2, False) :: Bool= 'True

Equations

Conversion to GHC Nat

Aliases

Nat

promoted Nat

Proofs