diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,16 @@ Changelog ========= +Version 0.1.3.0 +--------------- + +*August 23, 2019* + + + +* Add `Subset` and associated methods +* `interleaveShapes`, `swapInterleave`, `appendShape`, `prefixShape` + Version 0.1.2.0 --------------- diff --git a/list-witnesses.cabal b/list-witnesses.cabal --- a/list-witnesses.cabal +++ b/list-witnesses.cabal @@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack -- --- hash: 7abc29a51e67cb59dca3b968d5864b7bcfd1126df6a3bb4166c3eddd2999129f +-- hash: 719f24db96d689225456161daf1be9b65869796716720c8702c4de187265dc65 name: list-witnesses -version: 0.1.2.0 +version: 0.1.3.0 synopsis: Witnesses for working with type-level lists description: Collection of assorted inductive witnesses and functions for working with type-level lists. diff --git a/src/Data/Type/List/Sublist.hs b/src/Data/Type/List/Sublist.hs --- a/src/Data/Type/List/Sublist.hs +++ b/src/Data/Type/List/Sublist.hs @@ -30,6 +30,7 @@ -- ** Prefix Prefix(..), IsPrefix, autoPrefix , takeRec, prefixLens, takeIndex, weakenIndex + , prefixShape -- ** Suffix , Suffix(..), IsSuffix, autoSuffix , dropRec, suffixLens, dropIndex, shiftIndex @@ -37,6 +38,7 @@ , Append(..), IsAppend, autoAppend, withAppend , prefixToAppend, suffixToAppend , appendToPrefix, appendToSuffix, splitAppend + , appendShape -- ** Application , splitRec, appendRec, splitRecIso , splitIndex @@ -55,10 +57,21 @@ , Interleave(..), IsInterleave, autoInterleave , interleaveRec, unweaveRec, interleaveRecIso , injectIndexL, injectIndexR, unweaveIndex - , interleavedIxes + , interleavedIxes, swapInterleave + , interleaveShapes + -- * Subset + , Subset(..), IsSubset, autoSubset + , subsetComplement + , interleaveRToSubset, interleaveLToSubset + , subsetToInterleaveLeft, subsetToInterleaveRight + , subsetRec, getSubset + , subsetShapes + , subsetIxes + , weakenSubsetIndex, strengthenSubsetIndex ) where import Data.Bifunctor +import Data.Functor.Compose import Data.Kind import Data.Profunctor import Data.Singletons @@ -137,6 +150,16 @@ autoPrefix :: forall as bs. Auto (IsPrefix as) bs => Prefix as bs autoPrefix = auto @_ @(IsPrefix as) @bs +-- | Get the 'Shape' associated with a 'Prefix'. +-- +-- @since 0.1.3.0 +prefixShape + :: Prefix as bs + -> Shape [] as +prefixShape = \case + PreZ -> RNil + PreS p -> Proxy :& prefixShape p + -- | A @'Suffix' as bs@ witnesses that @as@ is a suffix of @bs@. -- -- Some examples: @@ -392,6 +415,16 @@ x :& xs -> \ys f -> withAppend xs ys $ \zs a -> f (x :& zs) (AppS a) +-- | Get the 'Shape' associated with an 'Append''s prefix. +-- +-- @since 0.1.3.0 +appendShape + :: Append as bs cs + -> Shape [] as +appendShape = \case + AppZ -> RNil + AppS a -> Proxy :& appendShape a + -- | Witness an isomorphism between 'Rec' and two parts that compose it. -- -- Read this type signature as: @@ -538,7 +571,7 @@ SufS s -> IS . shiftIndex s -- | A @'Interleave' as bs cs@ witnesses that @cs@ is @as@ interleaved with --- @bs. It is constructed by selectively zipping items from @as@ and @bs@ +-- @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 @@ -730,3 +763,224 @@ -> p (Rec g as, Rec g bs) (f (Rec g as, Rec g bs)) -> p (Rec g cs) (f (Rec g cs)) interleaveRecIso m = dimap (unweaveRec m) ((fmap . uncurry) (interleaveRec m)) + +-- | Swap the two halves of an 'Interleave'. +-- +-- @since 0.1.3.0 +swapInterleave + :: Interleave as bs cs + -> Interleave bs as cs +swapInterleave = \case + IntZ -> IntZ + IntL i -> IntR $ swapInterleave i + IntR i -> IntL $ swapInterleave i + +-- | Get the 'Shape's associated with an 'Interleave'. +-- +-- @since 0.1.3.0 +interleaveShapes + :: Interleave as bs cs + -> (Shape [] as, Shape [] bs, Shape [] cs) +interleaveShapes = \case + IntZ -> (RNil, RNil, RNil) + IntL i -> + let (as , bs , cs ) = interleaveShapes i + in (Proxy :& as, bs , Proxy :& cs) + IntR i -> + let (as , bs , cs ) = interleaveShapes i + in (as , Proxy :& bs, Proxy :& cs) + +-- | 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 +data Subset :: [k] -> [k] -> Type where + SubsetNil :: Subset '[] '[] + SubsetNo :: Subset as bs -> Subset as (b ': bs) + SubsetYes :: Subset as bs -> Subset (a ': as) (a ': bs) + +-- | Drop the right side of an 'Interleave', leaving only the left side. +interleaveLToSubset :: Interleave as bs cs -> Subset as cs +interleaveLToSubset = \case + IntZ -> SubsetNil + IntL i -> SubsetYes . interleaveLToSubset $ i + IntR i -> SubsetNo . interleaveLToSubset $ i + +-- | Drop the left side of an 'Interleave', leaving only the right side. +interleaveRToSubset :: Interleave as bs cs -> Subset bs cs +interleaveRToSubset = \case + IntZ -> SubsetNil + IntL i -> SubsetNo . interleaveRToSubset $ i + IntR i -> SubsetYes . interleaveRToSubset $ i + +-- | Convert a 'Subset' into an left 'Interleave', recovering the dropped +-- items. +subsetToInterleaveLeft + :: Subset as cs + -> (forall bs. Interleave as bs cs -> r) + -> r +subsetToInterleaveLeft = \case + SubsetNil -> \f -> f IntZ + SubsetNo s -> \f -> subsetToInterleaveLeft s (f . IntR) + SubsetYes s -> \f -> subsetToInterleaveLeft s (f . IntL) + +-- | Convert a 'Subset' into an right 'Interleave', recovering the dropped +-- items. +subsetToInterleaveRight + :: Subset bs cs + -> (forall as. Interleave as bs cs -> r) + -> r +subsetToInterleaveRight = \case + SubsetNil -> \f -> f IntZ + SubsetNo s -> \f -> subsetToInterleaveRight s (f . IntL) + SubsetYes s -> \f -> subsetToInterleaveRight s (f . IntR) + +-- | @as@ is a subset of @cs@; this function recovers @bs@, the subset of +-- @cs@ that is not @as@. +subsetComplement + :: Subset as cs + -> (forall bs. Subset bs cs -> r) + -> r +subsetComplement = \case + SubsetNil -> \f -> f SubsetNil + SubsetNo s -> \f -> subsetComplement s (f . SubsetYes) + SubsetYes s -> \f -> subsetComplement s (f . SubsetNo) + +deriving instance Show (Subset as bs) + + +-- | A type-level predicate that a given list is a "superset" of @as@, in +-- correct order +-- +-- @since 0.1.2.0 +type IsSubset as = TyPred (Subset as) + +instance Auto (IsSubset '[]) '[] where + auto = SubsetNil + +instance Auto (IsSubset as) bs => Auto (IsSubset as) (b ': bs) where + auto = SubsetNo (auto @_ @(IsSubset as) @bs) + +instance Auto (IsSubset as) bs => Auto (IsSubset (a ': as)) (a ': bs) where + auto = SubsetYes (auto @_ @(IsSubset as) @bs) + +instance (SDecide k, SingI (as :: [k])) => Decidable (IsSubset as) where + decide = case sing @as of + SNil -> \case + SNil -> Proved SubsetNil + _ `SCons` ys -> case decide @(IsSubset '[]) ys of + Proved s -> Proved $ SubsetNo s + Disproved v -> Disproved $ \case + SubsetNo s -> v s + x `SCons` (Sing :: Sing as') -> \case + SNil -> Disproved $ \case {} + y `SCons` ys -> case x %~ y of + Proved Refl -> case decide @(IsSubset as') ys of + Proved s -> Proved $ SubsetYes s + Disproved v -> case decide @(IsSubset as) ys of + Proved s -> Proved $ SubsetNo s + Disproved u -> Disproved $ \case + SubsetNo s -> u s + SubsetYes s -> v s + Disproved v -> case decide @(IsSubset as) ys of + Proved s -> Proved $ SubsetNo s + Disproved u -> Disproved $ \case + SubsetNo s -> u s + SubsetYes _ -> v Refl + +-- | Automatically generate an 'Subset' if @as@ and @bs@ are known +-- statically. +autoSubset :: forall as bs. Auto (IsSubset as) bs => Subset as bs +autoSubset = auto @_ @(IsSubset as) @bs + +-- | A lens into a subset of a record, indicated by a 'Subset'. +subsetRec :: Subset as bs -> Lens' (Rec f bs) (Rec f as) +subsetRec = \case + SubsetNil -> id + SubsetNo s -> \f -> \case + x :& xs -> (x :&) <$> subsetRec s f xs + SubsetYes s -> \f -> \case + x :& xs -> fmap (uncurry (:&)) + . getCompose + . subsetRec s (Compose . fmap (\(y :& ys) -> (y,ys)) . f . (x :&)) + $ xs + +-- | Take a subset out of a 'Rec'. An alias for @'view' ('subsetRec' s)@. +getSubset + :: Subset as bs + -> Rec f bs + -> Rec f as +getSubset = view . subsetRec + +-- | Get all of the indices of all the items in a 'Subset'. +subsetIxes + :: Subset as bs + -> Rec (Index bs) as +subsetIxes s = getSubset s . imapProd const $ sp + where + (_, sp) = subsetShapes s + +-- | Get the 'Shape's associated with a 'Subset'. +subsetShapes + :: Subset as bs + -> (Shape [] as, Shape [] bs) +subsetShapes = \case + SubsetNil -> (RNil, RNil) + SubsetNo s -> second (Proxy :&) $ subsetShapes s + SubsetYes s -> bimap (Proxy :&) (Proxy :&) $ subsetShapes s + +-- | 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'. +weakenSubsetIndex + :: Subset as bs + -> Index as a + -> Index bs a +weakenSubsetIndex = \case + SubsetNil -> \case {} + SubsetNo s -> IS . weakenSubsetIndex s + SubsetYes s -> \case + IZ -> IZ + IS i -> IS $ weakenSubsetIndex s i + +-- | 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'. +strengthenSubsetIndex + :: Subset as bs + -> Index bs a + -> Maybe (Index as a) +strengthenSubsetIndex = \case + SubsetNil -> \case {} + SubsetNo s -> \case + IZ -> Nothing + IS i -> strengthenSubsetIndex s i + SubsetYes s -> \case + IZ -> Just IZ + IS i -> IS <$> strengthenSubsetIndex s i