Copyright | (c) Justin Le 2018 |
---|---|
License | BSD3 |
Maintainer | justin@jle.im |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Witnesses regarding sublists of lists.
Synopsis
- data Prefix :: [k] -> [k] -> Type where
- takeRec :: Prefix as bs -> Rec f bs -> Rec f as
- 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)
- takeIndex :: Prefix as bs -> Index bs x -> Maybe (Index as x)
- weakenIndex :: Prefix as bs -> Index as x -> Index bs x
- data Suffix :: [k] -> [k] -> Type where
- dropRec :: Suffix as bs -> Rec f bs -> Rec f as
- 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)
- dropIndex :: Suffix as bs -> Index bs x -> Maybe (Index as x)
- shiftIndex :: Suffix as bs -> Index as x -> Index bs x
- data Append :: [k] -> [k] -> [k] -> Type where
- prefixToAppend :: Prefix as cs -> (forall bs. Append as bs cs -> r) -> r
- suffixToAppend :: Suffix bs cs -> (forall as. Append as bs cs -> r) -> r
- appendToPrefix :: Append as bs cs -> Prefix as cs
- appendToSuffix :: Append as bs cs -> Suffix bs cs
- splitAppend :: Append as bs cs -> (Prefix as cs, Suffix bs cs)
- splitRec :: Append as bs cs -> Rec f cs -> (Rec f as, Rec f bs)
- appendRec :: Append as bs cs -> Rec f as -> Rec f bs -> Rec f cs
- 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))
- splitIndex :: Append as bs cs -> Index cs x -> Either (Index as x) (Index bs x)
- data Interleave :: [k] -> [k] -> [k] -> Type where
- IntZ :: Interleave '[] '[] '[]
- IntL :: Interleave as bs cs -> Interleave (a ': as) bs (a ': cs)
- IntR :: Interleave as bs cs -> Interleave as (b ': bs) (b ': cs)
- interleaveRec :: Interleave as bs cs -> Rec f as -> Rec f bs -> Rec f cs
- unweaveRec :: Interleave as bs cs -> Rec f cs -> (Rec f as, Rec f bs)
- 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))
- injectIndexL :: Interleave as bs cs -> Index as a -> Index cs a
- injectIndexR :: Interleave as bs cs -> Index bs b -> Index cs b
- unweaveIndex :: Interleave as bs cs -> Index cs c -> Either (Index as c) (Index bs c)
Prefix and Suffix
Prefix
data Prefix :: [k] -> [k] -> Type where Source #
A
witnesses that Prefix
as bsas
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.
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) Source #
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) Source #
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 Source #
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 Source #
A
witnesses that Suffix
as bsas
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.
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) Source #
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) Source #
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 Source #
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
prefixToAppend :: Prefix as cs -> (forall bs. Append as bs cs -> r) -> r Source #
suffixToAppend :: Suffix bs cs -> (forall as. Append as bs cs -> r) -> r Source #
appendToPrefix :: Append as bs cs -> Prefix as cs Source #
appendToSuffix :: Append as bs cs -> Suffix bs cs Source #
splitAppend :: Append as bs cs -> (Prefix as cs, Suffix bs cs) Source #
Split an Append
into a Prefix
and Suffix
. Basically
appendToPrefix
and appendToSuffix
at the same time.
Application
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)) Source #
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.
Interleave
data Interleave :: [k] -> [k] -> [k] -> Type where Source #
A
witnesses that Interleave
as bs cscs
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
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) Source # | |
Defined in Data.Type.List.Sublist 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 Source #
unweaveRec :: Interleave as bs cs -> Rec f cs -> (Rec f as, Rec f bs) Source #
Given a Rec
, disinterleave it into two Rec
s 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)) Source #
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 Source #
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 Source #
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) Source #
Given an index on cs
, disinterleave it into either an index on as
or on bs
.
Since: 0.1.1.0