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)
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.
Recuct
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 cs)
(Rec f as, Rec f bs) (Rec f as, Rec f bs)
This can be used with the combinators from the lens library.