|START Conference Manager|
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)