Skip to content

Instantly share code, notes, and snippets.

View acowley's full-sized avatar

Anthony Cowley acowley

  • Philadelphia, PA, USA
View GitHub Profile
let
platform = crossPkgs.platforms.armv7l-hf-multiplatform;
crossSystem = {
config = "arm-linux-gnueabihf";
platform = platform;
libc = "glibc";
arch = "arm";
float = "hard";
fpu = "vfp";
{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, DataKinds, PolyKinds, TypeOperators, ScopedTypeVariables #-}
-- Lots of ways you can phrase this, but this works for me
-- For folks who haven't seen it before, this is "the essence of the sum type" and sigma stands for sum.
-- You see it far more often in dependent types than elsewhere because it becomes a lot more pleasant to
-- work with there, but it's doable in other contexts too. Think of the first parameter to the data
-- constructor as a generalized "tag" as we talk about in "tagged union", and the second parameter is the
-- "payload". It turns out that you can represent any simple sum type you could write in Haskell this way
-- by using a finite and enumerable `f`, but things can get more unusual when `f` isn't either. In such
-- cases, it's often easier to think of this as the essence of existential types.
// The two sweetspots are 8-bit and 4-bit tags. In the latter case you can fit 14 32-bit keys in
// a cacheline-sized bucket and still have one leftover byte for metadata.
// As for how to choose tags for particular problems, Google's Swiss table and Facebook's F14 table
// both use hash bits that weren't used for the bucket indexing. This is ideal from an entropy perspective
// but it can be better to use some particular feature of the key that you'd otherwise check against anyway.
// For example, for 32-bit keys (with a usable sentinel value) you could use the 8 low bits as the tag
// while storing the remaining 24 bits in the rest of the bucket; that fits 16 keys per bucket. Or if the keys
// are strings you could store the length as the discriminator: with an 8-bit tag, 0 means an empty slot,
// 1..254 means a string of that length, and 255 means a string of length 255 or longer. With a 4-bit tag