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 \}$.

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.