tomjaguarpaw / tilapia

Improving all Haskell's programmer interfaces
65 stars 2 forks source link

Explain correspondence between Data.Map.alter and Data.Map.adjust #4

Closed tomjaguarpaw closed 3 years ago

tomjaguarpaw commented 4 years ago

Data.Map has

adjust :: Ord k => (a -> a) -> k -> Map k a -> Map k a 
alter :: Ord k => (Maybe a -> Maybe a) -> k -> Map k a -> Map k a

with property

lookup k (alter f k m) = f (lookup k m)

I'm pretty sure that adjust = alter . fmap. Check this. If it's true then add it to the docs. If it's not true, add a counter example.

tomjaguarpaw commented 4 years ago

adjust: "Update a value at a specific key with the result of the provided function. When the key is not a member of the map, the original map is returned."

That means that

adjust f k m = case lookup k m of
    Nothing -> m
    Just v  -> insert k (f v) m

so

lookup k (adjust f k m)
== case lookup k m of
       Nothing -> lookup k m
       Just v  -> lookup k (insert k (f v) m)
== case lookup k m of
       Nothing -> Nothing
       Just v  -> Just (f v)
== fmap f (lookup k m)
== lookup k (alter (fmap f) k m)
== lookup k ((alter . fmap) f k m)

A function is defined by its arguments and a map is defined by its lookups, so this suffices to prove that adjust == alter . fmap.

tomjaguarpaw commented 4 years ago

PR: https://github.com/haskell/containers/pull/748 [EDIT: approved but not yet merged] [EDIT: merged]