types and type variable in Haskell

Question

Scratching at the surface of Haskell's type system, ran this:

Prelude> e = []
Prelude> ec = tail "a"
Prelude> en = tail [1]
Prelude> :t e
e :: [a]
Prelude> :t ec
ec :: [Char]
Prelude> :t en
en :: Num a => [a]
Prelude> en == e
True
Prelude> ec == e
True

Somehow, despite en and ec have different types, they both test True on == e. I say "somehow" not because I am surprised (I am not), but because I don't know what is the name of rule/mechanism that allows this. It is as if the type variable "a" in the expression "[] == en" is allowed to take on value of "Num" for the evaluation. And likewise when tested with "[] == ec", it is allowed to become "Char".

The reason I'm not sure my interpretation is correct is this:

Prelude> (en == e) && (ec == e)
True

, because intuitively this implies that in the same expression e assumes both values of Num and Char "at the same time" (at least that's how I'm used to interpret the semantics of &&). Unless the "assumption" of Char only acts during the evaluation of (ec == e), and (en == e) is evaluated independently, in a separate... reduction? (I'm guessing on a terminology here).

And then comes this:

Prelude> en == es

<interactive>:80:1: error:
    • No instance for (Num Char) arising from a use of ‘en’
    • In the first argument of ‘(==)’, namely ‘en’
      In the expression: en == es
      In an equation for ‘it’: it = en == es
Prelude> es == en

<interactive>:81:7: error:
    • No instance for (Num Char) arising from a use of ‘en’
    • In the second argument of ‘(==)’, namely ‘en’
      In the expression: es == en
      In an equation for ‘it’: it = es == en

Not surprise by the exception, but surprised that in both tests, the error message complains about "the use of 'en'" - and doesn't matter if it's the first or second operand.

Perhaps an important lesson needs to be learned about Haskell type system. Thank you for your time!

Answer 1

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

Answer 2

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.