Sorting and Searching by Distribution: From Generic Discrimination to Generic Tries

Fritz Henglein
University of Copenhagen

Abstract.

A discriminator partitions values associated with keys into groups listed in
ascending order. Discriminators can be defined generi- cally by structural
recursion on representations of ordering relations. Employing type-indexed
families we demonstrate how tries with an optimal- time lookup function can be
constructed generically in worst-case linear time. We provide generic
implementations of comparison, sorting, discrimination and trie building
functions and give equational proofs of correctness that highlight core
relations between these algorithms.

Joint work with Ralf Hinze, University of Oxford.