There was a thread on mastodon recently where Conor Mcbride was discussing some really cool stuff. I think the intent was to get at something more interesting, but this is the first place I’ve seen thinnings explained in a way without too many complex trappings around and it really clicked with me. I think I had a primed mind to see something useful to my current set of problems and solutions there. It unlocked a torrent of ideas related to lambda egraphs and generalized unions finds that I’m quite excited to talk about in the next couple posts.
But first we need to lay some ground work and discuss thinnings.
I’ve seen thinnings before as some mystifying Agda inductive with no obvious relevance to anything that could be useful to me. But they are a perfectly sensible mathematical object and do not have to be relegated to only usage in dependent type theory. You can perfectly well talk about them in Python or any profane (profane is intended as both compliment and criticism) language of your choosing.
A couple intuitive highlights:
Thinnings are witness data to a sublist question
Thinnings are visualizable as non overlapping strings going between n->m slots in an increasing way
Thinnings are representable as bool lists / bitvectors
Thinnings are the bulk clumping / compaction of de bruijn lifting and lowering operations like how permutations are the clumping of many swaps. Another way of saying it is that they are generated by them. Thinnings, like many actions, can be composed t . s , not just applied t(s(x)) . This is often a very small but also a very big shift in perspective.
Thinnings as Sublist Witnesses
I like thinking about “witness data” https://www.philipzucker.com/proof_objects/ . Given the witness data, some problem becomes easier in some sense to do (often an improvement in decidability or big O complexity, but I also accept a subjective “just becomes easier to think about”). Some examples of such data
... continue reading