The TABLE signature

« 210 Library Documentation

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.