Copyright	(c) Alice Rixte 2025
License	BSD 3
Maintainer	alice.rixte@u-bordeaux.fr
Stability	unstable
Portability	non-portable (GHC extensions)
Safe Haskell	None
Language	GHC2024

Data.Type.Int

Description

Type level integers.

Synopsis

data Signed a
- = Pos a
- | Neg a
- | Zero
type ZZ = Signed Nat
type family CmpSigned (a :: Signed k) (b :: Signed k) :: Ordering where ...
type family IsPos (a :: ZZ) :: Bool where ...
type family FlipOrdering (o :: Ordering) :: Ordering where ...
type family NormalizeInt (a :: ZZ) :: ZZ where ...
type family Abs (a :: ZZ) :: Nat where ...
type family Negate (a :: ZZ) :: ZZ where ...
type family AddCmp (cmp :: Ordering) (a :: ZZ) (b :: ZZ) :: ZZ where ...
type family Add (a :: ZZ) (b :: ZZ) :: ZZ where ...
type family Sub (a :: ZZ) (b :: ZZ) :: ZZ where ...
type family Mul (a :: ZZ) (b :: ZZ) :: ZZ where ...
type family Pow (a :: ZZ) (n :: Nat) :: ZZ where ...
class KnownInt (r :: ZZ) where
- intVal :: proxy r -> Integer
data SZZ (z :: ZZ) where
- SPos :: forall (n :: Nat). KnownNat n => SNat n -> SZZ ('Pos n)
- SNeg :: forall (n :: Nat). KnownNat n => SNat n -> SZZ ('Neg n)
- SZero :: SZZ ('Zero :: Signed Nat)
zero :: SZZ ('Zero :: Signed Nat)
pos :: forall (n :: Nat). KnownNat n => SZZ ('Pos n)
pos1 :: SZZ ('Pos 1)
pos2 :: SZZ ('Pos 2)
pos3 :: SZZ ('Pos 3)
pos4 :: SZZ ('Pos 4)
neg :: forall (n :: Nat). KnownNat n => SZZ ('Neg n)
neg1 :: SZZ ('Neg 1)
neg2 :: SZZ ('Neg 2)
neg3 :: SZZ ('Neg 3)
neg4 :: SZZ ('Neg 4)
fromSZZ :: forall (n :: ZZ). SZZ n -> Integer
withSomeSZZ :: Integer -> (forall (n :: ZZ). SZZ n -> r) -> r
withKnownInt :: forall (n :: ZZ) r. SZZ n -> (KnownInt n => r) -> r

Documentation

data Signed a Source #

Add a sign to any type

Constructors

Pos a
Neg a
Zero

Instances

Instances details

type Compare (a :: Signed k) (b :: Signed k) Source #
Instance details Defined in Data.Type.Int type Compare (a :: Signed k) (b :: Signed k) = CmpSigned a b

type ZZ = Signed Nat Source #

Type integers

ZZ represents the mathematical font for the set of integers

type family CmpSigned (a :: Signed k) (b :: Signed k) :: Ordering where ... Source #

Compare Signed kinds when those kinds are comparable.

Equations

CmpSigned ('Neg a :: Signed k) ('Neg b :: Signed k) = FlipOrdering (Compare a b)
CmpSigned ('Neg a :: Signed k) (b :: Signed k) = 'LT
CmpSigned ('Zero :: Signed k) ('Neg a :: Signed k) = 'GT
CmpSigned ('Zero :: Signed k) ('Zero :: Signed k) = 'EQ
CmpSigned ('Zero :: Signed k) ('Pos a :: Signed k) = 'GT
CmpSigned ('Pos a :: Signed k) ('Pos b :: Signed k) = Compare a b
CmpSigned ('Pos a :: Signed k) (b :: Signed k) = 'GT

type family IsPos (a :: ZZ) :: Bool where ... Source #

Equations

IsPos ('Pos a) = 'True
IsPos b = 'False

type family FlipOrdering (o :: Ordering) :: Ordering where ... Source #

Reverse the order of an Ordering

This should be declared in to Data.Type.Ord in base

Equations

FlipOrdering 'LT = 'GT
FlipOrdering 'EQ = 'EQ
FlipOrdering 'GT = 'LT

type family NormalizeInt (a :: ZZ) :: ZZ where ... Source #

Always use Zero instead of Pos 0 or Neg 0.

Equations

NormalizeInt ('Pos 0) = 'Zero :: Signed Nat
NormalizeInt ('Neg 0) = 'Zero :: Signed Nat
NormalizeInt n = n

type family Abs (a :: ZZ) :: Nat where ... Source #

Absolute value

Equations

Abs ('Pos a) = a
Abs ('Neg a) = a
Abs ('Zero :: Signed Nat) = 0

type family Negate (a :: ZZ) :: ZZ where ... Source #

Unary negation

Equations

Negate ('Pos a) = 'Neg a
Negate ('Neg a) = 'Pos a
Negate ('Zero :: Signed Nat) = 'Zero :: Signed Nat

type family AddCmp (cmp :: Ordering) (a :: ZZ) (b :: ZZ) :: ZZ where ... Source #

Utility family for Add

Equations

AddCmp _1 a ('Zero :: Signed Nat) = a
AddCmp _1 ('Zero :: Signed Nat) b = b
AddCmp _1 ('Pos a) ('Pos b) = 'Pos (a + b)
AddCmp _1 ('Neg a) ('Neg b) = 'Neg (a + b)
AddCmp 'EQ _1 _2 = 'Zero :: Signed Nat
AddCmp 'LT ('Pos a) ('Neg b) = 'Neg (b - a)
AddCmp 'GT ('Pos a) ('Neg b) = 'Pos (a - b)
AddCmp 'LT ('Neg a) ('Pos b) = 'Pos (b - a)
AddCmp 'GT ('Neg a) ('Pos b) = 'Neg (a - b)

type family Add (a :: ZZ) (b :: ZZ) :: ZZ where ... Source #

Addition

Equations

Add a b = AddCmp (Compare (Abs a) (Abs b)) a b

type family Sub (a :: ZZ) (b :: ZZ) :: ZZ where ... Source #

Subtraction

Equations

Sub a b = Add a (Negate b)

type family Mul (a :: ZZ) (b :: ZZ) :: ZZ where ... Source #

Multiplication

Equations

Mul a ('Zero :: Signed Nat) = a
Mul ('Zero :: Signed Nat) b = b
Mul ('Pos a) ('Pos b) = 'Pos (a * b)
Mul ('Pos a) ('Neg b) = 'Neg (a * b)
Mul ('Neg a) ('Pos b) = 'Neg (a * b)
Mul ('Neg a) ('Neg b) = 'Pos (a * b)

type family Pow (a :: ZZ) (n :: Nat) :: ZZ where ... Source #

Exponentiation

Equations

Pow ('Zero :: Signed Nat) 0 = 'Pos 1
Pow ('Zero :: Signed Nat) n = 'Zero :: Signed Nat
Pow ('Pos a) n = 'Pos (a ^ n)
Pow ('Neg a) n = If (Mod n 2 == 0) ('Pos (a ^ n)) ('Neg (a ^ n))

class KnownInt (r :: ZZ) where Source #

Gives the integer associated to a type-level integer.

Methods

intVal :: proxy r -> Integer Source #

Reify a type integer to an integer.

Instances

Instances details

KnownInt ('Zero :: Signed Nat) Source #
Instance details Defined in Data.Type.Int Methods intVal :: proxy ('Zero :: Signed Nat) -> Integer Source #
KnownNat n => KnownInt ('Neg n) Source #
Instance details Defined in Data.Type.Int Methods intVal :: proxy ('Neg n) -> Integer Source #
KnownNat n => KnownInt ('Pos n) Source #
Instance details Defined in Data.Type.Int Methods intVal :: proxy ('Pos n) -> Integer Source #

data SZZ (z :: ZZ) where Source #

Singleton type for type-level integers.

Constructors

SPos :: forall (n :: Nat). KnownNat n => SNat n -> SZZ ('Pos n)
SNeg :: forall (n :: Nat). KnownNat n => SNat n -> SZZ ('Neg n)
SZero :: SZZ ('Zero :: Signed Nat)

zero :: SZZ ('Zero :: Signed Nat) Source #

Singleton for zero.

pos :: forall (n :: Nat). KnownNat n => SZZ ('Pos n) Source #

Singleton for positive integers.

>>> :t pos @3
 pos @3 :: KnownNat 3 => SZZ ('Pos 3)

pos1 :: SZZ ('Pos 1) Source #

Integer singleton for 1.

pos2 :: SZZ ('Pos 2) Source #

Integer singleton for 2.

pos3 :: SZZ ('Pos 3) Source #

Integer singleton for 3.

pos4 :: SZZ ('Pos 4) Source #

Integer singleton for 4.

neg :: forall (n :: Nat). KnownNat n => SZZ ('Neg n) Source #

Singleton for negative integers.

>>> :t neg @3
neg @3 :: KnownNat 3 => SZZ ('Neg 3)

neg1 :: SZZ ('Neg 1) Source #

Integer singleton for -1.

neg2 :: SZZ ('Neg 2) Source #

Integer singleton for -2.

neg3 :: SZZ ('Neg 3) Source #

Integer singleton for -3.

neg4 :: SZZ ('Neg 4) Source #

Integer singleton for -4.

fromSZZ :: forall (n :: ZZ). SZZ n -> Integer Source #

Return the Integer corresponding to n in an SZZ n value.

withSomeSZZ :: Integer -> (forall (n :: ZZ). SZZ n -> r) -> r Source #

Convert an Integer into an SZZ n value, where n is a fresh type-level symbol.

withKnownInt :: forall (n :: ZZ) r. SZZ n -> (KnownInt n => r) -> r Source #

Convert an explicit SZZ n value into an implicit KnownInt n constraint.