Data.Singletons.Prelude.List

The singleton for lists

data family Sing (a :: k)

type SList

Basic functions

type family (a :: [a]) :++ (a :: [a]) :: [a] where ...

(%:++)

type family Head (a :: [a]) :: a where ...

sHead

type family Last (a :: [a]) :: a where ...

sLast

type family Tail (a :: [a]) :: [a] where ...

sTail

type family Init (a :: [a]) :: [a] where ...

sInit

type family Null (a :: [a]) :: Bool where ...

sNull

type family Length (a :: [a]) :: Nat where ...

sLength

List transformations

type family Map (a :: TyFun a b -> Type) (a :: [a]) :: [b] where ...

sMap

type family Reverse (a :: [a]) :: [a] where ...

sReverse

type family Intersperse (a :: a) (a :: [a]) :: [a] where ...

sIntersperse

type family Intercalate (a :: [a]) (a :: [[a]]) :: [a] where ...

sIntercalate

type family Transpose (a :: [[a]]) :: [[a]] where ...

sTranspose

type family Subsequences (a :: [a]) :: [[a]] where ...

sSubsequences

type family Permutations (a :: [a]) :: [[a]] where ...

sPermutations

Reducing lists (folds)

type family Foldl (a :: TyFun b (TyFun a b -> Type) -> Type) (a :: b) (a :: [a]) :: b where ...

sFoldl

type family Foldl' (a :: TyFun b (TyFun a b -> Type) -> Type) (a :: b) (a :: [a]) :: b where ...

sFoldl'

type family Foldl1 (a :: TyFun a (TyFun a a -> Type) -> Type) (a :: [a]) :: a where ...

sFoldl1

type family Foldl1' (a :: TyFun a (TyFun a a -> Type) -> Type) (a :: [a]) :: a where ...

sFoldl1'

type family Foldr (a :: TyFun a (TyFun b b -> Type) -> Type) (a :: b) (a :: [a]) :: b where ...

sFoldr

type family Foldr1 (a :: TyFun a (TyFun a a -> Type) -> Type) (a :: [a]) :: a where ...

sFoldr1

Special folds

type family Concat (a :: [[a]]) :: [a] where ...

sConcat

type family ConcatMap (a :: TyFun a [b] -> Type) (a :: [a]) :: [b] where ...

sConcatMap

type family And (a :: [Bool]) :: Bool where ...

sAnd

type family Or (a :: [Bool]) :: Bool where ...

sOr

type family Any_ (a :: TyFun a Bool -> Type) (a :: [a]) :: Bool where ...

sAny_

type family All (a :: TyFun a Bool -> Type) (a :: [a]) :: Bool where ...

sAll

type family Sum (a :: [a]) :: a where ...

sSum

type family Product (a :: [a]) :: a where ...

sProduct

type family Maximum (a :: [a]) :: a where ...

sMaximum

type family Minimum (a :: [a]) :: a where ...

sMinimum

any_

Building lists

Scans

type family Scanl (a :: TyFun b (TyFun a b -> Type) -> Type) (a :: b) (a :: [a]) :: [b] where ...

sScanl

type family Scanl1 (a :: TyFun a (TyFun a a -> Type) -> Type) (a :: [a]) :: [a] where ...

sScanl1

type family Scanr (a :: TyFun a (TyFun b b -> Type) -> Type) (a :: b) (a :: [a]) :: [b] where ...

sScanr

type family Scanr1 (a :: TyFun a (TyFun a a -> Type) -> Type) (a :: [a]) :: [a] where ...

sScanr1

Accumulating maps

type family MapAccumL (a :: TyFun acc (TyFun x (acc, y) -> Type) -> Type) (a :: acc) (a :: [x]) :: (acc, [y]) where ...

sMapAccumL

type family MapAccumR (a :: TyFun acc (TyFun x (acc, y) -> Type) -> Type) (a :: acc) (a :: [x]) :: (acc, [y]) where ...

sMapAccumR

Cyclical lists

type family Replicate (a :: Nat) (a :: a) :: [a] where ...

sReplicate

Unfolding

type family Unfoldr (a :: TyFun b (Maybe (a, b)) -> Type) (a :: b) :: [a] where ...

sUnfoldr

Sublists

Extracting sublists

type family Take (a :: Nat) (a :: [a]) :: [a] where ...

sTake

type family Drop (a :: Nat) (a :: [a]) :: [a] where ...

sDrop

type family SplitAt (a :: Nat) (a :: [a]) :: ([a], [a]) where ...

sSplitAt

type family TakeWhile (a :: TyFun a Bool -> Type) (a :: [a]) :: [a] where ...

sTakeWhile

type family DropWhile (a :: TyFun a Bool -> Type) (a :: [a]) :: [a] where ...

