On Fri, Nov 15, 2013 at 2:10 AM, Vlatko Basic <vlatko.basic@gmail.com> wrote:

I think I understand now why compiler calls it rigid and not "flexible" or whatever.
It is because the call site defines the parameter type, and when that parameter comes to function, its type is already rigidly determined. We just do not know its type. So the type is rigidly unknown, and not flexible.

Counterexample:

id2 :: a -> a

id2 = id . id

You're getting closer, but if you think of it from the viewpoint of the programmer who wrote the compiler (the same one who's wording all these error messages), it becomes really clear.

What you've basically got before you is an algorithm to check the validity of types.

So whereas the thing in question (whatever's denoted by 'a') is called a type 'variable', it doesn't 'vary' in (I'm guessing) the OO way.

When checking the types in your function, 'a' is fixed, i.e. made rigid, by what's known as a 'universal quantification'. So when you code up the type checking algorithm, you'd see a crystal-clear similarity to treating 'a' as if it were a monotype like Bool or String.

When checking the types in _uses_ of your function (say, something similar to 'id True') _that's_ when 'a' varies, i.e. in the sense that each use may fix 'a' to something different.

Overall, I think you're doing really well for someone groping with Haskell general and its type system in particular. The lingo can be misleading.

Personally, I think a lot can be made to fill the gap between trial-and-discovery and reading notationally-heavy formal texts like conf papers and textbooks (Pierce's TAPL).

-- Kim-Ee