std.hashmap

Maps from keys to values by the keys’ hashes: a hash array mapped trie (HAMT), as Clojure’s, Scala’s and Haskell’s unordered-containers’ maps are. Import it by a name, import std.hashmap as HashMap (HashMap.insert), as map’s names are its names too. The map comes first, as in std.ordmap.

import std.hashmap as HashMap

-- | >>> HashMap.lookup (seen ["x", "y"]) "y"
-- | Just (True)
seen : List String -> HashMap.HashMap String Bool
seen ws = HashMap.fromList (List.map (\w -> MkPair w True) ws)

Each level of the trie takes 5 bits of a key’s hash, so a node has up to 32 children, kept in an array as long as how many there are and found by a bitmap of which there are (the bits below a child’s, counted, are where it is); 3572 keys are 3 levels deep, a million 4. A key is compared once, where its hash has led, with the one there. Where nothing else holds a node, it is changed in place: a value changed (update) builds nothing. The map keeps how many keys it binds, as each walk finds them added or gone, so size reads it; remove says whether a key it deletes was there.

The keys’ type has a Hash (strings, integers, runes, booleans, and pairs, lists and Maybes of them) and an Equality, each found as an instance argument is. The order of toList and foldl is the trie’s, by the hashes: not the keys’, but the same on every backend.

std.hashtable has the same names, in flat arrays: faster and smaller where one owner fills and reads a map, but a change to a table held elsewhere too copies all of it, and its order is of how it came to be. A map whose old versions are kept is this one’s.

strHash

strHash : String -> Int

intHash

intHash : Int -> Int

strHashRange

strHashRange : String -> Int -> Int -> Int

The hash of s’s bytes from i up to j, as strHash (strSlice s i j) (the same clamping), the slice never made.

>>> strHashRange "hello, world" 7 12 == strHash "world"
True

strEqRange

strEqRange : String -> String -> Int -> Int -> Bool

Whether t is s’s bytes from i up to j, as strEq t (strSlice s i j), the slice never made.

>>> strEqRange "world" "hello, world" 7 12
True

trieSlot

trieSlot : Int -> Int -> Int -> Int

Hash

theory Hash a where
  hash : a -> Int

A type’s hash: two values equal have the same one.

hash

hash : {a : Type} -> {{hashing : Hash a}} -> a -> Int

instanceHashString

instance instanceHashString : Hash String

>>> hash "hello, world" == hash ("hello" ^ ", world")
True
>>> hash "a" == hash "b"
False

instanceHashInt

instance instanceHashInt : Hash Int

>>> List.map (\(i : Int) -> hash i == hash (i + 1)) [0, 1180591620717411303424]
Cons False (Cons False Nil)

instanceHashRune

instance instanceHashRune : Hash Rune

instanceHashBool

instance instanceHashBool : Hash Bool

combine

combine : Int -> Int -> Int

the hash of what is hashed h so far, then of x’s hash: in order, so that MkPair a b and MkPair b a differ

instanceHashPair

instance instanceHashPair : {a b : Type}
                          -> {{hashA : Hash a}}
                          -> {{hashB : Hash b}}
                          -> Hash (a, b)

>>> hash (MkPair 1 2 : Pair Int Int) == hash (MkPair 2 1 : Pair Int Int)
False

instanceHashMaybe

instance instanceHashMaybe : {a : Type}
                           -> {{hashing : Hash a}}
                           -> Hash (Maybe a)

instanceHashList

instance instanceHashList : {a : Type} -> {{hashing : Hash a}} -> Hash (List a)

>>> hash (["a", "b"] : List String) == hash (["b", "a"] : List String)
False

KeyView

theory KeyView k q where
  hashOf : q -> Int
  matches : k -> q -> Bool
  keyOf : q -> k

A view of a key, q, that stands for a key of type k without being one: what a map’s updateBy and lookupBy look a key up by, so that the key is made (keyOf) only where it is new to the map. Its hash is the key’s, and it matches the key it stands for and no other: hashOf q == hash (keyOf q), and matches k q where equal k (keyOf q).

