Search code examples
haskelltypestype-systems

types and type variable in Haskell


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!


Solution

  • 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