Prelude.Type.Families

A prelude for type-level programming with type families

Documentation

module Prelude

type family If p a b :: k

If

Type Classes

Show

type Show a = Shows a `[]`

type family Shows a t :: [Symbol]

Kind

type family Kind a :: *

Get kind of a type

Eq

type family a (==) b :: Bool

type (/=) a b = Not (a == b)

Ord

type family Compare a b :: Ordering

type (<) a b = FromOrdering True False False (Compare a b)

type (<=) a b = FromOrdering True True False (Compare a b)

type (>=) a b = FromOrdering False True True (Compare a b)

type (>) a b = FromOrdering False False True (Compare a b)

type Max a b = FromOrdering b a a (Compare a b)

type Min a b = FromOrdering a a b (Compare a b)

Enum

type family ToEnum i :: k

type family FromEnum a :: Integer

type Succ a = ToEnum (I 1 + FromEnum a)

type Pred a = ToEnum (FromEnum a `Minus` I 1)

type EnumFromTo a b = EnumFromTo_1 (FromEnum a < FromEnum b) a b

type family EnumFromTo_1 lt a b :: [k]

Bounded

type family MinBound :: k

type family MaxBound :: k

Primitive kinds

Unit

Maybe

Bool

type family Not a :: Bool

type family a (||) b :: Bool

type family a (&&) b :: Bool

Ordering

type family FromOrdering lt eq gt o :: k

type family CombineOrdering a b :: Ordering

Either

Tuples

type family Fst p :: a

type family Snd p :: b

Type Literals

Star

data StarKind

The Kind *

Predicates/Constraints

type Compose f g a = f (g a)

type family a ($) b :: k

type Id a = a

type Flip f a b = f a b

Lists

type family ShowsTail a x :: [Symbol]

type family Head l :: k

type family Tail l :: [k]

type family Last a :: k

type family Init a :: [k]

type family Null a :: Bool

type family Length a :: Integer

type family a (!!) i :: k

type family At_1 a b c d :: k

type family Drop i a :: [k]

type family a (++) b :: [k]

type family Concat a :: [k]

type Replicate i a = Replicate_1 (IsZero i) i a

type family Replicate_1 z i a :: [k]

type family And a :: Bool

type family Or a :: Bool

type family Elem a b :: Bool

type family Elem_1 p a b :: Bool

type NotElem a b = Not (Elem a b)

Integer

type family ShowsInteger_2 z i x :: [Symbol]

type family IsZero i :: Bool

type family Digit i :: Symbol

type family IntegerEqual p i j :: Bool

type family IntegerEnd i :: Bool

type IntegerEnd2 i j = IntegerEnd i && IntegerEnd j

type family a (+) b :: k

type AddWithCarry c i j = AddWithCarry_2 (IntegerEnd2 i j) c i j

type family AddWithCarry_2 end a b c :: Integer

type family AddWithCarry_3 h i j :: Integer

type family Add3 a b c :: (Bool, Bool)

Two bit sum of three bits Add3 a b c ~ '(sum, carry)

type family Minus a b :: k

type family Negate a :: k

type family a (*) b :: k

type Signum a = FromOrdering Ones Zeros (One Zeros) (Compare0 a)

type Abs a = FromOrdering (Negate a) a a (Compare0 a)

type Subtract a b = b `Minus` a

type Even i = IntegerHead i

type Odd i = Not (Even i)

type family Gcd_1 zs a b :: Integer

type family Gcd_3 z a b :: Integer

type Gcd a b = Gcd_1 (IsZero a && IsZero b) a b

type Gcd_2 a b = Gcd_3 (IsZero b) a b

type family Compare0 i :: Ordering

Misc functions from the Prelude

type Undefined = Error "undefined"

type family Error a :: k2

type family ERROR a :: k2

type family AsKindOf a b :: k

Bits

type family Xor a b :: k

type family Xor_2 end a b :: k

type family a (.&.) b :: k

type family BitwiseAnd_2 end a b :: k

type family Complement a :: k

Integral

type QuotRem a b = `((Signum a * Signum b) * Fst (QuotRem' (Abs a) (Abs b)), Signum a * Snd (QuotRem' (Abs a) (Abs b)))`

type family QuotRem'_2 p a b :: (Integer, Integer)

type family QuotRem'_3 b qr :: (Integer, Integer)

type family QuotRem'_4 p a b c :: (Integer, Integer)

type QuotRem' a b = QuotRem'_2 (a < b) a b

type Rem a b = Snd (QuotRem a b)

type Quot a b = Fst (QuotRem a b)

module GHC.TypeLits

module Prelude.Type.Integer

module Prelude.Type.Value