sDropWhile

type family DropWhileEnd (a :: TyFun a Bool -> Type) (a :: [a]) :: [a] where ...

sDropWhileEnd

type family Span (a :: TyFun a Bool -> Type) (a :: [a]) :: ([a], [a]) where ...

sSpan

type family Break (a :: TyFun a Bool -> Type) (a :: [a]) :: ([a], [a]) where ...

sBreak

type family Group (a :: [a]) :: [[a]] where ...

sGroup

type family Inits (a :: [a]) :: [[a]] where ...

sInits

type family Tails (a :: [a]) :: [[a]] where ...

sTails

Predicates

type family IsPrefixOf (a :: [a]) (a :: [a]) :: Bool where ...

sIsPrefixOf

type family IsSuffixOf (a :: [a]) (a :: [a]) :: Bool where ...

sIsSuffixOf

type family IsInfixOf (a :: [a]) (a :: [a]) :: Bool where ...

sIsInfixOf

Searching lists

Searching by equality

type family Elem (a :: a) (a :: [a]) :: Bool where ...

sElem

type family NotElem (a :: a) (a :: [a]) :: Bool where ...

sNotElem

type family Lookup (a :: a) (a :: [(a, b)]) :: Maybe b where ...

sLookup

Searching with a predicate

type family Find (a :: TyFun a Bool -> Type) (a :: [a]) :: Maybe a where ...

sFind

type family Filter (a :: TyFun a Bool -> Type) (a :: [a]) :: [a] where ...

sFilter

type family Partition (a :: TyFun a Bool -> Type) (a :: [a]) :: ([a], [a]) where ...

sPartition

Indexing lists

type family (a :: [a]) :!! (a :: Nat) :: a where ...

(%:!!)

type family ElemIndex (a :: a) (a :: [a]) :: Maybe Nat where ...

sElemIndex

type family ElemIndices (a :: a) (a :: [a]) :: [Nat] where ...

sElemIndices

type family FindIndex (a :: TyFun a Bool -> Type) (a :: [a]) :: Maybe Nat where ...

sFindIndex

type family FindIndices (a :: TyFun a Bool -> Type) (a :: [a]) :: [Nat] where ...

sFindIndices

Zipping and unzipping lists

type family Zip (a :: [a]) (a :: [b]) :: [(a, b)] where ...

sZip

type family Zip3 (a :: [a]) (a :: [b]) (a :: [c]) :: [(a, b, c)] where ...

sZip3

type family ZipWith (a :: TyFun a (TyFun b c -> Type) -> Type) (a :: [a]) (a :: [b]) :: [c] where ...

sZipWith

type family ZipWith3 (a :: TyFun a (TyFun b (TyFun c d -> Type) -> Type) -> Type) (a :: [a]) (a :: [b]) (a :: [c]) :: [d] where ...

sZipWith3

type family Unzip (a :: [(a, b)]) :: ([a], [b]) where ...

sUnzip

type family Unzip3 (a :: [(a, b, c)]) :: ([a], [b], [c]) where ...

sUnzip3

type family Unzip4 (a :: [(a, b, c, d)]) :: ([a], [b], [c], [d]) where ...

sUnzip4

type family Unzip5 (a :: [(a, b, c, d, e)]) :: ([a], [b], [c], [d], [e]) where ...

sUnzip5

type family Unzip6 (a :: [(a, b, c, d, e, f)]) :: ([a], [b], [c], [d], [e], [f]) where ...

sUnzip6

type family Unzip7 (a :: [(a, b, c, d, e, f, g)]) :: ([a], [b], [c], [d], [e], [f], [g]) where ...

sUnzip7

Special lists

"Set" operations

type family Nub (a :: [a]) :: [a] where ...

sNub

type family Delete (a :: a) (a :: [a]) :: [a] where ...

sDelete

type family (a :: [a]) :\\ (a :: [a]) :: [a] where ...

(%:\\)

type family Union (a :: [a]) (a :: [a]) :: [a] where ...

sUnion

type family Intersect (a :: [a]) (a :: [a]) :: [a] where ...

sIntersect

Ordered lists

type family Insert (a :: a) (a :: [a]) :: [a] where ...

sInsert

type family Sort (a :: [a]) :: [a] where ...

sSort

Generalized functions

The "By" operations

User-supplied equality (replacing an Eq context)

type family NubBy (a :: TyFun a (TyFun a Bool -> Type) -> Type) (a :: [a]) :: [a] where ...

sNubBy

type family DeleteBy (a :: TyFun a (TyFun a Bool -> Type) -> Type) (a :: a) (a :: [a]) :: [a] where ...

sDeleteBy

