data-diverse 1.1.0.0 → 1.2.0.0

raw patch · 9 files changed

+523/−40 lines, 9 filesdep ~containersPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: containers

API changes (from Hackage documentation)

Files

• README.md +9/−0
• data-diverse.cabal +2/−2
• src/Data/Diverse/Many.hs +32/−0
• src/Data/Diverse/Many/Internal.hs +274/−8
• src/Data/Diverse/TypeLevel.hs +62/−7
• src/Data/Diverse/TypeLevel/Internal.hs +4/−4
• src/Data/Diverse/Which/Internal.hs +10/−10
• test/Data/Diverse/ManySpec.hs +121/−0
• test/Data/Diverse/WhichSpec.hs +9/−9

@@ -14,6 +14,15 @@  # Changelog +* 1.2.0.0+  - Rerranged type variable for xxxL and xxxN functions so that the+    @x@ inferrred from label @l@ or index @n@ is after @proxy@.+    - This affects `fetch[L|N]`, `replace[L|N]`, `replace[L|N]'`, `pick[L|N]`+  - Depends on at least containers-0.5.8.2 for `Data.Sequence.insertAt`+  - Added splitting operations: `split[Before|After][|L|N]`, `inset[Before|After][|L|N]`,+    `insert[Before|After][|L|N]`, `remove[Before|After][|L|N]`+  - Renamed type function `Without` to `Remove` to be consistent with new `remove` method.+ * 1.1.0.0   - Added `CaseFunc` and `CaseFunc'` which replaces `CaseTypeable` (eg `CaseFunc @Typeable`)     <https://github.com/louispan/data-diverse/issues/6>

@@ -1,5 +1,5 @@ name:                data-diverse-version:             1.1.0.0+version:             1.2.0.0 synopsis:            Extensible records and polymorphic variants. description:         "Data.Diverse.Many" is an extensible record for any size encoded efficiently as (Seq Any).                      "Data.Diverse.Which" is a polymorphic variant of possibilities encoded as (Int, Any).@@ -39,7 +39,7 @@                        Data.Diverse.Which                        Data.Diverse.Which.Internal   build-depends:       base >= 4.7 && < 5-                     , containers >= 0.5 && < 0.6+                     , containers >= 0.5.8.2 && < 0.6                      , deepseq >= 1.4 && < 2                      , ghc-prim >= 0.5 && < 1                      , tagged >= 0.8.5 && < 1

@@ -71,6 +71,38 @@     , CollectorN     , forManyN     , collectN++    -- * Splitting operations++    -- * Splitting+    , splitBefore+    , splitBeforeL+    , splitBeforeN+    , splitAfter+    , splitAfterL+    , splitAfterN++    -- * inset multiple items+    , insetBefore+    , insetBeforeL+    , insetBeforeN+    , insetAfter+    , insetAfterL+    , insetAfterN++    -- * insert single item+    , insertBefore+    , insertBeforeL+    , insertBeforeN+    , insertAfter+    , insertAfterL+    , insertAfterN++    -- * Deleting single item+    , remove+    , removeL+    , removeN+     ) where  import Data.Diverse.Many.Internal

