| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Numeric.PositiveInteger
Description
This module provides a type for the positive integers, together with conversion functions and other operations.
When an operation is partial (for example, subtraction), the result
has a Maybe type, letting the user handle such case, without the
need for handling exceptions during evaluation.
As a result, PositiveInteger is not an instance of the Num class
or any of its subclasses. Functions are provided that offer similar
functionality.
It is recommended that you import this module qualified, as some of the function names clash with those from the Prelude.
Synopsis
- data PositiveInteger
- one :: PositiveInteger
- fromNatural :: Natural -> Maybe PositiveInteger
- fromIntegral :: Integral a => a -> Maybe PositiveInteger
- toNatural :: PositiveInteger -> Natural
- toNum :: Num a => PositiveInteger -> a
- fromTypeNat :: forall (n :: Nat) proxy. (KnownNat n, n > 0) => proxy n -> PositiveInteger
- withTypeNat :: PositiveInteger -> (forall (proxy :: Nat -> Type) (n :: Nat). (KnownNat n, n > 0) => proxy n -> a) -> a
- fromTypeNat1 :: forall proxy (n :: Nat). KnownNat n => proxy (1 + n) -> PositiveInteger
- withTypeNat1 :: PositiveInteger -> (forall (proxy :: Natural -> Type) (n :: Nat). KnownNat n => proxy (1 + n) -> a) -> a
- next :: PositiveInteger -> PositiveInteger
- add :: PositiveInteger -> PositiveInteger -> PositiveInteger
- sub :: PositiveInteger -> PositiveInteger -> Maybe PositiveInteger
- mul :: PositiveInteger -> PositiveInteger -> PositiveInteger
- div :: PositiveInteger -> PositiveInteger -> Maybe PositiveInteger
- length :: Foldable1 t => t a -> PositiveInteger
- take :: PositiveInteger -> NonEmpty a -> NonEmpty a
- replicate :: PositiveInteger -> a -> NonEmpty a
- replicateM :: Applicative f => PositiveInteger -> f a -> f (NonEmpty a)
Documentation
data PositiveInteger Source #
Unbounded positive integers.
No Num instance is provided, as no negative integers are available.
Instances
| Read PositiveInteger Source # | |
Defined in Numeric.PositiveInteger Methods readsPrec :: Int -> ReadS PositiveInteger # readList :: ReadS [PositiveInteger] # | |
| Show PositiveInteger Source # | |
Defined in Numeric.PositiveInteger Methods showsPrec :: Int -> PositiveInteger -> ShowS # show :: PositiveInteger -> String # showList :: [PositiveInteger] -> ShowS # | |
| Eq PositiveInteger Source # | |
Defined in Numeric.PositiveInteger Methods (==) :: PositiveInteger -> PositiveInteger -> Bool # (/=) :: PositiveInteger -> PositiveInteger -> Bool # | |
| Ord PositiveInteger Source # | |
Defined in Numeric.PositiveInteger Methods compare :: PositiveInteger -> PositiveInteger -> Ordering # (<) :: PositiveInteger -> PositiveInteger -> Bool # (<=) :: PositiveInteger -> PositiveInteger -> Bool # (>) :: PositiveInteger -> PositiveInteger -> Bool # (>=) :: PositiveInteger -> PositiveInteger -> Bool # max :: PositiveInteger -> PositiveInteger -> PositiveInteger # min :: PositiveInteger -> PositiveInteger -> PositiveInteger # | |
one :: PositiveInteger Source #
The number 1.
Conversions
To PositiveInteger
fromIntegral :: Integral a => a -> Maybe PositiveInteger Source #
Convert from a type that's instance of Integral.
Similar to Prelude's fromIntegral, but the result is
a Maybe, since the input might not be positive.
From PositiveInteger
toNatural :: PositiveInteger -> Natural Source #
Cast a positive integer to a natural number.
toNum :: Num a => PositiveInteger -> a Source #
Convert a positive integer to any type instance of Num.
This is equivalent to Prelude's fromIntegral when the input
type is PositiveInteger.
Type-level conversions
fromTypeNat :: forall (n :: Nat) proxy. (KnownNat n, n > 0) => proxy n -> PositiveInteger Source #
Convert a type-level natural to a positive integer.
Equivalent to natVal for positive integers.
Since: 0.1.1.0
withTypeNat :: PositiveInteger -> (forall (proxy :: Nat -> Type) (n :: Nat). (KnownNat n, n > 0) => proxy n -> a) -> a Source #
Convert a positive integer to a type-level natural and apply a function to it.
Since: 0.1.1.0
fromTypeNat1 :: forall proxy (n :: Nat). KnownNat n => proxy (1 + n) -> PositiveInteger Source #
Convert a type-level natural in n + 1 form to a positive integer.
Since: 0.1.2.0
withTypeNat1 :: PositiveInteger -> (forall (proxy :: Natural -> Type) (n :: Nat). KnownNat n => proxy (1 + n) -> a) -> a Source #
Convert a positive integer to a type-level natural in n + 1 form
and apply a function to it.
Since: 0.1.2.0
Operations
next :: PositiveInteger -> PositiveInteger Source #
Return the next positive integer.
add :: PositiveInteger -> PositiveInteger -> PositiveInteger Source #
Add two positive integers.
sub :: PositiveInteger -> PositiveInteger -> Maybe PositiveInteger Source #
Subtract two positive integers. If the result wouldn't be positive,
Nothing is returned.
mul :: PositiveInteger -> PositiveInteger -> PositiveInteger Source #
Multiply two positive integers.
div :: PositiveInteger -> PositiveInteger -> Maybe PositiveInteger Source #
Divide a positive integer by another. If the divisor is larger than
the dividend, Nothing is returned.
Positive lengths
length :: Foldable1 t => t a -> PositiveInteger Source #
Length of a non-empty data structure.
Non-empty lists
take :: PositiveInteger -> NonEmpty a -> NonEmpty a Source #
Take a positive number of elements from a non-empty list.
replicate :: PositiveInteger -> a -> NonEmpty a Source #
Produce a non-empty list with the same value repeated a given number of times.
replicateM :: Applicative f => PositiveInteger -> f a -> f (NonEmpty a) Source #
Repeat an action a given number of times and collect the results in a non-empty list.