The TABLE signature

Overview

Tables are mappings of keys to values. They can be defined formally as a set of key-value pairs, but we choose to denote tables as sets of mappings $(k \mapsto v)$. The key type is fixed by the Key substructure while the value type is polymorphic. Tables do not contain duplicate keys, and therefore each table associates a unique value with each key it contains. 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 α t
type α table = α t

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

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

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

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

val map : (α → β) → α table → β table
val mapKey : (Key.t * α → β) → α table → β table
val filter : (α → bool) → α table → α table
val filterKey : (Key.t * α → bool) → α table → α table

val reduce : (α * α → α) → α → α table → α
val iterate : (β * α → β) → β → α table → β
val iteratePrefixes : (β * α → β) → β → α table → (β table * β)

val union : (α * α → α) → α table * α table → α table
val intersection : (α * β → γ) → α table * β table → γ table
val difference : α table * β table → α table

val restrict : α table * Set.t → α table
val subtract : α table * Set.t → α table

val $ : (Key.t * α) → α table

Substructures

structure Key : EQKEY

The Key substructure defines the key type of tables, providing equality and other useful functions.

structure Seq : SEQUENCE

The Seq substructure defines the sequence type to and from which tables can be converted.

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

The Set substructure contains operations on sets with elements of type Key.t.

Types

type α t

The abstract table type.

type α table = α t

An alias for α t, for readability.

Values

val size : α table → int

Return the number of key-value pairs in a table.

val domain : α table → Set.t

Return the set of all keys in a table.

val range : α table → α Seq.t

Return a sequence of all values in a table. The order of the elements is implementation-defined.

val toString : (α → string) → α table → string

(toString f t) evaluates to a string representation of $t$ where each key is converted to a string with Key.toString and each value is converted with $f$. For example, the table $\{ (1 \mapsto 2), (3 \mapsto 42) \}$ might be represented by the string “{(1->2),(3->42)}“. The ordering of key-value pairs in the resulting string is implementation-defined.

val toSeq : α table → (Key.t * α) Seq.t

Return a sequence of all key-value pairs in a table. The order of the sequence is implementation-defined.

val find : α table → Key.t → α option

(find t k) returns (SOME $v$) if $(k \mapsto v) \in t$, and NONE otherwise.

val insert : α table * (Key.t * α) → α table

(insert (t, (k, v))) returns the table $t \cup \{(k \mapsto v)\}$ where $v$ is given precedence over $v'$ if there already exists a $(k \mapsto v') \in t$.

val insertWith : (α * α → α) → α table * (Key.t * α) → α table

(insertWith f (t, (k, v))) returns the table $t \cup \{(k \mapsto v)\}$ if $k$ is not already a member of $t$, otherwise it returns $t \cup \{(k \mapsto f (v', v))\}$ where $(k \mapsto v') \in t$.

val delete : α table * Key.t → α table

(delete (t, k)) deletes $k$ only if it is present in $t$. That is, it evaluates to $t \setminus \{(k \mapsto v)\}$ if $(k \mapsto v) \in t$. Otherwise, it evaluates to $t$.

val empty : unit → α table

Construct the empty table.

val singleton : Key.t * α → α table

(singleton (k, v)) evaluates to the singleton table $\{(k \mapsto v)\}$.

val tabulate : (Key.t → α) → Set.t → α table

(tabulate f x) evaluates to the table $\{ (k \mapsto f(k)) : k \in x \}$.

val collect : (Key.t * α) Seq.t → α Seq.t table

(collect s) takes a sequence of key-value pairs and associates each unique key with all values that were originally paired with it.

val fromSeq : (Key.t * α) Seq.t → α 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 : (α → β) → α table → β table

(map f t) returns the table $\{ (k \mapsto f(v)) : (k \mapsto v) \in t \}$.

val mapKey : (Key.t * α → β) → α table → β table

(mapKey f t) returns the table $\{ (k \mapsto f(k, v)) : (k \mapsto v) \in t \}$.

val filter : (α → bool) → α table → α table

(filter p t) returns the table containing every $(k \mapsto v) \in t$ which satisfies $p(v)$.

val filterKey : (Key.t * α → bool) → α table → α table

(filterKey p t) returns the table containing every $(k \mapsto v) \in t$ which satisfies $p(k, v)$.

val reduce : (α * α → α) → α → α table → α

(reduce f b t) is logically equivalent to (Seq.reduce f b (range t)).

val iterate : (β * α → β) → β → α table → β

(iterate f b t) is logically equivalent to (Seq.iterate f b (range t)).

val iteratePrefixes : (β * α → β) → β → α table → (β table * β)

(iteratePrefixes f b t) is logically equivalent to (fromSeq p, x) where $(p, x)$ = (Seq.iteratePrefixes f b (range t)).

val union : (α * α → α) → α table * α table → α 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 : (α * β → γ) → α table * β table → γ 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 : α table * β table → α table

(difference (a, b)) evaluates to the table $a \setminus b$.

val restrict : α table * Set.t → α table

restrict is basically an alias for intersection in that it restricts a table's domain by the elements of a set. The name is motivated by the interpretation of a table as a function, and therefore (restrict (t, x)) evaluates to $t\,|_x$.

val subtract : α table * Set.t → α table

subtract is basically an alias for difference in that it removes all mappings whose keys are given in a set. The name is once again motivated by the interpretation of a table as a function, where (subtract (t, x)) performs the domain subtraction of $t$ by $x$. This is also sometimes referred to as the domain anti-restriction.

val $ : (Key.t * α) → α table

An alias for singleton.