Skolem and existential types

In this post I explain what skolem variables are and how they relate to existential quantification. After reading this, you should have an intuition for how skolems work and why existential types are a natural extension from skolems. Lots of talk about existential types lately A couple of months ago a coworker of mine gave a talk on using existential types to address the expression problem. The talk was great and engaging, and provided a nice refresher on working with existentials - this isn’t something I use daily.

Mon May 31, 2021 930 words
Cuckoo Filter: Part 2

The API Due to the way buckets are maintained in cuckoo filters its possible to perform the three basic set operations, insert, delete, and member. Those three operations comprise the api into Data.CuckooFilter in the cuckoo-filter library package. As you’d expect for a data strucure that answers set membership questions, the API behaves exactly like the api for a set, with one big exception. As discussed in part 1, cuckoo filters (and cuckoo hashing in general) store fingerprints in hash buckets.

Sun Jan 27, 2019 1291 words
Cuckoo Filters: Part 1

Approximate Set Membership Several years ago I was hard at work building a near-realtime database of events happening around the world. This was a classic crawling problem, where I’d need to make sure I’m not checking the same location for events twice, or looking for events hosted by the same person twice. Initially the team and I were able to get away with using a regular Set for this, but as we scaled up to handle millions of sources this approach broke down.

Sun Jan 20, 2019 1253 words
Tricky Functor instances

I was recently started reading Thinking with Types and came upon a great explanation of variance and the role it plays in reasoning about functions. You’re probably familiar with Functor, which says that for some t a, if given a function f :: a -> b, you can transform the t a -> t b. Essentially, the essence of “functor-ness” is the ability to transform a result into another type. What about “anti-functorn-ness”, where you want to transform the input rather than the result of a function from a -> b?

Sun Jan 13, 2019 520 words