Data.Map.Justified

Description

A wrapper around Data.Map's Map for shifting the burden of proof that a key exists in a map from "lookup time" to "key creation time".

Motivation: Data.Map and Maybe values

Suppose you have a key-value mapping using Data.Map's type Map k v. Anybody making use of Map k v to look up or modify a value must take into account the possibility that the given key is not present.

In Data.Map, there are two strategies for dealing with absent keys:

1. Cause a runtime error (e.g. Data.Map's ! when the key is absent)
2. Return a Maybe value (e.g. Data.Map's lookup)

The first option introduces partial functions, so is not very palatable. But what is wrong with the second option?

To understand the problem with returning a Maybe value, let's ask what returning Maybe v from lookup :: k -> Map k v -> Maybe v really does for us. By returning a Maybe v value, lookup key table is saying "Your program must account for the possibility that key cannot be found in table. I will ensure that you account for this possibility by forcing you to handle the Nothing case." In effect, Data.Map is requiring the user to prove they have handled the possibility that a key is absent whenever they use the lookup function.

Laziness (the bad kind)

Every programmer has probably had the experience of knowing, somehow, that a certain key is going to be present in a map. In this case, the Maybe v feels like a burden: I already know that this key is in the map, why should I handle the Nothing case?

In this situation, it is tempting to reach for the partial function fromJust, or a pattern match like Nothing -> error "The impossible happened!". But as parts of the program are changed over time, you may find the impossible has become possible after all (or perhaps you'll see the dreaded and unhelpful *** Exception: Maybe.fromJust: Nothing)

It is tempting to reach for partial functions or "impossible" runtime errors here, because the programmer has proven that the key is a member of the map in some other way. They know that lookup should return a 'Just v' --- but the compiler doesn't know this!

The idea behind Data.Map.Justified is to encode the programmer's knowledge that a key is present, within the type system where it can be checked at compile-time. Once a key is known to be present, lookup will never fail. Your justification removes the Just!

How it works

Evidence that a key can indeed be found in a map is carried by a phantom type parameter ph shared by both the Map and Key types. If you are able to get your hands on a value of type Key ph k, then you must have already proven that the key is present in any value of type Map ph k v.

The Key ph k type is simply a newtype wrapper around k, but the phantom type ph allows Key ph k to represent both a key of type k and /a proof that the key is present in maps of type Map ph k v/.

There are several ways to prove that a key belongs to a map, but the simplest is to just use Data.Map.Justified's member function. In Data.Map, member has the type

member :: Ord k => k -> Map k v -> Bool

and reports whether or not the key can be found in the map. In Data.Map.Justified, Member has the type

member :: Ord k => k -> Map ph k v -> Maybe (Key ph k)

Instead of a boolean, member either says "the key is not present" (Nothing), or gives back the same key, augmented with evidence that they key is present. This key-plus-evidence can then be used to do any number of Maybe-free operations on the map.

Data.Map.Justified uses the same rank-2 polymorphism trick used in the ST monad to ensure that the ph phantom type can not be extracted; in effect, the proof that a key is present can't leak to contexts where the proof would no longer be valid.

Tutorial

See Data.Map.Justified.Tutorial for usage examples and FAQs.

Map and Key types

data Map ph k v

A Data.Map Map wrapper that allows direct lookup of keys that are known to exist in the map.

Here, "direct lookup" means that once a key has been proven to exist in the map, it can be used to extract a value directly from the map, rather than requiring a Maybe layer.

Map allows you to shift the burden of proof that a key exists in a map from "prove at every lookup" to "prove once per key".

Instances

Functor (Map ph k)

Methods

fmap :: (a -> b) -> Map ph k a -> Map ph k b

(<$) :: a -> Map ph k b -> Map ph k a

Foldable (Map ph k)

Methods

fold :: Monoid m => Map ph k m -> m

foldMap :: Monoid m => (a -> m) -> Map ph k a -> m

foldr :: (a -> b -> b) -> b -> Map ph k a -> b

foldr' :: (a -> b -> b) -> b -> Map ph k a -> b

foldl :: (b -> a -> b) -> b -> Map ph k a -> b

foldl' :: (b -> a -> b) -> b -> Map ph k a -> b

foldr1 :: (a -> a -> a) -> Map ph k a -> a

foldl1 :: (a -> a -> a) -> Map ph k a -> a

toList :: Map ph k a -> [a]

null :: Map ph k a -> Bool

length :: Map ph k a -> Int

elem :: Eq a => a -> Map ph k a -> Bool

maximum :: Ord a => Map ph k a -> a

minimum :: Ord a => Map ph k a -> a

sum :: Num a => Map ph k a -> a

product :: Num a => Map ph k a -> a

Traversable (Map ph k)

Methods

traverse :: Applicative f => (a -> f b) -> Map ph k a -> f (Map ph k b)

sequenceA :: Applicative f => Map ph k (f a) -> f (Map ph k a)

mapM :: Monad m => (a -> m b) -> Map ph k a -> m (Map ph k b)

sequence :: Monad m => Map ph k (m a) -> m (Map ph k a)

(Eq v, Eq k) => Eq (Map ph k v)

Methods

(==) :: Map ph k v -> Map ph k v -> Bool

(/=) :: Map ph k v -> Map ph k v -> Bool

(Ord v, Ord k) => Ord (Map ph k v)

Methods

compare :: Map ph k v -> Map ph k v -> Ordering

(<) :: Map ph k v -> Map ph k v -> Bool

(<=) :: Map ph k v -> Map ph k v -> Bool

(>) :: Map ph k v -> Map ph k v -> Bool

(>=) :: Map ph k v -> Map ph k v -> Bool

max :: Map ph k v -> Map ph k v -> Map ph k v

min :: Map ph k v -> Map ph k v -> Map ph k v

(Show v, Show k) => Show (Map ph k v)

Methods

showsPrec :: Int -> Map ph k v -> ShowS

show :: Map ph k v -> String

showList :: [Map ph k v] -> ShowS

data Key ph k

A key that knows it can be found in certain Maps.

The evidence that the key can be found in a map is carried by the type system via the phantom type parameter ph. Certain operations such as lookup will only type-check if the Key and the Map have the same phantom type parameter.

Instances

Eq k => Eq (Key ph k)

Methods

(==) :: Key ph k -> Key ph k -> Bool

(/=) :: Key ph k -> Key ph k -> Bool

Ord k => Ord (Key ph k)

Methods

compare :: Key ph k -> Key ph k -> Ordering

(<) :: Key ph k -> Key ph k -> Bool

(<=) :: Key ph k -> Key ph k -> Bool

(>) :: Key ph k -> Key ph k -> Bool

(>=) :: Key ph k -> Key ph k -> Bool

max :: Key ph k -> Key ph k -> Key ph k

min :: Key ph k -> Key ph k -> Key ph k

Show k => Show (Key ph k)

Methods

showsPrec :: Int -> Key ph k -> ShowS

show :: Key ph k -> String

showList :: [Key ph k] -> ShowS

theKey :: Key ph k -> k

Get a bare key out of a key-plus-evidence by forgetting what map the key can be found in.

theMap :: Map ph k v -> Map k v

Get the underlying Data.Map Map out of a Map.

Evaluation

withMap :: Map k v -> (forall ph. Map ph k v -> t) -> t

Evaluate an expression using justified key lookups into the given map.

import qualified Data.Map as M

withMap (M.fromList [(1,"A"), (2,"B")]) $ \m -> do

  -- prints "Found Key 1 with value A"
  case member 1 m of
    Nothing -> putStrLn "Missing key 1."
    Just k  -> putStrLn ("Found " ++ show k ++ " with value " ++ lookup k m)

  -- prints "Missing key 3."
  case member 3 m of
    Nothing -> putStrLn "Missing key 3."
    Just k  -> putStrLn ("Found " ++ show k ++ " with value " ++ lookup k m)

data KeyInfo

Information about whether a key is present or missing. See withRecMap and Data.Map.Justified.Tutorial's example4.

Constructors

Present

Missing

Instances

Eq KeyInfo

Methods

(==) :: KeyInfo -> KeyInfo -> Bool

(/=) :: KeyInfo -> KeyInfo -> Bool

Ord KeyInfo

Methods

compare :: KeyInfo -> KeyInfo -> Ordering

(<) :: KeyInfo -> KeyInfo -> Bool

(<=) :: KeyInfo -> KeyInfo -> Bool

(>) :: KeyInfo -> KeyInfo -> Bool

(>=) :: KeyInfo -> KeyInfo -> Bool

max :: KeyInfo -> KeyInfo -> KeyInfo

min :: KeyInfo -> KeyInfo -> KeyInfo

Show KeyInfo

Methods

showsPrec :: Int -> KeyInfo -> ShowS

show :: KeyInfo -> String

showList :: [KeyInfo] -> ShowS

type MissingReference k f = (k, f (k, KeyInfo))

A description of what key/value-containing-keys pairs failed to be found. See withRecMap and Data.Map.Justified.Tutorial's example4.

withRecMap :: (Ord k, Traversable f) => Map k (f k) -> (forall ph. Map ph k (f (Key ph k)) -> t) -> Either [MissingReference k f] t

Evaluate an expression using justified key lookups into the given map, when the values can contain references back to keys in the map.

Each referenced key is checked to ensure that it can be found in the map. If all referenced keys are found, they are augmented with evidence and the given function is applied. If some referenced keys are missing, information about the missing references is generated instead.

import qualified Data.Map as M

data Cell ptr = Nil | Cons ptr ptr deriving (Functor, Foldable, Traversable)

memory1 = M.fromList [(1, Cons 2 1), (2, Nil)]
withRecMap memory1 (const ()) -- Right ()

memory2 = M.fromList [(1, Cons 2 3), (2, Nil)]
withRecMap memory2 (const ()) -- Left [(1, Cons (2,Present) (3,Missing))]

Gathering evidence

member :: Ord k => k -> Map ph k v -> Maybe (Key ph k)

O(log n). Obtain evidence that the key is a member of the map.

Where Data.Map generally requires evidence that a key exists in a map at every use of some functions (e.g. Data.Map's lookup), Map requires the evidence up-front. After it is known that a key can be found, there is no need for Maybe types or run-time errors.

The Maybe value that has to be checked at every lookup in Data.Map is then shifted to a Maybe (Key ph k) that has to be checked in order to obtain evidence that a key is in the map.

Note that the "evidence" only exists at the type level, during compilation; there is no runtime distinction between keys and keys-plus-evidence.

withMap (M.fromList [(5,'a'), (3,'b')]) (isJust . member 1) == False
withMap (M.fromList [(5,'a'), (3,'b')]) (isJust . member 5) == True

keys :: Map ph k v -> [Key ph k]

A list of all of the keys in a map, along with proof that the keys exist within the map.

Lookup and update

lookup :: Ord k => Key ph k -> Map ph k v -> v

O(log n). Lookup the value at a key, known to be in the map.

The result is a v rather than a Maybe v, because the proof obligation that the key is in the map must already have been discharged to obtain a value of type Key ph k.

(!) :: Ord k => Map ph k v -> Key ph k -> v

O(log n). Find the value at a key. Unlike Data.Map's !, this function is total and can not fail at runtime.

adjust :: Ord k => (v -> v) -> Key ph k -> Map ph k v -> Map ph k v

Adjust the valid at a key, known to be in the map, using the given function.

Since the set of valid keys in the input map and output map are the same, keys that were valid for the input map remain valid for the output map.

adjustWithKey :: Ord k => (k -> v -> v) -> Key ph k -> Map ph k v -> Map ph k v

Adjust the valid at a key, known to be in the map, using the given function.

Since the set of valid keys in the input map and output map are the same, keys that were valid for the input map remain valid for the output map.

reinsert :: Ord k => Key ph k -> v -> Map ph k v -> Map ph k v

Replace the value at a key, known to be in the map.

Since the set of valid keys in the input map and output map are the same, keys that were valid for the input map remain valid for the output map.

Indexing

findIndex :: Ord k => Key ph k -> Map ph k a -> Key ph Int

O(log n). Return the index of a key, which is its zero-based index in the sequence sorted by keys. The index is a number from 0 up to, but not including, the size of the map. The index also carries a proof that it is valid for the map.

Unlike Data.Map's findIndex, this function can not fail at runtime.

elemAt :: Key ph Int -> Map ph k v -> (Key ph k, v)

O(log n). Retrieve an element by its index, i.e. by its zero-based index in the sequence sorted by keys.

Unlike Data.Map's elemAt, this function can not fail at runtime.

Utilities

tie :: (Functor f, Ord k) => (f a -> a) -> Map ph k (f (Key ph k)) -> Key ph k -> a

Build a value by "tying the knot" according to the references in the map.