Language.Symantic.Typing.List

List utilities at the type-level.

Type Index

type family Index xs x where ...

Return the position of a type within a list of them. This is useful to work around OverlappingInstances.

Equations

Index (x ': xs) x = Zero

Index (not_x ': xs) x = Succ (Index xs x)

Type family (++)

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

Equations

'[] ++ ys = ys

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

Type family Concat

type family Concat (xs :: [[k]]) :: [k] where ...

Equations

Concat '[] = '[]

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

Type family Concat_Constraints

type family Concat_Constraints (cs :: [Constraint]) :: Constraint where ...

Equations

Concat_Constraints '[] = ()

Concat_Constraints (c ': cs) = (c, Concat_Constraints cs)

Type family DeleteAll

type family DeleteAll (x :: k) (xs :: [k]) :: [k] where ...

Equations

DeleteAll x '[] = '[]

DeleteAll x (x ': xs) = DeleteAll x xs

DeleteAll x (y ': xs) = y ': DeleteAll x xs

Type family Head

type family Head (xs :: [k]) :: k where ...

Equations

Head (x ': _xs) = x

Type family Tail

type family Tail (xs :: [k]) :: [k] where ...

Equations

Tail (_x ': xs) = xs

Type family Nub

type family Nub (xs :: [k]) :: [k] where ...

Equations

Nub '[] = '[]

Nub (x ': xs) = x ': Nub (DeleteAll x xs)

Type Len

data Len xs where

Constructors

LenZ :: Len '[]

LenS :: Len xs -> Len (x ': xs)

Instances

Show (Len k vs)

Methods

showsPrec :: Int -> Len k vs -> ShowS

show :: Len k vs -> String

showList :: [Len k vs] -> ShowS

addLen :: Len a -> Len b -> Len (a ++ b)

shiftLen :: forall t b a. Len a -> Len (a ++ b) -> Len (a ++ (t ': b))

intLen :: Len xs -> Int

Class LenInj

class LenInj vs where

Minimal complete definition

lenInj

Methods

lenInj :: Len vs

Instances

LenInj k ([] k)

Methods

lenInj :: Len [k] vs

LenInj k as => LenInj k ((:) k a as)

Methods

lenInj :: Len ((k ': a) as) vs