typenums-0.1.4: Type level numbers using existing Nat functionality
Copyright(c) 2018-2021 Iris Ward
LicenseBSD3
Maintaineraditu.venyhandottir@gmail.com
Stabilityexperimental
Safe HaskellTrustworthy
LanguageHaskell2010

Data.TypeNums.Ints

Description

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.

Synopsis

Construction

data TInt Source #

(Kind) An integer that may be negative.

Constructors

Pos Nat 
Neg Nat 

Instances

Instances details
KnownNat n => KnownInt ('Pos n :: TInt) Source # 
Instance details

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt ('Pos n)

KnownNat n => KnownInt ('Neg n :: TInt) Source # 
Instance details

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt ('Neg n)

Linking type and value level

class KnownInt (n :: k) Source #

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

Instances details
KnownNat n => KnownInt (n :: Nat) Source # 
Instance details

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt n

KnownNat n => KnownInt ('Pos n :: TInt) Source # 
Instance details

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt ('Pos n)

KnownNat n => KnownInt ('Neg n :: TInt) Source # 
Instance details

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt ('Neg n)

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

Get the value associated with a type-level integer

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

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 Source #

This type represents unknown type-level integers.

Since: 0.1.1

Constructors

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

Instances

Instances details
Eq SomeInt Source # 
Instance details

Defined in Data.TypeNums.Ints

Methods

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

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

Ord SomeInt Source # 
Instance details

Defined in Data.TypeNums.Ints

Read SomeInt Source # 
Instance details

Defined in Data.TypeNums.Ints

Show SomeInt Source # 
Instance details

Defined in Data.TypeNums.Ints

someIntVal :: Integer -> SomeInt Source #

Convert an integer into an unknown type-level integer.

Since: 0.1.1