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 'a t
type 'a seq = 'a t
type 'a ord = 'a * 'a → order
datatype 'a listview = NIL | CONS of 'a * 'a seq
datatype 'a treeview = EMPTY | ONE of 'a | PAIR of 'a seq * 'a seq

exception Range
exception Size

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

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

val rev : 'a seq → 'a seq
val append : 'a seq * 'a seq → 'a seq
val flatten : 'a seq seq → 'a seq

val filter : ('a → bool) → 'a seq → 'a seq
val map : ('a → 'b) → 'a seq → 'b seq
val zip : 'a seq * 'b seq → ('a * 'b) seq
val zipWith : ('a * 'b → 'c) → 'a seq * 'b seq → 'c seq

val enum : 'a seq → (int * 'a) seq
val filterIdx : (int * 'a → bool) → 'a seq → 'a seq
val mapIdx : (int * 'a → 'b) → 'a seq → 'b seq
val update : 'a seq * (int * 'a) → 'a seq
val inject : 'a seq * (int * 'a) seq → 'a seq

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

val iterate : ('b * 'a → 'b) → 'b → 'a seq → 'b
val iteratePrefixes : ('b * 'a → 'b) → 'b → 'a seq → 'b seq * 'b
val iteratePrefixesIncl : ('b * 'a → 'b) → 'b → 'a seq → 'b seq
val reduce : ('a * 'a → 'a) → 'a → 'a seq → 'a
val scan : ('a * 'a → 'a) → 'a → 'a seq → 'a seq * 'a
val scanIncl : ('a * 'a → 'a) → 'a → 'a seq → 'a seq

val sort : 'a ord → 'a seq → 'a seq
val merge : 'a ord → 'a seq * 'a seq → 'a seq
val collect : 'a ord → ('a * 'b) seq → ('a * 'b seq) seq
val collate : 'a ord → 'a seq ord
val argmax : 'a ord → 'a seq → int

val $ : 'a → 'a seq
val % : 'a list → 'a seq

Types

type 'a t

type 'a seq = 'a t

The abstract sequence type 'a t has elements of type 'a. The alias 'a seq is for readability.

type 'a ord = 'a * 'a → order

An ordering on type 'a, for readability.

datatype 'a listview = NIL | CONS of 'a * 'a seq

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

datatype 'a treeview = EMPTY | ONE of 'a | PAIR of 'a seq * 'a 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 : 'a seq → int → 'a

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

val length : 'a seq → int

length s evaluates to $|s|$, the number of elements in $s$.

val toList : 'a seq → 'a list

Produces an index-preserving list representation of a sequence.

val toString : ('a → string) → 'a seq → string

toString f s produces a string representation of $s$. Each element of $s$ is converted to a string via $f$.

For example, (toString Int.toString $\langle 1,2,3 \rangle$) evaluates to the string “<1,2,3>”.

val equal : ('a * 'a → bool) → 'a seq * 'a seq → bool

equal f (s, t) returns whether or not $s$ and $t$ contain exactly the same elements, in the same order.

Individual element pairs are compared for equality with $f$.

val empty : unit → 'a seq

Construct an empty sequence.

val singleton : 'a → 'a seq

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

val tabulate : (int → 'a) → int → 'a 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 : 'a list → 'a seq

Produces an index-preserving sequence representation of a list.

val rev : 'a seq → 'a seq

rev s reverses the indexing of a sequence. That is, nth (rev s) i is equivalent to nth s (length s - i - 1).

val append : 'a seq * 'a seq → 'a seq

Concatenate two sequences.

val flatten : 'a seq seq → 'a 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 : ('a → bool) → 'a seq → 'a seq

filter p s evaluates to the subsequence of $s$ which contains every element satisfying the predicate $p$.

val map : ('a → 'b) → 'a seq → 'b seq

map f s applies $f$ to each element of $s$. It is logically equivalent to tabulate (f o nth s) (length s).

val zip : 'a seq * 'b seq → ('a * 'b) seq

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

val zipWith : ('a * 'b → 'c) → 'a seq * 'b seq → 'c seq

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

val enum : 'a seq → (int * 'a) seq

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

It is logically equivalent to tabulate (fn i => (i, nth s i)) (length s) .

val filterIdx : (int * 'a → bool) → 'a seq → 'a seq

Similar to filter, but also provides the index of each element to the predicate.

filterIdx f s is logically equivalent to map (fn (_, x) => x) (filter f (enum s)) .

val mapIdx : (int * 'a → 'b) → 'a seq → 'b seq

Similar map, but also provides the index of each element.

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

val update : 'a seq * (int * 'a) → 'a seq

update (s, (i, x)) evaluates to the sequence whose $i^\text{th}$ element is $x$, and whose other elements are unchanged from $s$.

If $i$ is out-of-bounds, it raises Range, otherwise it is logically equivalent to tabulate (fn j => if i = j then x else nth s j) (length s) .

val inject : 'a seq * (int * 'a) seq → 'a 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.

When all indices in $u$ are distinct, inject (s, u) is logically equivalent to iterate update s u.

val subseq : 'a seq → int * int → 'a 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.

val take : 'a seq → int → 'a seq

take s n takes the prefix of $s$ of length $n$. It is logically equivalent to subseq s (0, n).

val drop : 'a seq → int → 'a seq

drop s n drops the prefix of $s$ of length $n$. It is logically equivalent to subseq s (n, length s - n).

val splitHead : 'a seq → 'a listview

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

val splitMid : 'a seq → 'a treeview

splitMid s evaluates to EMPTY if $s$ is empty, 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 sizes of $l$ and $r$ are implementation-defined.

val iterate : ('b * 'a → 'b) → 'b → 'a seq → 'b

(iterate f b s) computes the iteration of $f$ on $s$ with left-association, using $b$ as the base case. It is logically equivalent to $$f(\dots f(f(b,~ s[0]),~ s[1]) \dots,~ s[|s|-1])$$

When $s$ is empty, it returns $b$.

iterate op+ 13 (fromList [1,2,3]) evaluates to 19.

val iteratePrefixes : ('b * 'a → 'b) → 'b → 'a seq → 'b seq * 'b

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 : ('b * 'a → 'b) → 'b → 'a seq → 'b seq

Similar to iteratePrefixes, except that the $i^\text{th}$ prefix of iteratePrefixesIncl f b s is inclusive of $s[i]$, rather than exclusive. It is logically equivalent to

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

The return type of iteratePrefixesIncl is slightly different than iteratePrefixes.

val reduce : ('a * 'a → 'a) → 'a → 'a seq → 'a

reduce f b s evaluates to $b$ when $s = \langle \rangle$, $x$ when $s = \langle x \rangle$, and otherwise is logically equivalent to

f (reduce f b l, reduce f b r)

where l = take s (n div 2) and r = drop s (n div 2).

reduce f b s is logically equivalent to iterate f b s when $f$ is associative and $b$ is a corresponding identity.

val scan : ('a * 'a → 'a) → 'a → 'a seq → 'a seq * 'a

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

val scanIncl : ('a * 'a → 'a) → 'a → 'a seq → 'a seq

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

val sort : 'a ord → 'a seq → 'a seq

(sort c s) reorders the elements of $s$ with respect to the comparison function $c$. The output is stable: any two elements considered equal by $c$ will appear in the same relative order in the output as they were in the input.

val merge : 'a ord → 'a seq * 'a seq → 'a seq

For sequences $s$ and $t$ already sorted with respect to c, (merge c (s, t)) is logically equivalent to sort c (append (s, t)).

val collect : 'a ord → ('a * 'b) seq → ('a * 'b seq) seq

collect cmp s takes a sequence $s$ of key-value pairs, deduplicates the keys, sorts them with respect to $c$, and pairs each unique key with all values that were originally associated with it in $s$. The resulting value-sequences retain their relative ordering from $s$.

Collecting $\langle (3,7), (2,6), (1,8), (3,5) \rangle$ produces $\left\langle (1, \langle 8 \rangle), (2, \langle 6 \rangle), (3, \langle 7, 5 \rangle) \right\rangle$.

val collate : 'a ord → 'a seq ord

collate c produces an ordering on sequences, derived lexicographically from c.

val argmax : 'a ord → 'a seq → int

argmax c s produces the index of the maximal value in $s$ with respect to c. Raises Range when $s$ is empty.

val $ : 'a → 'a seq

An alias for singleton.

val % : 'a list → 'a seq

An alias for fromList.