fin-0.3.1: Nat and Fin: peano naturals and finite numbers
Safe HaskellTrustworthy
LanguageHaskell2010

Data.Type.Nat

Description

Nat numbers. DataKinds stuff.

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

Synopsis

Natural, Nat numbers

data Nat Source #

Nat natural numbers.

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

Constructors

Z 
S Nat 

Instances

Instances details
Arbitrary Nat Source # 
Instance details

Defined in Data.Nat

Methods

arbitrary :: Gen Nat #

shrink :: Nat -> [Nat] #

CoArbitrary Nat Source # 
Instance details

Defined in Data.Nat

Methods

coarbitrary :: Nat -> Gen b -> Gen b #

Function Nat Source # 
Instance details

Defined in Data.Nat

Methods

function :: (Nat -> b) -> Nat :-> b #

Data Nat Source # 
Instance details

Defined in Data.Nat

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Nat -> c Nat #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Nat #

toConstr :: Nat -> Constr #

dataTypeOf :: Nat -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Nat) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat) #

gmapT :: (forall b. Data b => b -> b) -> Nat -> Nat #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r #

gmapQ :: (forall d. Data d => d -> u) -> Nat -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Nat -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Nat -> m Nat #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat #

Enum Nat Source # 
Instance details

Defined in Data.Nat

Methods

succ :: Nat -> Nat #

pred :: Nat -> Nat #

toEnum :: Int -> Nat #

fromEnum :: Nat -> Int #

enumFrom :: Nat -> [Nat] #

enumFromThen :: Nat -> Nat -> [Nat] #

enumFromTo :: Nat -> Nat -> [Nat] #

enumFromThenTo :: Nat -> Nat -> Nat -> [Nat] #

Num Nat Source # 
Instance details

Defined in Data.Nat

Methods

(+) :: Nat -> Nat -> Nat #

(-) :: Nat -> Nat -> Nat #

(*) :: Nat -> Nat -> Nat #

negate :: Nat -> Nat #

abs :: Nat -> Nat #

signum :: Nat -> Nat #

fromInteger :: Integer -> Nat #

Integral Nat Source # 
Instance details

Defined in Data.Nat

Methods

quot :: Nat -> Nat -> Nat #

rem :: Nat -> Nat -> Nat #

div :: Nat -> Nat -> Nat #

mod :: Nat -> Nat -> Nat #

quotRem :: Nat -> Nat -> (Nat, Nat) #

divMod :: Nat -> Nat -> (Nat, Nat) #

toInteger :: Nat -> Integer #

Real Nat Source # 
Instance details

Defined in Data.Nat

Methods

toRational :: Nat -> Rational #

Show Nat Source #

Nat is printed as Natural.

To see explicit structure, use explicitShow or explicitShowsPrec

Instance details

Defined in Data.Nat

Methods

showsPrec :: Int -> Nat -> ShowS #

show :: Nat -> String #

showList :: [Nat] -> ShowS #

NFData Nat Source # 
Instance details

Defined in Data.Nat

Methods

rnf :: Nat -> () #

Eq Nat Source # 
Instance details

Defined in Data.Nat

Methods

(==) :: Nat -> Nat -> Bool #

(/=) :: Nat -> Nat -> Bool #

Ord Nat Source # 
Instance details

Defined in Data.Nat

Methods

compare :: Nat -> Nat -> Ordering #

(<) :: Nat -> Nat -> Bool #

(<=) :: Nat -> Nat -> Bool #

(>) :: Nat -> Nat -> Bool #

(>=) :: Nat -> Nat -> Bool #

max :: Nat -> Nat -> Nat #

min :: Nat -> Nat -> Nat #

Hashable Nat Source # 
Instance details

Defined in Data.Nat

Methods

hashWithSalt :: Int -> Nat -> Int #

hash :: Nat -> Int #

Universe Nat Source #
>>> import qualified Data.Universe.Class as U
>>> take 10 (U.universe :: [Nat])
[0,1,2,3,4,5,6,7,8,9]

Since: 0.1.2

Instance details

Defined in Data.Nat

Methods

universe :: [Nat] #

Category LEProof Source #

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

Instance details

Defined in Data.Type.Nat.LE.ReflStep

Methods

id :: forall (a :: k). LEProof a a #

(.) :: forall (b :: k) (c :: k) (a :: k). LEProof b c -> LEProof a b -> LEProof a c #

TestEquality SNat Source # 
Instance details

Defined in Data.Type.Nat

Methods

testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b) #

EqP Fin Source #
>>> eqp FZ FZ
True
>>> eqp FZ (FS FZ)
False
>>> 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]

