Types, Tattoos and the Extent of Human Accomplishment

Another day, another post. Considered writing about terrorism, decided against it. I’ll save that for another time when I feel like I haven’t pissed off enough people. (Un?)fortunately that is not today, so instead I’m going to answer the question I probably get asked most often: “what does your tattoo mean?”

I’ve been asked that a few times a week for the last eighteen months, and I have yet to come up with a satisfactory, yet pithy, answer. This blog post aims to serve as at least the satisfactory version of the explanation. It is unlikely to pithy, because we have to talk about arcane mathematics and deep type-theoretical shit. And because I have a daily word quota.

Although it wasn’t my intent when I got it, I have since said that the meaning of this tattoo is to find a wife; I’ve promised myself that any woman who can successfully identify the meaning of my tattoo will be immediately proposed to. You might scoff, but it’s happened. Once. Turns out she was already married, and had a few kids, so she had to politely decline. Also that she had no idea who I was probably helped engender that response. The reason I bring this up, is that if you’re a cutie pie looking for a fantastic husband, you know where to find me, and you’ll soon know what the secret to my heart is.

Anyway, for those of you not in the know, my tattoo looks a lot like this:

map :: (a -> b) -> λa -> λb

Long-time readers who aren’t afraid of math and have great memories might recognize this as looking like a type in Haskell. They’d be right, but we haven’t discussed yet what λ means in this context. If you want a super clear understanding of the math behind my tat, it might be worthwhile refreshing yourself on the first few sections of that. If you don’t, feel free to keep reading; it’s OK; I won’t be offended.

So! What does my tattoo mean, you might have wondered at some point during having known me. The super short answer is: to me, it is why abstraction is possible, or equivalently why we can understand the universe.

The remainder of this post will be a digression into why it means those things. I’ll try to keep it gentle on the math, but, as you would expect from a math tattoo, there will be math. If you really don’t give a shit, and just want to tl;dr, search for “To cut a very long story short”, which is where I summarize what the fuck is going on.

Our first foray into this strange realm of things you’ve never seen before is the symbol ::, which unfortunately is overloaded as hell in programming. In C++ it’s called the scope operator, and rather notoriously, in PHP it’s called T_PAAMAYIM_NEKUDOTAYIM. Fun fact: that used to be my email for a year or two until I realized that nobody ever sent me emails because it was way too much damn work. In this context, we will call :: the type-of operator, and you should read it aloud as “is of type”. It describes a relationship between what’s on the left and what’s on the right of it. As a rule, the thing on the left is an instance of the category on the right.

A few examples will help cement the idea:

• 7 :: Number
• 100001 :: Number
• red :: Color
• garfield :: Cat
• orange :: Color
• sandy :: Person

Here both 7 and 100001 are of type Number, but garfield is a Cat. The type-of operator performs some mental book-keeping for us; it prevents us from comparing things that are incomparable. What do I mean by that? Well it doesn’t make sense to make any comparisons between red and 100001 – they’re of different types, and so comparing them is like the proverbial “comparing apples to oranges.” Except that it’s more egregious and is not to even be considered. Attempting to substitute one type with another is what we call a type error.

If you ever, ever, commit a type error, you’ve done something terribly wrong, and your answer is guaranteed to be not even wrong from there on out. Don’t do it. Just say no.

So, what have we learned so far? Well, we’ve learned that map “is of type” (a -> b) -> λa -> λb. We haven’t made much progress, but now at least we know that map is a thing and that weird math-y lookin’ thing is some category. But what?

We’ll start a little slower, with a motivating example. The arrow -> (read aloud as “to”) is indicative of a transformation of some “sort”. That “sort” turns out to be what you’re transforming from to what you’re transforming into. We express this as From -> To, where From and To are types of some sort.

This sounds a little crazy, but bear with me a little while longer. This weird arrow notation lets us describe some things that are otherwise sorta tricky to talk about. For example, we can think about the idea of a favorite color being a transformation from a Person to a Color.

favoriteColor :: Person -> Color

When we talk about favorite colors like this, it helps reinforce the idea that a favorite color is meaningless without talking about a specific person. There is no such thing as a favorite color existing out there in the universe, absent of any person. It has no platonic form, and it is only meaningful when we discuss the favorite color of someone.

So far, this system of types we’re developing is kinda neat, but it falls down pretty quickly if you push it at all. For example, all of our transformations so far are capable only of transforming one thing into another, but that’s silly. A transformation that is dependent on two things is easy to come up with. How about addition? a + b = c. Here, addition is a transformation from two numbers into a third. We will write this in our type system as:

add :: Number -> (Number -> Number)

which should be read as “add is of type Number to Number to Number”. I cover the mechanics behind this a little better in my post on type systems, which is a good place to read more about this if you care.

