The `ORDTABLE` signature

Overview

The ORDTABLE 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.

This interface is nearly identical to SET except for the following:

The Key substructure now ascribes to ORDKEY.

The Set substructure now ascribes to ORDSET.

There is additional functionality relying upon the ordering of keys, such as split, join, and getRange.
The toSeq function now specifies that it returns keys in sorted order.

Interface

structure Key : ORDKEY
structure Seq : SEQUENCE

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

exception Order

structure Set : ORDSET 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

val first : 'a table → (Key.t * 'a) option
val last : 'a table → (Key.t * 'a) option

val prev : 'a table * Key.t → (Key.t * 'a) option
val next : 'a table * Key.t → (Key.t * 'a) option

val split : 'a table * Key.t → 'a table * 'a option * 'a table
val join : 'a table * 'a table → 'a table

val getRange : 'a table → Key.t * Key.t → 'a table

val rank : 'a table * Key.t → int
val select : 'a table * int → (Key.t * 'a) option
val splitRank : 'a table * int → 'a table * 'a table

Substructures

structure Key : ORDKEY: The Key substructure defines the key type of tables, which are totally ordered according to the provided comparison function.
structure Seq : SEQUENCE: The Seq substructure defines the underlying sequence type, so that we may convert tables to and from sequences.
structure Set : ORDSET 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.

Exceptions

exception Order: Order is raised when the ordering invariant would be violated.

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 in sorted order of the keys they were associated with.
val toString : ('a → string) → 'a table → string: toString f t returns a string representation of $t$. Each key is converted to a string via Key.toString and each value is converted via $f$.
val toSeq : 'a table → (Key.t * 'a) Seq.t: Return a sequence of all key-value pairs in a table, sorted by key.
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.
val first : 'a table → (Key.t * 'a) option: Return the smallest key of a table (together with its associated value), or NONE if the table is empty.
val last : 'a table → (Key.t * 'a) option: Return the largest key of a table (together with its associated value), or NONE if the table is empty.
val prev : 'a table * Key.t → (Key.t * 'a) option: prev (t, k) returns the largest key (together with its associated value) in $t$ which is strictly less than $k$, or NONE if there is no such key.
val next : 'a table * Key.t → (Key.t * 'a) option: next (t, k) evaluates to the smallest key (together with its associated value) in $t$ which is strictly greater than $k$, or NONE if there is no such key.
val split : 'a table * Key.t → 'a table * 'a option * 'a table: split (t, k) evaluates to $(l, v, r)$, where $l$ consists of all key-value pairs with keys strictly smaller than $k$, $r$ consists of all key-value pairs with keys strictly greater than $k$, and $v$ is $k$'s associated value in $t$ (or NONE if $k$ is not present in $t$).
val join : 'a table * 'a table → 'a table: Given tables $a$ and $b$ where every key in $a$ is strictly smaller than every element in $b$, (join (a, b)) evaluates to $a \cup b$. Otherwise, it raises Order.
val getRange : 'a table → Key.t * Key.t → 'a table: getRange t (x, y) evaluates to $\{ (k \mapsto v) \in t\ |\ x \leq k \leq y \}$.
val rank : 'a table * Key.t → int: rank (t, k) evaluates to the number of keys in $t$ which are strictly smaller than $k$.
val select : 'a table * int → (Key.t * 'a) option: select (t, i) evaluates to the $i^\text{th}$ smallest key (together with its associated value) in $t$, or NONE if either $i < 0$ or $i \geq |t|$.
val splitRank : 'a table * int → 'a table * 'a table: splitRank (t, i) evaluates to $(l, r)$, where $l$ consists of the $i$ smallest keys of $t$, and $r$ is the set of the $|t| - i$ largest keys of $t$. Raises Fail if $i < 0$ or $i \geq |t|$.

The ORDTABLE signature