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.

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.

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