Data.Type.Nat · fin-0.3.2 · horizon-platform

Natural, Nat numbers

4 declarations

datadata Nat

#

Nat natural numbers.

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

Constructors

Z
S Nat

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 U>>> take 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

#

Convert Nat to Natural

Example1 expression

>>> toNatural 00

Example1 expression

>>> toNatural 22

Example1 expression

>>> toNatural $ S $ S $ Z2

valuefromNatural :: Natural -> Nat

#

Convert Natural to Nat

Example1 expression

>>> fromNatural 44

Example1 expression

>>> explicitShow (fromNatural 4)"S (S (S (S Z)))"

valuecata :: a -> (a -> a) -> Nat -> a

#

Fold Nat.

Example1 expression

>>> cata [] ('x' :) 2"xx"

Showing

2 declarations

valueexplicitShow :: Nat -> String

#

show displaying a structure of Nat.

Example1 expression

>>> explicitShow 0"Z"

Example1 expression

>>> explicitShow 2"S (S Z)"

valueexplicitShowsPrec :: Int -> Nat -> ShowS

#

showsPrec displaying a structure of Nat.

Singleton

4 declarations

datadata SNat (n :: Nat) where

#

Singleton of Nat.

Constructors

SZ :: SNat 'Z
SS :: SNatI n1 => SNat ('S n1)

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

#

A pattern with explicit argument

Example2 expressions

>>> let predSNat :: SNat (S n) -> SNat n; predSNat (SS' n) = n>>> predSNat (SS' (SS' SZ))SS

Example1 expression

>>> reflect $ predSNat (SS' (SS' SZ))1

valuesnatToNat :: SNat n -> Nat

#

Convert SNat to Nat.

Example1 expression

>>> snatToNat (snat :: SNat Nat1)1

valuesnatToNatural :: SNat n -> Natural

#

Convert SNat to Natural

Example1 expression

>>> snatToNatural (snat :: SNat Nat0)0

Example1 expression

>>> snatToNatural (snat :: SNat Nat2)2

Implicit

6 declarations

classclass SNatI (n :: Nat) where

#

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 -XPolyKinds>>> newtype Const a b = Const a deriving (Show)>>> induction (Const 0) (coerce ((+2) :: Int -> Int)) :: Const Int Nat3Const 6

Methods

induction :: f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n

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

valuesnat :: SNatI n => SNat n

#

Construct explicit SNat value.

valuewithSNat :: SNat n -> (SNatI n => r) -> r

#

Constructor SNatI dictionary from SNat.

valuereify :: Nat -> (forall (n :: Nat). SNatI n => Proxy n -> r) -> r

#

Reify Nat.

Example1 expression

>>> reify nat3 reflect3

valuereflect :: SNatI n => proxy n -> Nat

#

Reflect type-level Nat to the term level.

valuereflectToNum :: (SNatI n, Num m) => proxy n -> m

#

As reflect but with any Num.

Equality

4 declarations

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

#

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

familytype family EqNat (n :: Nat) (m :: Nat) :: Bool where

#

Type family used to implement == from Data.Type.Equality module.

Equations

EqNat 'Z 'Z = 'True
EqNat ('S n) ('S m) = EqNat n m
EqNat n m = 'False

valuediscreteNat :: (SNatI n, SNatI m) => Dec (n :~: m)

#

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

#

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

1 declaration

valueinduction1

:: SNatI n
=> f 'Z a
zero case
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a)
induction step
-> f n a

#

Induction on Nat, functor form. Useful for computation.

Example: unfoldedFix

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

#

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

4 declarations

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

#

Addition.

Example1 expression

>>> reflect (snat :: SNat (Plus Nat1 Nat2))3

Equations

Plus 'Z m = m
Plus ('S n) m = 'S (Plus n m)

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

#

Multiplication.

Example1 expression

>>> reflect (snat :: SNat (Mult Nat2 Nat3))6

Equations

Mult 'Z m = 'Z
Mult ('S n) m = Plus m (Mult n m)

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

#

Multiplication by two. Doubling.

Example1 expression

>>> reflect (snat :: SNat (Mult2 Nat4))8

Equations

Mult2 'Z = 'Z
Mult2 ('S n) = 'S ('S (Mult2 n))

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

#

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

DivMod2 'Z = '('Z, 'False)
DivMod2 ('S 'Z) = '('Z, 'True)
DivMod2 ('S ('S n)) = DivMod2' (DivMod2 n)

Conversion to GHC Nat

2 declarations

familytype family ToGHC (n :: Nat) :: Nat where

#

Convert to GHC Nat.

Example1 expression

>>> :kind! ToGHC Nat5ToGHC Nat5 :: GHC.Nat...= 5

Equations

ToGHC 'Z = 0
ToGHC ('S n) = 1 + ToGHC n

familytype family FromGHC (n :: Nat) :: Nat where

#

Convert from GHC Nat.

Example1 expression

>>> :kind! FromGHC 7FromGHC 7 :: Nat= 'S ('S ('S ('S ('S ('S ('S 'Z))))))

Equations

FromGHC 0 = 'Z
FromGHC n = 'S (FromGHC (n - 1))

Aliases

0 declarations

Nat

valuenat0 :: Nat

valuenat1 :: Nat

valuenat2 :: Nat

valuenat3 :: Nat

valuenat4 :: Nat

valuenat5 :: Nat

valuenat6 :: Nat

valuenat7 :: Nat

valuenat8 :: Nat

valuenat9 :: Nat

promoted Nat

typetype Nat0 = 'Z

#

typetype Nat1 = 'S Nat0

#

typetype Nat2 = 'S Nat1

#

typetype Nat3 = 'S Nat2

#

typetype Nat4 = 'S Nat3

#

typetype Nat5 = 'S Nat4

#

typetype Nat6 = 'S Nat5

#

typetype Nat7 = 'S Nat6

#

typetype Nat8 = 'S Nat7

#

typetype Nat9 = 'S Nat8

#

Proofs

6 declarations

valueproofPlusZeroN :: Plus Nat0 n :~: n

#

0 + n = n

valueproofPlusNZero :: SNatI n => Plus n Nat0 :~: n

#

n + 0 = n

valueproofMultZeroN :: Mult Nat0 n :~: Nat0

#

0 * n = 0

valueproofMultNZero :: SNatI n => proxy n -> Mult n Nat0 :~: Nat0

#

n * 0 = 0

valueproofMultOneN :: SNatI n => Mult Nat1 n :~: n

#

1 * n = n

valueproofMultNOne :: SNatI n => Mult n Nat1 :~: n

#

n * 1 = n