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

A discriminator partitions values associated with keys into groups listed in ascending order. Discriminators can be defined generically 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