Agda.Utils.AssocList

Additional functions for association lists.

Documentation

type AssocList k v = [(k, v)]

A finite map, represented as a set of pairs.

Invariant: at most one value per key.

lookup :: Eq k => k -> AssocList k v -> Maybe v

O(n). Reexport lookup.

keys :: AssocList k v -> [k]

O(n). Get the domain (list of keys) of the finite map.

insert :: k -> v -> AssocList k v -> AssocList k v

O(1). Add a new binding. Assumes the binding is not yet in the list.

update :: Eq k => k -> v -> AssocList k v -> AssocList k v

O(n). Update the value at a key. The key must be in the domain of the finite map. Otherwise, an internal error is raised.

updateAt :: Eq k => k -> (v -> v) -> AssocList k v -> AssocList k v

O(n). Update the value at a key with a certain function. The key must be in the domain of the finite map. Otherwise, an internal error is raised.

mapWithKey :: (k -> v -> v) -> AssocList k v -> AssocList k v

O(n). Map over an association list, preserving the order.

mapWithKeyM :: Applicative m => (k -> v -> m v) -> AssocList k v -> m (AssocList k v)

O(n). If called with a effect-producing function, violation of the invariant could matter here (duplicating effects).

mapKeysMonotonic :: (k -> k') -> AssocList k v -> AssocList k' v

O(n). Named in analogy to mapKeysMonotonic. To preserve the invariant, it is sufficient that the key transformation is injective (rather than monotonic).