START Conference Manager    

Generic Discrimination---Sorting and Partitioning Unshared Data in Linear Time

Fritz Henglein

The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP 2008)
Victoria, British Columbia, Canada, September 22-24, 2008

Abstract

We introduce the notion of discriminator as a generalization of both sorting and partitioning. Discriminators are indexed by denotations for (total pre)orders. The language of denotations allows definition of structural equivalence, lexicographic ordering, equivalence/ordering of lists under commutativity, idempotence (bag and set equivalence), and more.

We show that worst-case linear-time discriminators can be defined generically, by induction on the term language. The inductive definition yields a generic discriminator that encapsulates and generalizes both distributive sorting and multiset discrimination for strings and trees. We demonstrate that discriminators can be coded compactly using list comprehensions and Generalized Algebraic Data Types (GADTs). We give some examples of the uses of discriminators, including few-line specifications of recently discovered optimal time algorithms.

We use these results to argue that ordered (abstract) types or types with equality, specifically primitive types in programming languages, should expose their ordering relation/equality as a (sorting) discriminator, not a comparison function/equality test.

START Conference Manager (V2.54.6)