[Haskell-cafe] Word rigid in "`a' is a rigid type variable..."

[Kim-Ee Yeoh]

On Fri, Nov 15, 2013 at 2:10 AM, Vlatko Basic <vlatko.basic at 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20131115/c46e6591/attachment.html>