Understanding type variables in type annotations

Question

The Elm docs illustrate type variables like this:

> List.reverse
<function> : List a -> List a

...the type variable a can vary depending on how List.reverse is used. But in this case, we have an a in the argument and in the result. This means that if you give a List Int you must get a List Int as well.

The docs for Maybe.map show this annotation:

map : (a -> b) -> Maybe a -> Maybe b

So why are the types annotated as a and b when they must be the same type?
I expected a to track the type i.e.:

map : (a -> a) -> Maybe a -> Maybe a

Answer 1

So why are the types annotated as a and b when they must be the same type?

They don't! If map did use the same type variable for the input argument type and return type they would, but map can convert from one type to another. Here's a concrete example:

Maybe.map String.fromInt (Just 42)

String.fromInt has the type Int -> String and we use it as the first argument to Maybe.map. So if we try to substitute that in the of map:

String.fromInt : (Int -> String)
Maybe.map      : (a   -> b     ) -> Maybe a -> Maybe b

we see that Int substitutes a and String substitutes b. And therefore Maybe a has to be Maybe Int and Maybe b has to be Maybe String. Which means that if we try to give it a Maybe String instead:

Maybe.map String.fromInt (Just "foo")

we'll get an error:

The 2nd argument to `map` is not what I expect:

1 | foo = Maybe.map String.fromInt (Just "foo")
                                    ^^^^^^^^^^
This `Just` call produces:

    Maybe String

But `map` needs the 2nd argument to be:

    Maybe Int