Slice

data Slice = MkSlice String Int Int

A part of a string: its bytes from one place up to another, as strSlice takes them, the slice not made.

slice

slice : String -> Int -> Int -> Slice

The part of s from i up to j, as a Slice (where its type is not known, as a view’s is not, a tag is not enough).

instanceKeyViewStringSlice

instance instanceKeyViewStringSlice : KeyView String Slice

A string’s part stands for the string strSlice would make of it, hashed and compared where it is.

>>> instanceKeyViewStringSlice.hashOf (MkSlice "hello, world" 7 12) == hash "world"
True
>>> instanceKeyViewStringSlice.matches "world" (MkSlice "hello, world" 7 12)
True

Trie

data Trie k v
  = Vacant
  | Leaf Int k v
  | Collision Int (List (k, v))
  | Branch Int (Array (Trie k v))

A trie: nothing (only the whole map’s, never a child); a key, its hash and its value; keys of one hash, each with its value; or a node of children, a bitmap of which of the 32 there are.

HashMap

data HashMap k v = MkHashMap Int (Trie k v)

A map: how many keys it binds, and its trie.

empty

empty : {k v : Type} -> HashMap k v

The map of no keys.

Walked

data Walked k v a = MkWalked (Trie k v) a (Array (Trie k v))

update

update : {k v : Type}
       -> {{hashing : Hash k}}
       -> {{equality : Equality k}}
       -> HashMap k v
       -> k
       -> v
       -> (v -> v -> v)
       -> HashMap k v

The map with k bound to v, or, where it is bound, to f v old (Haskell’s insertWith): a value changed in one walk down the trie.

insert

insert : {k v : Type}
       -> {{hashing : Hash k}}
       -> {{equality : Equality k}}
       -> HashMap k v
       -> k
       -> v
       -> HashMap k v

The map with k bound to v (instead of what it was, if it was).

lookup

lookup : {k v : Type}
       -> {{hashing : Hash k}}
       -> {{equality : Equality k}}
       -> HashMap k v
       -> k
       -> Maybe v

What k is bound to, if it is.

remove

remove : {k v : Type}
       -> {{hashing : Hash k}}
       -> {{equality : Equality k}}
       -> HashMap k v
       -> k
       -> (Maybe v, HashMap k v)

What k was bound to, if it was, and the map without it (Rust’s remove): a delete that says whether the key was there, in one walk down the trie.

delete

delete : {k v : Type}
       -> {{hashing : Hash k}}
       -> {{equality : Equality k}}
       -> HashMap k v
       -> k
       -> HashMap k v

The map without k (as it was, if k was not in it; remove says which).

alter

alter : {k v : Type}
      -> {{hashing : Hash k}}
      -> {{equality : Equality k}}
      -> HashMap k v
      -> k
      -> (Maybe v -> Maybe v)
      -> HashMap k v

The map with k bound as f says, given what it is bound to, if it is: to f’s value, or (Nothing) to none (Haskell’s alter), in one walk down the trie.

foldl

foldl : {k v b : Type} -> (b -> k -> v -> b) -> b -> HashMap k v -> b

Each key and its value, from z, in the trie’s order (the hashes’).

size

size : {k v : Type} -> HashMap k v -> Int

How many keys are bound: kept as they are bound and deleted, not counted.

toList

toList : {k v : Type} -> HashMap k v -> List (k, v)

The keys and their values, in the trie’s order (the hashes’, not the keys’): sort them for another.

member

member : {k v : Type}
       -> {{hashing : Hash k}}
       -> {{equality : Equality k}}
       -> HashMap k v
       -> k
       -> Bool

Whether k is bound in it.

>>> List.map (member (insert (empty : HashMap String Int) "a" 1)) ["a", "b"]
Cons True (Cons False Nil)

keys

keys : {k v : Type} -> HashMap k v -> List k

The keys, in toList’s order.

