dependent-enummap 0.1.0.0 → 0.2.0.0

raw patch · 4 files changed

+241/−115 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• dependent-enummap.cabal +4/−4
• src/Data/Dependent/EnumMap/Strict/Internal.hs +219/−105
• test/Main.hs +14/−6

@@ -2,6 +2,10 @@  This package intends to follow the [Package Versioning Policy (PVP)](https://pvp.haskell.org/). +## 0.2.0.0 March 2026++- Simpler but more restrictive Enum1 class definition (one can always set `type Enum1Info f = f`, however, perhaps with a performance cost compared to the old definition).+ ## 0.1.0.0 May 2025  - Initial release.

@@ -1,6 +1,6 @@ cabal-version:   3.0 name:            dependent-enummap-version:         0.1.0.0+version:         0.2.0.0 synopsis:        A generalisation of EnumMap to dependent types description:   A generalisation of EnumMap to dependent key and value types. The key type@@ -9,7 +9,7 @@   operations in coercions accompanied by some runtime type-consistency   assertions. license:         BSD-3-Clause-copyright:       (c) 2025 Tom Smeding, Mikolaj Konarski+copyright:       (c) 2025-2026 Tom Smeding, Mikolaj Konarski author:          Tom Smeding, Mikolaj Konarski maintainer:      Tom Smeding <xhackage@tomsmeding.com> category:        Data, Dependent Types@@ -22,13 +22,13 @@     Data.Dependent.EnumMap.Strict.Internal     -- Data.Dependent.EnumMap.Strict.Unsafe   build-depends:-    base >= 4.15 && < 4.22,+    base >= 4.15 && < 4.23,     containers >= 0.6 && < 0.9,     dependent-sum >= 0.7 && < 0.8,     some >= 1 && < 2,   hs-source-dirs: src   default-language: Haskell2010-  ghc-options: -Wall -Wcompat -Widentities -Wredundant-constraints -Wunused-packages+  ghc-options: -Wall -Wcompat -Widentities -Wredundant-constraints -Wunused-packages -Wpartial-fields -Wredundant-bang-patterns -Woperator-whitespace -Wredundant-strictness-flags   test-suite test

@@ -1,5 +1,6 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-}@@ -7,16 +8,18 @@ {-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-} module Data.Dependent.EnumMap.Strict.Internal where  import Prelude hiding (lookup, map)  import Control.Exception+import Control.Monad ((<$!>)) import Data.Bifunctor (bimap, second) import Data.Coerce import Data.Dependent.Sum-import qualified Data.Foldable as Foldable-import qualified Data.IntMap.Strict as IM+import Data.Foldable qualified as Foldable+import Data.IntMap.Strict qualified as IM import Data.Kind (Type) import Data.Proxy import Data.Some@@ -25,12 +28,13 @@ import Unsafe.Coerce (unsafeCoerce)  type KV :: forall kind. (kind -> Type) -> (kind -> Type) -> Type-data KV k v = forall a. KV !(Enum1Info k) !(v a)+data KV k v = forall a. KV !(Enum1Info k a) !(v a) --- Invariant: the key-value pairs in a DEnumMap are type-consistent. That is to--- say: they have the same type-index. Any other type equalities, like between--- the key argument to 'lookup' and the key-value pairs in the map argument to--- 'lookup', may /not/ hold, and should be type-checked as much as we're able.+-- Invariant ensured by types: the key-value pairs in a DEnumMap+-- are type-consistent. That is to say: they have the same type-index.+-- Any other type equalities, like between the key argument to 'lookup'+-- and the key-value pairs in the map argument to 'lookup',+-- may /not/ hold, and should be runtime-type-checked as much as we're able. newtype DEnumMap k v = DEnumMap (IM.IntMap (KV k v))  instance (Enum1 k, forall a. Show (k a), forall a. Show (v a))@@ -59,21 +63,27 @@ -- -- __Note__: The methods on 'DEnumMap' attempt to check these laws using -- 'assert' assertions (which are by default __disabled__ when optimisations--- are on!), but full consistency cannot always be checked; if you break these--- laws in a sufficiently clever way, the internals of 'DEnumMap' may--- 'unsafeCoerce' unequal things and engage nasal demons, including crashes and--- worse.+-- are on!), but full consistency cannot always be checked;+-- __if you break these laws in a sufficiently clever way, the internals of 'DEnumMap' may 'unsafeCoerce' unequal things and engage nasal demons, including crashes and worse.__+--+-- To enable assertions in optimized builds, e.g., for test runs+-- using optimized code, add the following to the cabal.project.local+-- file of your project:+--+-- > package dependent-enummap+-- >   ghc-options: -fno-ignore-asserts+ class Enum1 f where-  type Enum1Info f-  fromEnum1 :: f a -> (Int, Enum1Info f)-  toEnum1 :: Int -> Enum1Info f -> Some f+  type Enum1Info f :: kind -> Type+  fromEnum1 :: f a -> (Int, Enum1Info f a)+  toEnum1 :: Int -> Enum1Info f a -> f a  dSumToKV :: Enum1 k => DSum k v -> (Int, KV k v) dSumToKV (k :=> v) = let (i, inf) = fromEnum1 k in (i, KV inf v)  -- | Assumes that the input was obtained via 'fromEnum1'. kVToDSum :: Enum1 k => (Int, KV k v) -> DSum k v-kVToDSum (i, KV inf v) = case toEnum1 i inf of Some k -> k :=> coe1 v+kVToDSum (i, KV inf v) = toEnum1 i inf :=> v  -- * Construction @@ -99,18 +109,19 @@ fromListWith f (l :: [DSum k v]) =   DEnumMap (IM.fromListWithKey              (\i (KV inf1 v1) (KV inf2 v2) ->-                typeCheck2 (Proxy @k) i inf1 inf2 $-                  KV inf1 (f v1 (coe1 v2)))+                case typeCheck2 (Proxy @k) i inf1 inf2 of+                  Refl -> KV inf1 (f v1 v2))              (dSumToKV <$> l)) -fromListWithKey :: (Enum1 k, TestEquality k)+fromListWithKey :: forall k v. (Enum1 k, TestEquality k)                 => (forall a. k a -> v a -> v a -> v a)                 -> [DSum k v] -> DEnumMap k v fromListWithKey f l =   DEnumMap (IM.fromListWithKey              (\i (KV inf1 v1) (KV inf2 v2) ->-                case toEnum1 i inf1 of-                  Some k1 -> typeCheck1 k1 i inf2 $ KV inf1 (f k1 (coe1 v1) (coe1 v2)))+                let k1 = toEnum1 @k i inf1+                in case typeCheck1 k1 i inf2 of+                     Refl -> KV inf1 (f k1 v1 v2))              (dSumToKV <$> l))  -- ** From Ascending Lists@@ -124,18 +135,19 @@ fromAscListWith f (l :: [DSum k v]) =   DEnumMap (IM.fromAscListWithKey              (\i (KV inf1 v1) (KV inf2 v2) ->-               typeCheck2 (Proxy @k) i inf1 inf2 $-                 KV inf1 (f v1 (coe1 v2)))+               case typeCheck2 (Proxy @k) i inf1 inf2 of+                 Refl -> KV inf1 (f v1 v2))              (dSumToKV <$> l)) -fromAscListWithKey :: (Enum1 k, TestEquality k)+fromAscListWithKey :: forall k v. (Enum1 k, TestEquality k)                    => (forall a. k a -> v a -> v a -> v a)                    -> [DSum k v] -> DEnumMap k v fromAscListWithKey f l =   DEnumMap (IM.fromAscListWithKey              (\i (KV inf1 v1) (KV inf2 v2) ->-               case toEnum1 i inf1 of-                 Some k1 -> typeCheck1 k1 i inf2 $ KV inf1 (f k1 (coe1 v1) (coe1 v2)))+               let k1 = toEnum1 @k i inf1+               in case typeCheck1 k1 i inf2 of+                    Refl -> KV inf1 (f k1 v1 v2))              (dSumToKV <$> l))  fromDistinctAscList :: Enum1 k => [DSum k v] -> DEnumMap k v@@ -159,7 +171,8 @@ insertWithKey f k v (DEnumMap m) =   let (i, inf) = fromEnum1 k   in DEnumMap (IM.insertWith-                (\_ (KV inf' v2) -> typeCheck1 k i inf' $ KV inf (f k v (coe1 v2)))+                (\_ (KV inf' v2) -> case typeCheck1 k i inf' of+                                      Refl -> KV inf (f k v v2))                 i (KV inf v) m)  insertLookupWithKey :: (Enum1 k, TestEquality k)@@ -169,7 +182,8 @@   let (i, inf) = fromEnum1 k       (!mx, !m') =         IM.insertLookupWithKey-          (\_ _ (KV inf' v2) -> typeCheck1 k i inf' $ KV inf (f k v (coe1 v2)))+          (\_ _ (KV inf' v2) -> case typeCheck1 k i inf' of+                                  Refl -> KV inf (f k v v2))           i (KV inf v) m      -- Note: type checking unnecessary here, because by the BangPatterns,      -- evaluating mx evaluates dmap, and the IntMap is strict, so the lambda@@ -177,7 +191,7 @@      -- Second note: the BangPatterns don't do anything operationally because      -- with the current implementation of IM.insertLookupWithKey, the pair      -- components are already strict.-  in ((\(KV _ v2) -> coe1 v2) <$> mx, DEnumMap m')+  in ((\(KV _ v2) -> coe1 v2) <$!> mx, DEnumMap m')  -- * Deletion\/Update @@ -190,7 +204,9 @@ adjustWithKey :: (Enum1 k, TestEquality k) => (k a -> v a -> v a) -> k a -> DEnumMap k v -> DEnumMap k v adjustWithKey f k (DEnumMap m) =   let (i, _) = fromEnum1 k-  in DEnumMap (IM.adjust (\(KV inf v) -> typeCheck1 k i inf $ KV inf (f k (coe1 v))) i m)+  in DEnumMap (IM.adjust (\(KV inf v) -> case typeCheck1 k i inf of+                                           Refl -> KV inf (f k v))+                         i m)  update :: (Enum1 k, TestEquality k) => (v a -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v update = updateWithKey . const@@ -199,7 +215,9 @@               => (k a -> v a -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v updateWithKey f k (DEnumMap m) =   let (i, _) = fromEnum1 k-  in DEnumMap (IM.update (\(KV inf v) -> typeCheck1 k i inf $ KV inf <$> f k (coe1 v)) i m)+  in DEnumMap (IM.update (\(KV inf v) -> case typeCheck1 k i inf of+                                           Refl -> KV inf <$> f k v)+                         i m)  updateLookupWithKey :: (Enum1 k, TestEquality k)                     => (k a -> v a -> Maybe (v a)) -> k a -> DEnumMap k v -> (Maybe (v a), DEnumMap k v)@@ -207,10 +225,11 @@   let (i, _) = fromEnum1 k       (!mx, !m') =         IM.updateLookupWithKey-          (\_ (KV inf v) -> typeCheck1 k i inf $ KV inf <$> f k (coe1 v))+          (\_ (KV inf v) -> case typeCheck1 k i inf of+                              Refl -> KV inf <$> f k v)           i m      -- Note: type checking unnecessary here for the same reason as insertLookupWithKey-  in ((\(KV _ v2) -> coe1 v2) <$> mx, DEnumMap m')+  in ((\(KV _ v2) -> coe1 v2) <$!> mx, DEnumMap m')  alter :: forall k v a. (Enum1 k, TestEquality k)       => (Maybe (v a) -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v@@ -220,7 +239,8 @@      f' :: Maybe (KV k v) -> Maybe (KV k v)     f' Nothing = KV inf <$> f Nothing-    f' (Just (KV inf' v)) = typeCheck1 k i inf' $ KV inf <$> f (Just (coe1 v))+    f' (Just (KV inf' v)) = case typeCheck1 k i inf' of+                              Refl -> KV inf <$> f (Just v)  alterF :: forall k v a f. (Functor f, Enum1 k, TestEquality k)        => (Maybe (v a) -> f (Maybe (v a))) -> k a -> DEnumMap k v -> f (DEnumMap k v)@@ -230,15 +250,19 @@      f' :: Maybe (KV k v) -> f (Maybe (KV k v))     f' Nothing = fmap (KV inf) <$> f Nothing-    f' (Just (KV inf' v)) = typeCheck1 k i inf' $ fmap (KV inf) <$> f (Just (coe1 v))+    f' (Just (KV inf' v)) = case typeCheck1 k i inf' of+                              Refl -> fmap (KV inf) <$> f (Just v)  -- * Query -- ** Lookup  lookup :: (Enum1 k, TestEquality k) => k a -> DEnumMap k v -> Maybe (v a)+{-# INLINEABLE lookup #-} lookup k (DEnumMap m) =   let (i, _) = fromEnum1 k-  in (\(KV inf v) -> typeCheck1 k i inf $ coe1 v) <$> IM.lookup i m+  in (\(KV inf v) -> case typeCheck1 k i inf of+                       Refl -> v)+     <$!> IM.lookup i m  (!?) :: (Enum1 k, TestEquality k) => DEnumMap k v -> k a -> Maybe (v a) (!?) m k = lookup k m@@ -247,7 +271,8 @@ findWithDefault def k (DEnumMap m) =   let (i, _) = fromEnum1 k   in case IM.findWithDefault (KV undefined def) i m of-       KV inf' v -> typeCheck1 k i inf' $ coe1 v+       KV inf' v -> case typeCheck1 k i inf' of+                      Refl -> v  find :: (Enum1 k, TestEquality k) => k a -> DEnumMap k v -> v a find k = findWithDefault (error ("Data.Dependent.EnumMap.!: key " ++ show (fst (fromEnum1 k)) ++ " is not an element of the map")) k@@ -262,10 +287,10 @@ notMember k m = not $ member k m  lookupLT, lookupGT, lookupLE, lookupGE :: Enum1 k => k a -> DEnumMap k v -> Maybe (DSum k v)-lookupLT k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$> IM.lookupLT i m-lookupGT k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$> IM.lookupGT i m-lookupLE k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$> IM.lookupLE i m-lookupGE k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$> IM.lookupGE i m+lookupLT k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$!> IM.lookupLT i m+lookupGT k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$!> IM.lookupGT i m+lookupLE k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$!> IM.lookupLE i m+lookupGE k (DEnumMap m) = let (i, _) = fromEnum1 k in kVToDSum <$!> IM.lookupGE i m  -- ** Size @@ -287,15 +312,18 @@ unionWith f (DEnumMap m1 :: DEnumMap k v) (DEnumMap m2) = DEnumMap (IM.unionWithKey f' m1 m2)   where     f' :: Int -> KV k v -> KV k v -> KV k v-    f' i (KV inf1 v1) (KV inf2 v2) = typeCheck2 (Proxy @k) i inf1 inf2 $ KV inf1 (f v1 (coe1 v2))+    f' i (KV inf1 v1) (KV inf2 v2) = case typeCheck2 (Proxy @k) i inf1 inf2 of+                                       Refl -> KV inf1 (f v1 v2) -unionWithKey :: (Enum1 k, TestEquality k)+unionWithKey :: forall k v. (Enum1 k, TestEquality k)              => (forall a. k a -> v a -> v a -> v a) -> DEnumMap k v -> DEnumMap k v -> DEnumMap k v unionWithKey f (DEnumMap m1 :: DEnumMap k v) (DEnumMap m2) = DEnumMap (IM.unionWithKey f' m1 m2)   where     f' :: Int -> KV k v -> KV k v -> KV k v-    f' i (KV inf1 v1) (KV inf2 v2) = case toEnum1 i inf1 of-      Some k1 -> typeCheck1 k1 i inf2 $ KV inf1 (f k1 (coe1 v1) (coe1 v2))+    f' i (KV inf1 v1) (KV inf2 v2) =+      let k1 = toEnum1 @k i inf1+      in case typeCheck1 k1 i inf2 of+           Refl -> KV inf1 (f k1 v1 v2)  unions :: (Foldable f, Enum1 k, TestEquality k) => f (DEnumMap k v) -> DEnumMap k v unions = Foldable.foldl' union empty@@ -318,15 +346,18 @@   where     f' :: Int -> KV k v1 -> KV k v2 -> Maybe (KV k v1)     f' i (KV inf1 v1) (KV inf2 v2) =-      typeCheck2 (Proxy @k) i inf1 inf2 $ KV inf1 <$> f (coe1 v1) (coe1 v2)+      case typeCheck2 (Proxy @k) i inf1 inf2 of+        Refl -> KV inf1 <$> f v1 v2  differenceWithKey :: forall k v1 v2. (Enum1 k, TestEquality k)                   => (forall a. k a -> v1 a -> v2 a -> Maybe (v1 a)) -> DEnumMap k v1 -> DEnumMap k v2 -> DEnumMap k v1 differenceWithKey f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.differenceWithKey f' m1 m2)   where     f' :: Int -> KV k v1 -> KV k v2 -> Maybe (KV k v1)-    f' i (KV inf1 v1) (KV inf2 v2) = case toEnum1 i inf1 of-      Some k1 -> typeCheck1 k1 i inf2 $ KV inf1 <$> f k1 (coe1 v1) (coe1 v2)+    f' i (KV inf1 v1) (KV inf2 v2) =+      let k1 = toEnum1 @k i inf1+      in case typeCheck1 k1 i inf2 of+           Refl -> KV inf1 <$> f k1 v1 v2  -- | Because the underlying maps are keyed on integers, it is possible to -- subtract a map from another even if the key types differ. This function@@ -343,8 +374,10 @@ differenceWithKey' f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.differenceWithKey f' m1 m2)   where     f' :: Int -> KV k1 v1 -> KV k2 v2 -> Maybe (KV k1 v1)-    f' i (KV inf1 v1) (KV inf2 v2) = case (toEnum1 i inf1, toEnum1 i inf2) of-      (Some k1, Some k2) -> KV inf1 <$> f k1 (coe1 v1) k2 (coe1 v2)+    f' i (KV inf1 v1) (KV inf2 v2) =+      let k1 = toEnum1 i inf1+          k2 = toEnum1 i inf2+      in KV inf1 <$> f k1 v1 k2 v2  -- ** Intersection @@ -357,15 +390,18 @@   where     f' :: Int -> KV k v1 -> KV k v2 -> KV k v3     f' i (KV inf1 v1) (KV inf2 v2) =-      typeCheck2 (Proxy @k) i inf1 inf2 $ KV inf1 $ f (coe1 v1) (coe1 v2)+      case typeCheck2 (Proxy @k) i inf1 inf2 of+        Refl -> KV inf1 $ f v1 v2  intersectionWithKey :: forall k v1 v2 v3. (Enum1 k, TestEquality k)                     => (forall a. k a -> v1 a -> v2 a -> v3 a) -> DEnumMap k v1 -> DEnumMap k v2 -> DEnumMap k v3 intersectionWithKey f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.intersectionWithKey f' m1 m2)   where     f' :: Int -> KV k v1 -> KV k v2 -> KV k v3-    f' i (KV inf1 v1) (KV inf2 v2) = case toEnum1 i inf1 of-      Some k1 -> typeCheck1 k1 i inf2 $ KV inf1 $ f k1 (coe1 v1) (coe1 v2)+    f' i (KV inf1 v1) (KV inf2 v2) =+      let k1 = toEnum1 @k i inf1+      in case typeCheck1 k1 i inf2 of+           Refl -> KV inf1 $ f k1 v1 v2  -- | Generalises 'intersectionWithKey' in the same way as 'differenceWithKey'' -- generalises 'differenceWithKey'.@@ -375,8 +411,10 @@ intersectionWithKey' f (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.intersectionWithKey f' m1 m2)   where     f' :: Int -> KV k1 v1 -> KV k2 v2 -> KV k1 v3-    f' i (KV inf1 v1) (KV inf2 v2) = case (toEnum1 i inf1, toEnum1 i inf2) of-      (Some k1, Some k2) -> KV inf1 $ f k1 (coe1 v1) k2 (coe1 v2)+    f' i (KV inf1 v1) (KV inf2 v2) =+      let k1 = toEnum1 i inf1+          k2 = toEnum1 i inf2+      in KV inf1 $ f k1 v1 k2 v2  -- ** Disjoint @@ -400,8 +438,10 @@   DEnumMap (IM.mergeWithKey f' (coerce g1) (coerce g2) m1 m2)   where     f' :: Int -> KV k v1 -> KV k v2 -> Maybe (KV k v3)-    f' i (KV inf1 v1) (KV inf2 v2) = case toEnum1 i inf1 of-      Some k1 -> typeCheck1 k1 i inf2 $ KV inf1 <$> f k1 (coe1 v1) (coe1 v2)+    f' i (KV inf1 v1) (KV inf2 v2) =+      let k1 = toEnum1 @k i inf1+      in case typeCheck1 k1 i inf2 of+           Refl -> KV inf1 <$> f k1 v1 v2  -- * Traversal -- ** Map@@ -411,28 +451,43 @@  mapWithKey :: Enum1 k => (forall a. k a -> v1 a -> v2 a) -> DEnumMap k v1 -> DEnumMap k v2 mapWithKey f (DEnumMap m) =-  DEnumMap (IM.mapWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> KV inf $ f k (coe1 v)) m)+  DEnumMap (IM.mapWithKey (\i (KV inf v) ->+                             let k = toEnum1 i inf+                             in KV inf $ f k v)+                          m)  traverseWithKey :: (Applicative f, Enum1 k)                 => (forall a. k a -> v1 a -> f (v2 a)) -> DEnumMap k v1 -> f (DEnumMap k v2) traverseWithKey f (DEnumMap m) =-  DEnumMap <$> IM.traverseWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> KV inf <$> f k (coe1 v)) m+  DEnumMap <$> IM.traverseWithKey (\i (KV inf v) ->+                                     let k = toEnum1 i inf+                                     in KV inf <$> f k v)+                                  m  traverseMaybeWithKey :: (Applicative f, Enum1 k)                      => (forall a. k a -> v1 a -> f (Maybe (v2 a))) -> DEnumMap k v1 -> f (DEnumMap k v2) traverseMaybeWithKey f (DEnumMap m) =-  DEnumMap <$> IM.traverseMaybeWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> fmap (KV inf) <$> f k (coe1 v)) m+  DEnumMap <$> IM.traverseMaybeWithKey (\i (KV inf v) ->+                                          let k = toEnum1 i inf+                                          in fmap (KV inf) <$> f k v)+                                       m  mapAccum :: Enum1 k => (forall a. acc -> v1 a -> (acc, v2 a)) -> acc -> DEnumMap k v1 -> (acc, DEnumMap k v2) mapAccum f = mapAccumWithKey (\x _ y -> f x y)  mapAccumWithKey :: Enum1 k => (forall a. acc -> k a -> v1 a -> (acc, v2 a)) -> acc -> DEnumMap k v1 -> (acc, DEnumMap k v2) mapAccumWithKey f acc0 (DEnumMap m) =-  second DEnumMap $ IM.mapAccumWithKey (\acc i (KV inf v) -> case toEnum1 i inf of Some k -> second (KV inf) $ f acc k (coe1 v)) acc0 m+  second DEnumMap $ IM.mapAccumWithKey (\acc i (KV inf v) ->+                                          let k = toEnum1 i inf+                                          in second (KV inf) $ f acc k v)+                                       acc0 m  mapAccumRWithKey :: Enum1 k => (forall a. acc -> k a -> v1 a -> (acc, v2 a)) -> acc -> DEnumMap k v1 -> (acc, DEnumMap k v2) mapAccumRWithKey f acc0 (DEnumMap m) =-  second DEnumMap $ IM.mapAccumRWithKey (\acc i (KV inf v) -> case toEnum1 i inf of Some k -> second (KV inf) $ f acc k (coe1 v)) acc0 m+  second DEnumMap $ IM.mapAccumRWithKey (\acc i (KV inf v) ->+                                           let k = toEnum1 i inf+                                           in second (KV inf) $ f acc k v)+                                        acc0 m  -- TODO: These are hard. Probably we can't avoid using a fold, analogously as in IntMap. -- mapKeys@@ -449,15 +504,24 @@  foldrWithKey :: Enum1 k => (forall a. k a -> v a -> acc -> acc) -> acc -> DEnumMap k v -> acc foldrWithKey f acc0 (DEnumMap m) =-  IM.foldrWithKey (\i (KV inf v) acc -> case toEnum1 i inf of Some k -> f k (coe1 v) acc) acc0 m+  IM.foldrWithKey (\i (KV inf v) acc ->+                     let k = toEnum1 i inf+                     in f k v acc)+                  acc0 m  foldlWithKey :: Enum1 k => (forall a. acc -> k a -> v a -> acc) -> acc -> DEnumMap k v -> acc foldlWithKey f acc0 (DEnumMap m) =-  IM.foldlWithKey (\acc i (KV inf v) -> case toEnum1 i inf of Some k -> f acc k (coe1 v)) acc0 m+  IM.foldlWithKey (\acc i (KV inf v) ->+                     let k = toEnum1 i inf+                     in f acc k v)+                  acc0 m  foldMapWithKey :: (Monoid m, Enum1 k) => (forall a. k a -> v a -> m) -> DEnumMap k v -> m foldMapWithKey f (DEnumMap m) =-  IM.foldMapWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> f k (coe1 v)) m+  IM.foldMapWithKey (\i (KV inf v) ->+                       let k = toEnum1 i inf+                       in f k v)+                    m  -- ** Strict folds @@ -469,11 +533,17 @@  foldrWithKey' :: Enum1 k => (forall a. k a -> v a -> acc -> acc) -> acc -> DEnumMap k v -> acc foldrWithKey' f acc0 (DEnumMap m) =-  IM.foldrWithKey' (\i (KV inf v) acc -> case toEnum1 i inf of Some k -> f k (coe1 v) acc) acc0 m+  IM.foldrWithKey' (\i (KV inf v) acc ->+                      let k = toEnum1 i inf+                      in f k v acc)+                   acc0 m  foldlWithKey' :: Enum1 k => (forall a. acc -> k a -> v a -> acc) -> acc -> DEnumMap k v -> acc foldlWithKey' f acc0 (DEnumMap m) =-  IM.foldlWithKey' (\acc i (KV inf v) -> case toEnum1 i inf of Some k -> f acc k (coe1 v)) acc0 m+  IM.foldlWithKey' (\acc i (KV inf v) ->+                      let k = toEnum1 i inf+                      in f acc k v)+                   acc0 m  -- * Conversion @@ -481,7 +551,7 @@ elems (DEnumMap m) = (\(KV _ v) -> Some v) <$> IM.elems m  keys :: Enum1 k => DEnumMap k v -> [Some k]-keys (DEnumMap m) = (\(k, KV inf _) -> toEnum1 k inf) <$> IM.assocs m+keys (DEnumMap m) = (\(k, KV inf _) -> Some (toEnum1 k inf)) <$> IM.assocs m  assocs :: Enum1 k => DEnumMap k v -> [DSum k v] assocs (DEnumMap m) = kVToDSum <$> IM.assocs m@@ -509,7 +579,10 @@  filterWithKey :: Enum1 k => (forall a. k a -> v a -> Bool) -> DEnumMap k v -> DEnumMap k v filterWithKey f (DEnumMap m) =-  DEnumMap (IM.filterWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> f k (coe1 v)) m)+  DEnumMap (IM.filterWithKey (\i (KV inf v) ->+                                let k = toEnum1 i inf+                                in f k v)+                             m)  -- TODO: Wait for DEnumSet. -- restrictKeys@@ -521,25 +594,38 @@  partitionWithKey :: Enum1 k => (forall a. k a -> v a -> Bool) -> DEnumMap k v -> (DEnumMap k v, DEnumMap k v) partitionWithKey f (DEnumMap m) =-  bimap DEnumMap DEnumMap (IM.partitionWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> f k (coe1 v)) m)+  bimap DEnumMap DEnumMap (IM.partitionWithKey (\i (KV inf v) ->+                                                  let k = toEnum1 i inf+                                                  in f k v)+                                               m)  -- | \(O(\min(n,W)^2)\). Because of the lack of a @takeWhileAntitoneWithValue@--- operation on 'IntMap', this function performs additional lookups to+-- operation on 'Data.IntMap.Strict.IntMap', this function performs additional lookups to -- reconstruct the full keys to pass to the predicate, resulting in a somewhat--- worse complexity than 'IM.takeWhileAntitone'.+-- worse complexity than 'Data.IntMap.Strict.takeWhileAntitone'. takeWhileAntitone :: Enum1 k => (forall a. k a -> Bool) -> DEnumMap k v -> DEnumMap k v takeWhileAntitone f (DEnumMap m) =-  DEnumMap (IM.takeWhileAntitone (\i -> case m IM.! i of KV inf _ -> case toEnum1 i inf of Some k -> f k) m)+  DEnumMap (IM.takeWhileAntitone (\i -> case m IM.! i of+                                          KV inf _ -> let k = toEnum1 i inf+                                                      in f k)+                                 m)  -- | \(O(\min(n,W)^2)\). See 'takeWhileAntitone'. dropWhileAntitone :: Enum1 k => (forall a. k a -> Bool) -> DEnumMap k v -> DEnumMap k v dropWhileAntitone f (DEnumMap m) =-  DEnumMap (IM.dropWhileAntitone (\i -> case m IM.! i of KV inf _ -> case toEnum1 i inf of Some k -> f k) m)+  DEnumMap (IM.dropWhileAntitone (\i -> case m IM.! i of+                                          KV inf _ -> let k = toEnum1 i inf+                                                      in f k)+                                 m)  -- | \(O(\min(n,W)^2)\). See 'takeWhileAntitone'. spanAntitone :: Enum1 k => (forall a. k a -> Bool) -> DEnumMap k v -> (DEnumMap k v, DEnumMap k v) spanAntitone f (DEnumMap m) =-  bimap DEnumMap DEnumMap (IM.spanAntitone (\i -> case m IM.! i of KV inf _ -> case toEnum1 i inf of Some k -> f k) m)+  bimap DEnumMap DEnumMap+        (IM.spanAntitone (\i -> case m IM.! i of+                                  KV inf _ -> let k = toEnum1 i inf+                                              in f k)+                         m)  mapMaybe :: Enum1 k => (forall a. v1 a -> Maybe (v2 a)) -> DEnumMap k v1 -> DEnumMap k v2 mapMaybe f = mapMaybeWithKey (const f)@@ -547,7 +633,10 @@ mapMaybeWithKey :: Enum1 k                 => (forall a. k a -> v1 a -> Maybe (v2 a)) -> DEnumMap k v1 -> DEnumMap k v2 mapMaybeWithKey f (DEnumMap m) =-  DEnumMap (IM.mapMaybeWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> KV inf <$> f k (coe1 v)) m)+  DEnumMap (IM.mapMaybeWithKey (\i (KV inf v) ->+                                  let k = toEnum1 i inf+                                  in KV inf <$> f k v)+                               m)  mapEither :: Enum1 k           => (forall a. v1 a -> Either (v2 a) (v3 a)) -> DEnumMap k v1 -> (DEnumMap k v2, DEnumMap k v3)@@ -556,16 +645,19 @@ mapEitherWithKey :: Enum1 k                  => (forall a. k a -> v1 a -> Either (v2 a) (v3 a)) -> DEnumMap k v1 -> (DEnumMap k v2, DEnumMap k v3) mapEitherWithKey f (DEnumMap m) =-  bimap DEnumMap DEnumMap (IM.mapEitherWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> bimap (KV inf) (KV inf) $ f k (coe1 v)) m)+  bimap DEnumMap DEnumMap (IM.mapEitherWithKey (\i (KV inf v) ->+                                                  let k = toEnum1 i inf+                                                  in bimap (KV inf) (KV inf) $ f k v)+                                               m)  split :: Enum1 k => k a -> DEnumMap k v -> (DEnumMap k v, DEnumMap k v) split k (DEnumMap m) = bimap DEnumMap DEnumMap (IM.split (fst $ fromEnum1 k) m)  splitLookup :: Enum1 k => k a -> DEnumMap k v -> (DEnumMap k v, Maybe (v a), DEnumMap k v) splitLookup k (DEnumMap m) =-  let (m1, mkv, m2) = IM.splitLookup (fst $ fromEnum1 k) m+  let (!m1, !mkv, !m2) = IM.splitLookup (fst $ fromEnum1 k) m      -- Note: this coe1 is fine because of the invariant on DEnumMap.-  in (DEnumMap m1, (\(KV _ v) -> coe1 v) <$> mkv, DEnumMap m2)+  in (DEnumMap m1, (\(KV _ v) -> coe1 v) <$!> mkv, DEnumMap m2)  splitRoot :: DEnumMap k v -> [DEnumMap k v] splitRoot (DEnumMap m) = DEnumMap <$> IM.splitRoot m@@ -590,10 +682,10 @@ -- * Min\/Max  lookupMin :: Enum1 k => DEnumMap k v -> Maybe (DSum k v)-lookupMin (DEnumMap m) = kVToDSum <$> IM.lookupMin m+lookupMin (DEnumMap m) = kVToDSum <$!> IM.lookupMin m  lookupMax :: Enum1 k => DEnumMap k v -> Maybe (DSum k v)-lookupMax (DEnumMap m) = kVToDSum <$> IM.lookupMax m+lookupMax (DEnumMap m) = kVToDSum <$!> IM.lookupMax m  findMin :: Enum1 k => DEnumMap k v -> DSum k v findMin (DEnumMap m) = kVToDSum $ IM.findMin m@@ -608,36 +700,42 @@ deleteMax (DEnumMap m) = DEnumMap $ IM.deleteMax m  deleteFindMin :: Enum1 k => DEnumMap k v -> (DSum k v, DEnumMap k v)-deleteFindMin (DEnumMap m) = bimap kVToDSum DEnumMap $ IM.deleteFindMin m+deleteFindMin (DEnumMap m) = bimap' kVToDSum DEnumMap $ IM.deleteFindMin m  deleteFindMax :: Enum1 k => DEnumMap k v -> (DSum k v, DEnumMap k v)-deleteFindMax (DEnumMap m) = bimap kVToDSum DEnumMap $ IM.deleteFindMax m+deleteFindMax (DEnumMap m) = bimap' kVToDSum DEnumMap $ IM.deleteFindMax m  updateMin :: Enum1 k => (forall a. v a -> Maybe (v a)) -> DEnumMap k v -> DEnumMap k v updateMin f = updateMinWithKey (const f)  updateMinWithKey :: Enum1 k => (forall a. k a -> v a -> Maybe (v a)) -> DEnumMap k v -> DEnumMap k v updateMinWithKey f (DEnumMap m) =-  DEnumMap (IM.updateMinWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> KV inf <$> f k (coe1 v)) m)+  DEnumMap (IM.updateMinWithKey (\i (KV inf v) ->+                                   let k = toEnum1 i inf+                                   in KV inf <$> f k v)+                                m)  updateMax :: Enum1 k => (forall a. v a -> Maybe (v a)) -> DEnumMap k v -> DEnumMap k v updateMax f = updateMaxWithKey (const f)  updateMaxWithKey :: Enum1 k => (forall a. k a -> v a -> Maybe (v a)) -> DEnumMap k v -> DEnumMap k v updateMaxWithKey f (DEnumMap m) =-  DEnumMap (IM.updateMaxWithKey (\i (KV inf v) -> case toEnum1 i inf of Some k -> KV inf <$> f k (coe1 v)) m)+  DEnumMap (IM.updateMaxWithKey (\i (KV inf v) ->+                                   let k = toEnum1 i inf+                                   in KV inf <$> f k v)+                                m)  minView :: DEnumMap k v -> Maybe (v a, DEnumMap k v)-minView (DEnumMap m) = bimap (\(KV _ v) -> coe1 v) DEnumMap <$> IM.minView m+minView (DEnumMap m) = bimap' (\(KV _ v) -> coe1 v) DEnumMap <$!> IM.minView m  maxView :: DEnumMap k v -> Maybe (v a, DEnumMap k v)-maxView (DEnumMap m) = bimap (\(KV _ v) -> coe1 v) DEnumMap <$> IM.maxView m+maxView (DEnumMap m) = bimap' (\(KV _ v) -> coe1 v) DEnumMap <$!> IM.maxView m  minViewWithKey :: Enum1 k => DEnumMap k v -> Maybe (DSum k v, DEnumMap k v)-minViewWithKey (DEnumMap m) = bimap kVToDSum DEnumMap <$> IM.minViewWithKey m+minViewWithKey (DEnumMap m) = bimap' kVToDSum DEnumMap <$!> IM.minViewWithKey m  maxViewWithKey :: Enum1 k => DEnumMap k v -> Maybe (DSum k v, DEnumMap k v)-maxViewWithKey (DEnumMap m) = bimap kVToDSum DEnumMap <$> IM.maxViewWithKey m+maxViewWithKey (DEnumMap m) = bimap' kVToDSum DEnumMap <$!> IM.maxViewWithKey m   -- * Helpers@@ -645,21 +743,37 @@ coe1 :: v a -> v b coe1 = unsafeCoerce -typeCheck1 :: (Enum1 k, TestEquality k)-           => k a -> Int -> Enum1Info k -> r -> r-typeCheck1 k1 i inf2 x =-  assert (case toEnum1 i inf2 of { Some k2 ->-          case testEquality k1 k2 of-            Just Refl -> True-            Nothing -> False })-         x+typeCheck1 :: forall k a b. (Enum1 k, TestEquality k)+           => k a -> Int -> Enum1Info k b -> k a :~: k b+typeCheck1 k1 i inf2 =+  let ret :: k a :~: k b+      ret = unsafeCoerce Refl+  in assert (let k2 = toEnum1 i inf2+             in case testEquality k1 k2 of+                  Just r -> justifies r ret True+                  Nothing -> False)+            ret+  where+    justifies :: a :~: b -> k a :~: k b -> r -> r+    justifies Refl _ x = x -typeCheck2 :: forall k proxy r. (Enum1 k, TestEquality k)-           => proxy k -> Int -> Enum1Info k -> Enum1Info k -> r -> r-typeCheck2 _ i inf1 inf2 x =-  assert (case toEnum1 @k i inf1 of { Some k1 ->-          case toEnum1 i inf2 of { Some k2 ->-          case testEquality k1 k2 of-            Just Refl -> True-            Nothing -> False }})-         x+typeCheck2 :: forall k proxy a b. (Enum1 k, TestEquality k)+           => proxy k -> Int -> Enum1Info k a -> Enum1Info k b -> k a :~: k b+typeCheck2 _ i inf1 inf2 =+  let ret :: k a :~: k b+      ret = unsafeCoerce Refl+  in assert (let k1 = toEnum1 @k i inf1+                 k2 = toEnum1 i inf2+             in case testEquality k1 k2 of+                  Just r -> justifies r ret True+                  Nothing -> False)+            ret+  where+    justifies :: a :~: b -> k a :~: k b -> r -> r+    justifies Refl _ x = x++bimap' :: (a -> b) -> (c -> d) -> (a, c) -> (b, d)+bimap' f g (a, c) =+  let !b = f a+      !d = g c+  in (b, d)

@@ -1,15 +1,16 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} module Main where -import qualified Data.Dependent.EnumMap.Strict as DE+import Data.Dependent.EnumMap.Strict qualified as DE+import Data.Dependent.EnumMap.Strict.Internal (coe1) import Data.Dependent.Sum-import Data.Some-+import Data.Functor.Const  data Tag = A | B | C   deriving (Show)@@ -21,9 +22,16 @@ deriving instance Show (STag tag)  instance DE.Enum1 STag where-  type Enum1Info STag = ()-  fromEnum1 = \case { SA -> (0, ()); SB -> (1, ()); SC -> (2, ()) }-  toEnum1 n () = case n of { 0 -> Some SA; 1 -> Some SB; 2 -> Some SC; _ -> error "invalid tag" }+  type Enum1Info STag = Const ()+  fromEnum1 = \case+                SA -> (0, Const ())+                SB -> (1, Const ())+                SC -> (2, Const ())+  toEnum1 n _ = case n of+                  0 -> coe1 SA+                  1 -> coe1 SB+                  2 -> coe1 SC+                  _ -> error "invalid tag"  data Value tag where   VA :: Int -> Value A