It knows because it does type inference. That is to say, whatever is on the right hand side of the equation has to have type `b`

(because the `mempty`

on the left has type `a -> b`

).

**Addendum :: More on () - yes I am keenly interested in that. Please expand.**

Sure! So in general, a useful way to think (informally) about a type is as a set of values. For example, `Bool`

corresponds to the set `{True, False}`

. When we say `True :: Bool`

, that’s like saying `True`

is an element of the set `{True, False}`

, or more colloquially, that `True`

lives in the space of Boolean values.

Similarly, `[Int]`

is the “space” of all possible lists of integers, so to say `[1] :: [Int]`

is to say that the list `[1]`

lives in this space.

The same holds for functions. For example, `Int -> Int`

is the space of all functions from the space of integers to the space of integers. So the statement `(\x -> x*2) :: Int -> Int`

is saying that the function `\x -> x*2`

lives in the space of integers.

Some of the common basic sets and operations on sets carry over to types in an illuminating way.

In particular, there is a set that has no values, commonly called the empty set, or the null set. This corresponds to the Haskell type `Void`

. `Void`

genuinely has no values in Haskell (modulo normal caveats), so there is no value `a :: Void`

(modulo normal caveats).

There is then a set with just one value, and this corresponds to the Haskell type `()`

. The single value that lives in the `()`

space is also named `()`

(Haskell often does this “pun” where values and their types share a name, which can be quite confusing if you’re not used to it). So we can write `() :: ()`

.

Things get more interesting when we turn to operations on sets. The cartesian product takes two sets `a`

and `b`

, and returns `a x b`

, the set of all pairs with the left element from `a`

and the right element from `b`

. In Haskell, there is a corresponding notion. Given two types `a`

and `b`

, we have a type `(a, b)`

. For a concrete example, take the types `Int`

and `Bool`

. We then have a type `(Int, Bool)`

and indeed, we have e.g. `(5, True) :: (Int, Bool)`

. In other words, `(Int, Bool)`

is the type of pairs of an `Int`

on the left and a `Bool`

on the right.

Similarly for sets, there is an operation called disjoint union, which takes two sets and gives you the set containing the elements from both. In Haskell the corresponding notion, for two types `a`

and `b`

is `Either a b`

. So for example, `Either Int Bool`

contains all the elements from `Int`

and also all the elements from `Bool`

. For instance `Right True :: Either Int Bool`

, and `Left 5 :: Either Int Bool`

.

Finally, there is the set of functions from a set `a`

to a set `b`

. Naturally in Haskell that corresponds to the type `a -> b`

.

OK, now for the arithmetic part. Let’s count the number of elements in various types.

size(`Void`

) : 0

size( `()`

) : 1

size( `(a,b)`

) = size(`a`

) * size(`b`

)

size( `Either a b`

) = size( `a`

) + size (`b`

).

size ( `a -> b`

) = size ( `a`

) ^ size ( `b`

)

If two types have the same size, they are isomorphic (i.e. they are basically the same, because we can map back and forth between them without losing information) so the above is often useful. For example, size(`Either () a`

) = 1 + size(a) = size(Maybe a), so `Either () a`

is isomorphic to `Maybe a`

.