Hey! So you probably came here because you were reading this post and you had some trouble with the notation I was using. Specifically, something like this:

 x :: Functor f => f a
fmap id x  id x

Okay, don’t panic. We can get through this together.

First off, I chose the symbol there so that it doesn’t look like a Haskell function definition: that’s a meta-statement about the behavior of Haskell, not actual Haskell code. Though the expressions on either side of the should be interpreted as Haskell code. Um, yeah.

But the first line there is probably what gave you pause.

In case you haven’t seen it before, is the symbol for universal quantification. You usually read it in English as “for all,” “for every,” or “for any.”

After that, there’s a variable with a type declaration (:: stuff). That means that I’m not talking about all values, just all values of a certain type.

So you can read a statement like ∀ x :: Int, x < 0 || x >= 0 as follows:

For all x where x has type Int, either x is less than 0 or x is greater than or equal to 0.

Or, less formally:

All Ints are either less than 0 or they’re greater than or equal to 0.

Exciting stuff.


The Functor law above could also be written like this:

∀ a :: (Any Haskell type)
∀ f :: Functor
∀ x :: f a
fmap id x ≡ x

Which makes it a little easier (though verbose) to translate into English:

For all a where a is a Haskell type, for all f where f is a Functor type constructor, and for all x where x is of type f a, the expression fmap id x should be equal to x.

But universal quantification is implied when you use a Haskell type variable like this:

x :: Functor f => f a

There’s sort of an implicit around the a and the f there. After all, if we were talking about a specific Functor, we would have written that.


Now let’s return to the law as I originally wrote it:

 x :: Functor f => f a
fmap id x  id x

And try to make sense of it with some concrete examples:

And so on, ∀ Functors and ∀ values you can think of.

Now back to your regularly scheduled programming.