3fab77c...main · typeable/refined-containers

git.iko.soy/typeable/refined-containers

13 files changed+1043−70

since splitsnapshots

unifiedsplit

refined-containers.cabal+1−1 src/Data/HashMap/Common/Refined.hs+82−15 src/Data/HashMap/Refined.hs+117−4 src/Data/HashMap/Strict/Refined.hs+116−3 src/Data/HashSet/Refined.hs+1−1 src/Data/IntMap/Common/Refined.hs+119−15 src/Data/IntMap/Refined.hs+122−4 src/Data/IntMap/Strict/Refined.hs+123−3 src/Data/IntSet/Refined.hs+1−1 src/Data/Map/Common/Refined.hs+118−15 src/Data/Map/Refined.hs+121−4 src/Data/Map/Strict/Refined.hs+121−3 src/Data/Set/Refined.hs+1−1

refined-containers.cabal+1−1

@@ -23,7 +23,7 @@ license: MIT

2323license-file: LICENSE

2424author: mniip@typeable.io

2525maintainer: mniip@typeable.io

26−version: 0.1.0.2

26+version: 0.1.2.0

2727build-type: Simple

2828

2929tested-with:

src/Data/HashMap/Common/Refined.hs+82−15

@@ -24,6 +24,7 @@ import Data.Reflection

2424import Data.Traversable.WithIndex

2525import Data.Type.Coercion

2626import Data.Type.Equality ((:~:)(..))

27+import Prelude hiding (zipWith)

2728import Refined

2829import Refined.Unsafe

2930import Unsafe.Coerce

@@ -95,7 +96,7 @@ data SomeHashMap k a where

9596--

9697-- @

