The SEQUENCE signature

Overview

The SEQUENCE signature is a comprehensive interface for a persistent sequence type. We use a number of notational conventions which can be seen here. For example, we write $|s|$ and $s[i]$ for the length and $i^\text{th}$ element of $s$, respectively.

Interface

type α t
type α seq = α t
type α ord = α * α → order
datatype α listview = NIL | CONS of α * α seq
datatype α treeview = EMPTY | ONE of α | PAIR of α seq * α seq

exception Range
exception Size

val nth : α seq → int → α
val length : α seq → int
val toList : α seq → α list
val toString : (α → string) → α seq → string
val equal : (α * α → bool) → α seq * α seq → bool

val empty : unit → α seq
val singleton : α → α seq
val tabulate : (int → α) → int → α seq
val fromList : α list → α seq

val rev : α seq → α seq
val append : α seq * α seq → α seq
val flatten : α seq seq → α seq

val filter : (α → bool) → α seq → α seq
val map : (α → β) → α seq → β seq
val zip : α seq * β seq → (α * β) seq
val zipWith : (α * β → γ) → α seq * β seq → γ seq

val enum : α seq → (int * α) seq
val filterIdx : (int * α → bool) → α seq → α seq
val mapIdx : (int * α → β) → α seq → β seq
val update : α seq * (int * α) → α seq
val inject : α seq * (int * α) seq → α seq

val subseq : α seq → int * int → α seq
val take : α seq → int → α seq
val drop : α seq → int → α seq
val splitHead : α seq → α listview
val splitMid : α seq → α treeview

val iterate : (β * α → β) → β → α seq → β
val iteratePrefixes : (β * α → β) → β → α seq → β seq * β
val iteratePrefixesIncl : (β * α → β) → β → α seq → β seq
val reduce : (α * α → α) → α → α seq → α
val scan : (α * α → α) → α → α seq → α seq * α
val scanIncl : (α * α → α) → α → α seq → α seq

val sort : α ord → α seq → α seq
val merge : α ord → α seq * α seq → α seq
val collect : α ord → (α * β) seq → (α * β seq) seq
val collate : α ord → α seq ord
val argmax : α ord → α seq → int

val $ : α → α seq
val % : α list → α seq

Types

type α t

The abstract sequence type.

type α seq = α t

An alias, for readability.

type α ord = α * α → order

An ordering on type α, for readability.

datatype α listview = NIL | CONS of α * α seq

View of a sequence as though it were a list, with a head and tail. See splitHead.

datatype α treeview = EMPTY | ONE of α | PAIR of α seq * α seq

View of a sequence as though it were a tree with data at the leaves. This is largely a syntactic convenience for 2-way divide-and-conquer algorithms on sequences. See splitMid.

Exceptions

exception Range

Range is raised whenever an invalid index into a sequence is used.

exception Size

Size is raised whenever a function is given a negative size.

Values

val nth : α seq → int → α

(nth s i) evaluates to $s[i]$, the $i^\text{th}$ element of $s$. Raises Range if $i$ is out of bounds.

val length : α seq → int

Return the length (number of elements) of a sequence.

val toList : α seq → α list

Return an index-preserving list representation of a sequence.

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

(toString f s) evaluates to a string representation of $s$. Each element of $s$ is converted to a string by an application of $f$. For example, (toString Int.toString $\langle 1,2,3 \rangle$) evaluates to the string “<1,2,3>”.

val equal : (α * α → bool) → α seq * α seq → bool

(equal f (s, t)) returns whether or not $s$ and $t$ contain exactly the same elements, in the same order. Equality of element pairs is determined by $f$.

val empty : unit → α seq

Construct an empty sequence.

val singleton : α → α seq

(singleton x) evaluates to $\langle x \rangle$.

val tabulate : (int → α) → int → α seq

(tabulate f n) evaluates to the length-$n$ sequence where the $i^\text{th}$ element is given by $f(i)$. Raises Size if $n<0$.

val fromList : α list → α seq

Return an index-preserving sequence representation of a list.

val rev : α seq → α seq

Reverse the indexing of a sequence.

val append : α seq * α seq → α seq

Concatenate two sequences.

val flatten : α seq seq → α seq

Concatenate a collection of sequences in the order they are given. For example, flatten $\langle \langle 1, 2 \rangle, \langle \rangle, \langle 3 \rangle \rangle$ evaluates to $\langle 1, 2, 3 \rangle$.

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

(filter p s) evaluates to the subsequence of $s$ containing every $x \in s$ which satisfies $p(x)$.

val map : (α → β) → α seq → β seq

(map f s) evaluates to a sequence whose $i^\text{th}$ element is given by $f(s[i])$.

val zip : α seq * β seq → (α * β) seq

(zip (s, t)) evaluates to a sequence of length $\min(|s|, |t|)$ whose $i^\text{th}$ element is $(s[i], t[i])$.

val zipWith : (α * β → γ) → α seq * β seq → γ seq

(zipWith f (s, t)) is logically equivalent to (map f (zip (s, t))).

val enum : α seq → (int * α) seq

(enum s) evaluates to a sequence where each element is paired with its index.

val filterIdx : (int * α → bool) → α seq → α seq

