Copyright	(c) 2018 Iris Ward
License	BSD3
Maintainer	aditu.venyhandottir@gmail.com
Stability	experimental
Safe Haskell	Trustworthy
Language	Haskell2010

Data.TypeNums.Ints

Contents

Construction
Linking type and value level

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

data TInt
- = Pos Nat
- | Neg Nat
class KnownInt (n :: k)
intVal :: forall n proxy. KnownInt n => proxy n -> Integer
intVal' :: forall n. KnownInt n => Proxy# n -> Integer
data SomeInt = KnownInt n => SomeInt (Proxy n)
someIntVal :: Integer -> SomeInt

Construction

data TInt Source #

(Kind) An integer that may be negative.

Constructors

Pos Nat
Neg Nat

Instances

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

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: typenums-0.1.1

Constructors

KnownInt n => SomeInt (Proxy n)

Instances

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 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 Source #
Instance details Defined in Data.TypeNums.Ints Methods readsPrec :: Int -> ReadS SomeInt # readList :: ReadS [SomeInt] # readPrec :: ReadPrec SomeInt # readListPrec :: ReadPrec [SomeInt] #
Show SomeInt Source #
Instance details Defined in Data.TypeNums.Ints Methods showsPrec :: Int -> SomeInt -> ShowS # show :: SomeInt -> String # showList :: [SomeInt] -> ShowS #

someIntVal :: Integer -> SomeInt Source #

Convert an integer into an unknown type-level integer.

Since: typenums-0.1.1