Let’s go back to our friend map :: (a -> b) -> λa -> λb, which if we put the parentheses in like we did for add, becomes map :: (a -> b) -> (λa -> λb). This, it seems, is more comprehensible: it’s a transformation from a transformation to another transformation. Progress, even if only slightly.

So what is a -> b? Why, a transformation from a to b, obviously. But… what is a? Well, a is a variable, in the same way that x is in algebra, and as such, it can refer to any other type. That means 7 :: a where a ~ Number, or garfield :: a where a ~ Cat. Here, ~ means “type equivalent”, which is to say, these types are the same thing.

There’s a subtle gotcha here, though. Just like in algebra x can be sometimes equal to 5 or sometimes equal to 10, it can’t be equal to both 5 and 7 simultaneously. x is best understood as a name for a substance whose value you don’t know, but you do know that it isn’t going to pull a fast one on you and change its identity. a is the same thing here; in some contexts it can be Cat, but in others it might be Color, but it is never both simultaneously.

What you’re going to hate me for, is that sometimes a is even Number -> (Color -> Person) or something crazy like that. a is any type. OK cool. So what’s b? Well, b is also any type. We use b instead of a to indicate that b and a are not necessarily the same type. They can be, but they don’t have to be.

Thus, a -> b is actually a transformation from any type to any other type. To me, though, a -> b is the type of thinking, or of an idea. If you take a squinty look at it, the process of having ideas is nothing more than a transformation from what you know into something else.

If you want to take it further, a -> b is the type of most actions in life. Eating is Food -> Energy; writing is Thoughts -> Text; I’m sure you get the picture.

We’re almost at the home stretch! map is of type Idea -> (λa -> λb). Notice that λa -> λb looks very similar to a -> b, except for those funny lambdas in the way. In fact, the as and bs refer to the same types in both transformations. So what is λ, then?

Intuitively, λ is a context, it’s the result of applying an abstract idea to something in particular. You could interpret λ as “having a resulting effect on the universe”, or something like that. In this sense, map can be seen as a transformation from an idea into reality.

Mathematically, λ is a functor, which is to say, a transformation over transformations, which preserves the “intent” of the transformation in some sense. It’s kinda sloppy to do so, but we could consider a functor to be something like Spanish:

writeInSpanish :: (Thoughts -> Text) -> (Spanish Thoughts -> Spanish Text)

You can see that writing in Spanish has the same “intent” as writing; they’re both transformations from Thoughts to Text, though when you do it in Spanish, there is an extra Spanish context that you need to keep around to ensure you don’t commit any type errors. You can also imagine something similar for German:

writeInGerman :: (Thoughts -> Text) -> (German Thoughts -> German Text)

This example isn’t fantastic, but that’s the problem with real life examples; we’re really used to doing this stuff fast-and-loose in our heads that trying to formalize it sounds confusing and unnecessary. I don’t have a solution for this unfortunately. I’m not sure if one exists, honestly.

Let’s look at the type of writeInSpanish again: (Thoughts -> Text) -> (Spanish Thoughts -> Spanish Text). It looks kind of familiar, no? Apply the following substitutions:

• writeInSpanish :: (Thoughts -> Text) -> (Spanish Thoughts -> Spanish Text), but let a ~ Thoughts
• writeInSpanish :: (a -> Text) -> (Spanish a -> Spanish Text), but let b ~ Text
• writeInSpanish :: (a -> b) -> (Spanish a -> Spanish b), but let λ ~ Spanish
• writeInSpanish :: (a -> b) -> (λa -> λb)

So it turns out that writeInSpanish :: (a -> b) -> (λa -> λb). Interesting. You can also do the same thing for writeInGerman. Hmmm. It looks like (a -> b) -> (λa -> λb) might be interesting for some deeper reasons than we’ve looked at so far.

If you look at doTheSameThingToEverythingInMyCollection :: (a -> b) -> ([a] -> [b]) where [a] is understood to be a collection of as (and likewise for b), we can look at this as lifting some transformation from a to b into a transformation from collections of a into collections of b. Here the context is “collections”, and if you let λ ~ [], we again get (a -> b) -> (λa -> λb).

To cut a very long story short, map, as it turns out, is the only primitive inhabitant of this weird type (a -> b) -> (λa -> λb). map is the fundamental transformation from ideas into contexts. Construction work is an example of using map to turn building blueprints into buildings. Applied mathematics is an example of using map to turn the boring stuff you learned in algebra class into getting the right answer when you grab two handfuls of apples, and for some reason, they add together.

map is the reason our thoughts can reflect reality. map is the reason abstract thought is possible. map is how we can understand things we can’t directly see with our senses. map is why we experience causality. It’s all of these things, and it’s much, much more general than all of those things. But those are the reasons I like it. To me, map is the only reason we humans are capable of being capable of anything. It’s the pure, unadulterated essence of all of our accomplishments. It’s human thought, boiled down into a pithy one-liner tattoo.

That’s what my tattoo means.