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	Haskell2010

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

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 #