Hi Brandon,

I understand the consequences (i.e. what to do to solve the problem), but you just made clear the reasons with one sentence

"To the type system, `a` and `b` are rigid, featureless boxes."

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.

I was looking it in the wrong direction, instead from call site to function, I was looking it from function to call site.
Maybe I'm still not used to the fact that all those checks are happening at compile time, and not at run-time.

As Twey also described, the compiler is adding type to the parameter at call site.


Thanks both for explaining that. :-)


vlatko

-------- Original Message --------
Subject: Re: [Haskell-cafe] Word rigid in "`a' is a rigid type variable..."
From: Brandon Allbery <allbery.b@gmail.com>
To: Vlatko Bašić <vlatko.basic@gmail.com>
Cc: Haskell-Cafe <haskell-cafe@haskell.org>
Date: 14.11.2013 15:17
On Thu, Nov 14, 2013 at 5:33 AM, Vlatko Basic <vlatko.basic@gmail.com> wrote:
-- You will need to let go of that "flexible" ...

Yes, sometimes I still have the feeling I'm not thinking fully Haskellish.
Maybe it's time form me to re-read about the type system.

I hinted at it in my follow-up message. Beginners often see that unadorned "a" and think that that means it can be "anything" and hence "flexible" --- but in fact it's "caller determined" and that *you can't do anything at all with it*. It's not flexible, it's a featureless black box you can't see inside or affect in any way. Your only options are ignore it or hand it off to something else.

To give an example of why that kind of thing can be useful, consider the map function:

    map :: (a -> b) -> [a] -> [b]

`map` itself can do nothing with `a` (or `b`). But it has also been given a function which *can* do something. Moreover, just from the type, you can work out exactly what that something must be! (Ignoring nontermination, which basically means that we're ignoring "cheating" by throwing an exception or etc.)

There is certainly flexibility here --- but that flexibility is not in the type system. To the type system, `a` and `b` are rigid, featureless boxes. But this lack of flexibility at the type level gives you flexibility at a different level, and at the same time gives you a guarantee: the type system won't let any implementation of `map` go behind your back and make changes to `a` or `b`, the only thing it's allowed to do it use the function you passed it. And in fact it only permits one sensible interpretation, which you can determine just from the type signature.
 
Can you recommend any resources that helped you in better understanding?

Not really, since I came at it somewhat "sideways". (In particular, I had already encountered functional programming via Lisp/Scheme and APL/J, and strong typing from exposure to SML.)

--
brandon s allbery kf8nh                               sine nomine associates
allbery.b@gmail.com                                  ballbery@sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net