9798-- 'withHashMap' ('fromHashMap' ...

98−-- $ \(m :: 'HashMap' s k a) -> doSomethingWith \@s

99+-- $ \\(m :: 'HashMap' s k a) -> doSomethingWith \@s

99100-- @

100101withHashMap

101102 :: forall k a r. SomeHashMap k a -> (forall s. HashMap s k a -> r) -> r

@@ -239,11 +240,25 @@ disjoint (HashMap m1) (HashMap m2)

239240

240241-- | Given two maps proven to have the same keys, for each key apply the

241242-- function to the associated values, to obtain a new map with the same keys.

242−zipWithKey

243+zipWith

243244 :: forall s k a b c. Hashable k

244− => (Key s k -> a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c

245−zipWithKey f (HashMap m1) (HashMap m2) = HashMap

246− $ HashMap.intersectionWithKey (f . unsafeKey) m1 m2

245+ => (a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c

246+zipWith f (HashMap m1) (HashMap m2) = HashMap $ HashMap.intersectionWith f m1 m2

247+

248+-- | Return the union of two maps. For keys that exist in both maps, the value

249+-- is taken from the first map.

250+--

251+-- @

252+-- 'union' = unionWith 'const'

253+-- @

254+union

255+ :: forall s t k a. Hashable k

256+ => HashMap s k a

257+ -> HashMap t k a

258+ -> SomeHashMapWith (UnionProof 'Hashed s t) k a

259+union (HashMap m1) (HashMap m2) = SomeHashMapWith

260+ (HashMap $ HashMap.union m1 m2)

261+ $ UnionProof unsafeSubset unsafeSubsetWith2

247262

248263-- | Remove the keys that appear in the second map from the first map.

249264difference

@@ -255,6 +270,20 @@ difference (HashMap m1) (HashMap m2)

255270 = SomeHashMapWith (HashMap $ HashMap.difference m1 m2)

256271 $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset

257272

273+-- | Return the intersection of two maps, taking values from the first map.

274+--

275+-- @

276+-- 'intersection' = intersectionWith 'const'

277+-- @

278+intersection

279+ :: forall s t k a b. Hashable k

280+ => HashMap s k a

281+ -> HashMap t k b

282+ -> SomeHashMapWith (IntersectionProof 'Hashed s t) k a

283+intersection (HashMap m1) (HashMap m2) = SomeHashMapWith

284+ (HashMap $ HashMap.intersection m1 m2)

285+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

286+

258287-- | Apply a function to all values in a map, together with their corresponding

259288-- keys, that are proven to be in the map. The set of keys remains the same.

260289mapWithKey

@@ -313,6 +342,25 @@ keysSet (HashMap m) = reify (HashMap.keysSet m)

313342toList :: forall s k a. HashMap s k a -> [(Key s k, a)]

314343toList = gcoerceWith (unsafeCastKey @s @k) $ coerce $ HashMap.toList @k @a

315344

345+-- | Retain only the values that satisfy the predicate, returning a potentially

346+-- smaller map.

347+filter

348+ :: forall s k a. (a -> Bool)

349+ -> HashMap s k a

350+ -> SomeHashMapWith (SupersetProof 'Hashed s) k a

351+filter p (HashMap m) = SomeHashMapWith (HashMap $ HashMap.filter p m)

352+ $ SupersetProof unsafeSubset

353+

354+-- | Retain only the keys that satisfy the predicate, returning a potentially

355+-- smaller map.

356+filterKeys

357+ :: forall s k a. (Key s k -> Bool)

358+ -> HashMap s k a

359+ -> SomeHashMapWith (SupersetProof 'Hashed s) k a

360+filterKeys p (HashMap m) = SomeHashMapWith

361+ (HashMap $ HashMap.filterWithKey (\k _ -> p (unsafeKey k)) m)

362+ $ SupersetProof unsafeSubset

363+

316364-- | Retain only the key-value pairs that satisfy the predicate, returning a

317365-- potentially smaller map.

318366filterWithKey

@@ -340,6 +388,25 @@ withoutKeys (HashMap m) = SomeHashMapWith

340388 (HashMap $ HashMap.difference m $ HashSet.toMap $ reflect $ Proxy @t)

341389 $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset

342390

391+-- | Partition a map into two disjoint submaps: those whose key-value pairs

392+-- satisfy the predicate, and those whose don't.

393+partition

394+ :: forall s k a. Hashable k -- TODO: this is only used in the proof

395+ => (a -> Bool)

396+ -> HashMap s k a

397+ -> Some2HashMapWith (PartitionProof 'Hashed s k) k a a

398+partition p (HashMap m) = Some2HashMapWith

399+ (HashMap $ HashMap.filter p m)

400+ (HashMap $ HashMap.filter (not . p) m)

401+ $ PartitionProof

402+ do \k -> case HashMap.lookup (unrefine k) m of

403+ Nothing -> error

404+ "partition: bug: Data.HashMap.Refined has been subverted"

405+ Just x -> if p x

406+ then Left $ unsafeKey $ unrefine k

407+ else Right $ unsafeKey $ unrefine k

408+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

409+

343410-- | Partition a map into two disjoint submaps: those whose key-value pairs

344411-- satisfy the predicate, and those whose don't.

345412partitionWithKey

@@ -374,15 +441,15 @@ castKey

374441castKey = castRefined

375442

376443-- | If keys can be interconverted (e.g. as proved by 'castKey'), then the maps

377−-- can be interconverted too. For example, 'zipWithKey' can be implemented via

378−-- 'Data.HashMap.Refined.intersectionWithKey' by proving that the set of keys

379−-- remains unchanged:

444+-- can be interconverted too. For example, 'Data.HashMap.Refined.zipWithKey' can

445+-- be implemented via 'Data.HashMap.Refined.intersectionWithKey' by proving that

446+-- the set of keys remains unchanged:

380447--

381448-- @

382−-- 'zipWithKey'

449+-- 'Data.HashMap.Refined.zipWithKey'

383450-- :: forall s k a b c. 'Hashable' k

384451-- => ('Key' s k -> a -> b -> c) -> 'HashMap' s k a -> 'HashMap' s k b -> 'HashMap' s k c

385−-- 'zipWithKey' f m1 m2

452+-- 'Data.HashMap.Refined.zipWithKey' f m1 m2

386453-- | v'SomeHashMapWith' @r m proof <- 'Data.HashMap.Refined.intersectionWithKey' (f . 'andLeft') m1 m2

387454-- , v'IntersectionProof' p1 p2 <- proof

388455-- , ( v'Coercion' :: t'Coercion' ('HashMap' r k c) ('HashMap' s k c))

@@ -407,10 +474,10 @@ instance TraversableWithIndex (Key s k) (HashMap s k) where

407474 itraverse = traverseWithKey

408475

409476-- | Similar to the instance for functions -- zip corresponding keys. To use

410−-- '<*>'/'Control.Applicative.liftA2' without 'KnownSet' see 'zipWithKey'.

477+-- '<*>'/'Control.Applicative.liftA2' without 'KnownHashSet' see 'zipWith'.

411478instance (Hashable k, KnownHashSet s k) => Applicative (HashMap s k) where

412479 pure x = fromSet \_ -> x

413− (<*>) = zipWithKey (const id)

480+ (<*>) = zipWith id

414481

415482-- | @'bind' m f@ is a map that for each key @k :: 'Key' s k@, contains the

416483-- value @f (m '!' k) '!' k@, similar to @'>>='@ for functions.

@@ -419,8 +486,8 @@ bind

419486 => HashMap s k a -> (a -> HashMap s k b) -> HashMap s k b

420487bind m f = mapWithKey (\k x -> f x ! k) m

421488

422−-- | Similar to the instance for functions. To use '>>=' without 'KnownSet' see

423−-- 'bind'.

489+-- | Similar to the instance for functions. To use '>>=' without 'KnownHashSet'

490+-- see 'bind'.

424491instance (Hashable k, KnownHashSet s k) => Monad (HashMap s k) where

425492 (>>=) = bind

426493

@@ -433,7 +500,7 @@ instance (Hashable k, KnownHashSet s k)

433500

434501-- | Append the values at the corresponding keys

435502instance (Hashable k, Semigroup a) => Semigroup (HashMap s k a) where

436− (<>) = zipWithKey (const (<>))

503+ (<>) = zipWith (<>)

437504

438505instance (Hashable k, KnownHashSet s k, Monoid a)

439506 => Monoid (HashMap s k a) where

src/Data/HashMap/Refined.hs+117−4

@@ -74,21 +74,29 @@ module Data.HashMap.Refined

7474 , Common.disjoint

7575 , DisjointProof(..)

7676 -- * Combine

77+ , zipWith

7778 , zipWithKey

7879 , bind

80+ , Common.union

81+ , unionWith

7982 , unionWithKey

8083 , UnionProof(..)

8184 , Common.difference

8285 , DifferenceProof(..)

86+ , differenceWith

8387 , differenceWithKey

8488 , PartialDifferenceProof(..)

89+ , Common.intersection

90+ , intersectionWith

8591 , intersectionWithKey

8692 , IntersectionProof(..)

8793 -- * Traversal

94+ , map

8895 , mapWithKey

8996 , traverseWithKey

9097 , mapAccumLWithKey

9198 , mapAccumRWithKey

99+ , mapKeys

92100 , mapKeysWith

93101 , MapProof(..)

94102 , backpermuteKeys

@@ -105,10 +113,15 @@ module Data.HashMap.Refined

105113 -- * Filter

106114 , Common.restrictKeys

107115 , Common.withoutKeys

116+ , Common.filter

117+ , Common.filterKeys

108118 , Common.filterWithKey

119+ , Common.partition

109120 , Common.partitionWithKey

110121 , PartitionProof(..)

122+ , mapMaybe

111123 , mapMaybeWithKey

124+ , mapEither

112125 , mapEitherWithKey

113126 -- * Casts

114127 , Common.castKey

@@ -123,7 +136,7 @@ import Data.Container.Refined.Unsafe

123136import Data.Functor

124137import Data.HashMap.Common.Refined

125138 ( HashMap(..), Key, unsafeCastKey, unsafeKey, SomeHashMapWith(..)

126− , Some2HashMapWith(..), fromSet, (!), zipWithKey, mapWithKey, traverseWithKey

139+ , Some2HashMapWith(..), fromSet, (!), zipWith, mapWithKey, traverseWithKey

127140 , bind

128141 )

129142import qualified Data.HashMap.Common.Refined as Common

@@ -131,7 +144,7 @@ import qualified Data.HashMap.Lazy as HashMap

131144import Data.Traversable

132145import Data.Traversable.WithIndex

133146import Data.Type.Coercion

134−import Prelude hiding (lookup, null)

147+import Prelude hiding (lookup, map, null, zipWith)

135148import Refined

136149import Refined.Unsafe

137150

@@ -330,6 +343,27 @@ updateLookupWithKey f k (HashMap m) =

330343 $ SupersetProof unsafeSubset

331344 )

332345

346+-- | Given two maps proven to have the same keys, for each key apply the

347+-- function to the associated values and the key, to obtain a new map with the

348+-- same keys.

349+zipWithKey

350+ :: forall s k a b c. Hashable k

351+ => (Key s k -> a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c

352+zipWithKey f (HashMap m1) (HashMap m2) = HashMap

353+ $ HashMap.intersectionWithKey (f . unsafeKey) m1 m2

354+

355+-- | Return the union of two maps, with a given combining function for keys that

356+-- exist in both maps simultaneously.

357+unionWith

358+ :: forall s t k a. Hashable k

359+ => (a -> a -> a)

360+ -> HashMap s k a

361+ -> HashMap t k a

362+ -> SomeHashMapWith (UnionProof 'Hashed s t) k a

363+unionWith f (HashMap m1) (HashMap m2) = SomeHashMapWith

364+ (HashMap $ HashMap.unionWith f m1 m2)

365+ $ UnionProof unsafeSubset unsafeSubsetWith2

366+

333367-- | Return the union of two maps, with a given combining function for keys that

334368-- exist in both maps simultaneously.

335369--

@@ -345,8 +379,20 @@ unionWithKey f (HashMap m1) (HashMap m2) = SomeHashMapWith

345379 (HashMap $ HashMap.unionWithKey (f . reallyUnsafeRefine) m1 m2)

346380 $ UnionProof unsafeSubset unsafeSubsetWith2

347381

348−-- | For keys that appear in both maps, the given function decides whether the

349−-- key is removed from the first map.

382+-- | Return the first map, but for keys that appear in both maps, the given

383+-- function decides whether the key is removed.

384+differenceWith

385+ :: forall s t k a b. Hashable k

386+ => (a -> b -> Maybe a)

387+ -> HashMap s k a

388+ -> HashMap t k b

389+ -> SomeHashMapWith (PartialDifferenceProof 'Hashed s t) k a

390+differenceWith f (HashMap m1) (HashMap m2) = SomeHashMapWith

391+ (HashMap $ HashMap.differenceWith f m1 m2)

392+ $ PartialDifferenceProof unsafeSubset unsafeSubset

393+

394+-- | Return the first map, but for keys that appear in both maps, the given

395+-- function decides whether the key is removed.

350396--

351397-- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@

352398-- respectively.

@@ -363,6 +409,17 @@ differenceWithKey f (HashMap m1) (HashMap m2) = SomeHashMapWith

363409 (HashMap.mapWithKey (,) m2))

364410 $ PartialDifferenceProof unsafeSubset unsafeSubset

365411

412+-- | Return the intersection of two maps with the given combining function.

413+intersectionWith

414+ :: forall s t k a b c. Hashable k

415+ => (a -> b -> c)

416+ -> HashMap s k a

417+ -> HashMap t k b

418+ -> SomeHashMapWith (IntersectionProof 'Hashed s t) k c

419+intersectionWith f (HashMap m1) (HashMap m2) = SomeHashMapWith

420+ (HashMap $ HashMap.intersectionWith f m1 m2)

421+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

422+

366423-- | Return the intersection of two maps with the given combining function.

367424--

368425-- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@

@@ -377,6 +434,10 @@ intersectionWithKey f (HashMap m1) (HashMap m2) = SomeHashMapWith

377434 (HashMap $ HashMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)

378435 $ IntersectionProof unsafeSubset unsafeSubsetWith2

379436

437+-- | Apply a function to all values in a map. The set of keys remains the same.

438+map :: forall s k a b. (a -> b) -> HashMap s k a -> HashMap s k b

439+map = coerce $ HashMap.map @a @b @k

440+

380441-- | Thread an accumularing argument through the map in ascending order of

381442-- hashes.

382443mapAccumLWithKey

@@ -395,6 +456,28 @@ mapAccumRWithKey

395456 -> (a, HashMap s k c)

396457mapAccumRWithKey f = imapAccumR (flip f)

397458

459+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results

460+-- into a new map. For keys that were mapped to the same new key, the value is

461+-- picked in an unspecified way.

462+mapKeys

463+ :: forall s k1 k2 a. Hashable k2

464+ => (Key s k1 -> k2)

465+ -> HashMap s k1 a

466+ -> SomeHashMapWith (MapProof 'Hashed s k1 k2) k2 a

467+mapKeys g (HashMap m) = SomeHashMapWith

468+ (HashMap $ HashMap.fromList

469+ $ HashMap.foldrWithKey (\k x xs -> (g $ unsafeKey k, x) : xs) [] m)

470+ $ MapProof (unsafeKey . g) \k2 ->

471+ case HashMap.lookup (unrefine k2) backMap of

472+ Nothing -> error "mapKeys: bug: Data.HashMap.Refined has been subverted"

473+ Just k1 -> k1

474+ where

475+ ~backMap = HashMap.fromList

476+ [ (k2, unsafeKey k1)

477+ | k1 <- HashMap.keys m

478+ , let !k2 = g $ unsafeKey k1

479+ ]

480+

398481-- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the

399482-- results into a new map. For keys that were mapped to the same new key, @c@

400483-- acts as the combining function for corresponding values.

@@ -419,6 +502,15 @@ mapKeysWith f g (HashMap m) = SomeHashMapWith

419502 , let !k2 = g $ unsafeKey k1

420503 ]

421504

505+-- | Apply a function to all values in a map and collect only the 'Just'

506+-- results, returning a potentially smaller map.

507+mapMaybe

508+ :: forall s k a b. (a -> Maybe b)

509+ -> HashMap s k a

510+ -> SomeHashMapWith (SupersetProof 'Hashed s) k b

511+mapMaybe f (HashMap m) = SomeHashMapWith (HashMap $ HashMap.mapMaybe f m)

512+ $ SupersetProof unsafeSubset

513+

422514-- | Apply a function to all values in a map, together with their corresponding

423515-- keys, and collect only the 'Just' results, returning a potentially smaller

424516-- map.

@@ -430,6 +522,27 @@ mapMaybeWithKey f (HashMap m)

430522 = SomeHashMapWith (HashMap $ HashMap.mapMaybeWithKey (f . unsafeKey) m)

431523 $ SupersetProof unsafeSubset

432524

525+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'

526+-- results into separate (disjoint) maps.

527+mapEither

528+ :: forall s k a b c. Hashable k -- TODO: this is only used in the proof

529+ => (a -> Either b c)

530+ -> HashMap s k a

531+ -> Some2HashMapWith (PartitionProof 'Hashed s k) k b c

532+mapEither p (HashMap m)

533+ | m' <- HashMap.map p m

534+ = Some2HashMapWith

535+ (HashMap $ HashMap.mapMaybe (either Just (const Nothing)) m')

536+ (HashMap $ HashMap.mapMaybe (either (const Nothing) Just) m')

537+ $ PartitionProof

538+ do \k -> case HashMap.lookup (unrefine k) m of

539+ Nothing -> error

540+ "mapEither: bug: Data.HashMap.Refined has been subverted"

541+ Just x -> case p x of

542+ Left _ -> Left $ unsafeKey $ unrefine k

543+ Right _ -> Right $ unsafeKey $ unrefine k

544+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

545+

433546-- | Apply a function to all values in a map, together with their corresponding

434547-- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

435548-- maps.

src/Data/HashMap/Strict/Refined.hs+116−3

@@ -74,21 +74,29 @@ module Data.HashMap.Strict.Refined

7474 , Common.disjoint

7575 , DisjointProof(..)

7676 -- * Combine

77+ , zipWith

7778 , zipWithKey

7879 , bind

80+ , Common.union

81+ , unionWith

7982 , unionWithKey

8083 , UnionProof(..)

8184 , Common.difference

8285 , DifferenceProof(..)

86+ , differenceWith

8387 , differenceWithKey

8488 , PartialDifferenceProof(..)

89+ , Common.intersection

90+ , intersectionWith

8591 , intersectionWithKey

8692 , IntersectionProof(..)

8793 -- * Traversal

94+ , map

8895 , mapWithKey

8996 , traverseWithKey

9097 , mapAccumLWithKey

9198 , mapAccumRWithKey

99+ , mapKeys

92100 , mapKeysWith

93101 , MapProof(..)

94102 , backpermuteKeys

@@ -105,10 +113,15 @@ module Data.HashMap.Strict.Refined

105113 -- * Filter

106114 , Common.restrictKeys

107115 , Common.withoutKeys

116+ , Common.filter

117+ , Common.filterKeys

108118 , Common.filterWithKey

119+ , Common.partition

109120 , Common.partitionWithKey

110121 , PartitionProof(..)

122+ , mapMaybe

111123 , mapMaybeWithKey

124+ , mapEither

112125 , mapEitherWithKey

113126 -- * Casts

114127 , Common.castKey

@@ -133,7 +146,7 @@ import Data.Reflection

133146import Data.Traversable

134147import Data.Traversable.WithIndex

135148import Data.Type.Coercion

136−import Prelude hiding (lookup, null)

149+import Prelude hiding (lookup, map, null, zipWith)

137150import Refined

138151import Refined.Unsafe

139152

@@ -340,12 +353,32 @@ updateLookupWithKey f k (HashMap m) =

340353

341354-- | Given two maps proven to have the same keys, for each key apply the

342355-- function to the associated values, to obtain a new map with the same keys.

356+zipWith

357+ :: forall s k a b c. Hashable k

358+ => (a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c

359+zipWith f (HashMap m1) (HashMap m2) = HashMap $ HashMap.intersectionWith f m1 m2

360+

361+-- | Given two maps proven to have the same keys, for each key apply the

362+-- function to the associated values and the key, to obtain a new map with the

363+-- same keys.

343364zipWithKey

344365 :: forall s k a b c. Hashable k

345366 => (Key s k -> a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c

346367zipWithKey = gcoerceWith (unsafeCastKey @s @k) $ coerce

347368 $ HashMap.intersectionWithKey @k @a @b @c

348369

370+-- | Return the union of two maps, with a given combining function for keys that

371+-- exist in both maps simultaneously.

372+unionWith

373+ :: forall s t k a. Hashable k

374+ => (a -> a -> a)

375+ -> HashMap s k a

376+ -> HashMap t k a

377+ -> SomeHashMapWith (UnionProof 'Hashed s t) k a

378+unionWith f (HashMap m1) (HashMap m2) = SomeHashMapWith

379+ (HashMap $ HashMap.unionWith f m1 m2)

380+ $ UnionProof unsafeSubset unsafeSubsetWith2

381+

349382-- | Return the union of two maps, with a given combining function for keys that

350383-- exist in both maps simultaneously.

351384--

@@ -361,8 +394,20 @@ unionWithKey f (HashMap m1) (HashMap m2) = SomeHashMapWith

361394 (HashMap $ HashMap.unionWithKey (f . reallyUnsafeRefine) m1 m2)

362395 $ UnionProof unsafeSubset unsafeSubsetWith2

363396

364−-- | For keys that appear in both maps, the given function decides whether the

365−-- key is removed from the first map.

397+-- | Return the first map, but for keys that appear in both maps, the given

398+-- function decides whether the key is removed.

399+differenceWith

400+ :: forall s t k a b. Hashable k

401+ => (a -> b -> Maybe a)

402+ -> HashMap s k a

403+ -> HashMap t k b

404+ -> SomeHashMapWith (PartialDifferenceProof 'Hashed s t) k a

405+differenceWith f (HashMap m1) (HashMap m2) = SomeHashMapWith

406+ (HashMap $ HashMap.differenceWith f m1 m2)

407+ $ PartialDifferenceProof unsafeSubset unsafeSubset

408+

409+-- | Return the first map, but for keys that appear in both maps, the given

410+-- function decides whether the key is removed.

366411--

367412-- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@

368413-- respectively.

@@ -379,6 +424,17 @@ differenceWithKey f (HashMap m1) (HashMap m2) = SomeHashMapWith

379424 (HashMap.mapWithKey (,) m2))

380425 $ PartialDifferenceProof unsafeSubset unsafeSubset

381426

427+-- | Return the intersection of two maps with the given combining function.

428+intersectionWith

429+ :: forall s t k a b c. Hashable k

430+ => (a -> b -> c)

431+ -> HashMap s k a

432+ -> HashMap t k b

433+ -> SomeHashMapWith (IntersectionProof 'Hashed s t) k c

434+intersectionWith f (HashMap m1) (HashMap m2) = SomeHashMapWith

435+ (HashMap $ HashMap.intersectionWith f m1 m2)

436+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

437+

382438-- | Return the intersection of two maps with the given combining function.

383439--

384440-- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@

@@ -393,6 +449,10 @@ intersectionWithKey f (HashMap m1) (HashMap m2) = SomeHashMapWith

393449 (HashMap $ HashMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)

394450 $ IntersectionProof unsafeSubset unsafeSubsetWith2

395451

452+-- | Apply a function to all values in a map. The set of keys remains the same.

453+map :: forall s k a b. (a -> b) -> HashMap s k a -> HashMap s k b

454+map = coerce $ HashMap.map @a @b @k

455+

396456-- | Apply a function to all values in a map, together with their corresponding

397457-- keys, that are proven to be in the map. The set of keys remains the same.

398458mapWithKey

@@ -427,6 +487,29 @@ mapAccumRWithKey

427487 -> (a, HashMap s k c)

428488mapAccumRWithKey f = imapAccumR (flip f)

429489

490+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results

491+-- into a new map. For keys that were mapped to the same new key, the value is

492+-- picked in an unspecified way.

493+mapKeys

494+ :: forall s k1 k2 a. Hashable k2

495+ => (Key s k1 -> k2)

496+ -> HashMap s k1 a

497+ -> SomeHashMapWith (MapProof 'Hashed s k1 k2) k2 a

498+mapKeys g (HashMap m) = SomeHashMapWith

499+ (HashMap $ HashMap.fromList

500+ $ HashMap.foldrWithKey (\k x xs -> (g $ unsafeKey k, x) : xs) [] m)

501+ $ MapProof (unsafeKey . g) \k2 ->

502+ case HashMap.lookup (unrefine k2) backMap of

503+ Nothing -> error

504+ "mapKeys: bug: Data.HashMap.Strict.Refined has been subverted"

505+ Just k1 -> k1

506+ where

507+ ~backMap = HashMap.fromList

508+ [ (k2, unsafeKey k1)

509+ | k1 <- HashMap.keys m

510+ , let !k2 = g $ unsafeKey k1

511+ ]

512+

430513-- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the

431514-- results into a new map. For keys that were mapped to the same new key, @c@

432515-- acts as the combining function for corresponding values.

@@ -451,6 +534,15 @@ mapKeysWith f g (HashMap m) = SomeHashMapWith

451534 , let !k2 = g $ unsafeKey k1

452535 ]

453536

537+-- | Apply a function to all values in a map and collect only the 'Just'

538+-- results, returning a potentially smaller map.

539+mapMaybe

540+ :: forall s k a b. (a -> Maybe b)

541+ -> HashMap s k a

542+ -> SomeHashMapWith (SupersetProof 'Hashed s) k b

543+mapMaybe f (HashMap m) = SomeHashMapWith (HashMap $ HashMap.mapMaybe f m)

544+ $ SupersetProof unsafeSubset

545+

454546-- | Apply a function to all values in a map, together with their corresponding

455547-- keys, and collect only the 'Just' results, returning a potentially smaller

456548-- map.

@@ -462,6 +554,27 @@ mapMaybeWithKey f (HashMap m)

462554 = SomeHashMapWith (HashMap $ HashMap.mapMaybeWithKey (f . unsafeKey) m)

463555 $ SupersetProof unsafeSubset

464556

557+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'

558+-- results into separate (disjoint) maps.

559+mapEither

560+ :: forall s k a b c. Hashable k -- TODO: this is only used in the proof

561+ => (a -> Either b c)

562+ -> HashMap s k a

563+ -> Some2HashMapWith (PartitionProof 'Hashed s k) k b c

564+mapEither p (HashMap m)

565+ | m' <- HashMap.map p m

566+ = Some2HashMapWith

567+ (HashMap $ HashMap.mapMaybe (either Just (const Nothing)) m')

568+ (HashMap $ HashMap.mapMaybe (either (const Nothing) Just) m')

569+ $ PartitionProof

570+ do \k -> case HashMap.lookup (unrefine k) m of

571+ Nothing -> error

572+ "mapEither: bug: Data.HashMap.Refined has been subverted"

573+ Just x -> case p x of

574+ Left _ -> Left $ unsafeKey $ unrefine k

575+ Right _ -> Right $ unsafeKey $ unrefine k

576+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

577+

465578-- | Apply a function to all values in a map, together with their corresponding

466579-- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

467580-- maps.

src/Data/HashSet/Refined.hs+1−1

@@ -165,7 +165,7 @@ data SomeHashSet a where

165165-- you a way to refer to the set (the parameter @s@), e.g.:

166166--

167167-- @

168−-- 'withHashSet' ('fromHashSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s

168+-- 'withHashSet' ('fromHashSet' ...) $ \\(_ :: 'Proxy' s) -> doSomethingWith \@s

169169-- @

170170withHashSet

171171 :: forall a r. SomeHashSet a

src/Data/IntMap/Common/Refined.hs+119−15

@@ -20,6 +20,7 @@ import Data.Reflection

2020import Data.Traversable.WithIndex

2121import Data.Type.Coercion

2222import Data.Type.Equality ((:~:)(..))

23+import Prelude hiding (zipWith)

2324import Refined

2425import Refined.Unsafe

2526import Unsafe.Coerce

@@ -103,7 +104,8 @@ data SomeIntMap a where

103104-- parameter @s@), e.g.:

104105--

105106-- @

106−-- 'withIntMap' ('fromIntMap' ...) $ \(m :: 'IntMap' s a) -> doSomethingWith \@s

107+-- 'withIntMap' ('fromIntMap' ...)

108+-- $ \\(m :: 'IntMap' s a) -> doSomethingWith \@s

107109-- @

108110withIntMap :: forall a r. SomeIntMap a -> (forall s. IntMap s a -> r) -> r

109111withIntMap (SomeIntMap m) k = k m

@@ -249,23 +251,36 @@ disjoint (IntMap m1) (IntMap m2)

249251

250252-- | Given two maps proven to have the same keys, for each key apply the

251253-- function to the associated values, to obtain a new map with the same keys.

252−zipWithKey

253− :: forall s a b c. (Key s -> a -> b -> c)

254+zipWith

255+ :: forall s a b c. (a -> b -> c)

254256 -> IntMap s a

255257 -> IntMap s b

256258 -> IntMap s c

257−zipWithKey f (IntMap m1) (IntMap m2) = IntMap

258− $ IntMap.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)

259+zipWith f (IntMap m1) (IntMap m2) = IntMap

260+ $ IntMap.mergeWithKey (\_ x y -> Just $ f x y)

259261 (\m -> if IntMap.null m

260262 then IntMap.empty

261− else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")

263+ else error "zipWith: bug: Data.IntMap.Refined has been subverted")

262264 (\m -> if IntMap.null m

263265 then IntMap.empty

264− else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")

266+ else error "zipWith: bug: Data.IntMap.Refined has been subverted")

265267 -- ^ Work around https://github.com/haskell/containers/issues/979

266268 m1

267269 m2

268270

271+-- | Return the union of two maps. For keys that exist in both maps, the value

272+-- is taken from the first map.

273+--

274+-- @

275+-- 'union' = unionWith 'const'

276+-- @

277+union

278+ :: forall s t a. IntMap s a

279+ -> IntMap t a

280+ -> SomeIntMapWith (UnionProof 'Int s t) a

281+union (IntMap m1) (IntMap m2) = SomeIntMapWith (IntMap $ IntMap.union m1 m2)

282+ $ UnionProof unsafeSubset unsafeSubsetWith2

283+

269284-- | Remove the keys that appear in the second map from the first map.

270285difference

271286 :: forall s t a b. IntMap s a

@@ -275,6 +290,19 @@ difference (IntMap m1) (IntMap m2) = SomeIntMapWith

275290 (IntMap $ IntMap.difference m1 m2)

276291 $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset

277292

293+-- | Return the intersection of two maps, taking values from the first map.

294+--

295+-- @

296+-- 'intersection' = intersectionWith 'const'

297+-- @

298+intersection

299+ :: forall s t a b. IntMap s a

300+ -> IntMap t b

301+ -> SomeIntMapWith (IntersectionProof 'Int s t) a

302+intersection (IntMap m1) (IntMap m2) = SomeIntMapWith

303+ (IntMap $ IntMap.intersection m1 m2)

304+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

305+

278306-- | Apply a function to all values in a map, together with their corresponding

279307-- keys, that are proven to be in the map. The set of keys remains the same.

280308mapWithKey :: forall s a b. (Key s -> a -> b) -> IntMap s a -> IntMap s b

@@ -331,6 +359,29 @@ toList = gcoerceWith (unsafeCastKey @s) $ coerce $ IntMap.toAscList @a

331359toDescList :: forall s a. IntMap s a -> [(Key s, a)]

332360toDescList = gcoerceWith (unsafeCastKey @s) $ coerce $ IntMap.toDescList @a

333361

362+-- | Retain only the key-value pairs that satisfy the predicate, returning a

363+-- potentially smaller map.

364+filter

365+ :: forall s a. (a -> Bool)

366+ -> IntMap s a

367+ -> SomeIntMapWith (SupersetProof 'Int s) a

368+filter p (IntMap m) = SomeIntMapWith (IntMap $ IntMap.filter p m)

369+ $ SupersetProof unsafeSubset

370+

371+-- | Retain only the key-value pairs that satisfy the predicate, returning a

372+-- potentially smaller map.

373+filterKeys

374+ :: forall s a. (Key s -> Bool)

375+ -> IntMap s a

376+ -> SomeIntMapWith (SupersetProof 'Int s) a

377+filterKeys p (IntMap m) = SomeIntMapWith

378+#if MIN_VERSION_containers(0, 8, 0)

379+ (IntMap $ IntMap.filterKeys (p . unsafeKey) m)

380+#else

381+ (IntMap $ IntMap.filterWithKey (\k _ -> p (unsafeKey k)) m)

382+#endif

383+ $ SupersetProof unsafeSubset

384+

334385-- | Retain only the key-value pairs that satisfy the predicate, returning a

335386-- potentially smaller map.

336387filterWithKey

@@ -366,6 +417,22 @@ withoutKeys (IntMap m) = SomeIntMapWith

366417#endif

367418 $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset

368419

420+-- | Partition a map into two disjoint submaps: those whose values satisfy the

421+-- predicate, and those whose don't.

422+partition

423+ :: forall s a. (a -> Bool)

424+ -> IntMap s a

425+ -> Some2IntMapWith (PartitionProof 'Int s Int) a a

426+partition p (IntMap m) = case IntMap.partition p m of

427+ (m1, m2) -> Some2IntMapWith (IntMap m1) (IntMap m2) $ PartitionProof

428+ do \k -> case IntMap.lookup (unrefine k) m of

429+ Nothing -> error

430+ "partition: bug: Data.IntMap.Refined has been subverted"

431+ Just x -> if p x

432+ then Left $ unsafeKey $ unrefine k

433+ else Right $ unsafeKey $ unrefine k

434+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

435+

369436-- | Partition a map into two disjoint submaps: those whose key-value pairs

370437-- satisfy the predicate, and those whose don't.

371438partitionWithKey

@@ -383,6 +450,43 @@ partitionWithKey p (IntMap m)

383450 else Right $ unsafeKey $ unrefine k

384451 unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

385452

453+-- | Take the a submap of keys up to a point where the predicate stops holding.

454+--

455+-- If @p@ is antitone ( $\forall x y, x < y \implies p(x) \ge p(y)$ ), then

456+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is

457+-- chosen in an unspecified way.

458+takeWhileAntitone

459+ :: forall s a. (Key s -> Bool)

460+ -> IntMap s a

461+ -> SomeIntMapWith (SupersetProof 'Int s) a

462+takeWhileAntitone p (IntMap m) = SomeIntMapWith

463+#if MIN_VERSION_containers(0, 6, 7)

464+ (IntMap $ IntMap.takeWhileAntitone (p . unsafeKey) m)

465+#else

466+ (IntMap $ IntMap.fromDistinctAscList

467+ $ List.takeWhile (p . unsafeKey . fst) $ IntMap.toAscList m)

468+#endif

469+ $ SupersetProof unsafeSubset

470+

471+-- | Take the a submap of keys starting from a point where the predicate stops

472+-- holding.

473+--

474+-- If @p@ is antitone ( $\forall x y, x < y \implies p(x) \ge p(y)$ ), then

475+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is

476+-- chosen in an unspecified way.

477+dropWhileAntitone

478+ :: forall s a. (Key s -> Bool)

479+ -> IntMap s a

480+ -> SomeIntMapWith (SupersetProof 'Int s) a

481+dropWhileAntitone p (IntMap m) = SomeIntMapWith

482+#if MIN_VERSION_containers(0, 6, 7)

483+ (IntMap $ IntMap.dropWhileAntitone (p . unsafeKey) m)

484+#else

485+ (IntMap $ IntMap.fromDistinctAscList

486+ $ List.dropWhile (p . unsafeKey . fst) $ IntMap.toAscList m)

487+#endif

488+ $ SupersetProof unsafeSubset

489+

386490-- | Divide a map into two disjoint submaps at a point where the predicate on

387491-- the keys stops holding.

388492--

@@ -457,17 +561,17 @@ castKey

457561castKey = castRefined

458562

459563-- | If keys can be interconverted (e.g. as proved by 'castKey'), then the maps

460−-- can be interconverted too. For example, 'zipWithKey' can be implemented via

461−-- 'Data.IntMap.Refined.intersectionWithKey' by proving that the set of keys

462−-- remains unchanged:

564+-- can be interconverted too. For example, 'Data.IntMap.Refined.zipWithKey' can

565+-- be implemented via 'Data.IntMap.Refined.intersectionWithKey' by proving that

566+-- the set of keys remains unchanged:

463567--

464568-- @

465−-- 'zipWithKey'

569+-- 'Data.IntMap.Refined.zipWithKey'

466570-- :: forall s a b c. ('Key' s -> a -> b -> c)

467571-- -> 'IntMap' s a

468572-- -> 'IntMap' s b

469573-- -> 'IntMap' s c

470−-- 'zipWithKey' f m1 m2

574+-- 'Data.IntMap.Refined.zipWithKey' f m1 m2

471575-- | v'SomeIntMapWith' @r m proof <- 'Data.IntMap.Refined.intersectionWithKey' (f . 'andLeft') m1 m2

472576-- , v'IntersectionProof' p1 p2 <- proof

473577-- , ( v'Coercion' :: t'Coercion' ('IntMap' r c) ('IntMap' s c))

@@ -494,10 +598,10 @@ instance TraversableWithIndex (Key s) (IntMap s) where

494598 itraverse = traverseWithKey

495599

496600-- | Similar to the instance for functions -- zip corresponding keys. To use

497−-- '<*>'/'Control.Applicative.liftA2' without 'KnownIntSet' see 'zipWithKey'.

601+-- '<*>'/'Control.Applicative.liftA2' without 'KnownIntSet' see 'zipWith'.

498602instance KnownIntSet s => Applicative (IntMap s) where

499603 pure x = fromSet \_ -> x

500− (<*>) = zipWithKey (const id)

604+ (<*>) = zipWith id

501605

502606-- | @'bind' m f@ is a map that for each key @k :: 'Key' s@, contains the

503607-- value @f (m '!' k) '!' k@, similar to @'>>='@ for functions.

@@ -517,7 +621,7 @@ instance KnownIntSet s => MonadReader (Key s) (IntMap s) where

517621

518622-- | Append the values at the corresponding keys

519623instance Semigroup a => Semigroup (IntMap s a) where

520− (<>) = zipWithKey (const (<>))

624+ (<>) = zipWith (<>)

521625

522626instance (KnownIntSet s, Monoid a) => Monoid (IntMap s a) where

523627 mempty = fromSet \_ -> mempty

src/Data/IntMap/Refined.hs+122−4

@@ -69,21 +69,29 @@ module Data.IntMap.Refined

6969 , Common.disjoint

7070 , DisjointProof(..)

7171 -- * Combine

72+ , zipWith

7273 , zipWithKey

7374 , bind

75+ , Common.union

76+ , unionWith

7477 , unionWithKey

7578 , UnionProof(..)

7679 , Common.difference

7780 , DifferenceProof(..)

81+ , differenceWith

7882 , differenceWithKey

7983 , PartialDifferenceProof(..)

84+ , Common.intersection

85+ , intersectionWith

8086 , intersectionWithKey

8187 , IntersectionProof(..)

8288 -- * Traversal

89+ , map

8390 , mapWithKey

8491 , traverseWithKey

8592 , mapAccumLWithKey

8693 , mapAccumRWithKey

94+ , mapKeys

8795 , mapKeysWith

8896 , MapProof(..)

8997 , backpermuteKeys

@@ -101,12 +109,19 @@ module Data.IntMap.Refined

101109 -- * Filter

102110 , Common.restrictKeys

103111 , Common.withoutKeys

112+ , Common.filter

113+ , Common.filterKeys

104114 , Common.filterWithKey

115+ , Common.partition

105116 , Common.partitionWithKey

106117 , PartitionProof(..)

118+ , Common.takeWhileAntitone

119+ , Common.dropWhileAntitone

107120 , Common.spanAntitone

108121 , PartialPartitionProof(..)

122+ , mapMaybe

109123 , mapMaybeWithKey

124+ , mapEither

110125 , mapEitherWithKey

111126 , Common.splitLookup

112127 , SplitProof(..)

@@ -130,13 +145,13 @@ import Data.Functor

130145import qualified Data.IntMap as IntMap

131146import Data.IntMap.Common.Refined

132147 ( IntMap(..), Key, unsafeCastKey, unsafeKey, SomeIntMapWith(..)

133− , Some2IntMapWith(..), fromSet, (!), zipWithKey, mapWithKey, traverseWithKey

148+ , Some2IntMapWith(..), fromSet, (!), zipWith, mapWithKey, traverseWithKey

134149 , bind

135150 )

136151import qualified Data.IntMap.Common.Refined as Common

137152import Data.Traversable

138153import Data.Type.Coercion

139−import Prelude hiding (lookup, null)

154+import Prelude hiding (lookup, map, null, zipWith)

140155import Refined

141156import Refined.Unsafe

142157

@@ -321,6 +336,37 @@ updateLookupWithKey f k (IntMap m)

321336 (v', !m') -> ((unsafeKey k,) <$> v',)

322337 $ SomeIntMapWith (IntMap m') $ SupersetProof unsafeSubset

323338

339+-- | Given two maps proven to have the same keys, for each key apply the

340+-- function to the associated values and the key, to obtain a new map with the

341+-- same keys.

342+zipWithKey

343+ :: forall s a b c. (Key s -> a -> b -> c)

344+ -> IntMap s a

345+ -> IntMap s b

346+ -> IntMap s c

347+zipWithKey f (IntMap m1) (IntMap m2) = IntMap

348+ $ IntMap.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)

349+ (\m -> if IntMap.null m

350+ then IntMap.empty

351+ else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")

352+ (\m -> if IntMap.null m

353+ then IntMap.empty

354+ else error "zipWithKey: bug: Data.IntMap.Refined has been subverted")

355+ -- ^ Work around https://github.com/haskell/containers/issues/979

356+ m1

357+ m2

358+

359+-- | Return the union of two maps, with a given combining function for keys that

360+-- exist in both maps simultaneously.

361+unionWith

362+ :: forall s t a. (a -> a -> a)

363+ -> IntMap s a

364+ -> IntMap t a

365+ -> SomeIntMapWith (UnionProof 'Int s t) a

366+unionWith f (IntMap m1) (IntMap m2) = SomeIntMapWith

367+ (IntMap $ IntMap.unionWith f m1 m2)

368+ $ UnionProof unsafeSubset unsafeSubsetWith2

369+

324370-- | Return the union of two maps, with a given combining function for keys that

325371-- exist in both maps simultaneously.

326372--

@@ -335,8 +381,19 @@ unionWithKey f (IntMap m1) (IntMap m2)

335381 = SomeIntMapWith (IntMap $ IntMap.unionWithKey (f . reallyUnsafeRefine) m1 m2)

336382 $ UnionProof unsafeSubset unsafeSubsetWith2

337383

338−-- | For keys that appear in both maps, the given function decides whether the

339−-- key is removed from the first map.

384+-- | Return the first map, but for keys that appear in both maps, the given

385+-- function decides whether the key is removed.

386+differenceWith

387+ :: forall s t a b. (a -> b -> Maybe a)

388+ -> IntMap s a

389+ -> IntMap t b

390+ -> SomeIntMapWith (PartialDifferenceProof 'Int s t) a

391+differenceWith f (IntMap m1) (IntMap m2) = SomeIntMapWith

392+ (IntMap $ IntMap.differenceWith f m1 m2)

393+ $ PartialDifferenceProof unsafeSubset unsafeSubset

394+

395+-- | Return the first map, but for keys that appear in both maps, the given

396+-- function decides whether the key is removed.

340397--

341398-- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@

342399-- respectively.

@@ -352,6 +409,16 @@ differenceWithKey f (IntMap m1) (IntMap m2) = SomeIntMapWith

352409 (IntMap $ IntMap.differenceWithKey (f . reallyUnsafeRefine) m1 m2)

353410 $ PartialDifferenceProof unsafeSubset unsafeSubset

354411

412+-- | Return the intersection of two maps with the given combining function.

413+intersectionWith

414+ :: forall s t a b c. (a -> b -> c)

415+ -> IntMap s a

416+ -> IntMap t b

417+ -> SomeIntMapWith (IntersectionProof 'Int s t) c

418+intersectionWith f (IntMap m1) (IntMap m2) = SomeIntMapWith

419+ (IntMap $ IntMap.intersectionWith f m1 m2)

420+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

421+

355422-- | Return the intersection of two maps with the given combining function.

356423--

357424-- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@

@@ -368,6 +435,10 @@ intersectionWithKey f (IntMap m1) (IntMap m2) = SomeIntMapWith

368435 (IntMap $ IntMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)

369436 $ IntersectionProof unsafeSubset unsafeSubsetWith2

370437

438+-- | Apply a function to all values in a map. The set of keys remains the same.

439+map :: forall s a b. (a -> b) -> IntMap s a -> IntMap s b

440+map = coerce $ IntMap.map @a @b

441+

371442-- | Thread an accumularing argument through the map in ascending order of keys.

372443mapAccumLWithKey

373444 :: forall s a b c. (a -> Key s -> b -> (a, c))

@@ -387,6 +458,27 @@ mapAccumRWithKey

387458mapAccumRWithKey = gcoerceWith (unsafeCastKey @s) $ coerce

388459 $ IntMap.mapAccumRWithKey @a @b @c

389460

461+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results

462+-- into a new map. For keys that were mapped to the same new key, the value

463+-- corresponding to the greatest of the original keys is retained.

464+mapKeys

465+ :: forall s a. (Key s -> Int)

466+ -> IntMap s a

467+ -> SomeIntMapWith (MapProof 'Int s Int Int) a

468+mapKeys g (IntMap m)

469+ = SomeIntMapWith (IntMap $ IntMap.mapKeys (g . unsafeKey) m)

470+ $ MapProof (unsafeKey . g) \k2 ->

471+ case IntMap.lookup (unrefine k2) backMap of

472+ Nothing -> error

473+ "mapKeys: bug: Data.IntMap.Refined has been subverted"

474+ Just k1 -> k1

475+ where

476+ ~backMap = IntMap.fromList

477+ [ (k2, unsafeKey k1)

478+ | k1 <- IntMap.keys m

479+ , let !k2 = g $ unsafeKey k1

480+ ]

481+

390482-- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the

391483-- results into a new map. For keys that were mapped to the same new key, @c@

392484-- acts as the combining function for corresponding values.

@@ -409,6 +501,15 @@ mapKeysWith f g (IntMap m)

409501 , let !k2 = g $ unsafeKey k1

410502 ]

411503

504+-- | Apply a function to all values in a map and collect only the 'Just'

505+-- results, returning a potentially smaller map.

506+mapMaybe

507+ :: forall s a b. (a -> Maybe b)

508+ -> IntMap s a

509+ -> SomeIntMapWith (SupersetProof 'Int s) b

510+mapMaybe f (IntMap m) = SomeIntMapWith (IntMap $ IntMap.mapMaybe f m)

511+ $ SupersetProof unsafeSubset

512+

412513-- | Apply a function to all values in a map, together with their corresponding

413514-- keys, and collect only the 'Just' results, returning a potentially smaller

414515-- map.

@@ -420,6 +521,23 @@ mapMaybeWithKey f (IntMap m)

420521 = SomeIntMapWith (IntMap $ IntMap.mapMaybeWithKey (f . unsafeKey) m)

421522 $ SupersetProof unsafeSubset

422523

524+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'

525+-- results into separate (disjoint) maps.

526+mapEither

527+ :: forall s a b c. (a -> Either b c)

528+ -> IntMap s a

529+ -> Some2IntMapWith (PartitionProof 'Int s Int) b c

530+mapEither p (IntMap m)

531+ = case IntMap.mapEither p m of

532+ (m1, m2) -> Some2IntMapWith (IntMap m1) (IntMap m2) $ PartitionProof

533+ do \k -> case IntMap.lookup (unrefine k) m of

534+ Nothing -> error

535+ "mapEither: bug: Data.IntMap.Refined has been subverted"

536+ Just x -> case p x of

537+ Left _ -> Left $ unsafeKey $ unrefine k

538+ Right _ -> Right $ unsafeKey $ unrefine k

539+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

540+

423541-- | Apply a function to all values in a map, together with their corresponding

424542-- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

425543-- maps.

src/Data/IntMap/Strict/Refined.hs+123−3

@@ -69,21 +69,29 @@ module Data.IntMap.Strict.Refined

6969 , Common.disjoint

7070 , DisjointProof(..)

7171 -- * Combine

72+ , zipWith

7273 , zipWithKey

7374 , bind

75+ , Common.union

76+ , unionWith

7477 , unionWithKey

7578 , UnionProof(..)

7679 , Common.difference

7780 , DifferenceProof(..)

81+ , differenceWith

7882 , differenceWithKey

7983 , PartialDifferenceProof(..)

84+ , Common.intersection

85+ , intersectionWith

8086 , intersectionWithKey

8187 , IntersectionProof(..)

8288 -- * Traversal

89+ , map

8390 , mapWithKey

8491 , traverseWithKey

8592 , mapAccumLWithKey

8693 , mapAccumRWithKey

94+ , mapKeys

8795 , mapKeysWith

8896 , MapProof(..)

8997 , backpermuteKeys

@@ -101,12 +109,19 @@ module Data.IntMap.Strict.Refined

101109 -- * Filter

102110 , Common.restrictKeys

103111 , Common.withoutKeys

112+ , Common.filter

113+ , Common.filterKeys

104114 , Common.filterWithKey

115+ , Common.partition

105116 , Common.partitionWithKey

106117 , PartitionProof(..)

118+ , Common.takeWhileAntitone

119+ , Common.dropWhileAntitone

107120 , Common.spanAntitone

108121 , PartialPartitionProof(..)

122+ , mapMaybe

109123 , mapMaybeWithKey

124+ , mapEither

110125 , mapEitherWithKey

111126 , Common.splitLookup

112127 , SplitProof(..)

@@ -137,7 +152,7 @@ import Data.Proxy

137152import Data.Reflection

138153import Data.Traversable

139154import Data.Type.Coercion

140−import Prelude hiding (lookup, null)

155+import Prelude hiding (lookup, map, null, zipWith)

141156import Refined

142157import Refined.Unsafe

143158

@@ -329,6 +344,28 @@ updateLookupWithKey f k (IntMap m)

329344

330345-- | Given two maps proven to have the same keys, for each key apply the

331346-- function to the associated values, to obtain a new map with the same keys.

347+zipWith

348+ :: forall s a b c. (a -> b -> c)

349+ -> IntMap s a

350+ -> IntMap s b

351+ -> IntMap s c

352+zipWith f (IntMap m1) (IntMap m2) = IntMap

353+ $ IntMap.mergeWithKey (\_ x y -> Just $ f x y)

354+ (\m -> if IntMap.null m

355+ then IntMap.empty

356+ else

357+ error "zipWith: bug: Data.IntMap.Strict.Refined has been subverted")

358+ (\m -> if IntMap.null m

359+ then IntMap.empty

360+ else

361+ error "zipWith: bug: Data.IntMap.Strict.Refined has been subverted")

362+ -- ^ Work around https://github.com/haskell/containers/issues/979

363+ m1

364+ m2

365+

366+-- | Given two maps proven to have the same keys, for each key apply the

367+-- function to the associated values and the key, to obtain a new map with the

368+-- same keys.

332369zipWithKey

333370 :: forall s a b c. (Key s -> a -> b -> c)

334371 -> IntMap s a

@@ -348,6 +385,17 @@ zipWithKey f (IntMap m1) (IntMap m2) = IntMap

348385 m1

349386 m2

350387

388+-- | Return the union of two maps, with a given combining function for keys that

389+-- exist in both maps simultaneously.

390+unionWith

391+ :: forall s t a. (a -> a -> a)

392+ -> IntMap s a

393+ -> IntMap t a

394+ -> SomeIntMapWith (UnionProof 'Int s t) a

395+unionWith f (IntMap m1) (IntMap m2) = SomeIntMapWith

396+ (IntMap $ IntMap.unionWith f m1 m2)

397+ $ UnionProof unsafeSubset unsafeSubsetWith2

398+

351399-- | Return the union of two maps, with a given combining function for keys that

352400-- exist in both maps simultaneously.

353401--

@@ -362,8 +410,19 @@ unionWithKey f (IntMap m1) (IntMap m2)

362410 = SomeIntMapWith (IntMap $ IntMap.unionWithKey (f . reallyUnsafeRefine) m1 m2)

363411 $ UnionProof unsafeSubset unsafeSubsetWith2

364412

365−-- | For keys that appear in both maps, the given function decides whether the

366−-- key is removed from the first map.

413+-- | Return the first map, but for keys that appear in both maps, the given

414+-- function decides whether the key is removed.

415+differenceWith

416+ :: forall s t a b. (a -> b -> Maybe a)

417+ -> IntMap s a

418+ -> IntMap t b

419+ -> SomeIntMapWith (PartialDifferenceProof 'Int s t) a

420+differenceWith f (IntMap m1) (IntMap m2) = SomeIntMapWith

421+ (IntMap $ IntMap.differenceWith f m1 m2)

422+ $ PartialDifferenceProof unsafeSubset unsafeSubset

423+

424+-- | Return the first map, but for keys that appear in both maps, the given

425+-- function decides whether the key is removed.

367426--

368427-- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@

369428-- respectively.

@@ -379,6 +438,16 @@ differenceWithKey f (IntMap m1) (IntMap m2) = SomeIntMapWith

379438 (IntMap $ IntMap.differenceWithKey (f . reallyUnsafeRefine) m1 m2)

380439 $ PartialDifferenceProof unsafeSubset unsafeSubset

381440

441+-- | Return the intersection of two maps with the given combining function.

442+intersectionWith

443+ :: forall s t a b c. (a -> b -> c)

444+ -> IntMap s a

445+ -> IntMap t b

446+ -> SomeIntMapWith (IntersectionProof 'Int s t) c

447+intersectionWith f (IntMap m1) (IntMap m2) = SomeIntMapWith

448+ (IntMap $ IntMap.intersectionWith f m1 m2)

449+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

450+

382451-- | Return the intersection of two maps with the given combining function.

383452--

384453-- You can use 'andLeft' and 'andRight' to obtain @'Key' s@ and @'Key' t@

@@ -395,6 +464,10 @@ intersectionWithKey f (IntMap m1) (IntMap m2) = SomeIntMapWith

395464 (IntMap $ IntMap.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)

396465 $ IntersectionProof unsafeSubset unsafeSubsetWith2

397466

467+-- | Apply a function to all values in a map. The set of keys remains the same.

468+map :: forall s a b. (a -> b) -> IntMap s a -> IntMap s b

469+map = coerce $ IntMap.map @a @b

470+

398471-- | Apply a function to all values in a map, together with their corresponding

399472-- keys, that are proven to be in the map. The set of keys remains the same.

400473mapWithKey :: forall s a b. (Key s -> a -> b) -> IntMap s a -> IntMap s b

@@ -428,6 +501,27 @@ mapAccumRWithKey

428501mapAccumRWithKey = gcoerceWith (unsafeCastKey @s) $ coerce

429502 $ IntMap.mapAccumRWithKey @a @b @c

430503

504+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results

505+-- into a new map. For keys that were mapped to the same new key, the value

506+-- corresponding to the greatest of the original keys is retained.

507+mapKeys

508+ :: forall s a. (Key s -> Int)

509+ -> IntMap s a

510+ -> SomeIntMapWith (MapProof 'Int s Int Int) a

511+mapKeys g (IntMap m)

512+ = SomeIntMapWith (IntMap $ IntMap.mapKeys (g . unsafeKey) m)

513+ $ MapProof (unsafeKey . g) \k2 ->

514+ case IntMap.lookup (unrefine k2) backMap of

515+ Nothing -> error

516+ "mapKeys: bug: Data.IntMap.Strict.Refined has been subverted"

517+ Just k1 -> k1

518+ where

519+ ~backMap = IntMap.fromList

520+ [ (k2, unsafeKey k1)

521+ | k1 <- IntMap.keys m

522+ , let !k2 = g $ unsafeKey k1

523+ ]

524+

431525-- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the

432526-- results into a new map. For keys that were mapped to the same new key, @c@

433527-- acts as the combining function for corresponding values.

@@ -450,6 +544,15 @@ mapKeysWith f g (IntMap m)

450544 , let !k2 = g $ unsafeKey k1

451545 ]

452546

547+-- | Apply a function to all values in a map and collect only the 'Just'

548+-- results, returning a potentially smaller map.

549+mapMaybe

550+ :: forall s a b. (a -> Maybe b)

551+ -> IntMap s a

552+ -> SomeIntMapWith (SupersetProof 'Int s) b

553+mapMaybe f (IntMap m) = SomeIntMapWith (IntMap $ IntMap.mapMaybe f m)

554+ $ SupersetProof unsafeSubset

555+

453556-- | Apply a function to all values in a map, together with their corresponding

454557-- keys, and collect only the 'Just' results, returning a potentially smaller

455558-- map.

@@ -461,6 +564,23 @@ mapMaybeWithKey f (IntMap m)

461564 = SomeIntMapWith (IntMap $ IntMap.mapMaybeWithKey (f . unsafeKey) m)

462565 $ SupersetProof unsafeSubset

463566

567+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'

568+-- results into separate (disjoint) maps.

569+mapEither

570+ :: forall s a b c. (a -> Either b c)

571+ -> IntMap s a

572+ -> Some2IntMapWith (PartitionProof 'Int s Int) b c

573+mapEither p (IntMap m)

574+ = case IntMap.mapEither p m of

575+ (m1, m2) -> Some2IntMapWith (IntMap m1) (IntMap m2) $ PartitionProof

576+ do \k -> case IntMap.lookup (unrefine k) m of

577+ Nothing -> error

578+ "mapEither: bug: Data.IntMap.Refined has been subverted"

579+ Just x -> case p x of

580+ Left _ -> Left $ unsafeKey $ unrefine k

581+ Right _ -> Right $ unsafeKey $ unrefine k

582+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

583+

464584-- | Apply a function to all values in a map, together with their corresponding

465585-- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

466586-- maps.

src/Data/IntSet/Refined.hs+1−1

@@ -169,7 +169,7 @@ data SomeIntSet where

169169-- you a way to refer to the set (the parameter @s@), e.g.:

170170--

171171-- @

172−-- 'withIntSet' ('fromIntSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s

172+-- 'withIntSet' ('fromIntSet' ...) $ \\(_ :: 'Proxy' s) -> doSomethingWith \@s

173173-- @

174174withIntSet

175175 :: forall r. SomeIntSet -> (forall s. KnownIntSet s => Proxy s -> r) -> r

src/Data/Map/Common/Refined.hs+118−15

@@ -20,6 +20,7 @@ import qualified Data.Set as Set

2020import Data.Traversable.WithIndex

2121import Data.Type.Coercion

2222import Data.Type.Equality ((:~:)(..))

23+import Prelude hiding (zipWith)

2324import Refined

2425import Refined.Unsafe

2526import Unsafe.Coerce

@@ -109,7 +110,7 @@ data SomeMap k a where

109110-- parameter @s@), e.g.:

110111--

111112-- @

112−-- 'withMap' ('fromMap' ...) $ \(m :: 'Map' s k a) -> doSomethingWith \@s

113+-- 'withMap' ('fromMap' ...) $ \\(m :: 'Map' s k a) -> doSomethingWith \@s

113114-- @

114115withMap :: forall k a r. SomeMap k a -> (forall s. Map s k a -> r) -> r

115116withMap (SomeMap m) k = k m

@@ -259,21 +260,33 @@ disjoint (Map m1) (Map m2)

259260

260261-- | Given two maps proven to have the same keys, for each key apply the

261262-- function to the associated values, to obtain a new map with the same keys.

262−zipWithKey

263+zipWith

263264 :: forall s k a b c. Ord k

264− => (Key s k -> a -> b -> c) -> Map s k a -> Map s k b -> Map s k c

265−zipWithKey f (Map m1) (Map m2) = Map

266− $ Map.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)

265+ => (a -> b -> c) -> Map s k a -> Map s k b -> Map s k c

266+zipWith f (Map m1) (Map m2) = Map

267+ $ Map.mergeWithKey (\_ x y -> Just $ f x y)

267268 (\m -> if Map.null m

268269 then Map.empty

269− else error "zipWithKey: bug: Data.Map.Refined has been subverted")

270+ else error "zipWith: bug: Data.Map.Refined has been subverted")

270271 (\m -> if Map.null m

271272 then Map.empty

272− else error "zipWithKey: bug: Data.Map.Refined has been subverted")

273+ else error "zipWith: bug: Data.Map.Refined has been subverted")

273274 -- ^ Work around https://github.com/haskell/containers/issues/979

274275 m1

275276 m2

276277

278+-- | Return the union of two maps. For keys that exist in both maps, the value

279+-- is taken from the first map.

280+--

281+-- @

282+-- 'union' = unionWith 'const'

283+-- @

284+union

285+ :: forall s t k a. Ord k

286+ => Map s k a -> Map t k a -> SomeMapWith (UnionProof 'Regular s t) k a

287+union (Map m1) (Map m2) = SomeMapWith (Map $ Map.union m1 m2)

288+ $ UnionProof unsafeSubset unsafeSubsetWith2

289+

277290-- | Remove the keys that appear in the second map from the first map.

278291difference

279292 :: forall s t k a b. Ord k

@@ -281,6 +294,20 @@ difference

281294difference (Map m1) (Map m2) = SomeMapWith (Map $ Map.difference m1 m2)

282295 $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset

283296

297+-- | Return the intersection of two maps, taking values from the first map.

298+--

299+-- @

300+-- 'intersection' = intersectionWith 'const'

301+-- @

302+intersection

303+ :: forall s t k a b. Ord k

304+ => Map s k a

305+ -> Map t k b

306+ -> SomeMapWith (IntersectionProof 'Regular s t) k a

307+intersection (Map m1) (Map m2)

308+ = SomeMapWith (Map $ Map.intersection m1 m2)

309+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

310+

284311-- | Apply a function to all values in a map, together with their corresponding

285312-- keys, that are proven to be in the map. The set of keys remains the same.

286313mapWithKey :: forall s k a b. (Key s k -> a -> b) -> Map s k a -> Map s k b

@@ -337,6 +364,29 @@ toList = gcoerceWith (unsafeCastKey @s @k) $ coerce $ Map.toAscList @k @a

337364toDescList :: forall s k a. Map s k a -> [(Key s k, a)]

338365toDescList = gcoerceWith (unsafeCastKey @s @k) $ coerce $ Map.toDescList @k @a

339366

367+-- | Retain only the values that satisfy the predicate, returning a potentially

368+-- smaller map.

369+filter

370+ :: forall s k a. (a -> Bool)

371+ -> Map s k a

372+ -> SomeMapWith (SupersetProof 'Regular s) k a

373+filter p (Map m) = SomeMapWith (Map $ Map.filter p m)

374+ $ SupersetProof unsafeSubset

375+

376+-- | Retain only the keys that satisfy the predicate, returning a potentially

377+-- smaller map.

378+filterKeys

379+ :: forall s k a. (Key s k -> Bool)

380+ -> Map s k a

381+ -> SomeMapWith (SupersetProof 'Regular s) k a

382+filterKeys p (Map m) = SomeMapWith

383+#if MIN_VERSION_containers(0, 8, 0)

384+ (Map $ Map.filterKeys (p . unsafeKey) m)

385+#else

386+ (Map $ Map.filterWithKey (\k _ -> p (unsafeKey k)) m)

387+#endif

388+ $ SupersetProof unsafeSubset

389+

340390-- | Retain only the key-value pairs that satisfy the predicate, returning a

341391-- potentially smaller map.

342392filterWithKey

@@ -371,6 +421,22 @@ withoutKeys (Map m) = SomeMapWith

371421#endif

372422 $ DifferenceProof unsafeSubset (\f g -> unsafeSubsetWith2 f g) unsafeSubset

373423

424+-- | Partition a map into two disjoint submaps: those whose values satisfy the

425+-- predicate, and those whose don't.

426+partition

427+ :: forall s k a. Ord k -- TODO: this is only used in the proof

428+ => (a -> Bool)

429+ -> Map s k a

430+ -> Some2MapWith (PartitionProof 'Regular s k) k a a

431+partition p (Map m) = case Map.partition p m of

432+ (m1, m2) -> Some2MapWith (Map m1) (Map m2) $ PartitionProof

433+ do \k -> case Map.lookup (unrefine k) m of

434+ Nothing -> error "partition: bug: Data.Map.Refined has been subverted"

435+ Just x -> if p x

436+ then Left $ unsafeKey $ unrefine k

437+ else Right $ unsafeKey $ unrefine k

438+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

439+

374440-- | Partition a map into two disjoint submaps: those whose key-value pairs

375441-- satisfy the predicate, and those whose don't.

376442partitionWithKey

@@ -388,6 +454,43 @@ partitionWithKey p (Map m) = case Map.partitionWithKey (p . unsafeKey) m of

388454 else Right $ unsafeKey $ unrefine k

389455 unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

390456

457+-- | Take the a submap of keys up to a point where the predicate stops holding.

458+--

459+-- If @p@ is antitone ( $\forall x y, x < y \implies p(x) \ge p(y)$ ), then

460+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is

461+-- chosen in an unspecified way.

462+takeWhileAntitone

463+ :: forall s k a. (Key s k -> Bool)

464+ -> Map s k a

465+ -> SomeMapWith (SupersetProof 'Regular s) k a

466+takeWhileAntitone p (Map m) = SomeMapWith

467+#if MIN_VERSION_containers(0, 5, 8)

468+ (Map $ Map.takeWhileAntitone (p . unsafeKey) m)

469+#else

470+ (Map $ Map.fromDistinctAscList

471+ $ List.takeWhile (p . unsafeKey . fst) $ Map.toAscList m)

472+#endif

473+ $ SupersetProof unsafeSubset

474+

475+-- | Take the a submap of keys starting from a point where the predicate stops

476+-- holding.

477+--

478+-- If @p@ is antitone ( $\forall x y, x < y \implies p(x) \ge p(y)$ ), then

479+-- this point is uniquely defined. If @p@ is not antitone, a splitting point is

480+-- chosen in an unspecified way.

481+dropWhileAntitone

482+ :: forall s k a. (Key s k -> Bool)

483+ -> Map s k a

484+ -> SomeMapWith (SupersetProof 'Regular s) k a

485+dropWhileAntitone p (Map m) = SomeMapWith

486+#if MIN_VERSION_containers(0, 5, 8)

487+ (Map $ Map.dropWhileAntitone (p . unsafeKey) m)

488+#else

489+ (Map $ Map.fromDistinctAscList

490+ $ List.dropWhile (p . unsafeKey . fst) $ Map.toAscList m)

491+#endif

492+ $ SupersetProof unsafeSubset

493+

391494-- | Divide a map into two disjoint submaps at a point where the predicate on

392495-- the keys stops holding.

393496--

@@ -460,15 +563,15 @@ castKey

460563castKey = castRefined

461564

462565-- | If keys can be interconverted (e.g. as proved by 'castKey'), then the maps

463−-- can be interconverted too. For example, 'zipWithKey' can be implemented via

464−-- 'Data.Map.Refined.intersectionWithKey' by proving that the set of keys

465−-- remains unchanged:

566+-- can be interconverted too. For example, 'Data.Map.Refined.zipWithKey' can be

567+-- implemented via 'Data.Map.Refined.intersectionWithKey' by proving that the

568+-- set of keys remains unchanged:

466569--

467570-- @

468−-- 'zipWithKey'

571+-- 'Data.Map.Refined.zipWithKey'

469572-- :: forall s k a b c. 'Ord' k

470573-- => ('Key' s k -> a -> b -> c) -> 'Map' s k a -> 'Map' s k b -> 'Map' s k c

471−-- 'zipWithKey' f m1 m2

574+-- 'Data.Map.Refined.zipWithKey' f m1 m2

472575-- | v'SomeMapWith' @r m proof <- 'Data.Map.Refined.intersectionWithKey' (f . 'andLeft') m1 m2

473576-- , v'IntersectionProof' p1 p2 <- proof

474577-- , ( v'Coercion' :: t'Coercion' ('Map' r k c) ('Map' s k c))

@@ -493,10 +596,10 @@ instance TraversableWithIndex (Key s k) (Map s k) where

493596 itraverse = traverseWithKey

494597

495598-- | Similar to the instance for functions -- zip corresponding keys. To use

496−-- '<*>'/'Control.Applicative.liftA2' without 'KnownSet' see 'zipWithKey'.

599+-- '<*>'/'Control.Applicative.liftA2' without 'KnownSet' see 'zipWith'.

497600instance (Ord k, KnownSet s k) => Applicative (Map s k) where

498601 pure x = fromSet \_ -> x

499− (<*>) = zipWithKey (const id)

602+ (<*>) = zipWith id

500603

501604-- | @'bind' m f@ is a map that for each key @k :: 'Key' s k@, contains the

502605-- value @f (m '!' k) '!' k@, similar to @'>>='@ for functions.

@@ -516,7 +619,7 @@ instance (Ord k, KnownSet s k) => MonadReader (Key s k) (Map s k) where

516619

517620-- | Append the values at the corresponding keys

518621instance (Ord k, Semigroup a) => Semigroup (Map s k a) where

519− (<>) = zipWithKey (const (<>))

622+ (<>) = zipWith (<>)

520623

521624instance (Ord k, KnownSet s k, Monoid a) => Monoid (Map s k a) where

522625 mempty = fromSet \_ -> mempty

src/Data/Map/Refined.hs+121−4

@@ -78,21 +78,29 @@ module Data.Map.Refined

7878 , Common.disjoint

7979 , DisjointProof(..)

8080 -- * Combine

81+ , zipWith

8182 , zipWithKey

8283 , bind

84+ , Common.union

85+ , unionWith

8386 , unionWithKey

8487 , UnionProof(..)

8588 , Common.difference

8689 , DifferenceProof(..)

90+ , differenceWith

8791 , differenceWithKey

8892 , PartialDifferenceProof(..)

93+ , Common.intersection

94+ , intersectionWith

8995 , intersectionWithKey

9096 , IntersectionProof(..)

9197 -- * Traversal

98+ , map

9299 , mapWithKey

93100 , traverseWithKey

94101 , mapAccumLWithKey

95102 , mapAccumRWithKey

103+ , mapKeys

96104 , mapKeysWith

97105 , MapProof(..)

98106 , backpermuteKeys

@@ -110,12 +118,19 @@ module Data.Map.Refined

110118 -- * Filter

111119 , Common.restrictKeys

112120 , Common.withoutKeys

121+ , Common.filter

122+ , Common.filterKeys

113123 , Common.filterWithKey

124+ , Common.partition

114125 , Common.partitionWithKey

115126 , PartitionProof(..)

127+ , Common.takeWhileAntitone

128+ , Common.dropWhileAntitone

116129 , Common.spanAntitone

117130 , PartialPartitionProof(..)

131+ , mapMaybe

118132 , mapMaybeWithKey

133+ , mapEither

119134 , mapEitherWithKey

120135 , Common.splitLookup

121136 , SplitProof(..)

@@ -139,12 +154,12 @@ import Data.Functor

139154import qualified Data.Map as Map

140155import Data.Map.Common.Refined

141156 ( Map(..), Key, unsafeCastKey, unsafeKey, SomeMapWith(..), Some2MapWith(..)

142− , fromSet, (!), zipWithKey, mapWithKey, traverseWithKey, bind

157+ , fromSet, (!), zipWith, mapWithKey, traverseWithKey, bind

143158 )

144159import qualified Data.Map.Common.Refined as Common

145160import Data.Traversable

146161import Data.Type.Coercion

147−import Prelude hiding (lookup, null)

162+import Prelude hiding (lookup, map, null, zipWith)

148163import Refined

149164import Refined.Unsafe

150165

@@ -332,6 +347,35 @@ updateLookupWithKey f k (Map m)

332347 (v', !m') -> ((unsafeKey k,) <$> v',)

333348 $ SomeMapWith (Map m') $ SupersetProof unsafeSubset

334349

350+-- | Given two maps proven to have the same keys, for each key apply the

351+-- function to the associated values and the key, to obtain a new map with the

352+-- same keys.

353+zipWithKey

354+ :: forall s k a b c. Ord k

355+ => (Key s k -> a -> b -> c) -> Map s k a -> Map s k b -> Map s k c

356+zipWithKey f (Map m1) (Map m2) = Map

357+ $ Map.mergeWithKey (\k x y -> Just $ f (unsafeKey k) x y)

358+ (\m -> if Map.null m

359+ then Map.empty

360+ else error "zipWithKey: bug: Data.Map.Refined has been subverted")

361+ (\m -> if Map.null m

362+ then Map.empty

363+ else error "zipWithKey: bug: Data.Map.Refined has been subverted")

364+ -- ^ Work around https://github.com/haskell/containers/issues/979

365+ m1

366+ m2

367+

368+-- | Return the union of two maps, with a given combining function for keys that

369+-- exist in both maps simultaneously.

370+unionWith

371+ :: forall s t k a. Ord k

372+ => (a -> a -> a)

373+ -> Map s k a

374+ -> Map t k a

375+ -> SomeMapWith (UnionProof 'Regular s t) k a

376+unionWith f (Map m1) (Map m2) = SomeMapWith (Map $ Map.unionWith f m1 m2)

377+ $ UnionProof unsafeSubset unsafeSubsetWith2

378+

335379-- | Return the union of two maps, with a given combining function for keys that

336380-- exist in both maps simultaneously.

337381--

@@ -347,8 +391,20 @@ unionWithKey f (Map m1) (Map m2)

347391 = SomeMapWith (Map $ Map.unionWithKey (f . reallyUnsafeRefine) m1 m2)

348392 $ UnionProof unsafeSubset unsafeSubsetWith2

349393

350−-- | For keys that appear in both maps, the given function decides whether the

351−-- key is removed from the first map.

394+-- | Return the first map, but for keys that appear in both maps, the given

395+-- function decides whether the key is removed.

396+differenceWith

397+ :: forall s t k a b. Ord k

398+ => (a -> b -> Maybe a)

399+ -> Map s k a

400+ -> Map t k b

401+ -> SomeMapWith (PartialDifferenceProof 'Regular s t) k a

402+differenceWith f (Map m1) (Map m2)

403+ = SomeMapWith (Map $ Map.differenceWith f m1 m2)

404+ $ PartialDifferenceProof unsafeSubset unsafeSubset

405+

406+-- | Return the first map, but for keys that appear in both maps, the given

407+-- function decides whether the key is removed.

352408--

353409-- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@

354410-- respectively.

@@ -362,6 +418,17 @@ differenceWithKey f (Map m1) (Map m2)

362418 = SomeMapWith (Map $ Map.differenceWithKey (f . reallyUnsafeRefine) m1 m2)

363419 $ PartialDifferenceProof unsafeSubset unsafeSubset

364420

421+-- | Return the intersection of two maps with the given combining function.

422+intersectionWith

423+ :: forall s t k a b c. Ord k

424+ => (a -> b -> c)

425+ -> Map s k a

426+ -> Map t k b

427+ -> SomeMapWith (IntersectionProof 'Regular s t) k c

428+intersectionWith f (Map m1) (Map m2)

429+ = SomeMapWith (Map $ Map.intersectionWith f m1 m2)

430+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

431+

365432-- | Return the intersection of two maps with the given combining function.

366433--

367434-- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@

@@ -376,6 +443,10 @@ intersectionWithKey f (Map m1) (Map m2)

376443 = SomeMapWith (Map $ Map.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)

377444 $ IntersectionProof unsafeSubset unsafeSubsetWith2

378445

446+-- | Apply a function to all values in a map. The set of keys remains the same.

447+map :: forall s k a b. (a -> b) -> Map s k a -> Map s k b

448+map = coerce $ Map.map @a @b @k

449+

379450-- | Thread an accumularing argument through the map in ascending order of keys.

380451mapAccumLWithKey

381452 :: forall s k a b c. (a -> Key s k -> b -> (a, c))

@@ -395,6 +466,26 @@ mapAccumRWithKey

395466mapAccumRWithKey = gcoerceWith (unsafeCastKey @s @k) $ coerce

396467 $ Map.mapAccumRWithKey @a @k @b @c

397468

469+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results

470+-- into a new map. For keys that were mapped to the same new key, the value

471+-- corresponding to the greatest of the original keys is retained.

472+mapKeys

473+ :: forall s k1 k2 a. Ord k2

474+ => (Key s k1 -> k2)

475+ -> Map s k1 a

476+ -> SomeMapWith (MapProof 'Regular s k1 k2) k2 a

477+mapKeys g (Map m)

478+ = SomeMapWith (Map $ Map.mapKeys (g . unsafeKey) m)

479+ $ MapProof (unsafeKey . g) \k2 -> case Map.lookup (unrefine k2) backMap of

480+ Nothing -> error "mapKeys: bug: Data.Map.Refined has been subverted"

481+ Just k1 -> k1

482+ where

483+ ~backMap = Map.fromList

484+ [ (k2, unsafeKey k1)

485+ | k1 <- Map.keys m

486+ , let !k2 = g $ unsafeKey k1

487+ ]

488+

398489-- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the

399490-- results into a new map. For keys that were mapped to the same new key, @c@

400491-- acts as the combining function for corresponding values.

@@ -416,6 +507,15 @@ mapKeysWith f g (Map m)

416507 , let !k2 = g $ unsafeKey k1

417508 ]

418509

510+-- | Apply a function to all values in a map and collect only the 'Just'

511+-- results, returning a potentially smaller map.

512+mapMaybe

513+ :: forall s k a b. (a -> Maybe b)

514+ -> Map s k a

515+ -> SomeMapWith (SupersetProof 'Regular s) k b

516+mapMaybe f (Map m) = SomeMapWith (Map $ Map.mapMaybe f m)

517+ $ SupersetProof unsafeSubset

518+

419519-- | Apply a function to all values in a map, together with their corresponding

420520-- keys, and collect only the 'Just' results, returning a potentially smaller

421521-- map.

@@ -427,6 +527,23 @@ mapMaybeWithKey f (Map m)

427527 = SomeMapWith (Map $ Map.mapMaybeWithKey (f . unsafeKey) m)

428528 $ SupersetProof unsafeSubset

429529

530+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'

531+-- results into separate (disjoint) maps.

532+mapEither

533+ :: forall s k a b c. Ord k -- TODO: this is only used in the proof

534+ => (a -> Either b c)

535+ -> Map s k a

536+ -> Some2MapWith (PartitionProof 'Regular s k) k b c

537+mapEither p (Map m) = case Map.mapEither p m of

538+ (m1, m2) -> Some2MapWith (Map m1) (Map m2) $ PartitionProof

539+ do \k -> case Map.lookup (unrefine k) m of

540+ Nothing -> error

541+ "mapEither: bug: Data.Map.Refined has been subverted"

542+ Just x -> case p x of

543+ Left _ -> Left $ unsafeKey $ unrefine k

544+ Right _ -> Right $ unsafeKey $ unrefine k

545+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

546+

430547-- | Apply a function to all values in a map, together with their corresponding

431548-- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

432549-- maps.

src/Data/Map/Strict/Refined.hs+121−3

@@ -78,21 +78,29 @@ module Data.Map.Strict.Refined

7878 , Common.disjoint

7979 , DisjointProof(..)

8080 -- * Combine

81+ , zipWith

8182 , zipWithKey

8283 , bind

84+ , Common.union

85+ , unionWith

8386 , unionWithKey

8487 , UnionProof(..)

8588 , Common.difference

8689 , DifferenceProof(..)

90+ , differenceWith

8791 , differenceWithKey

8892 , PartialDifferenceProof(..)

93+ , Common.intersection

94+ , intersectionWith

8995 , intersectionWithKey

9096 , IntersectionProof(..)

9197 -- * Traversal

98+ , map

9299 , mapWithKey

93100 , traverseWithKey

94101 , mapAccumLWithKey

95102 , mapAccumRWithKey

103+ , mapKeys

96104 , mapKeysWith

97105 , MapProof(..)

98106 , backpermuteKeys

@@ -110,12 +118,19 @@ module Data.Map.Strict.Refined

110118 -- * Filter

111119 , Common.restrictKeys

112120 , Common.withoutKeys

121+ , Common.filter

122+ , Common.filterKeys

113123 , Common.filterWithKey

124+ , Common.partition

114125 , Common.partitionWithKey

115126 , PartitionProof(..)

127+ , Common.takeWhileAntitone

128+ , Common.dropWhileAntitone

116129 , Common.spanAntitone

117130 , PartialPartitionProof(..)

131+ , mapMaybe

118132 , mapMaybeWithKey

133+ , mapEither

119134 , mapEitherWithKey

120135 , Common.splitLookup

121136 , SplitProof(..)

@@ -146,7 +161,7 @@ import Data.Proxy

146161import Data.Reflection

147162import Data.Traversable

148163import Data.Type.Coercion

149−import Prelude hiding (lookup, null)

164+import Prelude hiding (lookup, map, null, zipWith)

150165import Refined

151166import Refined.Unsafe

152167

@@ -341,6 +356,24 @@ updateLookupWithKey f k (Map m)

341356

342357-- | Given two maps proven to have the same keys, for each key apply the

343358-- function to the associated values, to obtain a new map with the same keys.

359+zipWith

360+ :: forall s k a b c. Ord k

361+ => (a -> b -> c) -> Map s k a -> Map s k b -> Map s k c

362+zipWith f (Map m1) (Map m2) = Map

363+ $ Map.mergeWithKey (\_ x y -> Just $ f x y)

364+ (\m -> if Map.null m

365+ then Map.empty

366+ else error "zipWith: bug: Data.Map.Strict.Refined has been subverted")

367+ (\m -> if Map.null m

368+ then Map.empty

369+ else error "zipWith: bug: Data.Map.Strict.Refined has been subverted")

370+ -- ^ Work around https://github.com/haskell/containers/issues/979

371+ m1

372+ m2

373+

374+-- | Given two maps proven to have the same keys, for each key apply the

375+-- function to the associated values and the key, to obtain a new map with the

376+-- same keys.

344377zipWithKey

345378 :: forall s k a b c. Ord k

346379 => (Key s k -> a -> b -> c) -> Map s k a -> Map s k b -> Map s k c

@@ -356,6 +389,17 @@ zipWithKey f (Map m1) (Map m2) = Map

356389 m1

357390 m2

358391

392+-- | Return the union of two maps, with a given combining function for keys that

393+-- exist in both maps simultaneously.

394+unionWith

395+ :: forall s t k a. Ord k

396+ => (a -> a -> a)

397+ -> Map s k a

398+ -> Map t k a

399+ -> SomeMapWith (UnionProof 'Regular s t) k a

400+unionWith f (Map m1) (Map m2) = SomeMapWith (Map $ Map.unionWith f m1 m2)

401+ $ UnionProof unsafeSubset unsafeSubsetWith2

402+

359403-- | Return the union of two maps, with a given combining function for keys that

360404-- exist in both maps simultaneously.

361405--

@@ -371,8 +415,20 @@ unionWithKey f (Map m1) (Map m2)

371415 = SomeMapWith (Map $ Map.unionWithKey (f . reallyUnsafeRefine) m1 m2)

372416 $ UnionProof unsafeSubset unsafeSubsetWith2

373417

374−-- | For keys that appear in both maps, the given function decides whether the

375−-- key is removed from the first map.

418+-- | Return the first map, but for keys that appear in both maps, the given

419+-- function decides whether the key is removed.

420+differenceWith

421+ :: forall s t k a b. Ord k

422+ => (a -> b -> Maybe a)

423+ -> Map s k a

424+ -> Map t k b

425+ -> SomeMapWith (PartialDifferenceProof 'Regular s t) k a

426+differenceWith f (Map m1) (Map m2)

427+ = SomeMapWith (Map $ Map.differenceWith f m1 m2)

428+ $ PartialDifferenceProof unsafeSubset unsafeSubset

429+

430+-- | Return the first map, but for keys that appear in both maps, the given

431+-- function decides whether the key is removed.

376432--

377433-- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@

378434-- respectively.

@@ -386,6 +442,17 @@ differenceWithKey f (Map m1) (Map m2)

386442 = SomeMapWith (Map $ Map.differenceWithKey (f . reallyUnsafeRefine) m1 m2)

387443 $ PartialDifferenceProof unsafeSubset unsafeSubset

388444

445+-- | Return the intersection of two maps with the given combining function.

446+intersectionWith

447+ :: forall s t k a b c. Ord k

448+ => (a -> b -> c)

449+ -> Map s k a

450+ -> Map t k b

451+ -> SomeMapWith (IntersectionProof 'Regular s t) k c

452+intersectionWith f (Map m1) (Map m2)

453+ = SomeMapWith (Map $ Map.intersectionWith f m1 m2)

454+ $ IntersectionProof unsafeSubset unsafeSubsetWith2

455+

389456-- | Return the intersection of two maps with the given combining function.

390457--

391458-- You can use 'andLeft' and 'andRight' to obtain @'Key' s k@ and @'Key' t k@

@@ -400,6 +467,10 @@ intersectionWithKey f (Map m1) (Map m2)

400467 = SomeMapWith (Map $ Map.intersectionWithKey (f . reallyUnsafeRefine) m1 m2)

401468 $ IntersectionProof unsafeSubset unsafeSubsetWith2

402469

470+-- | Apply a function to all values in a map. The set of keys remains the same.

471+map :: forall s k a b. (a -> b) -> Map s k a -> Map s k b

472+map = coerce $ Map.map @a @b @k

473+

403474-- | Apply a function to all values in a map, together with their corresponding

404475-- keys, that are proven to be in the map. The set of keys remains the same.

405476mapWithKey :: forall s k a b. (Key s k -> a -> b) -> Map s k a -> Map s k b

@@ -433,6 +504,27 @@ mapAccumRWithKey

433504mapAccumRWithKey = gcoerceWith (unsafeCastKey @s @k) $ coerce

434505 $ Map.mapAccumRWithKey @a @k @b @c

435506

507+-- | @'mapKeys' f m@ applies @f@ to each key of @m@ and collects the results

508+-- into a new map. For keys that were mapped to the same new key, the value

509+-- corresponding to the greatest of the original keys is retained.

510+mapKeys

511+ :: forall s k1 k2 a. Ord k2

512+ => (Key s k1 -> k2)

513+ -> Map s k1 a

514+ -> SomeMapWith (MapProof 'Regular s k1 k2) k2 a

515+mapKeys g (Map m)

516+ = SomeMapWith (Map $ Map.mapKeys (g . unsafeKey) m)

517+ $ MapProof (unsafeKey . g) \k2 -> case Map.lookup (unrefine k2) backMap of

518+ Nothing -> error

519+ "mapKeys: bug: Data.Map.Strict.Refined has been subverted"

520+ Just k1 -> k1

521+ where

522+ ~backMap = Map.fromList

523+ [ (k2, unsafeKey k1)

524+ | k1 <- Map.keys m

525+ , let !k2 = g $ unsafeKey k1

526+ ]

527+

436528-- | @'mapKeysWith' c f m@ applies @f@ to each key of @m@ and collects the

437529-- results into a new map. For keys that were mapped to the same new key, @c@

438530-- acts as the combining function for corresponding values.

@@ -455,6 +547,15 @@ mapKeysWith f g (Map m)

455547 , let !k2 = g $ unsafeKey k1

456548 ]

457549

550+-- | Apply a function to all values in a map and collect only the 'Just'

551+-- results, returning a potentially smaller map.

552+mapMaybe

553+ :: forall s k a b. (a -> Maybe b)

554+ -> Map s k a

555+ -> SomeMapWith (SupersetProof 'Regular s) k b

556+mapMaybe f (Map m) = SomeMapWith (Map $ Map.mapMaybe f m)

557+ $ SupersetProof unsafeSubset

558+

458559-- | Apply a function to all values in a map, together with their corresponding

459560-- keys, and collect only the 'Just' results, returning a potentially smaller

460561-- map.

@@ -466,6 +567,23 @@ mapMaybeWithKey f (Map m)

466567 = SomeMapWith (Map $ Map.mapMaybeWithKey (f . unsafeKey) m)

467568 $ SupersetProof unsafeSubset

468569

570+-- | Apply a function to all values in a map and collect the 'Left' and 'Right'

571+-- results into separate (disjoint) maps.

572+mapEither

573+ :: forall s k a b c. Ord k -- TODO: this is only used in the proof

574+ => (a -> Either b c)

575+ -> Map s k a

576+ -> Some2MapWith (PartitionProof 'Regular s k) k b c

577+mapEither p (Map m) = case Map.mapEither p m of

578+ (m1, m2) -> Some2MapWith (Map m1) (Map m2) $ PartitionProof

579+ do \k -> case Map.lookup (unrefine k) m of

580+ Nothing -> error

581+ "mapEither: bug: Data.Map.Strict.Refined has been subverted"

582+ Just x -> case p x of

583+ Left _ -> Left $ unsafeKey $ unrefine k

584+ Right _ -> Right $ unsafeKey $ unrefine k

585+ unsafeSubset unsafeSubsetWith2 \f g -> unsafeSubsetWith2 f g

586+

469587-- | Apply a function to all values in a map, together with their corresponding

470588-- keys, and collect the 'Left' and 'Right' results into separate (disjoint)

471589-- maps.

src/Data/Set/Refined.hs+1−1

@@ -185,7 +185,7 @@ data SomeSet a where

185185-- you a way to refer to the set (the parameter @s@), e.g.:

186186--

187187-- @

188−-- 'withSet' ('fromSet' ...) $ \(_ :: 'Proxy' s) -> doSomethingWith \@s

188+-- 'withSet' ('fromSet' ...) $ \\(_ :: 'Proxy' s) -> doSomethingWith \@s

189189-- @

190190withSet

191191 :: forall a r. SomeSet a -> (forall s. KnownSet s a => Proxy s -> r) -> r