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:

• fmap id Nothing should be equal to Nothing (with Maybe as f and Int as a).
• fmap id (Just "hello") should be equal to Just "hello" (with Maybe as f and String as a).
• fmap id [1, 2, 3] should be equal to [1, 2, 3] (with [] as f and Int as a)
• fmap id succ should be equal to succ (with (->) Int as f and Int as a)
  • Unfortunately, Haskell doesn’t support sections for the -> type constructor, or I would have said that f were (Int ->) instead. I think that’s a little more readable.
  • The actual type of succ is more generic than that, but this statement is still true.
  • If this doesn’t make sense yet, don’t worry about it.
• fmap id (Just (1, "two")) should be equal to Just (1, "two") (with Maybe as f and (Int, String) as a).
• fmap id (putStrLn "hi") should be equal to putStrLn "hi" (with IO as f and () as a)

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

Now back to your regularly scheduled programming.