type family DeleteFirstsBy (a :: TyFun a (TyFun a Bool -> Type) -> Type) (a :: [a]) (a :: [a]) :: [a] where ...

sDeleteFirstsBy

type family UnionBy (a :: TyFun a (TyFun a Bool -> Type) -> Type) (a :: [a]) (a :: [a]) :: [a] where ...

sUnionBy

type family IntersectBy (a :: TyFun a (TyFun a Bool -> Type) -> Type) (a :: [a]) (a :: [a]) :: [a] where ...

sIntersectBy

type family GroupBy (a :: TyFun a (TyFun a Bool -> Type) -> Type) (a :: [a]) :: [[a]] where ...

sGroupBy

User-supplied comparison (replacing an Ord context)

type family SortBy (a :: TyFun a (TyFun a Ordering -> Type) -> Type) (a :: [a]) :: [a] where ...

sSortBy

type family InsertBy (a :: TyFun a (TyFun a Ordering -> Type) -> Type) (a :: a) (a :: [a]) :: [a] where ...

sInsertBy

type family MaximumBy (a :: TyFun a (TyFun a Ordering -> Type) -> Type) (a :: [a]) :: a where ...

sMaximumBy

type family MinimumBy (a :: TyFun a (TyFun a Ordering -> Type) -> Type) (a :: [a]) :: a where ...

sMinimumBy

The "generic" operations

type family GenericLength (a :: [a]) :: i where ...

sGenericLength

Defunctionalization symbols

type NilSym0

data (:$) l

data l :$$ l

type t :$$$ t

type t :++$$$ t

data l :++$$ l

data (:++$) l

data HeadSym0 l

type HeadSym1 t

data LastSym0 l

type LastSym1 t

data TailSym0 l

type TailSym1 t

data InitSym0 l

type InitSym1 t

data NullSym0 l

type NullSym1 t

data LengthSym0 l

type LengthSym1 t

data MapSym0 l

data MapSym1 l l

type MapSym2 t t

data ReverseSym0 l

type ReverseSym1 t

data IntersperseSym0 l

data IntersperseSym1 l l

type IntersperseSym2 t t

data IntercalateSym0 l

data IntercalateSym1 l l

type IntercalateSym2 t t

data TransposeSym0 l

type TransposeSym1 t

data SubsequencesSym0 l

type SubsequencesSym1 t

data PermutationsSym0 l

type PermutationsSym1 t

data FoldlSym0 l

data FoldlSym1 l l

data FoldlSym2 l l l

type FoldlSym3 t t t

data Foldl'Sym0 l

data Foldl'Sym1 l l

data Foldl'Sym2 l l l

type Foldl'Sym3 t t t

data Foldl1Sym0 l

data Foldl1Sym1 l l

type Foldl1Sym2 t t

data Foldl1'Sym0 l

data Foldl1'Sym1 l l

type Foldl1'Sym2 t t

data FoldrSym0 l

data FoldrSym1 l l

data FoldrSym2 l l l

type FoldrSym3 t t t

data Foldr1Sym0 l

data Foldr1Sym1 l l

type Foldr1Sym2 t t

data ConcatSym0 l

type ConcatSym1 t

data ConcatMapSym0 l

data ConcatMapSym1 l l

type ConcatMapSym2 t t

data AndSym0 l

type AndSym1 t

data OrSym0 l

type OrSym1 t

data Any_Sym0 l

data Any_Sym1 l l

type Any_Sym2 t t

data AllSym0 l

data AllSym1 l l

type AllSym2 t t

data SumSym0 l

type SumSym1 t

data ProductSym0 l

type ProductSym1 t

data MaximumSym0 l

type MaximumSym1 t

data MinimumSym0 l

type MinimumSym1 t

data ScanlSym0 l

data ScanlSym1 l l

data ScanlSym2 l l l

type ScanlSym3 t t t

data Scanl1Sym0 l

data Scanl1Sym1 l l

type Scanl1Sym2 t t

data ScanrSym0 l

data ScanrSym1 l l

data ScanrSym2 l l l

type ScanrSym3 t t t

data Scanr1Sym0 l

data Scanr1Sym1 l l

type Scanr1Sym2 t t

data MapAccumLSym0 l

data MapAccumLSym1 l l

data MapAccumLSym2 l l l

type MapAccumLSym3 t t t

data MapAccumRSym0 l

data MapAccumRSym1 l l

data MapAccumRSym2 l l l

type MapAccumRSym3 t t t

data ReplicateSym0 l

data ReplicateSym1 l l

type ReplicateSym2 t t

data UnfoldrSym0 l

data UnfoldrSym1 l l

type UnfoldrSym2 t t

data TakeSym0 l

data TakeSym1 l l

type TakeSym2 t t

data DropSym0 l

