Apparent Type variable behaviour incoherence clarification in Haskell

Question

Disclosure: I'm a Scala Programmer learning Haskell.

I'd like to understand type variable behaviour a bit better.

Contrary to Scala it seems we can declare variable of generic type (i.e. type variable). That is generic are not limited to function. However I can't understand the following deprecencies and would like some explanation for this.

Why is it that the following code does work on function:

g :: a -> a -- a can take the concrete type Num a => a or something else like Bool
g x = x

g 10
--g 10 :: Num a => a

g True
--g True :: Bool

However the following strange thing happen with variable as opposed to function

e :: a
e = 1
--  No instance for (Num a) arising from the literal ‘1’
--      Possible fix:
--      add (Num a) to the context of
--        the type signature for:
--          e1 :: forall a. a
--    In the expression: 1
--    In an equation for ‘e1’: e1 = 1

Same thing of course if I type the following in the REPL

e :: a; e = 1

Q1 ) From that it would seem we have a difference of Behaviour of generic type (i.e. type variable) between variable and function ? Why is that ? or what is it i am not seeing or getting yet ?

Now the strange part

If in the Repl however I do

 e :: a; e = undefined

and then

e = 1

then i get

:t e
-- e1 :: Num p => p

So using undefined in the REPL "at least", I get back the Behaviour of Generic type on function.

Q2) What actually is going on here ? This all thing doe not sound super coherent to me. Can anyone explain please ?

Answer 1

Type variables in Haskell are universally quantified. This means that the actual type of g is

g :: ∀ a . a -> a

The quantifier is normally implicit, but you can actually spell it out in Haskell source (as forall) if you enable certain GHC extensions.

What does it mean? Well quite literally, g has type a -> a for all possible values of a. That is, g is a Bool->Boll and a String->String and an Int->Int function. It has all of these types.

When you write g x = x, you are not breaking the promise given by the type of g, namely, that the argument can be of any type and the result must be of the same type. Indeed, the result is x and the argument is also x, and x obviously has the same type as x.

However, if you write g x = x + 42, this breaks the promise. x cannot be of type Bool or String any more. So the compiler will complain.

Now, the notation

e :: a

in a very similar way should be interpreted as

e :: ∀ a . a

This means e has type a for all possible values of a. That is, it has every possible type: Int and String and Bool and Int->Int and infinitely many others.

You could satisfy the type by defining e as

e = undefined

(and indeed this is basically the only way you can satisfy it). However, if you write

e = 1

you break the promise given by the type of e. So you will get the same kind of error as above.

If you write e = undefined and afterwards e = 1, then in a REPL the second definition shadows the first one, so you have two different variables named e, each of its own type. If you are using REPL you can redefine any name at any time you want, this is what REPL is for! This is of course impossible in a normal Haskell module.