>>> keys (insert (empty : HashMap String Int) "a" 1)
Cons "a" Nil

values

values : {k v : Type} -> HashMap k v -> List v

The values, in toList’s order.

>>> values (insert (empty : HashMap String Int) "a" 1)
Cons 1 Nil

instanceIterateHashMap

instance instanceIterateHashMap : {k v : Type} -> Iterate (HashMap k v)

A hash map, each key and its value in the trie’s order, as toList has them: for p in m goes through that list.

fromList

fromList : {k v : Type}
         -> {{hashing : Hash k}}
         -> {{equality : Equality k}}
         -> List (k, v)
         -> HashMap k v

The map of the pairs, a later one’s value for a key twice.

>>> lookup (fromList [MkPair "a" 1, MkPair "b" 2]) "b"
Just 2
>>> lookup (fromList [MkPair "a" 1, MkPair "b" 2]) "c"
Nothing
>>> lookup (insert (fromList [MkPair 2 "deux"]) 2 "two") 2
Just "two"
>>> size (fromList [MkPair "a" 1, MkPair "b" 2, MkPair "a" 3])
2
>>> foldl (\n k v -> n + k * v) 0 (fromList [MkPair 2 3, MkPair 4 5])
26
>>> List.sortOn (\p -> fst p) (toList (fromList [MkPair "b" 2, MkPair "a" 1]))
Cons (MkPair "a" 1) (Cons (MkPair "b" 2) Nil)
>>> toList (update (fromList [MkPair "a" 2]) "a" 1 (\new old -> new + old))
Cons (MkPair "a" 3) Nil
>>> lookup (update (fromList [MkPair "a" 2]) "b" 5 (\new old -> new + old)) "b"
Just 5
>>> toList (delete (fromList [MkPair "a" 1, MkPair "b" 2]) "a")
Cons (MkPair "b" 2) Nil
>>> size (delete (fromList [MkPair 1 "one"]) 7)
1
>>> size (delete (fromList [MkPair 1 "one", MkPair 2 "two"]) 1)
1
>>> fst (remove (fromList [MkPair "a" 1, MkPair "b" 2]) "a")
Just 1
>>> fst (remove (insert (empty : HashMap String Int) "a" 1) "c")
Nothing
>>> toList (snd (remove (fromList [MkPair "a" 1, MkPair "b" 2]) "a"))
Cons (MkPair "b" 2) Nil
>>> size (alter (fromList [MkPair 1 "one"]) 2 (\old -> Just "two"))
2
>>> toList (alter (fromList [MkPair "a" 2]) "a" (\old -> Just (maybe 1 (\n -> n + 1) old)))
Cons (MkPair "a" 3) Nil
>>> toList (alter (fromList [MkPair 1 "one"]) 1 (\old -> Nothing))
Nil
>>> lookup (alter (fromList [MkPair 1 "one"]) 3 (\old -> Just "three")) 3
Just "three"

updateBy

updateBy : {k v q : Type}
         -> {{view : KeyView k q}}
         -> HashMap k v
         -> q
         -> v
         -> (v -> v -> v)
         -> HashMap k v

update of the key a view stands for (KeyView): the key made of it only where it is new to the map, so that counting the parts of a string (slice), most of them there already, makes no string for those.

>>> lookup (updateBy (fromList [MkPair "ab" 1]) (slice "xaby" 1 3) 5 (\new old -> new + old)) "ab"
Just 6
>>> toList (updateBy (empty : HashMap String Int) (slice "xaby" 1 3) 5 (\new old -> new + old))
Cons (MkPair "ab" 5) Nil

lookupBy

lookupBy : {k v q : Type}
         -> {{view : KeyView k q}}
         -> HashMap k v
         -> q
         -> Maybe v

lookup of the key a view stands for (KeyView), no key made.

>>> lookupBy (fromList [MkPair "ab" 1]) (slice "xaby" 1 3)
Just 1
>>> lookupBy (fromList [MkPair "ab" 1]) (slice "xaby" 1 2)
Nothing