[Haskell-cafe] Musings on type systems

[Tillmann Rendel]

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?

   Tillmann