data DropSym1 l l

type DropSym2 t t

data SplitAtSym0 l

data SplitAtSym1 l l

type SplitAtSym2 t t

data TakeWhileSym0 l

data TakeWhileSym1 l l

type TakeWhileSym2 t t

data DropWhileSym0 l

data DropWhileSym1 l l

type DropWhileSym2 t t

data DropWhileEndSym0 l

data DropWhileEndSym1 l l

type DropWhileEndSym2 t t

data SpanSym0 l

data SpanSym1 l l

type SpanSym2 t t

data BreakSym0 l

data BreakSym1 l l

type BreakSym2 t t

data GroupSym0 l

type GroupSym1 t

data InitsSym0 l

type InitsSym1 t

data TailsSym0 l

type TailsSym1 t

data IsPrefixOfSym0 l

data IsPrefixOfSym1 l l

type IsPrefixOfSym2 t t

data IsSuffixOfSym0 l

data IsSuffixOfSym1 l l

type IsSuffixOfSym2 t t

data IsInfixOfSym0 l

data IsInfixOfSym1 l l

type IsInfixOfSym2 t t

data ElemSym0 l

data ElemSym1 l l

type ElemSym2 t t

data NotElemSym0 l

data NotElemSym1 l l

type NotElemSym2 t t

data LookupSym0 l

data LookupSym1 l l

type LookupSym2 t t

data FindSym0 l

data FindSym1 l l

type FindSym2 t t

data FilterSym0 l

data FilterSym1 l l

type FilterSym2 t t

data PartitionSym0 l

data PartitionSym1 l l

type PartitionSym2 t t

data (:!!$) l

data l :!!$$ l

type t :!!$$$ t

data ElemIndexSym0 l

data ElemIndexSym1 l l

type ElemIndexSym2 t t

data ElemIndicesSym0 l

data ElemIndicesSym1 l l

type ElemIndicesSym2 t t

data FindIndexSym0 l

data FindIndexSym1 l l

type FindIndexSym2 t t

data FindIndicesSym0 l

data FindIndicesSym1 l l

type FindIndicesSym2 t t

data ZipSym0 l

data ZipSym1 l l

type ZipSym2 t t

data Zip3Sym0 l

data Zip3Sym1 l l

data Zip3Sym2 l l l

type Zip3Sym3 t t t

data ZipWithSym0 l

data ZipWithSym1 l l

data ZipWithSym2 l l l

type ZipWithSym3 t t t

data ZipWith3Sym0 l

data ZipWith3Sym1 l l

data ZipWith3Sym2 l l l

data ZipWith3Sym3 l l l l

type ZipWith3Sym4 t t t t

data UnzipSym0 l

type UnzipSym1 t

data Unzip3Sym0 l

type Unzip3Sym1 t

data Unzip4Sym0 l

type Unzip4Sym1 t

data Unzip5Sym0 l

type Unzip5Sym1 t

data Unzip6Sym0 l

type Unzip6Sym1 t

data Unzip7Sym0 l

type Unzip7Sym1 t

data NubSym0 l

type NubSym1 t

data DeleteSym0 l

data DeleteSym1 l l

type DeleteSym2 t t

data (:\\$) l

data l :\\$$ l

type t :\\$$$ t

data UnionSym0 l

data UnionSym1 l l

type UnionSym2 t t

data IntersectSym0 l

data IntersectSym1 l l

type IntersectSym2 t t

data InsertSym0 l

data InsertSym1 l l

type InsertSym2 t t

data SortSym0 l

type SortSym1 t

data NubBySym0 l

data NubBySym1 l l

type NubBySym2 t t

data DeleteBySym0 l

data DeleteBySym1 l l

data DeleteBySym2 l l l

type DeleteBySym3 t t t

data DeleteFirstsBySym0 l

data DeleteFirstsBySym1 l l

data DeleteFirstsBySym2 l l l

type DeleteFirstsBySym3 t t t

data UnionBySym0 l

data UnionBySym1 l l

data UnionBySym2 l l l

type UnionBySym3 t t t

data IntersectBySym0 l

data IntersectBySym1 l l

data IntersectBySym2 l l l

type IntersectBySym3 t t t

data GroupBySym0 l

data GroupBySym1 l l

type GroupBySym2 t t

data SortBySym0 l

data SortBySym1 l l

type SortBySym2 t t

data InsertBySym0 l

data InsertBySym1 l l

data InsertBySym2 l l l

type InsertBySym3 t t t

data MaximumBySym0 l

data MaximumBySym1 l l

type MaximumBySym2 t t

data MinimumBySym0 l

data MinimumBySym1 l l

type MinimumBySym2 t t

data GenericLengthSym0 l

type GenericLengthSym1 t