Primus.TypeLevel

Documentation

pnat :: forall n. KnownNat n => Int

extract an int from a Nat

type family FailUnless b err where ...

fail with error message if "b" is 'False

Equations

FailUnless 'False err = TypeError ('Text "FailUnless: " :<>: err)

FailUnless 'True _ = ()

type family Fst tp where ...

"fst" at the typelevel

Equations

Fst '(a, _) = a

type family Snd tp where ...

"snd" at the typelevel

Equations

Snd '(_, b) = b

type family Fsts rs where ...

"map fst" at the typelevel

Equations

Fsts '[] = '[]

Fsts ('(a, _) ': rs) = a ': Fsts rs

type family Snds rs where ...

"map snd" at the typelevel

Equations

Snds '[] = '[]

Snds ('(_, b) ': rs) = b ': Snds rs

type family LengthT rs where ...

length at the typelevel

Equations

LengthT '[] = 0

LengthT '[_] = 1

LengthT '[_, _] = 2

LengthT '[_, _, _] = 3

LengthT '[_, _, _, _] = 4

LengthT (_ ': (_ ': (_ ': (_ ': (_ ': rs))))) = 5 + LengthT rs

type family NotEqTC a b where ...

ensure that two types are not equal

Equations

NotEqTC a a = TypeError ('Text "NotEqTC: found equal")

NotEqTC _ _ = ()

type family Cons1T a ys = result | result -> a ys where ...

cons a type to a nonempty list at the type level

Equations

Cons1T a (b :| bs) = a :| (b ': bs)

type family SnocT as b where ...

snoc a type list to a type

Equations

SnocT '[] b = '[b]

SnocT (a ': as) b = a ': SnocT as b

type family InitT xs where ...

get the init of a list

Equations

InitT '[] = TypeError ('Text "InitT: undefined for empty indices")

InitT '[_] = '[]

InitT (n ': (m ': ns)) = n ': InitT (m ': ns)

type family LastT ns where ...

peel off the bottom-most index in the matrix

Equations

LastT '[a] = a

LastT (_ ': (a1 ': as)) = LastT (a1 ': as)

type family ApplyConstraints1 xs x where ...

create a constraint from a type and list of constraints taking a type

Equations

ApplyConstraints1 '[] _ = ()

ApplyConstraints1 (c ': cs) x = (c x, ApplyConstraints1 cs x)

type family ApplyConstraint c xs where ...

create a constraint from a list of types and a constraint that take a type

Equations

ApplyConstraint _ '[] = ()

ApplyConstraint c (x ': xs) = (c x, ApplyConstraint c xs)

type family ApplyConstraints cs xs where ...

create a constraint from a list of types and list of constraints that take a type

Equations

ApplyConstraints '[] _ = ()

ApplyConstraints (c ': cs) xs = (ApplyConstraint c xs, ApplyConstraints cs xs)

type family UnsnocT ns where ...

unsnoc a type level nonempty list

Equations

UnsnocT '[] = TypeError ('Text "UnsnocT: undefined for empty indices")

UnsnocT '[a] = '('[], a)

UnsnocT (a ': (a1 ': as)) = FirstConsT a (UnsnocT (a1 ': as))

type family FirstConsT a b = result | result -> a b where ...

cons a type to the first element in a tuple

Equations

FirstConsT a '(as, c) = '(a ': as, c)

type family ToITupleT x = result | result -> x where ...

convert a flat tuple type to an inductive tuple

Equations

ToITupleT (One a1) = (a1, ())

ToITupleT (a1, a2) = (a1, (a2, ()))

ToITupleT (a1, a2, a3) = (a1, (a2, (a3, ())))

ToITupleT (a1, a2, a3, a4) = (a1, (a2, (a3, (a4, ()))))

ToITupleT (a1, a2, a3, a4, a5) = (a1, (a2, (a3, (a4, (a5, ())))))

ToITupleT (a1, a2, a3, a4, a5, a6) = (a1, (a2, (a3, (a4, (a5, (a6, ()))))))

ToITupleT (a1, a2, a3, a4, a5, a6, a7) = (a1, (a2, (a3, (a4, (a5, (a6, (a7, ())))))))

ToITupleT (a1, a2, a3, a4, a5, a6, a7, a8) = (a1, (a2, (a3, (a4, (a5, (a6, (a7, (a8, ()))))))))

ToITupleT (a1, a2, a3, a4, a5, a6, a7, a8, a9) = (a1, (a2, (a3, (a4, (a5, (a6, (a7, (a8, (a9, ())))))))))

ToITupleT (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) = (a1, (a2, (a3, (a4, (a5, (a6, (a7, (a8, (a9, (a10, ()))))))))))

type family FromITupleT x = result | result -> x where ...

convert an inductive tuple to a flat tuple type

Equations

FromITupleT (a1, ()) = One a1

FromITupleT (a1, (a2, ())) = (a1, a2)

FromITupleT (a1, (a2, (a3, ()))) = (a1, a2, a3)

FromITupleT (a1, (a2, (a3, (a4, ())))) = (a1, a2, a3, a4)

FromITupleT (a1, (a2, (a3, (a4, (a5, ()))))) = (a1, a2, a3, a4, a5)

FromITupleT (a1, (a2, (a3, (a4, (a5, (a6, ())))))) = (a1, a2, a3, a4, a5, a6)

FromITupleT (a1, (a2, (a3, (a4, (a5, (a6, (a7, ()))))))) = (a1, a2, a3, a4, a5, a6, a7)

FromITupleT (a1, (a2, (a3, (a4, (a5, (a6, (a7, (a8, ())))))))) = (a1, a2, a3, a4, a5, a6, a7, a8)

FromITupleT (a1, (a2, (a3, (a4, (a5, (a6, (a7, (a8, (a9, ()))))))))) = (a1, a2, a3, a4, a5, a6, a7, a8, a9)

FromITupleT (a1, (a2, (a3, (a4, (a5, (a6, (a7, (a8, (a9, (a10, ())))))))))) = (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)

class ITupleC x where

conversions to and from an inductive tuple and a flat tuple

Methods

toITupleC :: x -> ToITupleT x

fromITupleC :: ToITupleT x -> x

Instances

ITupleC (One a1)

Defined in Primus.TypeLevel

Methods

toITupleC :: One a1 -> ToITupleT (One a1)

fromITupleC :: ToITupleT (One a1) -> One a1

ITupleC (a1, a2)

Defined in Primus.TypeLevel

Methods

toITupleC :: (a1, a2) -> ToITupleT (a1, a2)

fromITupleC :: ToITupleT (a1, a2) -> (a1, a2)

ITupleC (a1, a2, a3)

Defined in Primus.TypeLevel

Methods

toITupleC :: (a1, a2, a3) -> ToITupleT (a1, a2, a3)

fromITupleC :: ToITupleT (a1, a2, a3) -> (a1, a2, a3)

ITupleC (a1, a2, a3, a4)

Defined in Primus.TypeLevel

Methods

toITupleC :: (a1, a2, a3, a4) -> ToITupleT (a1, a2, a3, a4)

fromITupleC :: ToITupleT (a1, a2, a3, a4) -> (a1, a2, a3, a4)

ITupleC (a1, a2, a3, a4, a5)

Defined in Primus.TypeLevel

Methods

toITupleC :: (a1, a2, a3, a4, a5) -> ToITupleT (a1, a2, a3, a4, a5)

fromITupleC :: ToITupleT (a1, a2, a3, a4, a5) -> (a1, a2, a3, a4, a5)

ITupleC (a1, a2, a3, a4, a5, a6)

Defined in Primus.TypeLevel

Methods

toITupleC :: (a1, a2, a3, a4, a5, a6) -> ToITupleT (a1, a2, a3, a4, a5, a6)

fromITupleC :: ToITupleT (a1, a2, a3, a4, a5, a6) -> (a1, a2, a3, a4, a5, a6)

ITupleC (a1, a2, a3, a4, a5, a6, a7)

Defined in Primus.TypeLevel

Methods

toITupleC :: (a1, a2, a3, a4, a5, a6, a7) -> ToITupleT (a1, a2, a3, a4, a5, a6, a7)

fromITupleC :: ToITupleT (a1, a2, a3, a4, a5, a6, a7) -> (a1, a2, a3, a4, a5, a6, a7)

ITupleC (a1, a2, a3, a4, a5, a6, a7, a8)

Defined in Primus.TypeLevel

Methods

toITupleC :: (a1, a2, a3, a4, a5, a6, a7, a8) -> ToITupleT (a1, a2, a3, a4, a5, a6, a7, a8)

fromITupleC :: ToITupleT (a1, a2, a3, a4, a5, a6, a7, a8) -> (a1, a2, a3, a4, a5, a6, a7, a8)

ITupleC (a1, a2, a3, a4, a5, a6, a7, a8, a9)

Defined in Primus.TypeLevel

Methods

toITupleC :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> ToITupleT (a1, a2, a3, a4, a5, a6, a7, a8, a9)

fromITupleC :: ToITupleT (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9)

ITupleC (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)

Defined in Primus.TypeLevel

Methods

toITupleC :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> ToITupleT (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)

fromITupleC :: ToITupleT (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10)

type family xs ++ ys where ... infixr 5

append two type level lists

Equations

'[] ++ ys = ys

(x ': xs) ++ ys = x ': (xs ++ ys)

type family x :=> y where ...

type level boolean implication

Equations

'False :=> _ = 'True

'True :=> x = x

_ :=> 'False = 'True

_ :=> 'True = 'True

x :=> x = 'True