The SEQUENCE signature

Overview

structure ArraySequence

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

type 'a seq
type 'a ord = 'a * 'a -> order
datatype 'a listview = NIL | CONS of 'a * 'a seq
datatype 'a treeview = EMPTY | ELT of 'a | NODE 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 map2 : ('a * 'b -> 'c) -> 'a seq -> 'b seq -> 'c seq
val zip : 'a seq -> 'b seq -> ('a * 'b) 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 inject : (int * 'a) seq -> '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 showl : 'a seq -> 'a listview
val showt : 'a seq -> 'a treeview

val iter : ('b * 'a -> 'b) -> 'b -> 'a seq -> 'b
val iterh : ('b * 'a -> 'b) -> 'b -> 'a seq -> 'b seq * 'b
val reduce : ('a * 'a -> 'a) -> 'a -> 'a seq -> 'a
val scan : ('a * 'a -> 'a) -> 'a -> 'a seq -> 'a seq * 'a
val scani : ('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 list -> 'a seq

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$.