1. 23
    1. 2

      skimmed. this is a very real problem. taking a step back from the limitations of extant program optimisers—we would like to be able to optimise algorithms and data structures. but while the ‘hard’ requirements a hash table has of its hashing functions are fairly easy to state, verify, and preserve—no abstract side effects—the ‘soft’ requirements (hash quality) are harder (if they weren’t, it would be easy to synthesise and analyse hash functions).

      that said, i would expect you can get to a fairly good place by specifying some basic axioms for transforming the abstract ‘schedules’ of particular families of hash functions—probably just ordering/decomposition and queueing?—the idea being that:

      1. the ‘hard’ properties of the axioms (that they maintain abstract purity) can be verified mechanically (so no matter what hashing schedule the optimiser picks, the hash table will never give incorrect results)
      2. the ‘soft’ properties will not be mechanically verified (so you can go quadratic), but
      3. the human will attempt to design the axioms so that no application of them can ruin hash quality; and so the optimiser can, as usual, just pick the schedule that it thinks will run the fastest

      it’s not a panacea though. i designed a hash table a while ago that was a variant of swisstable using polymur (hi @orlp) specialised to keys of a couple words, and i fused hashing with length reduction in a way that weakened the hash slightly. i determined that this was unlikely to affect the performance of the table, but doing that kind of thing generically seems challenging

      1. 1

        @orlp

        huh i thought he had a lobsters acct. can’t find it. guess not