This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| let | |
| platform = crossPkgs.platforms.armv7l-hf-multiplatform; | |
| crossSystem = { | |
| config = "arm-linux-gnueabihf"; | |
| platform = platform; | |
| libc = "glibc"; | |
| arch = "arm"; | |
| float = "hard"; | |
| fpu = "vfp"; |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# 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. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // 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 |
OlderNewer