types and type variable in Haskell

When we say that e :: [a], it means that e is a list of elements of any type. Which type? Any type! Whichever type you happen to need at the moment.

If you're coming from a non-ML language, this might be a bit easier to understand by looking at a function (rather than a value) first. Consider this:

f x = [x]

The type of this function is f :: a -> [a]. This means, roughly, that this function works for any type a. You give it a value of this type, and it will give you back a list with elements of that type. Which type? Any type! Whichever you happen to need.

When I call this function, I effectively choose which type I want at the moment. If I call it like f 'x', I choose a = Char, and if I call it like f True, I choose a = Bool. So the important point here is that whoever calls a function chooses the type parameter.

But I don't have to choose it just once and for all eternity. Instead, I choose the type parameter every time I call the function. Consider this:

pair = (f 'x', f True)

Here I'm calling f twice, and I choose different type parameters every time - first time I choose a = Char, and second time I choose a = Bool.

Ok, now for the next step: when I choose the type parameter, I can do it in several ways. In the example above, I choose it by passing a value parameter of the type I want. But another way is to specify the type of result I want. Consider this:

g x = []

a :: [Int]
a = g 0

b :: [Char]
b = g 42

Here, the function g ignores its parameter, so there is no relation between its type and the result of g. But I am still able to choose the type of that result by having it constrained by the surrounding context.

And now, the mental leap: a function without any parameters (aka a "value") is not that different from a function with parameters. It just has zero parameters, that's all.

If a value has type parameters (like your value e for example), I can choose that type parameter every time I "call" that value, just as easily as if it was a function. So in the expression e == ec && e == en you're simply "calling" the value e twice, choosing different type parameters on every call - much like I've done in the pair example above.

---

The confusion about Num is an altogether different matter.

You see, Num is not a type. It's a type class. Type classes are sort of like interfaces in Java or C#, except you can declare them later, not necessarily together with the type that implements them.

So the signature en :: Num a => [a] means that en is a list with elements of any type, as long as that type implements ("has an instance of") the type class Num.

And the way type inference in Haskell works is, the compiler will first determine the most concrete types it can, and then try to find implementations ("instances") of the required type classes for those types.

In your case, the compiler sees that en :: [a] is being compared to ec :: [Char], and it figures: "oh, I know: a must be Char!" And then it goes to find the class instances and notices that a must have an instance of Num, and since a is Char, it follows that Char must have an instance of Num. But it doesn't, and so the compiler complains: "can't find (Num Char)"

As for "arising from the use of en" - well, that's because en is the reason that a Num instance is required. en is the one that has Num in its type signature, so its presence is what causes the requirement of Num

Sometimes, it is convenient to think about polymorphic functions as functions taking explicit type arguments. Let's consider the polymorphic identity function as an example.

id :: forall a . a -> a
id x = x

We can think of this function as follows:

• first, the function takes as input a type argument named a
• second, the function takes as input a value x of the previously chosen type a
• last, the function returns x (of type a)

Here's a possible call:

id @Bool True

Above, the @Bool syntax passes Bool for the first argument (type argument a), while True is passed as the second argument (x of type a = Bool).

A few other ones:

id @Int 42
id @String "hello"
id @(Int, Bool) (3, True)

We can even partially apply id passing only the type argument:

id @Int       :: Int -> Int
id @String    :: String -> String
...

Now, note that in most cases Haskell allows us to omit the type argument. I.e. we can write id "hello" and GHC will try to infer the missing type argument. Roughly it works as follows: id "hello" is transformed into id @t "hello" for some unknown type t, then according to the type of id this call can only type check if "hello" :: t, and since "hello" :: String, we can infer t = String.

Type inference is extremely common in Haskell. Programmers rarely specify their type arguments, and let GHC do its job.

In your case:

e :: forall a . [a]
e = []
ec :: [Char]
ec = tail "1"
en :: [Int]
en = tail [1]

Variable e is bound to a polymorphic value. That is, it actually is a sort-of function which takes a type argument a (which can also be omitted), and returns a list of type [a].

Instead, ec does not take any type argument. It's a plain list of type [Char]. Similarly for en.

We can then use

ec == (e @Char)    -- both of type [Char]
en == (e @Int)     -- both of type [Int]

Or we can let the type inference engine to determine the implicit type arguments

ec == e     -- @Char inferred
en == e     -- @Int inferred

The latter can be misleading, since it seems that ec,e,en must have the same type. In fact, they have not, since different implicit type arguments are being inferred.