Module

Type.Data.List

Package: purescript-typelevel-lists
Repository: PureFunctor/purescript-typelevel-lists

Type-level heterogenous list of kinds for PureScript

#List' Source

data List' :: Type

Represents the type-level list.

#Item' Source

data Item' :: Type

Represents type-level list items.

#Nil' Source

data Nil' :: List'

Represents an empty List'.

Instances

#Cons' Source

data Cons' :: Item' -> List' -> List'

Prepends any Item' to a List', creating a new List'.

Instances

IsMember x (Cons' x xs) True
(IsMember x ys r) => IsMember x (Cons' y ys) r
(Concat xs ys zs) => Concat (Cons' x xs) ys (Cons' x zs)
IsEmpty (Cons' x xs) False
(Init' z zs ws) => Init' y (Cons' z zs) (Cons' y ws)
(Init' x xs ys) => Init (Cons' x xs) ys
Last (Cons' x Nil') x
(Last xs ys) => Last (Cons' x xs) ys
(SumInt n (Pos (Succ Z)) m, Length' xs m r) => Length' (Cons' x xs) n r
(SumInt n (Neg (Succ Z)) m, Take m xs ys) => Take n (Cons' x xs) (Cons' x ys)
(SumInt n (Neg (Succ Z)) m, Drop m xs ys) => Drop n (Cons' x xs) ys

#type (:>) Source

Operator alias for Type.Data.List.Cons' (right-associative / precedence 1)

#TypeItem Source

data TypeItem :: Type -> Item'

Wraps a Type into an Item'.

#SymbolItem Source

data SymbolItem :: Symbol -> Item'

Wraps a Symbol into an Item'.

#IsMember Source

class IsMember (x :: Item') (xs :: List') (r :: Boolean) | x xs -> r

Performs membership testing given an Item' and a List'.

Instances

IsMember x Nil' False
IsMember x (Cons' x xs) True
(IsMember x ys r) => IsMember x (Cons' y ys) r

#Concat Source

class Concat (xs :: List') (ys :: List') (zs :: List') | xs ys -> zs

Concatenates two List's together.

Instances

Concat Nil' ys ys
(Concat xs ys zs) => Concat (Cons' x xs) ys (Cons' x zs)

#IsEmpty Source

class IsEmpty (xs :: List') (r :: Boolean) | xs -> r

Determines whether List' is empty.

Instances

IsEmpty Nil' True
IsEmpty (Cons' x xs) False

#Init Source

class Init (xs :: List') (ys :: List') | xs -> ys

Takes the init items of a List'.

Instances

(Init' x xs ys) => Init (Cons' x xs) ys

#Init' Source

class Init' (xs :: Item') (ys :: List') (zs :: List') | xs ys -> zs

Internal type class that acts as an accumulator.

Instances

Init' xs Nil' Nil'
(Init' z zs ws) => Init' y (Cons' z zs) (Cons' y ws)

#Last Source

class Last (xs :: List') (x :: Item') | xs -> x

Returns the last item of a List'.

Instances

Last (Cons' x Nil') x
(Last xs ys) => Last (Cons' x xs) ys

#Length Source

class Length (xs :: List') (r :: Int) | xs -> r

Computes the length of a List' as a Type.Data.Peano.Int

Instances

(Length' xs (Pos Z) r) => Length xs r

#Length' Source

class Length' (xs :: List') (n :: Int) (r :: Int) | xs n -> r

Internal type that acts as an accumulator

Instances

Length' Nil' n n
(SumInt n (Pos (Succ Z)) m, Length' xs m r) => Length' (Cons' x xs) n r

#Take Source

class Take (n :: Int) (xs :: List') (ys :: List') | n xs -> ys

Takes an n amount of Item's from a List'.

Instances

Take (Pos Z) xs Nil'
Take n Nil' Nil'
(SumInt n (Neg (Succ Z)) m, Take m xs ys) => Take n (Cons' x xs) (Cons' x ys)

#Drop Source

class Drop (n :: Int) (xs :: List') (ys :: List') | n ys -> ys

Drops an n amount of Item's from a List'.

Instances

Drop (Pos Z) xs xs
Drop n Nil' Nil'
(SumInt n (Neg (Succ Z)) m, Drop m xs ys) => Drop n (Cons' x xs) ys

#ListProxy Source

data ListProxy (l :: List')

A value-level proxy for List'

Constructors

ListProxy

#ItemProxy Source

data ItemProxy (i :: Item')

A value-level proxy for Item'

Constructors

ItemProxy

Modules: Type.Data.List