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.

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.

- Unfortunately, Haskell doesn’t support sections for the
`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.