The `TABLE` signature

Overview

The TABLE interface specifies a mapping from keys to values, written as $\{k_1 \mapsto v_1, k_2 \mapsto v_2, \dots \}$.

Tables do not have duplicate keys, so there is a unique associated value for each key in the domain of a table. The key type is given by the Key substructure, and the value type is polymorphic.

We include a Set substructure to reinforce the relationship between tables and sets.

We use a number of notational conventions which can be seen here. For example, we write $|t|$ for the number of key-value pairs in a table $t$, and the empty table is denoted either $\{\}$ or $\emptyset$.

Interface

structure Key : EQKEY
structure Seq : SEQUENCE

type 'a t
type 'a table = 'a t

structure Set : SET where Key = Key and Seq = Seq

val size : 'a table → int
val domain : 'a table → Set.t
val range : 'a table → 'a Seq.t
val toString : ('a → string) → 'a table → string
val toSeq : 'a table → (Key.t * 'a) Seq.t

val find : 'a table → Key.t → 'a option
val insert : 'a table * (Key.t * 'a) → 'a table
val insertWith : ('a * 'a → 'a) → 'a table * (Key.t * 'a) → 'a table
val delete : 'a table * Key.t → 'a table

val empty : unit → 'a table
val singleton : Key.t * 'a → 'a table
val tabulate : (Key.t → 'a) → Set.t → 'a table
val collect : (Key.t * 'a) Seq.t → 'a Seq.t table
val fromSeq : (Key.t * 'a) Seq.t → 'a table

val map : ('a → 'b) → 'a table → 'b table
val mapKey : (Key.t * 'a → 'b) → 'a table → 'b table
val filter : ('a → bool) → 'a table → 'a table
val filterKey : (Key.t * 'a → bool) → 'a table → 'a table

val reduce : ('a * 'a → 'a) → 'a → 'a table → 'a
val iterate : ('b * 'a → 'b) → 'b → 'a table → 'b
val iteratePrefixes : ('b * 'a → 'b) → 'b → 'a table → ('b table * 'b)

val union : ('a * 'a → 'a) → 'a table * 'a table → 'a table
val intersection : ('a * 'b → 'c) → 'a table * 'b table → 'c table
val difference : 'a table * 'b table → 'a table

val restrict : 'a table * Set.t → 'a table
val subtract : 'a table * Set.t → 'a table

val $ : (Key.t * 'a) → 'a table

Substructures

structure Key : EQKEY: The Key substructure defines the type of keys in a table, which may be compared for equality.
structure Seq : SEQUENCE: The Seq substructure defines underlying sequence type, so that we may convert tables to and from sequences.
structure Set : SET where Key = Key and Seq = Seq: The Set substructure contains operations on sets with elements of type Key.t.

Types

type 'a t
type 'a table = 'a t: The abstract table type with values of type 'a. The type table is for readability in the signature.

Values

val size : 'a table → int: The number of key-value pairs in a table.
val domain : 'a table → Set.t: Return the set of all keys in a table.
val range : 'a table → 'a Seq.t: Return a sequence of all values in a table. The order of the elements is implementation-defined.
val toString : ('a → string) → 'a table → string: toString f t returns a string representation of $t$. Each key is converted to a stirng via Key.toString and each value is converted via $f$.
The ordering of key-value pairs in the resulting string is implementation-defined.
val toSeq : 'a table → (Key.t * 'a) Seq.t: Return a sequence of all key-value pairs in a table. The order of the sequence is implementation-defined.
val find : 'a table → Key.t → 'a option: find t k returns (SOME $v$) if $(k \mapsto v) \in t$, and NONE otherwise.
val insert : 'a table * (Key.t * 'a) → 'a table: insert (t, (k, v)) returns the table $t \cup \{(k \mapsto v)\}$. If $k$ is already in $t$, then the new value $v$ is given precedence. It is logically equivalent to insertWith (fn (_, v) => v) (t, (k,v)) .
val insertWith : ('a * 'a → 'a) → 'a table * (Key.t * 'a) → 'a table: insertWith f (t, (k, v)) returns the table $t \cup \{(k \mapsto v)\}$ if $k$ is not already a member of $t$, and otherwise it returns $t \cup \{(k \mapsto f (v', v))\}$ where $(k \mapsto v')$ is already in $t$.
val delete : 'a table * Key.t → 'a table: delete (t, k) removes the key $k$ from $t$ only if $k$ is a member of $t$. That is, if $(k \mapsto v) \in t$ then it returns $t \setminus \{(k \mapsto v)\}$, otherwise it returns $t$.
val empty : unit → 'a table: Construct the empty table.
val singleton : Key.t * 'a → 'a table: singleton (k, v) constructs the singleton table $\{(k \mapsto v)\}$.
val tabulate : (Key.t → 'a) → Set.t → 'a table: tabulate f s evaluates to the table $\{ (k \mapsto f(k)) : k \in s \}$.
val collect : (Key.t * 'a) Seq.t → 'a Seq.t table: collect s takes a sequence of key-value pairs and produces a table where each unique key $k$ is paired with $\langle v : (k', v) \in s | k' = k \rangle$.
val fromSeq : (Key.t * 'a) Seq.t → 'a table: Return the table representation of a sequence of key-value pairs. If there are duplicate keys, then take the value associated with the first occurence in the sequence.
val map : ('a → 'b) → 'a table → 'b table: map f t returns the table $\{ (k \mapsto f(v)) : (k \mapsto v) \in t \}$.
val mapKey : (Key.t * 'a → 'b) → 'a table → 'b table: mapKey f t returns the table $\{ (k \mapsto f(k, v)) : (k \mapsto v) \in t \}$.
val filter : ('a → bool) → 'a table → 'a table: filter p t produces a table containing all $(k \mapsto v) \in t$ which satisfies $p(v)$.
val filterKey : (Key.t * 'a → bool) → 'a table → 'a table: filterKey p t returns the table containing every $(k \mapsto v) \in t$ which satisfies $p(k, v)$.
val reduce : ('a * 'a → 'a) → 'a → 'a table → 'a: reduce f b t is logically equivalent to Seq.reduce f b (range t).
val iterate : ('b * 'a → 'b) → 'b → 'a table → 'b: iterate f b t is logically equivalent to Seq.iterate f b (range t).
val iteratePrefixes : ('b * 'a → 'b) → 'b → 'a table → ('b table * 'b): iteratePrefixes f b t is logically equivalent to (fromSeq p, x) where $(p, x)$ = Seq.iteratePrefixes f b (range t).
val union : ('a * 'a → 'a) → 'a table * 'a table → 'a table: union f (a, b) evaluates to $a \cup b$. For keys $k$ where $(k \mapsto v) \in a$ and $(k \mapsto w) \in b$, we have $(k \mapsto f (v, w))$ in the resulting table.
val intersection : ('a * 'b → 'c) → 'a table * 'b table → 'c table: intersection f (a, b) evaluates to the table $a \cap b$. Every intersecting key $k$ is mapped to $f (v, w)$, where $(k \mapsto v) \in a$ and $(k \mapsto w) \in b$.
val difference : 'a table * 'b table → 'a table: difference (a, b) evaluates to the table $a \setminus b$.
val restrict : 'a table * Set.t → 'a table: restrict returns the table of $\{ (k \mapsto v) \in t | k \in s \}$. It is therefore essentially an intersection. The name is motivated by the notion of restricting a function to a smaller domain, where we interpret a table as a function.
val subtract : 'a table * Set.t → 'a table: subtract returns the table of $\{ (k \mapsto v) \in t | k \notin s \}$. The name is motivated by the notion of a domain subtraction on a function.
val $ : (Key.t * 'a) → 'a table: An alias for singleton.