@@ -88,6 +88,38 @@     , CollectorN     , forManyN     , collectN++    -- * Splitting operations++    -- * Splitting+    , splitBefore+    , splitBeforeL+    , splitBeforeN+    , splitAfter+    , splitAfterL+    , splitAfterN++    -- * inset multiple items+    , insetBefore+    , insetBeforeL+    , insetBeforeN+    , insetAfter+    , insetAfterL+    , insetAfterN++    -- * insert single item+    , insertBefore+    , insertBeforeL+    , insertBeforeN+    , insertAfter+    , insertAfterL+    , insertAfterN++    -- * Deleting single item+    , remove+    , removeL+    , removeN+     ) where  import Control.Applicative@@ -292,7 +324,7 @@ nil :: Many '[] nil = Many S.empty --- | Create a Many from a single value. Analogous to 'M.singleton'+-- | Create a Many from a single value. Analogous to 'S.singleton' single :: x -> Many '[x] single v = Many (S.singleton (unsafeCoerce v)) @@ -407,6 +439,240 @@  -------------------------------------------------- +-- | Split a Many into two, where the last type in the first Many is unique @x@+splitAfter_+    :: forall x xs n proxy.+       (KnownNat n, n ~ IndexOf x xs)+    => proxy x -> Many xs -> (Many (To x xs), Many (After x xs))+splitAfter_ _ (Many xs) = let (as, bs) = S.splitAt (i + 1) xs in (Many as, Many bs)+  where+    i = fromInteger (natVal @n Proxy) :: Int++-- | Split a Many into two, where the first type in the second Many is unique @x@+splitBefore_+    :: forall x xs n proxy.+       (KnownNat n, n ~ IndexOf x xs)+    => proxy x -> Many xs -> (Many (Before x xs), Many (From x xs))+splitBefore_ _ (Many xs) = let (as, bs) = S.splitAt i xs in (Many as, Many bs)+  where+    i = fromInteger (natVal @n Proxy) :: Int++-- | Split a Many into two, where the last type in the first Many is unique @x@+splitAfter+    :: forall x xs proxy.+       (UniqueMember x xs)+    => proxy x -> Many xs -> (Many (To x xs), Many (After x xs))+splitAfter _ = splitAfter_ (Proxy @x)++-- | Split a Many into two, where the first type in the second Many is unique @x@+splitBefore+    :: forall x xs proxy.+       (UniqueMember x xs)+    => proxy x -> Many xs -> (Many (Before x xs), Many (From x xs))+splitBefore _ = splitBefore_ (Proxy @x)++-- | Split a Many into two, where the last type in the first Many is unique label @l@+splitAfterL+    :: forall l xs proxy x.+       (UniqueLabelMember l xs, x ~ KindAtLabel l xs)+    => proxy l -> Many xs -> (Many (To x xs), Many (After x xs))+splitAfterL _ = splitAfter_ (Proxy @x)++-- | Split a Many into two, where the first type in the second Many is unique label @l@+splitBeforeL+    :: forall l xs proxy x.+       (UniqueLabelMember l xs, x ~ KindAtLabel l xs)+    => proxy l -> Many xs -> (Many (Before x xs), Many (From x xs))+splitBeforeL _ = splitBefore_ (Proxy @x)++-- | Split a Many into two, where the second Many starts at index @(n + 1)@+splitAfterN+    :: forall n xs proxy.+       (KnownNat n, n + 1 <= Length xs)+    => proxy n -> Many xs -> (Many (ToIndex n xs), Many (AfterIndex n xs))+splitAfterN _ (Many xs) = let (as, bs) = S.splitAt (i + 1) xs in (Many as, Many bs)+  where+    i = fromInteger (natVal @n Proxy) :: Int++-- | Split a Many into two, where the second Many starts at index @n@+splitBeforeN+    :: forall n xs proxy.+       (KnownNat n, n + 1 <= Length xs)+    => proxy n -> Many xs -> (Many (BeforeIndex n xs), Many (FromIndex n xs))+splitBeforeN _ (Many xs) = let (as, bs) = S.splitAt i xs in (Many as, Many bs)+  where+    i = fromInteger (natVal @n Proxy) :: Int++--------------------------------------------------++-- | Insert a Many into another Many, inserting after a unique @x@+insetAfter_+    :: forall x ys xs n proxy.+       (KnownNat n, n ~ IndexOf x xs)+    => proxy x -> Many ys -> Many xs -> Many (Append (To x xs) (Append ys (After x xs)))+insetAfter_ _ (Many ys) (Many xs) = let (as, bs) = S.splitAt (i + 1) xs in Many (as S.>< ys S.>< bs)+  where+    i = fromInteger (natVal @n Proxy) :: Int++-- | Insert a Many into another Many, inserting before a unique @x@+insetBefore_+    :: forall x ys xs n proxy.+       (KnownNat n, n ~ IndexOf x xs)+    => proxy x -> Many ys -> Many xs -> Many (Append (Before x xs) (Append ys (From x xs)))+insetBefore_ _ (Many ys) (Many xs) = let (as, bs) = S.splitAt i xs in Many (as S.>< ys S.>< bs)+  where+    i = fromInteger (natVal @n Proxy) :: Int++-- | Insert a Many into another Many, inserting after a unique @x@+insetAfter+    :: forall x ys xs proxy.+       (UniqueMember x xs)+    => proxy x -> Many ys -> Many xs -> Many (Append (To x xs) (Append ys (After x xs)))+insetAfter _ = insetAfter_ (Proxy @x)++-- | Insert a Many into another Many, inserting before a unique @x@+insetBefore+    :: forall x ys xs proxy.+       (UniqueMember x xs)+    => proxy x -> Many ys -> Many xs -> Many (Append (Before x xs) (Append ys (From x xs)))+insetBefore _ = insetBefore_ (Proxy @x)++-- | Insert a Many into another Many, inserting after a unique label @l@+insetAfterL+    :: forall l ys xs proxy x.+       (UniqueLabelMember l xs, x ~ KindAtLabel l xs)+    => proxy l -> Many ys -> Many xs -> Many (Append (To x xs) (Append ys (After x xs)))+insetAfterL _ = insetAfter_ (Proxy @x)++-- | Insert a Many into another Many, inserting before a unique label @l@+insetBeforeL+    :: forall l ys xs proxy x.+       (UniqueLabelMember l xs, x ~ KindAtLabel l xs)+    => proxy l -> Many ys -> Many xs -> Many (Append (Before x xs) (Append ys (From x xs)))+insetBeforeL _ = insetBefore_ (Proxy @x)++-- | Insert a Many into another Many, starting at index @(n + 1)@+insetAfterN+    :: forall n ys xs proxy.+       (KnownNat n, n + 1 <= Length xs)+    => proxy n -> Many ys -> Many xs -> Many (Append (ToIndex n xs) (Append ys (AfterIndex n xs)))+insetAfterN _ (Many ys) (Many xs) = let (as, bs) = S.splitAt (i + 1) xs in Many (as S.>< ys S.>< bs)+  where+    i = fromInteger (natVal @n Proxy) :: Int++-- | Insert a Many into another Many, starting at index @n@+insetBeforeN+    :: forall n ys xs proxy.+       (KnownNat n, n + 1 <= Length xs)+    => proxy n -> Many ys -> Many xs -> Many (Append (BeforeIndex n xs) (Append ys (FromIndex n xs)))+insetBeforeN _ (Many ys) (Many xs) = let (as, bs) = S.splitAt i xs in Many (as S.>< ys S.>< bs)+  where+    i = fromInteger (natVal @n Proxy) :: Int++--------------------------------------------------++-- | Insert an item into a Many, inserting after unique type @x@+insertAfter_+    :: forall x y xs n proxy.+       (KnownNat n, n ~ IndexOf x xs)+    => proxy x -> y -> Many xs -> Many (Append (To x xs) (y ': After x xs))+insertAfter_ _ y (Many xs) = Many (S.insertAt (i + 1) (unsafeCoerce y) xs)+  where+    i = fromInteger (natVal @n Proxy) :: Int++-- | Insert an item into a Many, inserting before unique type @x@+insertBefore_+    :: forall x y xs n proxy.+       (KnownNat n, n ~ IndexOf x xs)+    => proxy x -> y -> Many xs -> Many (Append (Before x xs) (y ': From x xs))+insertBefore_ _ y (Many xs) = Many (S.insertAt i (unsafeCoerce y) xs)+  where+    i = fromInteger (natVal @n Proxy) :: Int++-- | Insert an item into a Many, inserting after unique type @x@+insertAfter+    :: forall x y xs proxy.+       (UniqueMember x xs)+    => proxy x -> y -> Many xs -> Many (Append (To x xs) (y ': After x xs))+insertAfter _ = insertAfter_ (Proxy @x)++-- | Insert an item into a Many, inserting before unique type @x@+insertBefore+    :: forall x y xs proxy.+       (UniqueMember x xs)+    => proxy x -> y -> Many xs -> Many (Append (Before x xs) (y ': From x xs))+insertBefore _ = insertBefore_ (Proxy @x)++-- | Insert an item into a Many, inserting after unique label @l@+insertAfterL+    :: forall l y xs proxy x.+       (UniqueLabelMember l xs, x ~ KindAtLabel l xs)+    => proxy l -> y -> Many xs -> Many (Append (To x xs) (y ': After x xs))+insertAfterL _ = insertAfter_ (Proxy @x)++-- | Insert an item into a Many, inserting before unique label @l@+insertBeforeL+    :: forall l y xs proxy x.+       (UniqueLabelMember l xs, x ~ KindAtLabel l xs)+    => proxy l -> y -> Many xs -> Many (Append (Before x xs) (y ': From x xs))+insertBeforeL _ = insertBefore_ (Proxy @x)++-- | Insert an item into a Many, inserting after index @n@+insertAfterN+    :: forall n y xs proxy.+       (KnownNat n, n + 1 <= Length xs)+    => proxy n -> y -> Many xs -> Many (Append (ToIndex n xs) (y ': AfterIndex n xs))+insertAfterN _ y (Many xs) = Many (S.insertAt (i + 1) (unsafeCoerce y) xs)+  where+    i = fromInteger (natVal @n Proxy) :: Int++-- | Insert an item into a Many, inserting before index @n@+insertBeforeN+    :: forall n y xs proxy.+       (KnownNat n, n + 1 <= Length xs)+    => proxy n -> y -> Many xs -> Many (Append (BeforeIndex n xs) (y ': FromIndex n xs))+insertBeforeN _ y (Many xs) = Many (S.insertAt i (unsafeCoerce y) xs)+  where+    i = fromInteger (natVal @n Proxy) :: Int++--------------------------------------------------++-- | Remove the unique @x@ from a Many.+-- Not named 'delete' to avoid conflicts with 'Data.List.delete'+remove_+    :: forall x xs n proxy.+       (KnownNat n, n ~ IndexOf x xs)+    => proxy x -> Many xs -> Many (Remove x xs)+remove_ _ (Many xs) = Many (S.deleteAt i xs)+  where+    i = fromInteger (natVal @n Proxy) :: Int++-- | Remove the unique @x@ from a Many.+-- Not named 'delete' to avoid conflicts with 'Data.List.delete'+remove+    :: forall x xs proxy.+       (UniqueMember x xs)+    => proxy x -> Many xs -> Many (Remove x xs)+remove _ = remove_ (Proxy @x)++-- | Remove the unique label @l@ from a Many.+removeL+    :: forall l xs proxy x.+       (UniqueLabelMember l xs, x ~ KindAtLabel l xs)+    => proxy l -> Many xs -> Many (Remove x xs)+removeL _ = remove_ (Proxy @x)++-- | Remove the @n@-th item from a Many.+removeN+    :: forall n xs proxy.+       (KnownNat n, n + 1 <= Length xs)+    => proxy n -> Many xs -> Many (RemoveIndex n xs)+removeN _ (Many xs) = Many (S.deleteAt i xs)+  where+    i = fromInteger (natVal @n Proxy) :: Int++--------------------------------------------------+ -- | Getter by unique type. Get the field with type @x@. -- -- @@@ -431,7 +697,7 @@ -- 'fetchL' \@Foo Proxy y \`shouldBe` Tagged \@Foo \'X' -- 'fetchL' \@"Hi" Proxy y \`shouldBe` Tagged \@"Hi" True -- @-fetchL :: forall l x xs proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> x+fetchL :: forall l xs proxy x. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> x fetchL _ = fetch_ @x  --------------------------------------------------@@ -442,7 +708,7 @@ -- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' 'nil' -- 'fetchN' @1 Proxy x \`shouldBe` False -- @-fetchN :: forall n x xs proxy. MemberAt n x xs => proxy n -> Many xs -> x+fetchN :: forall n xs proxy x. MemberAt n x xs => proxy n -> Many xs -> x fetchN p (Many xs) = let !x = S.index xs i in (unsafeCoerce x) -- forcing x to avoid storing Seq in thunk   where i = fromInteger (natVal p) @@ -470,7 +736,7 @@ replace' :: forall x y xs proxy. UniqueMember x xs => proxy x -> Many xs -> y -> Many (Replace x y xs) replace' = replace'_ -replace'_ :: forall x y xs n proxy. (KnownNat n, n ~ IndexOf x xs) => proxy x -> Many xs -> y -> Many (Replace x y xs)+replace'_ :: forall x y xs proxy n. (KnownNat n, n ~ IndexOf x xs) => proxy x -> Many xs -> y -> Many (Replace x y xs) replace'_ _ (Many xs) v = Many (S.update i (unsafeCoerce v) xs)   where i = fromInteger (natVal @n Proxy) @@ -485,7 +751,7 @@ -- 'replaceL' \@\"Hello" Proxy y (Tagged \@\"Hello" 7) \`shouldBe` --     (5 :: Int) './' False './' Tagged \@Foo \'X' './' Tagged \@\"Hello" (7 :: Int) './' 'nil' -- @-replaceL :: forall l x xs proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> x -> Many xs+replaceL :: forall l xs proxy x. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> x -> Many xs replaceL _ = replace_ @x  -- | Polymorphic setter by unique type. Set the field with type @x@, and replace with type @y@@@ -497,7 +763,7 @@ -- replaceL' \@\"Hello" Proxy y (Tagged \@\"Hello" False) \`shouldBe` --     (5 :: Int) './' False './' Tagged \@Foo \'X' './' Tagged \@\"Hello" False './' 'nil' -- @-replaceL' :: forall l x y xs proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> y -> Many (Replace x y xs)+replaceL' :: forall l y xs proxy x. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> Many xs -> y -> Many (Replace x y xs) replaceL' _ = replace'_ @x Proxy  --------------------------------------------------@@ -508,12 +774,12 @@ -- let x = (5 :: Int) './' False './' \'X' './' Just \'O' './' 'nil' -- 'replaceN' \@0 Proxy x 7 `shouldBe` -- @-replaceN :: forall n x y xs proxy. MemberAt n x xs => proxy n -> Many xs -> y -> Many xs+replaceN :: forall n xs proxy x. MemberAt n x xs => proxy n -> Many xs -> x -> Many xs replaceN p (Many xs) v = Many (S.update i (unsafeCoerce v) xs)   where i = fromInteger (natVal p)  -- | Polymorphic version of 'replaceN'-replaceN' :: forall n x y xs proxy. MemberAt n x xs => proxy n -> Many xs -> y -> Many (ReplaceIndex n y xs)+replaceN' :: forall n y xs proxy x. MemberAt n x xs => proxy n -> Many xs -> y -> Many (ReplaceIndex n y xs) replaceN' p (Many xs) v = Many (S.update i (unsafeCoerce v) xs)   where i = fromInteger (natVal p) 

