Data.TypeNums.Ints

Type level integers can be used in the same way as type level naturals from GHC.TypeLits, for example 3. However, a minus sign is not recognised in this context, so a negative type-level integer is instead written as Neg n.

Construction

data TInt

(Kind) An integer that may be negative.

Constructors

Pos Nat

Neg Nat

Instances

KnownNat n => KnownInt ('Pos n :: TInt)

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt ('Pos n)

KnownNat n => KnownInt ('Neg n :: TInt)

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt ('Neg n)

Linking type and value level

class KnownInt (n :: k)

This class gives the (value-level) integer associated with a type-level integer. There are instances of this class for every concrete natural: 0, 1, 2, etc. There are also instances of this class for every negated natural, such as Neg 1.

Minimal complete definition

intSing

Instances

KnownNat n => KnownInt (n :: Nat)

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt n

KnownNat n => KnownInt ('Pos n :: TInt)

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt ('Pos n)

KnownNat n => KnownInt ('Neg n :: TInt)

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt ('Neg n)

intVal :: forall n proxy. KnownInt n => proxy n -> Integer

Get the value associated with a type-level integer

intVal' :: forall n. KnownInt n => Proxy# n -> Integer

Get the value associated with a type-level integer. The difference between this function and intVal is that it takes a Proxy# parameter, which has zero runtime representation and so is entirely free.

data SomeInt

This type represents unknown type-level integers.

Since: 0.1.1

Constructors

forall n.KnownInt n => SomeInt (Proxy n)

Instances

Eq SomeInt

Defined in Data.TypeNums.Ints

Methods

(==) :: SomeInt -> SomeInt -> Bool

(/=) :: SomeInt -> SomeInt -> Bool

Ord SomeInt

Defined in Data.TypeNums.Ints

Methods

compare :: SomeInt -> SomeInt -> Ordering

(<) :: SomeInt -> SomeInt -> Bool

(<=) :: SomeInt -> SomeInt -> Bool

(>) :: SomeInt -> SomeInt -> Bool

(>=) :: SomeInt -> SomeInt -> Bool

max :: SomeInt -> SomeInt -> SomeInt

min :: SomeInt -> SomeInt -> SomeInt

Read SomeInt

Defined in Data.TypeNums.Ints

Methods

readsPrec :: Int -> ReadS SomeInt

readList :: ReadS [SomeInt]

readPrec :: ReadPrec SomeInt

readListPrec :: ReadPrec [SomeInt]

Show SomeInt

Defined in Data.TypeNums.Ints

Methods

showsPrec :: Int -> SomeInt -> ShowS

show :: SomeInt -> String

showList :: [SomeInt] -> ShowS

someIntVal :: Integer -> SomeInt

Convert an integer into an unknown type-level integer.

Since: 0.1.1