[Haskell-cafe] Musings on type systems

[Andrew Coppin]

On 20/11/2010 08:42 AM, Tillmann Rendel wrote:
> Hi Andrew,
>
> Andrew Coppin wrote:
>> Now, what about type variables? What do they do? Well now, that seems to
>> be slightly interesting, since a type variable holds an entire type
>> (whereas normal program variables just hold a single value), and each
>> occurrance of the same variable is statically guaranteed to hold the
>> same thing at all times. It's sort of like how every instance of a
>> normal program variable holds the same value, except that you don't
>> explicitly say what that value is; the compiler infers it.
>
> What do you mean by "hold the same thing at all times"?
>
> Consider the following program:
>
>   id :: forall a . a -> a
>   id x = x
>
>   call1 :: Bool
>   call1 = id True
>
>   call2 :: Int
>   call2 = id 42
>
> This program contains a type variable a, and a value variable x. Now, 
> these variables do *not* mean the same thing at all times. In the 
> first call of id, a is Bool and x is True; but in the second call of 
> id, a is Int and x is 42. If these variables would mean the same thing 
> at all times, I would expect them to be called constants, wouldn't you?

That would be why I said "instance of a variable", rather than 
"variable". (There's also the alpha conversion problem, for example.)