A Prefix as bs witnesses that as is a prefix of bs.

Some examples:

PreZ                    :: Prefix '[]      '[1,2,3]
PreS PreZ               :: Prefix '[1]     '[1,2,3]
PreS (PreS PreZ)        :: Prefix '[1,2]   '[1,2,3]
PreS (PreS (PreS PreZ)) :: Prefix '[1,2,3] '[1,2,3]

Rule of thumb for construction: the number of PreS is the number of items in the prefix.

This is essentially the first half of an Append, but is conceptually easier to work with.

A type-level predicate that a given list has as as a prefix.

Since: 0.1.2.0

Automatically generate a Prefix if as and bs are known statically.

Since: 0.1.2.0

Take items from a Rec corresponding to a given Prefix.

A lens into the prefix of a Rec.

Shave off the final inhabitants of an Index, keeping only indices a part of a given prefix. If the index is out of range, Nothing will be returned.

This is essentially splitIndex, but taking only Left results.

An index pointing to a given item in a prefix is also an index pointing to the same item in the full list. This "weakens" the bounds of an index, widening the list at the end but preserving the original index. This is the inverse of takeIndex.

Get the Shape associated with a Prefix.

Since: 0.1.3.0

A Suffix as bs witnesses that as is a suffix of bs.

Some examples:

SufZ                    :: Suffix '[1,2,3] '[1,2,3]
SufS SufZ               :: Suffix   '[2,3] '[1,2,3]
SufS (SufS SufZ)        :: Suffix     '[3] '[1,2,3]
SufS (SufS (SufS SufZ)) :: Suffix      '[] '[1,2,3]

Rule of thumb for construction: the number of SufS is the number of items to "drop" before getting the suffix.

This is essentially the second half of an Append, but is conceptually easier to work with.

A type-level predicate that a given list has as as a suffix.

Since: 0.1.2.0

Automatically generate a Suffix if as and bs are known statically.

Since: 0.1.2.0

Drop items from a Rec corresponding to a given Suffix.

A lens into the suffix of a Rec.

Shave off the initial inhabitants of an Index, keeping only indices a part of a given suffix If the index is out of range, Nothing will be returned.

This is essentially splitIndex, but taking only Right results.

An index pointing to a given item in a suffix can be transformed into an index pointing to the same item in the full list. This is the inverse of dropIndex.

An Append as bs cs witnesses that cs is the result of appending as and bs.

Some examples:

AppZ                     :: Append '[]  '[1,2]   '[1,2]
AppZ                     :: Append '[]  '[1,2,3] '[1,2,3]
AppS AppZ                :: Append '[0] '[1,2]   '[0,1,2]

Rule of thumb for construction: the number of AppS is the number of items in the first list.

This basically combines Prefix and Suffix.

A type-level predicate that a given list is the result of appending of as and bs.

Since: 0.1.2.0

Automatically generate an Append if as, bs and cs are known statically.

Since: 0.1.2.0

Given as and bs, create an Append as bs cs with, with cs existentially quantified

Convert a Prefix to an Append, with an existential bs.

Convert a Suffix to an Append, with an existential as.

Convert an Append to a Prefix, forgetting the suffix.

Convert an Append to a Suffix, forgetting the prefix

Split an Append into a Prefix and Suffix. Basically appendToPrefix and appendToSuffix at the same time.

Get the Shape associated with an Append's prefix.

Since: 0.1.3.0

Split a Rec into a prefix and suffix. Basically takeRec and dropRec combined.

Append two Recs together according to an Append.

Witness an isomorphism between Rec and two parts that compose it.

Read this type signature as:

splitRecIso
    :: Append as  bs  cs
    -> Iso' (Rec f cs) (Rec f as, Rec f bs)

This can be used with the combinators from the lens library.

The Append tells the point to split the Rec at.

Split an Index by an Append. If the Index was in the first part of the list, it'll return Left. If it was in the second part, it'll return Right.

This is essentially takeIndex and dropIndex at the same time.

A useful pattern synonym for using Append with ++ from Data.Singletons.Prelude.List.

As a pattern, this brings (as ++ bs) ~ cs into the context whenever you use it to match on an Append as bs cs.

As an expression, this constructs an Append as bs cs as long as you have (as ++ bs) ~ cs in the context.

Since: 0.1.2.0

Witness that Append as bs cs implies (as ++ bs) ~ cs, using ++ from Data.Singletons.Prelude.List.

Since: 0.1.2.0

appendWit stated as a Predicate implication.

Since: 0.1.2.0

The inverse of appendWit: if we know (as ++ bs) ~ cs (using ++ from Data.Singletons.Prelude.List), we can create an Append as bs cs given structure witnesses Sing.

Since: 0.1.2.0

A useful pattern synonym for using Append with ++ from Data.Vinyl.TypeLevel.

As a pattern, this brings (as ++ bs) ~ cs into the context whenever you use it to match on an Append as bs cs.

As an expression, this constructs an Append as bs cs as long as you have (as ++ bs) ~ cs in the context.

Since: 0.1.2.0

Witness that Append as bs cs implies (as ++ bs) ~ cs, using ++ from Data.Vinyl.TypeLevel.

Since: 0.1.2.0

appendWitV stated as a Predicate implication.

Since: 0.1.2.0

The inverse of appendWitV: if we know (as ++ bs) ~ cs (using ++ from Data.Vinyl.TypeLevel), we can create an Append as bs cs given structure witnesses Sing.

