Data.Type.List.Sublist

Witnesses regarding sublists of lists.

Prefix and Suffix

Prefix

data Prefix :: [k] -> [k] -> Type where

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.

Constructors

PreZ :: Prefix '[] as

PreS :: Prefix as bs -> Prefix (a ': as) (a ': bs)

Instances

(SDecide k, SingI as) => Decidable (IsPrefix as :: TyFun [k] Type -> Type)

Defined in Data.Type.List.Sublist

Methods

decide :: Decide (IsPrefix as)

Auto (IsPrefix ([] :: [k]) :: TyFun [k] Type -> Type) (bs :: [k])

Defined in Data.Type.List.Sublist

Methods

auto :: IsPrefix [] @@ bs

Auto (IsPrefix as) bs => Auto (IsPrefix (a2 ': as) :: TyFun [a1] Type -> Type) (a2 ': bs :: [a1])

Defined in Data.Type.List.Sublist

Methods

auto :: IsPrefix (a2 ': as) @@ (a2 ': bs)

Show (Prefix as bs)

Defined in Data.Type.List.Sublist

Methods

showsPrec :: Int -> Prefix as bs -> ShowS

show :: Prefix as bs -> String

showList :: [Prefix as bs] -> ShowS

type IsPrefix as = TyPred (Prefix as)

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

Since: 0.1.2.0

autoPrefix :: forall as bs. Auto (IsPrefix as) bs => Prefix as bs

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

Since: 0.1.2.0

takeRec :: Prefix as bs -> Rec f bs -> Rec f as

Take items from a Rec corresponding to a given Prefix.

prefixLens :: Prefix as bs -> Lens' (Rec f bs) (Rec f as)

A lens into the prefix of a Rec.

takeIndex :: Prefix as bs -> Index bs x -> Maybe (Index as x)

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.

weakenIndex :: Prefix as bs -> Index as x -> Index bs x

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.

prefixShape :: Prefix as bs -> Shape [] as

Get the Shape associated with a Prefix.

Since: 0.1.3.0

Suffix

data Suffix :: [k] -> [k] -> Type where

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.

Constructors

SufZ :: Suffix as as

SufS :: Suffix as bs -> Suffix as (b ': bs)

Instances

(SDecide k, SingI as) => Decidable (IsSuffix as :: TyFun [k] Type -> Type)

Defined in Data.Type.List.Sublist

Methods

decide :: Decide (IsSuffix as)

Auto (IsSuffix as :: TyFun [k] Type -> Type) (as :: [k])

Defined in Data.Type.List.Sublist

Methods

auto :: IsSuffix as @@ as

Auto (IsSuffix as) bs => Auto (IsSuffix as :: TyFun [a] Type -> Type) (b ': bs :: [a])

Defined in Data.Type.List.Sublist

Methods

auto :: IsSuffix as @@ (b ': bs)

Show (Suffix as bs)

Defined in Data.Type.List.Sublist

Methods

showsPrec :: Int -> Suffix as bs -> ShowS

show :: Suffix as bs -> String

showList :: [Suffix as bs] -> ShowS

type IsSuffix as = TyPred (Suffix as)

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

Since: 0.1.2.0

autoSuffix :: forall as bs. Auto (IsSuffix as) bs => Suffix as bs

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

Since: 0.1.2.0

dropRec :: Suffix as bs -> Rec f bs -> Rec f as

Drop items from a Rec corresponding to a given Suffix.

suffixLens :: Suffix as bs -> Lens' (Rec f bs) (Rec f as)

A lens into the suffix of a Rec.

dropIndex :: Suffix as bs -> Index bs x -> Maybe (Index as x)

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.

shiftIndex :: Suffix as bs -> Index as x -> Index bs x

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.

Append

data Append :: [k] -> [k] -> [k] -> Type where

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.

Constructors

AppZ :: Append '[] as as

AppS :: Append as bs cs -> Append (a ': as) bs (a ': cs)

Instances

(SDecide k, SingI as, SingI bs) => Decidable (IsAppend as bs :: TyFun [k] Type -> Type)

Defined in Data.Type.List.Sublist

Methods

decide :: Decide (IsAppend as bs)

SingI as => Decidable (Found (AppendedTo as) :: TyFun [k] Type -> Type)

Defined in Data.Type.List.Sublist

Methods

decide :: Decide (Found (AppendedTo as))

SingI as => Provable (Found (AppendedTo as) :: TyFun [k] Type -> Type)

Defined in Data.Type.List.Sublist

Methods

prove :: Prove (Found (AppendedTo as))

Auto (IsAppend ([] :: [k]) as :: TyFun [k] Type -> Type) (as :: [k])

Defined in Data.Type.List.Sublist

Methods

auto :: IsAppend [] as @@ as

Auto (IsAppend as bs) cs => Auto (IsAppend (a2 ': as) bs :: TyFun [a1] Type -> Type) (a2 ': cs :: [a1])

Defined in Data.Type.List.Sublist

Methods

auto :: IsAppend (a2 ': as) bs @@ (a2 ': cs)

Show (Append as bs cs)

Defined in Data.Type.List.Sublist

Methods

showsPrec :: Int -> Append as bs cs -> ShowS

show :: Append as bs cs -> String

showList :: [Append as bs cs] -> ShowS

type IsAppend as bs = TyPred (Append as bs)

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

Since: 0.1.2.0

autoAppend :: forall as bs cs. Auto (IsAppend as bs) cs => Append as bs cs

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

Since: 0.1.2.0

withAppend :: Rec f as -> Rec f bs -> (forall cs. Rec f cs -> Append as bs cs -> r) -> r

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

prefixToAppend :: Prefix as cs -> (forall bs. Append as bs cs -> r) -> r

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

suffixToAppend :: Suffix bs cs -> (forall as. Append as bs cs -> r) -> r

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

appendToPrefix :: Append as bs cs -> Prefix as cs

Convert an Append to a Prefix, forgetting the suffix.

appendToSuffix :: Append as bs cs -> Suffix bs cs

Convert an Append to a Suffix, forgetting the prefix

splitAppend :: Append as bs cs -> (Prefix as cs, Suffix bs cs)

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

appendShape :: Append as bs cs -> Shape [] as

Get the Shape associated with an Append's prefix.

Since: 0.1.3.0

Application

splitRec :: Append as bs cs -> Rec f cs -> (Rec f as, Rec f bs)

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

appendRec :: Append as bs cs -> Rec f as -> Rec f bs -> Rec f cs

Append two Recs together according to an Append.

splitRecIso :: (Profunctor p, Functor f) => Append as bs cs -> p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs)) -> p (Rec g cs) (f (Rec g cs))

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.

splitIndex :: Append as bs cs -> Index cs x -> Either (Index as x) (Index bs x)

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.

Witnesses

Singletons

pattern AppendWit :: forall as bs cs. (RecApplicative as, RecApplicative bs) => (as ++ bs) ~ cs => Append as bs cs

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

appendWit :: Append as bs cs -> (as ++ bs) :~: cs

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

Since: 0.1.2.0

implyAppend :: IsAppend as bs --> EqualTo (as ++ bs)

appendWit stated as a Predicate implication.

Since: 0.1.2.0

unAppendWit :: (as ++ bs) ~ cs => Rec f as -> Rec f bs -> Append as bs cs

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

Vinyl

pattern AppendWitV :: forall as bs cs. (RecApplicative as, RecApplicative bs) => (as ++ bs) ~ cs => Append as bs cs

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

appendWitV :: Append as bs cs -> (as ++ bs) :~: cs

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

Since: 0.1.2.0

implyAppendV :: IsAppend as bs --> EqualTo (as ++ bs)

appendWitV stated as a Predicate implication.

Since: 0.1.2.0

unAppendWitV :: (as ++ bs) ~ cs => Rec f as -> Rec f bs -> Append as bs cs

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

Both

pattern AppendWit' :: forall as bs cs. (RecApplicative as, RecApplicative bs) => ((as ++ bs) ~ cs, (as ++ bs) ~ cs) => Append as bs cs

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

convertAppends :: Append as bs cs -> (as ++ bs) :~: (as ++ bs)

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.

type AppendedTo as = TyPP (Append as)

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

Interleave

data Interleave :: [k] -> [k] -> [k] -> Type where

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

Constructors

IntZ :: Interleave '[] '[] '[]

IntL :: Interleave as bs cs -> Interleave (a ': as) bs (a ': cs)

IntR :: Interleave as bs cs -> Interleave as (b ': bs) (b ': cs)

Instances

(SDecide k, SingI as, SingI bs) => Decidable (IsInterleave as bs :: TyFun [k] Type -> Type)

Defined in Data.Type.List.Sublist

Methods

decide :: Decide (IsInterleave as bs)

Auto (IsInterleave ([] :: [k]) ([] :: [k]) :: TyFun [k] Type -> Type) ([] :: [k])

Defined in Data.Type.List.Sublist

Methods

auto :: IsInterleave [] [] @@ []

Auto (IsInterleave as bs) cs => Auto (IsInterleave as (b ': bs) :: TyFun [a] Type -> Type) (b ': cs :: [a])

Defined in Data.Type.List.Sublist

Methods

auto :: IsInterleave as (b ': bs) @@ (b ': cs)

Auto (IsInterleave as bs) cs => Auto (IsInterleave (a2 ': as) bs :: TyFun [a1] Type -> Type) (a2 ': cs :: [a1])

Defined in Data.Type.List.Sublist

Methods

auto :: IsInterleave (a2 ': as) bs @@ (a2 ': cs)

Show (Interleave as bs cs)

Defined in Data.Type.List.Sublist

Methods

showsPrec :: Int -> Interleave as bs cs -> ShowS

show :: Interleave as bs cs -> String

showList :: [Interleave as bs cs] -> ShowS

type IsInterleave as bs = TyPred (Interleave as bs)

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

Since: 0.1.2.0

autoInterleave :: forall as bs cs. Auto (IsInterleave as bs) cs => Interleave as bs cs

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

Since: 0.1.2.0

interleaveRec :: Interleave as bs cs -> Rec f as -> Rec f bs -> Rec f cs

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

Since: 0.1.1.0

unweaveRec :: Interleave as bs cs -> Rec f cs -> (Rec f as, Rec f bs)

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

Since: 0.1.1.0

interleaveRecIso :: (Profunctor p, Functor f) => Interleave as bs cs -> p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs)) -> p (Rec g cs) (f (Rec g cs))

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

injectIndexL :: Interleave as bs cs -> Index as a -> Index cs a

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

Since: 0.1.1.0

injectIndexR :: Interleave as bs cs -> Index bs b -> Index cs b

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

Since: 0.1.1.0

unweaveIndex :: Interleave as bs cs -> Index cs c -> Either (Index as c) (Index bs c)

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

Since: 0.1.1.0

interleavedIxes :: Interleave as bs cs -> Rec (Index as :+: Index bs) cs

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

Warning: O(n^2)

Since: 0.1.2.0

swapInterleave :: Interleave as bs cs -> Interleave bs as cs

Swap the two halves of an Interleave.

Since: 0.1.3.0

interleaveShapes :: Interleave as bs cs -> (Shape [] as, Shape [] bs, Shape [] cs)

Get the Shapes associated with an Interleave.

Since: 0.1.3.0

Subset

data Subset :: [k] -> [k] -> Type where

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

Constructors

SubsetNil :: Subset '[] '[]

SubsetNo :: Subset as bs -> Subset as (b ': bs)

SubsetYes :: Subset as bs -> Subset (a ': as) (a ': bs)

Instances

(SDecide k, SingI as) => Decidable (IsSubset as :: TyFun [k] Type -> Type)

Defined in Data.Type.List.Sublist

Methods

decide :: Decide (IsSubset as)

Auto (IsSubset ([] :: [k]) :: TyFun [k] Type -> Type) ([] :: [k])

Defined in Data.Type.List.Sublist

Methods

auto :: IsSubset [] @@ []

Auto (IsSubset as) bs => Auto (IsSubset (a2 ': as) :: TyFun [a1] Type -> Type) (a2 ': bs :: [a1])

Defined in Data.Type.List.Sublist

Methods

auto :: IsSubset (a2 ': as) @@ (a2 ': bs)

Auto (IsSubset as) bs => Auto (IsSubset as :: TyFun [a] Type -> Type) (b ': bs :: [a])

Defined in Data.Type.List.Sublist

Methods

auto :: IsSubset as @@ (b ': bs)

Show (Subset as bs)

Defined in Data.Type.List.Sublist

Methods

showsPrec :: Int -> Subset as bs -> ShowS

show :: Subset as bs -> String

showList :: [Subset as bs] -> ShowS

type IsSubset as = TyPred (Subset as)

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

Since: 0.1.2.0

autoSubset :: forall as bs. Auto (IsSubset as) bs => Subset as bs

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

subsetComplement :: Subset as cs -> (forall bs. Subset bs cs -> r) -> r

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

interleaveRToSubset :: Interleave as bs cs -> Subset bs cs

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

interleaveLToSubset :: Interleave as bs cs -> Subset as cs

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

subsetToInterleaveLeft :: Subset as cs -> (forall bs. Interleave as bs cs -> r) -> r

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

subsetToInterleaveRight :: Subset bs cs -> (forall as. Interleave as bs cs -> r) -> r

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

subsetRec :: Subset as bs -> Lens' (Rec f bs) (Rec f as)

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

getSubset :: Subset as bs -> Rec f bs -> Rec f as

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

subsetShapes :: Subset as bs -> (Shape [] as, Shape [] bs)

Get the Shapes associated with a Subset.

subsetIxes :: Subset as bs -> Rec (Index bs) as

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

weakenSubsetIndex :: Subset as bs -> Index as a -> Index bs a

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.

strengthenSubsetIndex :: Subset as bs -> Index bs a -> Maybe (Index as a)

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.