Type.RowList.Limits.ExactCount

class ExactCount (count :: Int) (rl :: RowList) | count -> rl

Instances

• ExactCount (Pos Z) Nil
• ExactCount (Pos (Succ Z)) (Cons l1 t1 Nil)
• ExactCount (Pos (Succ (Succ Z))) (Cons l1 t1 (Cons l2 t2 Nil))
• ExactCount (Pos (Succ (Succ (Succ Z)))) (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 Nil)))
• ExactCount (Pos (Succ (Succ (Succ (Succ Z))))) (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 (Cons l4 t4 Nil))))
• ExactCount (Pos (Succ (Succ (Succ (Succ (Succ Z)))))) (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 (Cons l4 t4 (Cons l5 t5 Nil)))))
• ExactCount (Pos (Succ (Succ (Succ (Succ (Succ (Succ Z))))))) (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 (Cons l4 t4 (Cons l5 t5 (Cons l6 t6 Nil))))))
• ExactCount (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z)))))))) (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 (Cons l4 t4 (Cons l5 t5 (Cons l6 t6 (Cons l7 t7 Nil)))))))
• ExactCount (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z))))))))) (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 (Cons l4 t4 (Cons l5 t5 (Cons l6 t6 (Cons l7 t7 (Cons l8 t8 Nil))))))))
• ExactCount (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z)))))))))) (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 (Cons l4 t4 (Cons l5 t5 (Cons l6 t6 (Cons l7 t7 (Cons l8 t8 (Cons l9 t9 Nil)))))))))
• ExactCount (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z))))))))))) (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 (Cons l4 t4 (Cons l5 t5 (Cons l6 t6 (Cons l7 t7 (Cons l8 t8 (Cons l9 t9 (Cons l10 t10 Nil))))))))))

class (ExactCount (Pos Z) rl) <= ExactCountEmpty (rl :: RowList) 

Instances

• ExactCountEmpty Nil

class (ExactCount (Pos Z) rl) <= ExactCountZero (rl :: RowList) 

Instances

• ExactCountZero Nil

class (ExactCount (Pos (Succ Z)) rl) <= ExactCountOne (rl :: RowList) 

Instances

• ExactCountOne (Cons l1 t1 Nil)

class (ExactCount (Pos (Succ (Succ Z))) rl) <= ExactCountTwo (rl :: RowList) 

Instances

• ExactCountTwo (Cons l1 t1 (Cons l2 t2 Nil))

class (ExactCount (Pos (Succ (Succ (Succ Z)))) rl) <= ExactCountThree (rl :: RowList) 

Instances

• ExactCountThree (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 Nil)))

class (ExactCount (Pos (Succ (Succ (Succ (Succ Z))))) rl) <= ExactCountFour (rl :: RowList) 

Instances

• ExactCountFour (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 (Cons l4 t4 Nil))))

class (ExactCount (Pos (Succ (Succ (Succ (Succ (Succ Z)))))) rl) <= ExactCountFive (rl :: RowList) 

Instances

• ExactCountFive (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 (Cons l4 t4 (Cons l5 t5 Nil)))))

class (ExactCount (Pos (Succ (Succ (Succ (Succ (Succ (Succ Z))))))) rl) <= ExactCountSix (rl :: RowList) 

Instances

• ExactCountSix (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 (Cons l4 t4 (Cons l5 t5 (Cons l6 t6 Nil))))))

class (ExactCount (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z)))))))) rl) <= ExactCountSeven (rl :: RowList) 

Instances

• ExactCountSeven (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 (Cons l4 t4 (Cons l5 t5 (Cons l6 t6 (Cons l7 t7 Nil)))))))

class (ExactCount (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z))))))))) rl) <= ExactCountEight (rl :: RowList) 

Instances

• ExactCountEight (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 (Cons l4 t4 (Cons l5 t5 (Cons l6 t6 (Cons l7 t7 (Cons l8 t8 Nil))))))))

class (ExactCount (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z)))))))))) rl) <= ExactCountNine (rl :: RowList) 

Instances

• ExactCountNine (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 (Cons l4 t4 (Cons l5 t5 (Cons l6 t6 (Cons l7 t7 (Cons l8 t8 (Cons l9 t9 Nil)))))))))

