Ian Henry

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 `Int`s 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.

``````∀ 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, ∀ `Functor`s and ∀ values you can think of.

Now back to your regularly scheduled programming.