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

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

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

Take items from a Rec corresponding to a given Prefix.

prefixLens :: forall as bs g f. Functor f => Prefix as bs -> (Rec g as -> f (Rec g as)) -> Rec g bs -> f (Rec g bs)

A lens into the prefix of a Rec.

Read this type signature as:

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

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

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

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

Drop items from a Rec corresponding to a given Suffix.

suffixLens :: forall as bs g f. Functor f => Suffix as bs -> (Rec g as -> f (Rec g as)) -> Rec g bs -> f (Rec g bs)

A lens into the suffix of a Rec.

Read this type signature as:

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

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

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

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.

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 a 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

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

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