Safe Haskell | Trustworthy |
---|---|
Language | Haskell2010 |
Synopsis
- data Nat
- toNatural :: Nat -> Natural
- fromNatural :: Natural -> Nat
- cata :: a -> (a -> a) -> Nat -> a
- explicitShow :: Nat -> String
- explicitShowsPrec :: Int -> Nat -> ShowS
- data SNat (n :: Nat) where
- snatToNat :: forall n. SNat n -> Nat
- snatToNatural :: forall n. SNat n -> Natural
- class SNatI (n :: Nat) where
- snat :: SNatI n => SNat n
- withSNat :: SNat n -> (SNatI n => r) -> r
- reify :: forall r. Nat -> (forall n. SNatI n => Proxy n -> r) -> r
- reflect :: forall n proxy. SNatI n => proxy n -> Nat
- reflectToNum :: forall n m proxy. (SNatI n, Num m) => proxy n -> m
- eqNat :: forall n m. (SNatI n, SNatI m) => Maybe (n :~: m)
- type family EqNat (n :: Nat) (m :: Nat) where ...
- discreteNat :: forall n m. (SNatI n, SNatI m) => Dec (n :~: m)
- cmpNat :: forall n m. (SNatI n, SNatI m) => GOrdering n m
- induction1 :: forall n f a. SNatI n => f 'Z a -> (forall m. SNatI m => f m a -> f ('S m) a) -> f n a
- unfoldedFix :: forall n a proxy. SNatI n => proxy n -> (a -> a) -> a
- type family Plus (n :: Nat) (m :: Nat) :: Nat where ...
- type family Mult (n :: Nat) (m :: Nat) :: Nat where ...
- type family Mult2 (n :: Nat) :: Nat where ...
- type family DivMod2 (n :: Nat) :: (Nat, Bool) where ...
- type family ToGHC (n :: Nat) :: Nat where ...
- type family FromGHC (n :: Nat) :: Nat where ...
- nat0 :: Nat
- nat1 :: Nat
- nat2 :: Nat
- nat3 :: Nat
- nat4 :: Nat
- nat5 :: Nat
- nat6 :: Nat
- nat7 :: Nat
- nat8 :: Nat
- nat9 :: Nat
- type Nat0 = 'Z
- type Nat1 = 'S Nat0
- type Nat2 = 'S Nat1
- type Nat3 = 'S Nat2
- type Nat4 = 'S Nat3
- type Nat5 = 'S Nat4
- type Nat6 = 'S Nat5
- type Nat7 = 'S Nat6
- type Nat8 = 'S Nat7
- type Nat9 = 'S Nat8
- proofPlusZeroN :: Plus Nat0 n :~: n
- proofPlusNZero :: SNatI n => Plus n Nat0 :~: n
- proofMultZeroN :: Mult Nat0 n :~: Nat0
- proofMultNZero :: forall n proxy. SNatI n => proxy n -> Mult n Nat0 :~: Nat0
- proofMultOneN :: SNatI n => Mult Nat1 n :~: n
- proofMultNOne :: SNatI n => Mult n Nat1 :~: n
Natural, Nat numbers
Nat natural numbers.
Better than GHC's built-in Nat
for some use cases.
Instances
Arbitrary Nat Source # | |
CoArbitrary Nat Source # | |
Function Nat Source # | |
Data Nat Source # | |
Defined in Data.Nat 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 # 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 # | |
Num Nat Source # | |
Integral Nat Source # | |
Real Nat Source # | |
Defined in Data.Nat toRational :: Nat -> Rational # | |
Show Nat Source # | To see explicit structure, use |
NFData Nat Source # | |
Eq Nat Source # | |
Ord Nat Source # | |
Hashable Nat Source # | |
Universe Nat Source # |
Since: 0.1.2 |
Category LEProof Source # | The other variant ( |
TestEquality SNat Source # | |
Defined in Data.Type.Nat | |
EqP Fin Source # |
Since: 0.2.2 |
EqP SNat Source # | Since: 0.2.2 |
GNFData SNat Source # | Since: 0.2.1 |
Defined in Data.Type.Nat | |
GCompare SNat Source # | Since: 0.2.1 |
GEq SNat Source # | Since: 0.2.1 |
GShow Fin Source # | Since: 0.2.2 |
GShow SNat Source # | Since: 0.2.1 |
Defined in Data.Type.Nat gshowsPrec :: forall (a :: k). Int -> SNat a -> ShowS # | |
OrdP Fin Source # |
Since: 0.2.2 |
OrdP SNat Source # | Since: 0.2.2 |
fromNatural :: Natural -> Nat Source #
Showing
explicitShow :: Nat -> String Source #
Singleton
data SNat (n :: Nat) where Source #
Singleton of Nat
.
Instances
TestEquality SNat Source # | |
Defined in Data.Type.Nat | |
EqP SNat Source # | Since: 0.2.2 |
GNFData SNat Source # | Since: 0.2.1 |
Defined in Data.Type.Nat | |
GCompare SNat Source # | Since: 0.2.1 |
GEq SNat Source # | Since: 0.2.1 |
GShow SNat Source # | Since: 0.2.1 |
Defined in Data.Type.Nat gshowsPrec :: forall (a :: k). Int -> SNat a -> ShowS # | |
OrdP SNat Source # | Since: 0.2.2 |
Show (SNat p) Source # | |
SNatI n => Boring (SNat n) Source # | Since: 0.2.1 |
Defined in Data.Type.Nat | |
NFData (SNat n) Source # | Since: 0.2.1 |
Defined in Data.Type.Nat | |
Eq (SNat a) Source # | Since: 0.2.2 |
Ord (SNat a) Source # | Since: 0.2.2 |
snatToNatural :: forall n. SNat n -> Natural Source #
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
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 #
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.
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
:: 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
type family Mult (n :: Nat) (m :: Nat) :: Nat where ... Source #
Multiplication.
>>>
reflect (snat :: SNat (Mult Nat2 Nat3))
6
type family Mult2 (n :: Nat) :: Nat where ... Source #
Multiplication by two. Doubling.
>>>
reflect (snat :: SNat (Mult2 Nat4))
8
type family DivMod2 (n :: Nat) :: (Nat, Bool) where ... Source #
Conversion to GHC Nat
type family ToGHC (n :: Nat) :: Nat where ... Source #
Convert to GHC Nat
.
>>>
:kind! ToGHC Nat5
ToGHC Nat5 :: GHC.Nat... = 5
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))))))