summaryrefslogtreecommitdiff
path: root/src/Data
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data')
-rw-r--r--src/Data/Dependent/EnumMap/Strict/Internal.hs171
1 files changed, 80 insertions, 91 deletions
diff --git a/src/Data/Dependent/EnumMap/Strict/Internal.hs b/src/Data/Dependent/EnumMap/Strict/Internal.hs
index 85fa621..6cc46a3 100644
--- a/src/Data/Dependent/EnumMap/Strict/Internal.hs
+++ b/src/Data/Dependent/EnumMap/Strict/Internal.hs
@@ -7,6 +7,7 @@
{-# LANGUAGE TypeFamilies #-}
module Data.Dependent.EnumMap.Strict.Internal where
+import Control.Exception
import Data.Bifunctor (bimap)
import Data.Dependent.Sum
import qualified Data.IntMap.Strict as IM
@@ -27,6 +28,31 @@ instance (Enum1 k, forall a. Show (k a), forall a. Show (v a))
showsPrec d mp = showParen (d > 10) $
showString "fromList " . showListWith (\(k :=> v) -> showsPrec 2 k . showString " :=> " . showsPrec 1 v) (toList mp)
+-- | This class attempts to generalise 'Enum' to indexed data types: data types
+-- with a GADT-like type parameter. Conversion to an 'Int' naturally loses type
+-- information, and furthermore it is common to actually need some additional
+-- data alongside the 'Int' to be able to reconstruct the original (in
+-- 'toEnum1'). This additional data lives in 'Enum1Info'. The laws are:
+--
+-- [Unique IDs]
+-- If @'fst' ('fromEnum1' x) == 'fst' ('fromEnum1' y)@ then @'testEquality' x y == 'Just' 'Refl' && x '==' y@
+-- [Persistent IDs]
+-- @'fst' ('fromEnum1' ('uncurry' 'toEnum1' ('fromEnum1' x))) == 'fst' ('fromEnum1' x)@
+--
+-- The "Unique IDs" law states that if the IDs of two values are equal, then
+-- the values themselves must have the same type index, and furthermore be
+-- equal. If @f@ does not implement 'TestEquality' or 'Eq', the law should
+-- morally hold (but most of the API will be unusable).
+--
+-- The "Persistent IDs" law states that reconstructing a value using 'toEnum1'
+-- does not change its ID.
+--
+-- __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.
class Enum1 f where
type Enum1Info f
fromEnum1 :: f a -> (Int, Enum1Info f)
@@ -35,6 +61,7 @@ class Enum1 f where
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
@@ -55,23 +82,24 @@ singleton k v =
fromList :: Enum1 k => [DSum k v] -> DEnumMap k v
fromList l = DEnumMap (IM.fromList (map dSumToKV l))
--- TODO: check that inf1 and inf2 match somehow? Comment why not needed or not possible, if so
-fromListWith :: Enum1 k
+fromListWith :: (Enum1 k, TestEquality k)
=> (forall a. v a -> v a -> v a)
-> [DSum k v] -> DEnumMap k v
-fromListWith f l =
- DEnumMap (IM.fromListWith
- (\(KV inf1 v1) (KV _ v2) -> KV inf1 (f (coe1 v1) (coe1 v2)))
+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)))
(map dSumToKV l))
--- TODO: check that inf1 and inf2 match somehow? Comment why not needed or not possible, if so
-fromListWithKey :: Enum1 k
+fromListWithKey :: (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 _ v2) -> case toEnum1 i inf1 of
- Some k -> KV inf1 (f k (coe1 v1) (coe1 v2)))
+ (\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)))
(map dSumToKV l))
-- ** From Ascending Lists
@@ -79,23 +107,24 @@ fromListWithKey f l =
fromAscList :: Enum1 k => [DSum k v] -> DEnumMap k v
fromAscList l = DEnumMap (IM.fromAscList (map dSumToKV l))
--- TODO: check that inf1 and inf2 match somehow? Comment why not needed or not possible, if so
-fromAscListWith :: Enum1 k
+fromAscListWith :: (Enum1 k, TestEquality k)
=> (forall a. v a -> v a -> v a)
-> [DSum k v] -> DEnumMap k v
-fromAscListWith f l =
- DEnumMap (IM.fromAscListWith
- (\(KV inf1 v1) (KV _ v2) -> KV inf1 (f (coe1 v1) (coe1 v2)))
+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)))
(map dSumToKV l))
--- TODO: check that inf1 and inf2 match somehow? Comment why not needed or not possible, if so
-fromAscListWithKey :: Enum1 k
+fromAscListWithKey :: (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 _ v2) -> case toEnum1 i inf1 of
- Some k -> KV inf1 (f k (coe1 v1) (coe1 v2)))
+ (\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)))
(map dSumToKV l))
fromDistinctAscList :: Enum1 k => [DSum k v] -> DEnumMap k v
@@ -108,22 +137,18 @@ insert k v (DEnumMap m) =
let (i, inf) = fromEnum1 k
in DEnumMap (IM.insert i (KV inf v) m)
-insertWith :: Enum1 k
+insertWith :: (Enum1 k, TestEquality k)
=> (v a -> v a -> v a)
-> k a -> v a -> DEnumMap k v -> DEnumMap k v
-insertWith f k v (DEnumMap m) =
- let (i, inf) = fromEnum1 k
- in DEnumMap (IM.insertWith
- (\(KV _ v1) (KV _ v2) -> KV inf (f (coe1 v1) (coe1 v2)))
- i (KV inf v) m)
+insertWith = insertWithKey . const
-insertWithKey :: Enum1 k
+insertWithKey :: (Enum1 k, TestEquality k)
=> (k a -> v a -> v a -> v a)
-> k a -> v a -> DEnumMap k v -> DEnumMap k v
insertWithKey f k v (DEnumMap m) =
let (i, inf) = fromEnum1 k
in DEnumMap (IM.insertWith
- (\(KV _ v1) (KV _ v2) -> KV inf (f k (coe1 v1) (coe1 v2)))
+ (\_ (KV inf' v2) -> typeCheck1 k i inf' $ KV inf (f k v (coe1 v2)))
i (KV inf v) m)
-- insertLookupWithKey
@@ -134,15 +159,9 @@ delete :: Enum1 k => k a -> DEnumMap k v -> DEnumMap k v
delete k (DEnumMap m) = DEnumMap (IM.delete (fst (fromEnum1 k)) m)
adjust :: (Enum1 k, TestEquality k) => (v a -> v a) -> k a -> DEnumMap k v -> DEnumMap k v
-adjust = adjust' typeCheckK
-
-adjustUnsafe :: Enum1 k => (v a -> v a) -> k a -> DEnumMap k v -> DEnumMap k v
-adjustUnsafe = adjust' don'tCheckK
-
-adjust' :: Enum1 k => Checker k a -> (v a -> v a) -> k a -> DEnumMap k v -> DEnumMap k v
-adjust' ch f k (DEnumMap m) =
+adjust f k (DEnumMap m) =
let (i, _) = fromEnum1 k
- in DEnumMap (IM.adjust (\(KV inf v) -> ch i k inf $ KV inf (f (coe1 v))) i m)
+ in DEnumMap (IM.adjust (\(KV inf v) -> typeCheck1 k i inf $ KV inf (f (coe1 v))) i m)
-- adjustWithKey
-- update
@@ -150,19 +169,13 @@ adjust' ch f k (DEnumMap m) =
-- updateLookupWithKey
alter :: forall k v a. (Enum1 k, TestEquality k) => (Maybe (v a) -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v
-alter = alter' typeCheckK
-
-alterUnsafe :: forall k v a. Enum1 k => (Maybe (v a) -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v
-alterUnsafe = alter' don'tCheckK
-
-alter' :: forall k v a. Enum1 k => Checker k a -> (Maybe (v a) -> Maybe (v a)) -> k a -> DEnumMap k v -> DEnumMap k v
-alter' ch f k (DEnumMap m) = DEnumMap (IM.alter f' i m)
+alter f k (DEnumMap m) = DEnumMap (IM.alter f' i m)
where
(i, inf) = fromEnum1 k
f' :: Maybe (KV k v) -> Maybe (KV k v)
f' Nothing = KV inf <$> f Nothing
- f' (Just (KV inf' v)) = ch i k inf' $ KV inf <$> f (Just (coe1 v))
+ f' (Just (KV inf' v)) = typeCheck1 k i inf' $ KV inf <$> f (Just (coe1 v))
-- alterF
@@ -170,30 +183,18 @@ alter' ch f k (DEnumMap m) = DEnumMap (IM.alter f' i m)
-- ** Lookup
lookup :: (Enum1 k, TestEquality k) => k a -> DEnumMap k v -> Maybe (v a)
-lookup = lookup' typeCheckK
-
-lookupUnsafe :: Enum1 k => k a -> DEnumMap k v -> Maybe (v a)
-lookupUnsafe = lookup' don'tCheckK
-
-lookup' :: Enum1 k => Checker k a -> k a -> DEnumMap k v -> Maybe (v a)
-lookup' ch k (DEnumMap m) =
+lookup k (DEnumMap m) =
let (i, _) = fromEnum1 k
- in (\(KV inf v) -> ch i k inf $ coe1 v) <$> IM.lookup i m
+ in (\(KV inf v) -> typeCheck1 k i inf $ coe1 v) <$> IM.lookup i m
-- (!?)
-- (!)
findWithDefault :: (Enum1 k, TestEquality k) => v a -> k a -> DEnumMap k v -> v a
-findWithDefault = findWithDefault' typeCheckK
-
-findWithDefaultUnsafe :: Enum1 k => v a -> k a -> DEnumMap k v -> v a
-findWithDefaultUnsafe = findWithDefault' don'tCheckK
-
-findWithDefault' :: Enum1 k => Checker k a -> v a -> k a -> DEnumMap k v -> v a
-findWithDefault' ch def k (DEnumMap m) =
+findWithDefault def k (DEnumMap m) =
let (i, _) = fromEnum1 k
in case IM.findWithDefault (KV undefined def) i m of
- KV inf' v -> ch i k inf' $ coe1 v
+ KV inf' v -> typeCheck1 k i inf' $ coe1 v
member :: Enum1 k => k a -> DEnumMap k v -> Bool
member k (DEnumMap m) = IM.member (fst (fromEnum1 k)) m
@@ -217,26 +218,14 @@ size (DEnumMap m) = IM.size m
-- ** Union
union :: (Enum1 k, TestEquality k) => DEnumMap k v -> DEnumMap k v -> DEnumMap k v
-union = unionWith const -- if we're checking, we need unionWith anyway, so might as well just delegate here already
-
--- in the unsafe variant, we can make do with IM.union, which is slightly faster than IM.unionWith, so let's specialise
-unionUnsafe :: DEnumMap k v -> DEnumMap k v -> DEnumMap k v
-unionUnsafe (DEnumMap m1) (DEnumMap m2) = DEnumMap (IM.union m1 m2)
+union = unionWith const -- if we're type checking, we need unionWith anyway, so might as well just delegate here already
unionWith :: (Enum1 k, TestEquality k)
=> (forall a. v a -> v a -> v a) -> DEnumMap k v -> DEnumMap k v -> DEnumMap k v
-unionWith f (m1 :: DEnumMap k v) = unionWith' (typeCheckSK (Proxy @k)) f m1
-
-unionWithUnsafe :: (forall a. v a -> v a -> v a) -> DEnumMap k v -> DEnumMap k v -> DEnumMap k v
-unionWithUnsafe f (m1 :: DEnumMap k v) = unionWith' (don'tCheckSK (Proxy @k)) f m1
-
-unionWith' :: CheckerSplit k
- -> (forall a. v a -> v a -> v a)
- -> DEnumMap k v -> DEnumMap k v -> DEnumMap k v
-unionWith' ch f (DEnumMap m1 :: DEnumMap k v) (DEnumMap m2) = DEnumMap (IM.unionWithKey f' m1 m2)
+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) = ch i inf1 inf2 $ KV inf1 (f v1 (coe1 v2))
+ f' i (KV inf1 v1) (KV inf2 v2) = typeCheck2 (Proxy @k) i inf1 inf2 $ KV inf1 (f v1 (coe1 v2))
-- unionWithKey
-- unions
@@ -382,21 +371,21 @@ maxViewWithKey (DEnumMap m) = bimap kVToDSum DEnumMap <$> IM.maxViewWithKey m
coe1 :: v a -> v b
coe1 = unsafeCoerce
-type CheckerSplit k = forall r. Int -> Enum1Info k -> Enum1Info k -> r -> r
-
-typeCheckSK :: forall k proxy. (Enum1 k, TestEquality k) => proxy k -> CheckerSplit k
-typeCheckSK _ i inf1 inf2 = case toEnum1 @k i inf1 of Some k -> typeCheckK i k inf2
-
-don'tCheckSK :: proxy k -> CheckerSplit k
-don'tCheckSK _ _ _ _ = id
-
-type Checker k a = forall r. Int -> k a -> Enum1Info k -> r -> r
-
-typeCheckK :: (Enum1 k, TestEquality k) => Checker k a
-typeCheckK i k1 inf cont
- | Some k2 <- toEnum1 i inf
- , Just Refl <- testEquality k1 k2 = cont
- | otherwise = errorWithoutStackTrace "DEnumMap: keys with same Int but different types"
-
-don'tCheckK :: Checker k a
-don'tCheckK _ _ _ = id
+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
+
+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
generated by cgit v1.2.3-70-g09d2 (git 2.48.1) at 2025-05-10 01:06:11 +0200