theory

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.

What’s a Fixpoint? For some reason, functional programming seems to have developed a reputation for using confusing and/or complex names to describe various concepts. I recall this being more or less my impression as I transitioned from the “standard” OOP+imperative style into functional programming, so I’d like to start dispelling some of the confusion. This piece will talk through one of the basic, albeit more obscure, building blocks for functional programming that was a bit intimidating upon my first contact with it.

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.

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?

A few weeks ago I gave a talk at work about Lambda Calculus. I had intended to speak only about the Y-combinator (post about that is forthcoming), but ended up spending two-thirds of my time rushing through an explanation of the untyped Lambda Calculus. Afterwards a few teammates suggested that the material in that talk would be better served with a blog post, so here we are. The untyped lambda calculus isn’t particularly useful for day-to-day programming unless you happen to work in language design, but its fascinating and well worth a trip down the rabbit hole.