ModuleAgda-2.7.0.1Haskell2010

Agda.Utils.AssocList

Additional functions for association lists.

1 type
10 values

PackageAgda-2.7.0.1
Exports11
LanguageHaskell2010
LicenceMIT
SourceAssocList.hs

valueapply :: Ord k => AssocList k v -> k -> Maybe v

Lookup keys in the same association list often. Use partially applied to create partial function apply m :: k -> Maybe v.

First time: O(n log n) in the worst case.
Subsequently: O(log n).

Specification: apply m == (lookup m).

valueinsert :: k -> v -> AssocList k v -> AssocList k v

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

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

A finite map, represented as a set of pairs.

Invariant: at most one value per key.

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

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

valuekeys :: AssocList k v -> [k]

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

valueupdate :: 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.

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

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

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

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

valueupdateAt :: 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.

valuemapWithKeyM

:: 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).

valuelookup :: Eq a => a -> [(a, b)] -> Maybe b

\mathcal{O}(n). lookup key assocs looks up a key in an association list. For the result to be Nothing, the list must be finite.

Examples

Example1 expression

>>> lookup 2 []Nothing

Example1 expression

>>> lookup 2 [(1, "first")]Nothing

Example1 expression

>>> lookup 2 [(1, "first"), (2, "second"), (3, "third")]Just "second"