The SEQUENCE signature

Overview

A sequence is an ordered finite list of elements, indexed by natural numbers. The SEQUENCE signature defines such a sequence type and provides a number of operations and predicates on values of that type. If $s$ is a sequence with $n$ elements, we may denote $s$ with the notation $\langle s_0, s_1, \ldots, s_{n-1} \rangle$ where $s_i$ is the $i^{th}$ element of $s$ and the length of $s$ is written $|s|=n$.

Interface

Types

type 'a seq

This is the abstract type that represents a sequence as described in the overview.

type 'a ord = 'a * 'a -> order

This type represents an ordering on the type 'a as a function from pairs of elements to order.

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

A listview provides a view of the abstract sequence type as a list.

datatype 'a treeview = EMPTY | ELT of 'a | NODE of 'a seq * 'a seq

A treeview provides a view of the abstract sequence type as a tree.

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^{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

(toList s) converts a sequence to its logically equivalent, index-preserving list form.

val toString : ('a -> string) -> 'a seq -> string

(toString elemToStr s) evaluates to a string representation of $s$. This representation begins with “<”, followed by the results of applying elemToStr to each element of $s$ in ascending index order interleaved with “,”, and ends with “>”.

val equal : ('a * 'a -> bool) -> 'a seq * 'a seq -> bool

(equal elemEq (x, y)) evaluates to true if $x$ and $y$ contain the same elements, where element equality is determined by elemEq.

val empty : unit -> 'a seq

(empty()) evaluates to $\langle\rangle$, the empty sequence.

val singleton : 'a -> 'a seq

(singleton x) evaluates to $\langle x\rangle$, the sequence containing only the element $x$.

val tabulate : (int -> 'a) -> int -> 'a seq

(tabulate f n) evalutes to a $n$-length sequence $s$ where each element $s_i$ is the result of evaluating $f(i)$. Raises Size if $n<0$.

val fromList : 'a list -> 'a seq

(fromList l) evaluates to the index-preserving sequence representation of $l$.

val rev : 'a seq -> 'a seq

(rev s) reverses the ordering of elements in $s$.

val append : 'a seq * 'a seq -> 'a seq

(append (x, y)) evaluates to the sequence which is the concatenation of $x$ and $y$.

val flatten : 'a seq seq -> 'a seq

(flatten s) evaluates to the sequence which is the concatenation of all sequences in $s$ in the order that they appear in $s$.

val filter : ('a -> bool) -> 'a seq -> 'a seq

(filter p s) evaluates to the longest subsequence $s'$ of $s$ such that $p(e)$ evaluates to true for every element $e$ of $s'$.

val map : ('a -> 'b) -> 'a seq -> 'b seq

(map f s) evaluates to the sequence $r$ where each $r_i$ is the result of applying $f$ to $s_i$.

val map2 : ('a * 'b -> 'c) -> 'a seq -> 'b seq -> 'c seq

(map2 f x y) evaluates to the sequence $r$ such that $r_i$ is the result of applying $f$ to the pair ($x_{i}$, $y_{i}$) for all valid indices $i$ into both $x$ and $y$. It follows from the definition that $|r| = \mathsf{min}(|x|,|y|)$.

val zip : 'a seq -> 'b seq -> ('a * 'b) seq

zip is logically equivalent to (map2 (fn x => x)).

val enum : 'a seq -> (int * 'a) seq

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

val filterIdx : ((int * 'a) -> bool) -> 'a seq -> 'a seq

(filterIdx p s) evaluates to a subsequence which contains all elements $s_i$ of $s$ for which $p (i,\:s_i)$ evaluates to true.

val mapIdx : ((int * 'a) -> 'b) -> 'a seq -> 'b seq

(mapIdx f s) evaluates to the sequence $r$ where each $r_i$ is the result of evaluating $f (i,\:s_i)$.

val inject : (int * 'a) seq -> 'a seq -> 'a seq

If $updates$ is a sequence of index-value pairs, (inject updates s) evaluates to a sequence with updated values of $s$ as given by $updates$. If there are duplicate indices in $updates$, the last one is written and the others are ignored. Raises Range if any indices are out-of-bounds.

val subseq : 'a seq -> int * int -> 'a seq

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

val take : 'a seq * int -> 'a seq

(take (s, n)) evaluates to the contiguous subsequence containing the first $n$ elements of $s$. Raises Size if $n<0$, or raises Range if $n>|s|$.

val drop : 'a seq * int -> 'a seq

(drop (s, n)) evaluates to the contiguous subsequence containing the last $|s|-n$ elements of $s$. Raises Size if $n>|s|$, or raises Range if $n<0$.

val showl : 'a seq -> 'a listview

If s is an empty sequence, (showl s) evaluates to NIL. Otherwise, (showl s) evaluates to CONS ($s_0,\:s'$), where $s'$ is the contiguous subsequence containing the last $|s|-1$ elements of $s$.

val showt : 'a seq -> 'a treeview

If s is an empty sequence, (showt s) evaluates to EMPTY. If s is a singleton sequence, (showt s) evaluates to ELT $s_0$. Otherwise, (showt s) evaluates to NODE (take (s, $|s|$ div 2), drop (s, $|s|$ div 2)).

val iter : ('b * 'a -> 'b) -> 'b -> 'a seq -> 'b

(iter f b s) computes the iteration of $f$ on $s$ with left-association and $b$ as the base case. If $|s|=0$, (iter f b s) evaluates to $b$. Otherwise, it is logically equivalent to

$f(\dots f(f(b,~ s_0),~ s_1) \dots,~ s_{n-1})$

val iterh : ('b * 'a -> 'b) -> 'b -> 'a seq -> 'b seq * 'b

iterh is a generalization of iter that also computes the sequence of all partial results produced by the iterated application of $f$. That is, (iterh f b s) is logically equivalent to

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

Note that the first element in the tuple does not include the application of $f$ on the last element of $s$, but instead has $b$ as its first element.

val reduce : ('a * 'a -> 'a) -> 'a -> 'a seq -> 'a

If $|s|=0$, (reduce f b s) evaluates to $b$. Otherwise, the reduce tree of the sequence $s$ is defined as the divide and conquer tree formed by recursively splitting $s$ in half until singleton elements at the leaves are reached (see showt). The $f$-reduced value $v$ over this tree is then combined with the base case $b$ and (reduce f b s) evaluates to $f(b,\:v)$. For associative functions $f$, (reduce f b s) is logically equivalent to (iter f b s).

val scan : ('a * 'a -> 'a) -> 'a -> 'a seq -> 'a seq * 'a

If $f$ is an associative function and $b$ is a left-identity of $f$, (scan f b s) is logically equivalent to

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

val scani : ('a * 'a -> 'a) -> 'a -> 'a seq -> 'a seq

If $f$ is an associative function and $b$ is a left-identity of $f$, (scani f b s) is logically equivalent to

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

val sort : 'a ord -> 'a seq -> 'a seq

(sort cmp s) sorts the elements of $s$ with respect to $cmp$.

val merge : 'a ord -> 'a seq -> 'a seq -> 'a seq

If $x$ and $y$ are sorted sequences with respect to $cmp$, (merge cmp x y) evaluates to an $|x|+|y|$-length sequence which contains the elements of $x$ and $y$ sorted with respect to $cmp$. The behavior of merge is undefined if $x$ and $y$ are not both sorted.

val collect : 'a ord -> ('a * 'b) seq -> ('a * 'b seq) seq

(collect cmp s) evaluates to a sequence of sequences where each unique first component of elements of $s$ is paired with the sequence of second components of elements of $s$. The resulting sequence is sorted by the first components with respect to $cmp$. The elements in the second components appear in their original order in $s$.

val collate : 'a ord -> 'a seq ord

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

val argmax : 'a ord -> 'a seq -> int

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