std.map

Maps of keys to values, whichever they are: a theory of what std.ordmap, std.hashmap and std.hashtable each do, so that a definition written once works on any of them, and a program picks one by its type.

import std.hashmap as HashMap
import std.map as Map

-- | how many times each word appears, in a map of any kind
counts : {c : Type} -> {{m : Map.Mapping c @ { Key = String, Value = Int }}} -> List String -> c
counts ws = List.foldl (\t w -> m.insert t w (1 + fromMaybe 0 (m.lookup t w))) m.empty ws

Which one to pick:

• std.hashmap, a trie by the keys’ hashes: stable — its order is the hashes’, of what it binds alone — and a change to a map held elsewhere too (an old version kept) copies one path of it.
• std.hashtable, flat arrays: unstable — its order is of how it came to be — and a change to a table held elsewhere too copies all of it; but where one owner fills and reads it, the fastest.
• std.ordmap, a balanced tree by the keys’ Order: in the keys’ order.

Import this module for the instances too: an instance is in scope only in a module that imports its own.

Mapping

theory Mapping c where
  Key : Type
  Value : Type
  empty : c
  insert : c -> Key -> Value -> c
  lookup : c -> Key -> Maybe Value
  remove : c -> Key -> (Maybe Value, c)
  size : c -> Int
  foldl : {b : Type} -> (b -> Key -> Value -> b) -> b -> c -> b

A map c of keys (Key) to values (Value): the map of none, a key bound, looked up and removed (and what it was bound to, if it was), how many keys are bound, and each key and its value folded, in the map’s order.

empty

empty : {c : Type} -> {{m : Mapping c}} -> c

The map of no keys, of the kind c.

insert

insert : {c : Type} -> {{m : Mapping c}} -> c -> m.Key -> m.Value -> c

The map with key bound to value.

lookup

lookup : {c : Type} -> {{m : Mapping c}} -> c -> m.Key -> Maybe m.Value

What key is bound to, if it is.

remove

remove : {c : Type} -> {{m : Mapping c}} -> c -> m.Key -> (Maybe m.Value, c)

What key was bound to, if it was, and the map without it.

size

size : {c : Type} -> {{m : Mapping c}} -> c -> Int

How many keys are bound.

foldl

foldl : {c b : Type}
      -> {{m : Mapping c}}
      -> (b -> m.Key -> m.Value -> b)
      -> b
      -> c
      -> b

Each key and its value, from z, in the map’s order.

instanceMappingHashMap

instance instanceMappingHashMap : {k v : Type}
                                -> {{hashing : HashMap.Hash k}}
                                -> {{equality : Equality k}}
                                -> Mapping (HashMap.HashMap k v)

A hash map (std.hashmap): stable, its order the keys’ hashes’.

instanceMappingHashTable

instance instanceMappingHashTable : {k v : Type}
                                  -> {{hashing : HashMap.Hash k}}
                                  -> {{equality : Equality k}}
                                  -> Mapping (HashTable.HashTable k v)

A hash table (std.hashtable): unstable, its order of how it came to be.

instanceMappingOrdMap

instance instanceMappingOrdMap : {k v : Type}
                               -> {{ord : Order k}}
                               -> Mapping (OrdMap.OrdMap k v)

A map ordered by its keys (std.ordmap): in the keys’ order.

tally

tally : {c : Type} -> {{m : Mapping c @ { Value = Int }}} -> List m.Key -> c

How many times each key is in ks, in a map of any kind.

>>> HashMap.lookup (tally ["a", "b", "a"] : HashMap.HashMap String Int) "a"
Just 2
>>> HashTable.lookup (tally ["a", "b", "a"] : HashTable.HashTable String Int) "b"
Just 1
>>> OrdMap.toList (tally ["b", "a", "b"] : OrdMap.OrdMap String Int)
Cons (MkPair "a" 1) (Cons (MkPair "b" 2) Nil)