Since: 0.2.2

Instance details

Defined in Data.Fin

Methods

eqp :: forall (a :: k) (b :: k). Fin a -> Fin b -> Bool #

EqP SNat Source #

Since: 0.2.2

Instance details

Defined in Data.Type.Nat

Methods

eqp :: forall (a :: k) (b :: k). SNat a -> SNat b -> Bool #

GNFData SNat Source #

Since: 0.2.1

Instance details

Defined in Data.Type.Nat

Methods

grnf :: forall (a :: k). SNat a -> () #

GCompare SNat Source #

Since: 0.2.1

Instance details

Defined in Data.Type.Nat

Methods

gcompare :: forall (a :: k) (b :: k). SNat a -> SNat b -> GOrdering a b #

GEq SNat Source #

Since: 0.2.1

Instance details

Defined in Data.Type.Nat

Methods

geq :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b) #

GShow Fin Source #

Since: 0.2.2

Instance details

Defined in Data.Fin

Methods

gshowsPrec :: forall (a :: k). Int -> Fin a -> ShowS #

GShow SNat Source #

Since: 0.2.1

Instance details

Defined in Data.Type.Nat

Methods

gshowsPrec :: forall (a :: k). Int -> SNat a -> ShowS #

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

Since: 0.2.2

Instance details

Defined in Data.Fin

Methods

comparep :: forall (a :: k) (b :: k). Fin a -> Fin b -> Ordering #

OrdP SNat Source #

Since: 0.2.2

Instance details

Defined in Data.Type.Nat

Methods

comparep :: forall (a :: k) (b :: k). SNat a -> SNat b -> Ordering #

toNatural :: Nat -> Natural Source #

Convert Nat to Natural

>>> toNatural 0
0
>>> toNatural 2
2
>>> toNatural $ S $ S $ Z
2

fromNatural :: Natural -> Nat Source #

Convert Natural to Nat

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

cata :: a -> (a -> a) -> Nat -> a Source #

Fold Nat.

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

Showing

explicitShow :: Nat -> String Source #

show displaying a structure of Nat.

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

explicitShowsPrec :: Int -> Nat -> ShowS Source #

showsPrec displaying a structure of Nat.

Singleton

data SNat (n :: Nat) where Source #

Singleton of Nat.

Constructors

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

Instances

Instances details
TestEquality SNat Source # 
Instance details

Defined in Data.Type.Nat

Methods

testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b) #

EqP SNat Source #

Since: 0.2.2

Instance details

Defined in Data.Type.Nat

Methods

eqp :: forall (a :: k) (b :: k). SNat a -> SNat b -> Bool #

GNFData SNat Source #

Since: 0.2.1

Instance details

Defined in Data.Type.Nat

Methods

grnf :: forall (a :: k). SNat a -> () #

GCompare SNat Source #

Since: 0.2.1

Instance details

Defined in Data.Type.Nat

Methods

gcompare :: forall (a :: k) (b :: k). SNat a -> SNat b -> GOrdering a b #

GEq SNat Source #

Since: 0.2.1

Instance details

Defined in Data.Type.Nat

Methods

geq :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b) #

GShow SNat Source #

Since: 0.2.1

Instance details

Defined in Data.Type.Nat

Methods

gshowsPrec :: forall (a :: k). Int -> SNat a -> ShowS #

OrdP SNat Source #

Since: 0.2.2

Instance details

Defined in Data.Type.Nat

Methods

comparep :: forall (a :: k) (b :: k). SNat a -> SNat b -> Ordering #

Show (SNat p) Source # 
Instance details

Defined in Data.Type.Nat

Methods

showsPrec :: Int -> SNat p -> ShowS #

show :: SNat p -> String #

showList :: [SNat p] -> ShowS #

SNatI n => Boring (SNat n) Source #

Since: 0.2.1

Instance details

Defined in Data.Type.Nat

Methods

boring :: SNat n #

NFData (SNat n) Source #

Since: 0.2.1

Instance details

Defined in Data.Type.Nat

Methods

rnf :: SNat n -> () #

Eq (SNat a) Source #

Since: 0.2.2

Instance details

Defined in Data.Type.Nat

Methods

(==) :: SNat a -> SNat a -> Bool #

(/=) :: SNat a -> SNat a -> Bool #

Ord (SNat a) Source #

Since: 0.2.2

Instance details

Defined in Data.Type.Nat

Methods

compare :: SNat a -> SNat a -> Ordering #

(<) :: SNat a -> SNat a -> Bool #