@@ -104,10 +104,10 @@     KindsAtLabels (l ': ls) xs = KindAtLabel l xs ': KindsAtLabels ls xs  -- | The typelist @xs@ without first @x@. It is okay for @x@ not to exist in @xs@-type family Without (x :: k) (xs :: [k]) :: [k] where-    Without x '[] = '[]-    Without x (x ': xs) = xs-    Without x (y ': xs) = y ': Without x xs+type family Remove (x :: k) (xs :: [k]) :: [k] where+    Remove x '[] = '[]+    Remove x (x ': xs) = xs+    Remove x (y ': xs) = y ': Remove x xs  -- | The typelist @xs@ with the first @x@ replaced by @y@. It is okay for @x@ not to exist in @xs@ type Replace (x :: k) (y :: k) (xs :: [k]) = ReplaceImpl x y xs@@ -117,7 +117,7 @@ type Replaces (xs :: [k]) (ys :: [k]) (zs :: [k]) = ReplacesImpl xs ys xs ys zs  -- | The typelist @xs@ without the type at Nat @n@. @n@ must be within bounds of @xs@-type WithoutIndex (n :: Nat) (xs :: [k]) = WithoutIndexImpl n xs n xs+type RemoveIndex (n :: Nat) (xs :: [k]) = RemoveIndexImpl n xs n xs  -- | The typelist @xs@ without the type at Nat @n@ replaced by @y@. @n@ must be within bounds of @xs@ type ReplaceIndex (n :: Nat) (y :: k) (xs :: [k]) = ReplaceIndexImpl n xs n y xs@@ -125,6 +125,58 @@ -- | The typelist @xs@ replaced by @ys@ at the indices @ns@. @ns@ and @ys@ must be the same length. @ns@ must be within bounds of @xs@ type ReplacesIndex (ns :: [Nat]) (ys :: [k]) (xs :: [k]) = ReplacesIndexImpl 0 ns ys xs +-- | Returns the typelist up to and excluding @x@. If @x@ doesn't exist, then the original @xs@ is returned.+type family Before (x :: k) (xs :: [k]) :: [k] where+     Before x '[] = '[]+     Before x (x ': xs) = '[]+     Before x (y ': xs) = y ': Before x xs++-- | Returns the typelist up to and including @x@. If @x@ doesn't exist, then the original @xs@ is returned.+type family To (x :: k) (xs :: [k]) :: [k] where+     To x '[] = '[]+     To x (x ': xs) = '[x]+     To x (y ': xs) = y ': To x xs++-- | Returns the typelist after and excluding @x@. If @x@ doesn't exist, then an empty '[] is returned.+type family After (x :: k) (xs :: [k]) :: [k] where+     After x '[] = '[]+     After x (x ': xs) = xs+     After x (y ': xs) = After x xs++-- | Returns the typelist after and including @x@. If @x@ doesn't exist, then an empty '[] is returned.+type family From (x :: k) (xs :: [k]) :: [k] where+     From x '[] = '[]+     From x (x ': xs) = (x ': xs)+     From x (y ': xs) = From x xs++-- | Returns the typelist before (and exluding) index @n@.+-- If @n@ is larger then the @xs@ size, then the original @xs@ is returned.+type family BeforeIndex (n :: Nat) (xs :: [k]) :: [k] where+     BeforeIndex n '[] = '[]+     BeforeIndex 0 xs = '[]+     BeforeIndex n (x ': xs) = x ': BeforeIndex (n - 1) xs++-- | Returns the typelist up to (and including) index @n@.+-- If @n@ is larger then the @xs@ size, then the original @xs@ is returned.+type family ToIndex (n :: Nat) (xs :: [k]) :: [k] where+     ToIndex n '[] = '[]+     ToIndex 0 (x ': xs) = '[x]+     ToIndex n (x ': xs) = x ': ToIndex (n - 1) xs++-- | Returns the typelist after (and exluding) index @n@.+-- If @n@ is larger then the @xs@ size, then an empty '[] is returned.+type family AfterIndex (n :: Nat) (xs :: [k]) :: [k] where+     AfterIndex n '[] = '[]+     AfterIndex 0 (_ ': xs) = xs+     AfterIndex n (x ': xs) = AfterIndex (n - 1) xs++-- | Returns the typelist from (and including) index @n@.+-- If @n@ is larger then the @xs@ size, then an empty '[] is returned.+type family FromIndex (n :: Nat) (xs :: [k]) :: [k] where+     FromIndex n '[] = '[]+     FromIndex 0 xs = xs+     FromIndex n (x ': xs) = FromIndex (n - 1) xs+ -- | Get the typelist without the 'Head' type type family Tail (xs :: [k]) :: [k] where     Tail '[] = TypeError ('Text "Tail error: empty type list")@@ -135,19 +187,22 @@     Head '[] = TypeError ('Text "Head error: empty type list")     Head (x ': xs) = x --- | Get the last type in a typelist type family Last (xs :: [k]) :: k where     Last '[] = TypeError ('Text "Last error: empty type list")     Last (x ': x' ': xs) = Last (x' ': xs)     Last '[x] = x +type family Length (xs :: [k]) :: Nat where+    Length '[] = 0+    Length (x ': xs) = 1 + Length xs+ -- | Ensures two typelists are the same length type SameLength (xs :: [k1]) (ys :: [k2]) = SameLengthImpl xs ys xs ys  -- | Set complement. Returns the set of things in @xs@ that are not in @ys@. type family Complement (xs :: [k]) (ys :: [k]) :: [k] where     Complement xs '[] = xs-    Complement xs (y ': ys)  = Complement (Without y xs) ys+    Complement xs (y ': ys)  = Complement (Remove y xs) ys  -- | Returns a @xs@ appended with @ys@ type family Append (xs :: [k]) (ys :: [k]) :: [k] where

@@ -117,16 +117,16 @@                                             ':<>: 'Text "’")  -- | The typelist @xs@ without the type at Nat @n@. @n@ must be within bounds of @xs@-type family WithoutIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: [k] where-    WithoutIndexImpl i ctx n '[] = TypeError ('Text "WithoutIndex error: Index ‘"+type family RemoveIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (xs :: [k]) :: [k] where+    RemoveIndexImpl i ctx n '[] = TypeError ('Text "RemoveIndex error: Index ‘"                                        ':<>: 'ShowType i                                        ':<>: 'Text "’"                                        ':<>: 'Text " is out of bounds of "                                        ':<>: 'Text "‘"                                        ':<>: 'ShowType ctx                                        ':<>: 'Text "’")-    WithoutIndexImpl i ctx 0 (x ': xs) = xs-    WithoutIndexImpl i ctx n (x ': xs) = x ': WithoutIndexImpl i ctx (n - 1) xs+    RemoveIndexImpl i ctx 0 (x ': xs) = xs+    RemoveIndexImpl i ctx n (x ': xs) = x ': RemoveIndexImpl i ctx (n - 1) xs  -- | The typelist @xs@ without the type at Nat @n@ replaced by @y@. @n@ must be within bounds of @xs@ type family ReplaceIndexImpl (i :: Nat) (ctx :: [k]) (n :: Nat) (y :: k) (xs :: [k]) :: [k] where

@@ -189,7 +189,7 @@ --     x = 'trialL' \@Foo Proxy y -- x `shouldBe` (Right (Tagged 5)) -- @-pickL :: forall l x xs proxy. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> x -> Which xs+pickL :: forall l xs proxy x. (UniqueLabelMember l xs, x ~ KindAtLabel l xs) => proxy l -> x -> Which xs pickL _ = pick_ @x  -- | A variation of 'pick' into a 'Which' of a single type.@@ -213,7 +213,7 @@ -- @ -- 'pickN' (Proxy \@4) (5 :: Int) :: Which '[Bool, Int, Char, Bool, Int, Char] -- @-pickN :: forall n x xs proxy. MemberAt n x xs => proxy n -> x -> Which xs+pickN :: forall n xs proxy x. MemberAt n x xs => proxy n -> x -> Which xs pickN _ = Which (fromInteger (natVal @n Proxy)) . unsafeCoerce  -- | It is 'obvious' what value is inside a 'Which' of one type.@@ -235,13 +235,13 @@ trial     :: forall x xs.        (UniqueMember x xs)-    => Which xs -> Either (Which (Without x xs)) x+    => Which xs -> Either (Which (Remove x xs)) x trial = trial_  trial_     :: forall n x xs.        (KnownNat n, n ~ IndexOf x xs)-    => Which xs -> Either (Which (Without x xs)) x+    => Which xs -> Either (Which (Remove x xs)) x trial_ (Which n v) = let i = fromInteger (natVal @n Proxy)                   in if n == i                      then Right (unsafeCoerce v)@@ -273,14 +273,14 @@ -- x `shouldBe` (Right (Tagged 5)) -- @ trialL-    :: forall l x xs proxy.+    :: forall l xs proxy x.        (UniqueLabelMember l xs, x ~ KindAtLabel l xs)-    => proxy l -> Which xs -> Either (Which (Without x xs)) x+    => proxy l -> Which xs -> Either (Which (Remove x xs)) x trialL _ = trial_ @_ @x  -- | Variation of 'trialL' which returns a Maybe trialL'-    :: forall l x xs proxy.+    :: forall l xs proxy x.        (UniqueLabelMember l xs, x ~ KindAtLabel l xs)     => proxy l -> Which xs -> Maybe x trialL' _ = trial_' @_ @x@@ -309,9 +309,9 @@ -- 'trialN' \@_ \@1 Proxy x \`shouldBe` Left ('pick' \'A') :: 'Which' '[Int, Char, Maybe String] -- @ trialN-    :: forall n x xs proxy.+    :: forall n xs proxy x.        (MemberAt n x xs)-    => proxy n -> Which xs -> Either (Which (WithoutIndex n xs)) x+    => proxy n -> Which xs -> Either (Which (RemoveIndex n xs)) x trialN _ (Which n v) = let i = fromInteger (natVal @n Proxy)                   in if n == i                      then Right (unsafeCoerce v)@@ -321,7 +321,7 @@  -- | Variation of 'trialN' which returns a Maybe trialN'-    :: forall n x xs proxy.+    :: forall n xs proxy x.        (MemberAt n x xs)     => proxy n -> Which xs -> Maybe x trialN' _ (Which n v) = let i = fromInteger (natVal @n Proxy)

@@ -26,6 +26,7 @@  data Foo data Bar+data Dee  spec :: Spec spec = do@@ -322,3 +323,123 @@                 z = ("5" :: String) ./ ("6" :: String) ./ ("7" :: String) ./ ("8" :: String) ./ nil             afmap (CaseFunc' @Num (+10)) x `shouldBe` y             afmap (CaseFunc @Show @String show) x `shouldBe` z++        it "can be split into two 'Many's" $ do+            let x = (5 :: Int) ./ False ./ 'X' ./ Just True ./ Just 'A' ./ nil+                y = (Tagged 5 :: Tagged Foo Int) ./ False ./ Tagged @Dee 'X' ./ Just True ./ Tagged @Bar (Just 'A') ./ nil+                x1a = (5 :: Int) ./ False ./ nil+                x1b = 'X' ./ Just True ./ Just 'A' ./ nil+                x2a = (5 :: Int) ./ False ./ 'X' ./ nil+                x2b = Just True ./ Just 'A' ./ nil+                y1a = (Tagged 5 :: Tagged Foo Int) ./ False ./ nil+                y1b = Tagged @Dee 'X' ./ Just True ./ Tagged @Bar (Just 'A') ./ nil+                y2a = (Tagged 5 :: Tagged Foo Int) ./ False ./ Tagged @Dee 'X' ./ nil+                y2b = Just True ./ Tagged @Bar (Just 'A') ./ nil++            splitBefore (Proxy @Int) x `shouldBe` (nil, x)+            splitBeforeL (Proxy @Foo) y `shouldBe` (nil, y)+            splitBeforeN (Proxy @0) x `shouldBe` (nil, x)+            splitAfter (Proxy @Int) x `shouldBe` let (a, b) = viewf x in (single a, b)+            splitAfterL (Proxy @Foo) y `shouldBe` let (a, b) = viewf y in (single a, b)+            splitAfterN (Proxy @0) x `shouldBe` let (a, b) = viewf x in (single a, b)++            splitBefore (Proxy @(Maybe Char)) x `shouldBe` let (a, b) = viewb x in (a, single b)+            splitBeforeL (Proxy @Bar) y `shouldBe` let (a, b) = viewb y in (a, single b)+            splitBeforeN (Proxy @4) x `shouldBe` let (a, b) = viewb x in (a, single b)+            splitAfter (Proxy @(Maybe Char)) x `shouldBe` (x, nil)+            splitAfterL (Proxy @Bar) y `shouldBe` (y, nil)+            splitAfterN (Proxy @4) x `shouldBe` (x, nil)++            splitBefore (Proxy @(Char)) x `shouldBe` (x1a, x1b)+            splitBeforeL (Proxy @Dee) y `shouldBe` (y1a, y1b)+            splitBeforeN (Proxy @2) x `shouldBe` (x1a, x1b)+            splitAfter(Proxy @(Char)) x `shouldBe` (x2a, x2b)+            splitAfterL (Proxy @Dee) y `shouldBe` (y2a, y2b)+            splitAfterN (Proxy @2) x `shouldBe` (x2a, x2b)++        it "can be 'inset'ted into another 'Many'" $ do+            let x = (5 :: Int) ./ False ./ 'X' ./ Just True ./ Just 'A' ./ nil+                y = (Tagged 5 :: Tagged Foo Int) ./ False ./ Tagged @Dee 'X' ./ Just True ./ Tagged @Bar (Just 'A') ./ nil+                x1a = (5 :: Int) ./ False ./ nil+                x1b = 'X' ./ Just True ./ Just 'A' ./ nil+                x2a = (5 :: Int) ./ False ./ 'X' ./ nil+                x2b = Just True ./ Just 'A' ./ nil+                y1a = (Tagged 5 :: Tagged Foo Int) ./ False ./ nil+                y1b = Tagged @Dee 'X' ./ Just True ./ Tagged @Bar (Just 'A') ./ nil+                y2a = (Tagged 5 :: Tagged Foo Int) ./ False ./ Tagged @Dee 'X' ./ nil+                y2b = Just True ./ Tagged @Bar (Just 'A') ./ nil+                z = True ./ 'Y' ./ nil++            insetBefore (Proxy @Int) z x `shouldBe` z /./ x+            insetBeforeL (Proxy @Foo) z y `shouldBe` z /./ y+            insetBeforeN (Proxy @0) z x `shouldBe` z /./ x+            insetAfter (Proxy @Int) z x `shouldBe` let (a, b) = viewf x in a ./ z /./ b+            insetAfterL (Proxy @Foo) z y `shouldBe` let (a, b) = viewf y in a ./ z /./ b+            insetAfterN (Proxy @0) z x `shouldBe` let (a, b) = viewf x in a ./ z /./ b++            insetBefore (Proxy @(Maybe Char)) z x `shouldBe` let (a, b) = viewb x in a /./ (z \. b)+            insetBeforeL (Proxy @Bar) z y `shouldBe` let (a, b) = viewb y in a /./ (z \. b)+            insetBeforeN (Proxy @4) z x `shouldBe` let (a, b) = viewb x in a /./ (z \. b)+            insetAfter (Proxy @(Maybe Char)) z x `shouldBe` x /./ z+            insetAfterL (Proxy @Bar) z y `shouldBe` y /./ z+            insetAfterN (Proxy @4) z x `shouldBe` x /./ z++            insetBefore (Proxy @(Char)) z x `shouldBe` x1a /./ z /./ x1b+            insetBeforeL (Proxy @Dee) z y `shouldBe` y1a /./ z /./ y1b+            insetBeforeN (Proxy @2) z x `shouldBe` x1a /./ z /./ x1b+            insetAfter(Proxy @(Char)) z x `shouldBe` x2a /./ z /./ x2b+            insetAfterL (Proxy @Dee) z y `shouldBe` y2a /./ z /./ y2b+            insetAfterN (Proxy @2) z x `shouldBe` x2a /./ z /./ x2b++        it "can be 'insert'ted with an item at a specific place" $ do+            let x = (5 :: Int) ./ False ./ 'X' ./ Just True ./ Just 'A' ./ nil+                y = (Tagged 5 :: Tagged Foo Int) ./ False ./ Tagged @Dee 'X' ./ Just True ./ Tagged @Bar (Just 'A') ./ nil+                x1a = (5 :: Int) ./ False ./ nil+                x1b = 'X' ./ Just True ./ Just 'A' ./ nil+                x2a = (5 :: Int) ./ False ./ 'X' ./ nil+                x2b = Just True ./ Just 'A' ./ nil+                y1a = (Tagged 5 :: Tagged Foo Int) ./ False ./ nil+                y1b = Tagged @Dee 'X' ./ Just True ./ Tagged @Bar (Just 'A') ./ nil+                y2a = (Tagged 5 :: Tagged Foo Int) ./ False ./ Tagged @Dee 'X' ./ nil+                y2b = Just True ./ Tagged @Bar (Just 'A') ./ nil+                z = True++            insertBefore (Proxy @Int) z x `shouldBe` z ./ x+            insertBeforeL (Proxy @Foo) z y `shouldBe` z ./ y+            insertBeforeN (Proxy @0) z x `shouldBe` z ./ x+            insertAfter (Proxy @Int) z x `shouldBe` let (a, b) = viewf x in a ./ single z /./ b+            insertAfterL (Proxy @Foo) z y `shouldBe` let (a, b) = viewf y in a ./ single z /./ b+            insertAfterN (Proxy @0) z x `shouldBe` let (a, b) = viewf x in a ./ single z /./ b++            insertBefore (Proxy @(Maybe Char)) z x `shouldBe` let (a, b) = viewb x in a /./ (single z \. b)+            insertBeforeL (Proxy @Bar) z y `shouldBe` let (a, b) = viewb y in a /./ (single z \. b)+            insertBeforeN (Proxy @4) z x `shouldBe` let (a, b) = viewb x in a /./ (single z \. b)+            insertAfter (Proxy @(Maybe Char)) z x `shouldBe` x /./ single z+            insertAfterL (Proxy @Bar) z y `shouldBe` y /./ single z+            insertAfterN (Proxy @4) z x `shouldBe` x /./ single z++            insertBefore (Proxy @(Char)) z x `shouldBe` x1a /./ single z /./ x1b+            insertBeforeL (Proxy @Dee) z y `shouldBe` y1a /./ single z /./ y1b+            insertBeforeN (Proxy @2) z x `shouldBe` x1a /./ single z /./ x1b+            insertAfter(Proxy @(Char)) z x `shouldBe` x2a /./ single z /./ x2b+            insertAfterL (Proxy @Dee) z y `shouldBe` y2a /./ single z /./ y2b+            insertAfterN (Proxy @2) z x `shouldBe` x2a /./ single z /./ x2b+++        it "can 'remove' an item at a specific place" $ do+            let x = (5 :: Int) ./ False ./ 'X' ./ Just True ./ Just 'A' ./ nil+                y = (Tagged 5 :: Tagged Foo Int) ./ False ./ Tagged @Dee 'X' ./ Just True ./ Tagged @Bar (Just 'A') ./ nil+                x' = (5 :: Int) ./ False ./ Just True ./ Just 'A' ./ nil+                y' = (Tagged 5 :: Tagged Foo Int) ./ False ./ Just True ./ Tagged @Bar (Just 'A') ./ nil++            remove (Proxy @Int) x `shouldBe` snd (viewf x)+            removeL (Proxy @Foo) y `shouldBe` snd (viewf y)+            removeN (Proxy @0) x `shouldBe` snd (viewf x)++            remove (Proxy @(Maybe Char)) x `shouldBe` fst (viewb x)+            removeL (Proxy @Bar) y `shouldBe` fst (viewb y)+            removeN (Proxy @4) x `shouldBe` fst (viewb x)++            remove (Proxy @(Char)) x `shouldBe` x'+            removeL (Proxy @Dee) y `shouldBe` y'+            removeN (Proxy @2) x `shouldBe` x'

@@ -96,12 +96,12 @@             obvious d `shouldBe` 5          it "can be 'trialN'led until its final 'obvious' value" $ do-            let a = pickN @2 @_ @'[Char, Bool, Int, Bool, Char, String] Proxy (5 :: Int)-                b = pickN @2 @_ @'[Char, Bool, Int, Char, String] Proxy (5 :: Int)-                c = pickN @2 @_ @'[Char, Bool, Int, String] Proxy (5 :: Int)-                d = pickN @1 @_ @'[Bool, Int, String] Proxy (5 :: Int)-                e = pickN @1 @_ @'[Bool, Int] Proxy (5 :: Int)-                f = pickN @0 @_ @'[Int] Proxy (5 :: Int)+            let a = pickN @2 @'[Char, Bool, Int, Bool, Char, String] Proxy (5 :: Int)+                b = pickN @2 @'[Char, Bool, Int, Char, String] Proxy (5 :: Int)+                c = pickN @2 @'[Char, Bool, Int, String] Proxy (5 :: Int)+                d = pickN @1 @'[Bool, Int, String] Proxy (5 :: Int)+                e = pickN @1 @'[Bool, Int] Proxy (5 :: Int)+                f = pickN @0 @'[Int] Proxy (5 :: Int)             trial @Int a `shouldBe` Right 5             trialN @2 Proxy a `shouldBe` Right 5             trialN @3 Proxy a `shouldBe` Left b@@ -155,7 +155,7 @@             x `shouldBe` pick (5 :: Int)          it "the 'diversify'ed type can't use indistinct fields from the original 'Many'" $ do-            let y = pickN @0 @_ @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int+            let y = pickN @0 @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int                 -- Compile error: Int is a duplicate                 -- x = diversify @[String, String, Char, Bool, Int] y             y `shouldBe` y@@ -183,13 +183,13 @@             x `shouldBe` Left (pick (5 :: Int))          it "the 'reinterpret'ed from type can't indistinct fields'" $ do-            let y = pickN @0 @_ @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int+            let y = pickN @0 @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int                 -- Compile error: Int is a duplicate                 -- x = reinterpret @[String, String, Char, Bool] y             y `shouldBe` y          it "the 'reinterpret' type can't use indistinct fields from the original 'Many'" $ do-            let y = pickN @0 @_ @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int+            let y = pickN @0 @[Int, Char, Int] Proxy (5 :: Int) -- duplicate Int                 -- Compile error: Int is a duplicate                 -- x = reinterpret @[String, String, Char, Bool, Int] y             y `shouldBe` y