class (ExactCount (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Z))))))))))) rl) <= ExactCountTen (rl :: RowList) 

Instances

• ExactCountTen (Cons l1 t1 (Cons l2 t2 (Cons l3 t3 (Cons l4 t4 (Cons l5 t5 (Cons l6 t6 (Cons l7 t7 (Cons l8 t8 (Cons l9 t9 (Cons l10 t10 Nil))))))))))

data Nil :: RowList

The empty RowList.

data Cons :: Symbol -> Type -> RowList -> RowList

Constructs a new RowList from a label, a type, and an existing tail RowList. E.g: Cons "x" Int (Cons "y" Int Nil).

class RowToList (row :: Row Type) (list :: RowList) | row -> list

Compiler solved type class for generating a RowList from a closed row of types. Entries are sorted by label and duplicates are preserved in the order they appeared in the row.

data RowList :: Type

A type level list representation of a row of types.

data Z :: Nat

Represents 0

Instances

• IsNat Z
• SumNat a Z a
• SumNat Z a a
• ProductNat Z a Z

  0 * a = 0

• ProductNat (Succ Z) a a

  1 * a = a

• ExponentiationNat a Z (Succ Z)
• CompareNat Z a LT
• CompareNat a Z GT
• IsZeroNat Z True

data Succ :: Nat -> Nat

Represents Successor of a Nat: (Succ a) ^= 1 + a

Instances

• (IsNat a) => IsNat (Succ a)
• (SumNat a b c) => SumNat (Succ a) b (Succ c)
• ProductNat (Succ Z) a a

  1 * a = a

• (ProductNat a b ab, SumNat ab b result) => ProductNat (Succ a) b result

  (1 + a) * b = b + a * b

• ExponentiationNat a Z (Succ Z)
• (ExponentiationNat a b ab, ProductNat ab a result) => ExponentiationNat a (Succ b) result
• (CompareNat a b ord) => CompareNat (Succ a) (Succ b) ord
• IsZeroNat (Succ a) False

data Pos :: Nat -> Int

Represents a posivite number

Pos (Succ Z) ^= + 1

Instances

• (IsNat n) => IsInt (Pos n)
• (SumInt (Pos a) (Pos b) (Pos c')) => SumInt (Pos (Succ a)) (Pos b) (Pos (Succ c'))
• (SumInt (Pos a) (Neg b) c) => SumInt (Pos (Succ a)) (Neg (Succ b)) c
• (SumInt (Neg a) (Pos b) c) => SumInt (Neg (Succ a)) (Pos (Succ b)) c
• SumInt (Pos Z) (Pos b) (Pos b)
• SumInt (Neg (Succ a)) (Pos Z) (Neg (Succ a))
• SumInt (Pos Z) (Neg (Succ b)) (Neg (Succ b))
• SumInt (Pos a) (Neg Z) (Pos a)
• SumInt (Neg Z) (Pos a) (Pos a)
• Inverse (Pos Z) (Pos Z)
• Inverse (Pos a) (Neg a)
• Inverse (Neg Z) (Pos Z)
• Inverse (Neg a) (Pos a)
• (ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Neg a) (Pos b) (Neg c)
• (ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Neg a) (Neg b) (Pos c)
• ProductInt (Pos Z) a (Pos Z)
• ProductInt (Pos (Succ Z)) a a
• (ProductInt (Pos a) (Pos b) (Pos c)) => ProductInt (Pos a) (Neg b) (Neg c)
• (ProductInt (Pos a) b ab, SumInt ab b result) => ProductInt (Pos (Succ a)) b result
• (IsZeroNat a isZero) => IsZeroInt (Pos a) isZero

type P9 = Pos D9

type P8 = Pos D8

type P7 = Pos D7

type P6 = Pos D6

type P5 = Pos D5

type P4 = Pos D4

type P3 = Pos D3

type P2 = Pos D2

type P10 = Pos D10

type P1 = Pos D1

type P0 = Pos D0

data Int :: Type

Represents a whole Number ℤ

Note: Pos Z and Neg Z both represent 0