Numeric.Type.List

Provides type-level operations on lists.

Basic operations

type family (as :: [k]) ++ (bs :: [k]) :: [k] where ... infixr 5

List concatenation

Equations

'[] ++ bs = bs

as ++ '[] = as

(a :+ as) ++ bs = a :+ (as ++ bs)

type (+:) (ns :: [k]) (n :: k) = Snoc ns n infixl 5

Synonym for a type-level snoc (injective!)

type (:+) (a :: k) (as :: [k]) = a ': as infixr 5

Synonym for a type-level cons (injective, since this is just a synonym for the list constructor)

type Empty = '[]

Synonym for an empty type-level list

type Cons (n :: k) (ns :: [k]) = n :+ ns

Prefix-style synonym for cons

type Snoc (ns :: [k]) (n :: k) = GetSnoc k (DoSnoc k ns n)

Prefix-style synonym for snoc

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

Equations

Head (x :+ xs) = x

Head (KEmpty k) = TypeError (Text "Head: empty type-level list." :$$: FamErrMsg k)

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

Equations

Tail (x :+ xs) = xs

Tail (KEmpty k) = TypeError (Text "Tail: empty type-level list." :$$: FamErrMsg k)

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

Equations

Init '[x] = '[]

Init (x :+ xs) = x :+ Init xs

Init (KEmpty k) = TypeError (Text "Init: empty type-level list." :$$: FamErrMsg k)

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

Equations

Last '[x] = x

Last (x :+ xs) = Last xs

Last (KEmpty k) = TypeError (Text "Last: empty type-level list." :$$: FamErrMsg k)

type Concat (as :: [k]) (bs :: [k]) = as ++ bs

Prefix-style synonym for concatenation

type Reverse (xs :: [k]) = Reversed k (DoReverse k xs)

Reverse a type-level list (injective!)

type family Take (n :: Nat) (xs :: [k]) :: [k] where ...

Equations

Take _ '[] = '[]

Take 0 xs = '[]

Take n (x :+ xs) = x :+ Take (n - 1) xs

type family Drop (n :: Nat) (xs :: [k]) :: [k] where ...

Equations

Drop _ '[] = '[]

Drop 0 xs = xs

Drop n (x :+ xs) = Drop (n - 1) xs

type family Length (xs :: [k]) :: Nat where ...

Equations

Length '[] = 0

Length (_ ': xs) = 1 + Length xs

type family All (f :: k -> Constraint) (xs :: [k]) :: Constraint where ...

Equations

All _ '[] = ()

All f (x ': xs) = (f x, All f xs)

type family Map (f :: a -> b) (xs :: [a]) :: [b] where ...

Equations

Map f '[] = '[]

Map f (x ': xs) = f x ': Map f xs

Working with concatenations

type family Suffix (as :: [k]) (asbs :: [k]) :: [k] where ...

Equations

Suffix '[] bs = bs

Suffix as as = '[]

Suffix (_ :+ as) (_ :+ asbs) = Suffix as asbs

type family Prefix (bs :: [k]) (asbs :: [k]) :: [k] where ...

Equations

Prefix '[] as = as

Prefix bs bs = '[]

Prefix bs asbs = Take (Length asbs - Length bs) asbs

type family IsPrefix (as :: [k]) (asbs :: [k]) :: Bool where ...

Equations

IsPrefix '[] _ = True

IsPrefix (a :+ as) (a :+ asbs) = IsPrefix as asbs

IsPrefix as as = True

IsPrefix _ _ = False

type family IsSuffix (as :: [k]) (asbs :: [k]) :: Bool where ...

Equations

IsSuffix '[] _ = True

IsSuffix bs bs = True

IsSuffix bs (_ :+ sbs) = IsSuffix bs sbs

IsSuffix _ _ = False

Term level functions

class (asbs ~ Concat as bs, as ~ Prefix bs asbs, bs ~ Suffix as asbs, IsSuffix bs asbs ~ True, IsPrefix as asbs ~ True) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) | as bs -> asbs, as asbs -> bs, bs asbs -> as

Represent a triple of lists forming a relation `as ++ bs ~ asbs`

Instances

(asbs ~ Concat as bs, as ~ Prefix bs asbs, bs ~ Suffix as asbs, IsSuffix bs asbs ~ True, IsPrefix as asbs ~ True) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k])

Defined in Numeric.Type.List