Since: 0.1.2.0

Combine the powers of AppendWit and AppendWitV by matching on an Append to witness (as ++ bs) ~ cs for both ++ from Data.Singletons.Prelude.List and Data.Vinyl.TypeLevel. This also witnesses that (as ++ bs) ~ (as ++ bs) (for the two different ++s) by transitive property.

Since: 0.1.2.0

Given a witness Append as bs cs, prove that singleton's ++ from Data.Singletons.Prelude.List is the same as vinyl's ++ Data.Vinyl.TypeLevel.

A parameterized predicate that you can use with select: With an AppendedTo as, you can give bs and get cs in return, where cs is the appending of as and bs.

Run it with:

selectTC :: SingI as => Sing bs -> Σ [k] (IsAppend as bs)

select for AppendedTo is pretty much just withAppend.

Since: 0.1.2.0

A Interleave as bs cs witnesses that cs is as interleaved with bs. It is constructed by selectively zipping items from as and bs together, like mergesort or riffle shuffle.

You construct an Interleave from as and bs by picking "which item" from as and bs to add to cs.

Some examples:

IntL (IntL (IntR (IntR IntZ))) :: Interleave '[1,2] '[3,4] '[1,2,3,4]
IntR (IntR (IntL (IntL IntZ))) :: Interleave '[1,2] '[3,4] '[3,4,1,2]
IntL (IntR (IntL (IntR IntZ))) :: Interleave '[1,2] '[3,4] '[1,3,2,4]
IntR (IntL (IntR (IntL IntZ))) :: Interleave '[1,2] '[3,4] '[3,1,4,2]

Since: 0.1.1.0

A type-level predicate that a given list is the "interleave" of as and bs.

Since: 0.1.2.0

Automatically generate an Interleave if as, bs, and cs are known statically.

Prefers the left side if there is an ambiguity:

IntL (IntR (IntR IntZ) :: Interleave '[1] '[1,2] '[1,1,2]
IntR (IntL (IntR IntZ) :: Interleave '[1] '[1,2] '[1,1,2]

autoInterleave '[1] '[1,2] '[1,1,2] == IntL (IntR (IntR IntZ)

Since: 0.1.2.0

Given two Recs, interleave the two to create a combined Rec.

Since: 0.1.1.0

Given a Rec, disinterleave it into two Recs corresponding to an Interleave.

Since: 0.1.1.0

Witness an isomorphism between Rec and two parts that interleave it.

Read this type signature as:

interleaveRecIso
    :: Interleave as  bs  cs
    -> Iso' (Rec f cs) (Rec f as, Rec f bs)

This can be used with the combinators from the lens library.

The Interleave tells how to unweave the Rec.

Since: 0.1.1.0

Interleave an Index on as into a full index on cs, which is as interleaved with bs.

Since: 0.1.1.0

Interleave an Index on bs into a full index on cs, which is as interleaved with bs.

Since: 0.1.1.0

Given an index on cs, disinterleave it into either an index on as or on bs.

Since: 0.1.1.0

Turn an Interleave into a Rec of indices from either sublist.

Warning: O(n^2)

Since: 0.1.2.0

Swap the two halves of an Interleave.

Since: 0.1.3.0

Get the Shapes associated with an Interleave.

Since: 0.1.3.0

A Subset as bs witnesses that as is some subset of bs, with items in the same order. It is constructed by specifying what item to include or exclude in bs from as. It is essentially Interleave, but without one of the two initial parameters.

You construct an Subset from cs by picking "which item" from bs to add to as.

Some examples:

SubsetNo  (SubsetNo  (SubsetNo  SubsetNil)) :: Subset '[]      '[1,2,3]
SubsetYes (SubsetNo  (SubsetNo  SubsetNil)) :: Subset '[1]     '[1,2,3]
SubsetNo  (SubsetNo  (SubsetYes SubsetNil)) :: Subset '[3]     '[1,2,3]
SubsetYes (SubsetNo  (SubsetYes SubsetNil)) :: Subset '[1,3]   '[1,2,3]
SubsetYes (SubsetYes (SubsetYes SubsetNil)) :: Subset '[1,2,3] '[1,2,3]

Since: 0.1.3.0

A type-level predicate that a given list is a "superset" of as, in correct order

Since: 0.1.2.0

Automatically generate an Subset if as and bs are known statically.

as is a subset of cs; this function recovers bs, the subset of cs that is not as.

Drop the left side of an Interleave, leaving only the right side.

Drop the right side of an Interleave, leaving only the left side.

Convert a Subset into an left Interleave, recovering the dropped items.

Convert a Subset into an right Interleave, recovering the dropped items.

A lens into a subset of a record, indicated by a Subset.

Take a subset out of a Rec. An alias for view (subsetRec s).

Get the Shapes associated with a Subset.

Get all of the indices of all the items in a Subset.

Because as is a subset of bs, an index into as should also be an index into bs. This performs that transformation.

This is like a version of injectIndexL or injectIndexR, for Subset.

Because as is a subset of bs, we can sometimes transform an index into bs into an index into as. This performs that transformation. If it succeeds, it means that the index in bs also exists in as; otherwise, it means that the index in bs was excluded from as.

Note that if the index into a was excluded from as, it doesn't necessarily mean that there is no a in bs --- bs could contain a duplicate that was included into as. This converts into an index to the exact same item (positionlly) in the list, if it is possible.

This is like a version of unweaveIndex, but for Subset.