(<=) :: SNat a -> SNat a -> Bool #

(>) :: SNat a -> SNat a -> Bool #

(>=) :: SNat a -> SNat a -> Bool #

max :: SNat a -> SNat a -> SNat a #

min :: SNat a -> SNat a -> SNat a #

snatToNat :: forall n. SNat n -> Nat Source #

Convert SNat to Nat.

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

snatToNatural :: forall n. SNat n -> Natural Source #

Convert SNat to Natural

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

Implicit

class 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.

>>> :set -XPolyKinds
>>> newtype Const a b = Const a deriving (Show)
>>> induction (Const 0) (coerce ((+2) :: Int -> Int)) :: Const Int Nat3
Const 6

Methods

induction Source #

Arguments

:: f 'Z

zero case

-> (forall m. SNatI m => f m -> f ('S m))

induction step

-> f n 

Instances

Instances details
SNatI 'Z Source # 
Instance details

Defined in Data.Type.Nat

Methods

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

SNatI n => SNatI ('S n) Source # 
Instance details

Defined in Data.Type.Nat

Methods

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

snat :: SNatI n => SNat n Source #

Construct explicit SNat value.

withSNat :: SNat n -> (SNatI n => r) -> r Source #

Constructor SNatI dictionary from SNat.

Since: 0.0.3

reify :: forall r. Nat -> (forall n. SNatI n => Proxy n -> r) -> r Source #

Reify Nat.

>>> reify nat3 reflect
3

reflect :: forall n proxy. SNatI n => proxy n -> Nat Source #

Reflect type-level Nat to the term level.

reflectToNum :: forall n m proxy. (SNatI n, Num m) => proxy n -> m Source #

As reflect but with any Num.

Equality

eqNat :: forall n m. (SNatI n, SNatI m) => Maybe (n :~: m) Source #

Decide equality of type-level numbers.

>>> eqNat :: Maybe (Nat3 :~: Plus Nat1 Nat2)
Just Refl
>>> eqNat :: Maybe (Nat3 :~: Mult Nat2 Nat2)
Nothing

type family EqNat (n :: Nat) (m :: Nat) where ... Source #

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 

discreteNat :: forall n m. (SNatI n, SNatI m) => Dec (n :~: m) Source #

Decide equality of type-level numbers.

>>> decShow (discreteNat :: Dec (Nat3 :~: Plus Nat1 Nat2))
"Yes Refl"

Since: 0.0.3

cmpNat :: forall n m. (SNatI n, SNatI m) => GOrdering n m Source #

Decide equality of type-level numbers.

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

Induction

induction1 Source #

Arguments

:: forall n f a. SNatI n 
=> f 'Z a

zero case

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

induction step

-> f n a 

Induction on Nat, functor form. Useful for computation.

Example: unfoldedFix

unfoldedFix :: forall n a proxy. 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

type family Plus (n :: Nat) (m :: Nat) :: Nat where ... Source #

Addition.

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

Equations

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

type family Mult (n :: Nat) (m :: Nat) :: Nat where ... Source #

Multiplication.

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

Equations

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

type family Mult2 (n :: Nat) :: Nat where ... Source #

Multiplication by two. Doubling.

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

Equations

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

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

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

>>> :kind! DivMod2 Nat7 == '(Nat3, True)
DivMod2 Nat7 == '(Nat3, True) :: Bool
= 'True
>>> :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

type family ToGHC (n :: Nat) :: Nat where ... Source #

Convert to GHC Nat.

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

Equations

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

type family FromGHC (n :: Nat) :: Nat where ... Source #

Convert from GHC Nat.

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

Equations

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

Aliases

Nat

promoted Nat

type Nat0 = 'Z Source #

type Nat1 = 'S Nat0 Source #

type Nat2 = 'S Nat1 Source #

type Nat3 = 'S Nat2 Source #

type Nat4 = 'S Nat3 Source #

type Nat5 = 'S Nat4 Source #

type Nat6 = 'S Nat5 Source #

type Nat7 = 'S Nat6 Source #

type Nat8 = 'S Nat7 Source #

type Nat9 = 'S Nat8 Source #

Proofs

proofPlusNZero :: SNatI n => Plus n Nat0 :~: n Source #

n + 0 = n

proofMultNZero :: forall n proxy. SNatI n => proxy n -> Mult n Nat0 :~: Nat0 Source #

n * 0 = 0

proofMultOneN :: SNatI n => Mult Nat1 n :~: n Source #

1 * n = n

proofMultNOne :: SNatI n => Mult n Nat1 :~: n Source #

n * 1 = n