(filterIdx p s) evaluates to the subsequence of $s$ containing every $s[i]$ which satisfies $p (i, s[i])$.

val mapIdx : (int * α → β) → α seq → β seq

(mapIdx f s) is logically equivalent to (map f (enum s)).

val update : α seq * (int * α) → α seq

(update (s, (i, x))) evaluates to the sequence for which the $i^\text{th}$ element is $x$, and all other elements are unchanged from $s$. Raises Range if $i$ is out of bounds.

val inject : α seq * (int * α) seq → α seq

inject (s, u) produces a new sequence where, for each $(i,x) \in u$, the $i^\text{th}$ element of s has been replaced with $x$. If there are multiple updates specified at the same index, then all but one of them are ignored non-deterministically. Raises Range if any $(i,\_) \in u$ is out-of-bounds.

val subseq : α seq → int * int → α seq

(subseq s (i, n)) evaluates to the contiguous subsequence of $s$ starting at index $i$ with length $n$. Raises Size if $n<0$. Raises Range if the subsequence is out of bounds or otherwise ill-defined.

val take : α seq → int → α seq

(take s n) is logically equivalent to (subseq s (0, n)).

val drop : α seq → int → α seq

(drop s n) is logically equivalent to (subseq s (n, length s - n)).

val splitHead : α seq → α listview

(splitHead s) evalues to NIL if $s$ is empty, and otherwise is logically equivalent to CONS ($s[0]$, drop $s$ 1).

val splitMid : α seq → α treeview

(splitMid s) evaluates to EMPTY if $s = \langle \rangle$, (ONE $x$) if $s = \langle x \rangle$, and (PAIR ($l, r$)) otherwise, where both $l$ and $r$ are nonempty and their concatenation is $s$. The exact sizes of $l$ and $r$ are implementation-defined.

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

(iterate f b s) computes the iteration of $f$ on $s$ with left-association and $b$ as the base case. If $s = \langle\rangle$, (iterate f b s) evaluates to $b$. Otherwise, it is logically equivalent to \[ f(\dots f(f(b,~ s[0]),~ s[1]) \dots,~ s[|s|-1]) \]

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

(iteratePrefixes f b s) is logically equivalent to

(tabulate (fn i => iterate f b (take s i)) (length s), iterate f b s)

That is, it produces the iteration of $f$ for each prefix of $s$.

val iteratePrefixesIncl : (β * α → β) → β → α seq → β seq

(iteratePrefixesIncl f b s) is logically equivalent to

tabulate (fn i => iterate f b (take s (i+1))) (length s)

Just like iterate, it produces the iteration of $f$ for each prefix of $s$, except that the prefix at the $i^\text{th}$ position is now inclusive of $s[i]$ (whereas iterate is exclusive).

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

(reduce f b s) is logically equivalent to $b$ if $|s| = 0$, $s[0]$ if $|s| = 1$, and

f (reduce f b (take s (n div 2)), reduce f b (drop s (n div 2)))

otherwise where $|s| = n$.

Note that for an associative function $f$ and corresponding identity $b$, (reduce f b s) is logically equivalent to (iterate f b s).

val scan : (α * α → α) → α → α seq → α seq * α

For an associative function $f$ and corresponding identity $b$, (scan f b s) is logically equivalent to

(tabulate (fn i => reduce f b (take s i)) (length s), reduce f b s)

Note that under these assumptions, (scan f b s) is also logically equivalent to (iteratePrefixes f b s).

val scanIncl : (α * α → α) → α → α seq → α seq

For an associative function $f$ and corresponding identity $b$, (scanIncl f b s) is logically equivalent to

tabulate (fn i => reduce f b (take s (i+1))) (length s)

Note that under these assumptions, (scanIncl f b s) is also logically equivalent to (iteratePrefixesIncl f b s).

val sort : α ord → α seq → α seq

(sort cmp s) sorts the elements of $s$ with respect to cmp. The output is stable; that is, any two elements who are considered equal with respect to cmp will appear in the same order in the output as they did in the input.

val merge : α ord → α seq * α seq → α seq

For sequences $s$ and $t$ sorted with respect to cmp, (merge cmp (s, t)) evaluates to the sorted sequence containing all elements of both $s$ and $t$.

val collect : α ord → (α * β) seq → (α * β seq) seq

(collect cmp s) takes a sequence of key-value pairs and associates each unique key with all values that were originally paired with it. The resulting sequence is sorted by keys with respect to cmp, and the ordering of each value sequence reflects the ordering in the original sequence. For example, collecting $\langle (3,7), (2,6), (1,8), (3,5) \rangle$ produces the sequence $\left\langle (1, \langle 8 \rangle), (2, \langle 6 \rangle), (3, \langle 7, 5 \rangle) \right\rangle$.

val collate : α ord → α seq ord

(collate cmp) evaluates to an ordering on sequences derived lexicographically from cmp.

val argmax : α ord → α seq → int

(argmax cmp s) evaluates to the index of a maximal value in $s$ with respect to cmp. Raises Range if $s = \langle\rangle$.

val $ : α → α seq

An alias for singleton.

val % : α list → α seq

An alias for fromList.