We introduce the notion of discrimination as a generalization of
both sorting and partitioning and show that discriminators (discrimination
functions) can be dened generically, by structural recursion
on order and equivalence expressions denoting a rich class of total preorders
and equivalence relations, respectively.
Discriminators improve the asymptotic performance of generic comparison-
based sorting and partitioning, yet do not expose more information
than the underlying ordering relation, respectively equivalence.
For a large class of order and equivalence expressions, including all
standard orders for rst-order recursive types, the discriminators execute
in worst-case linear time.
The generic discriminators can be coded compactly using list comprehensions,
with order expressions specied using Generalized Algebraic
Data Types (GADTs). We give some examples of the uses of discriminators,
including a new most-signicant-digit lexicographic sorting
algorithm and type isomorphism with an associative-commutative
operator. Full source code of discriminators and their applications is
included.1
We argue discriminators should be basic operations for primitive
and abstract types with equality. The basic multiset discriminator for
references, originally due to Paige et al., is shown to be both ecient
and fully abstract: it nds all duplicates of all references occurring
in a list in linear time without leaking information about their representation.
In particular, it behaves deterministically in the presence
of garbage collection and nondeterministic heap allocation even when
references are represented as raw machine addresses. In contrast, having
only a binary equality test as in ML requires (n2) time, and
allowing hashing for performance reasons as in Java, makes execution
nondeterministic and complicates garbage collection.