On Wed, Nov 13, 2013 at 12:42 PM, Brandon Allbery wrote:

On Wed, Nov 13, 2013 at 12:24 PM, Vlatko Basic wrote:

...

Thanks for explanation. If I understood correctly, 'rigid' refers the requirement, not the type itself.

I think that more intuitive/understandable would be something like

...

'b' has too rigid type for 'a' ...

Not really, unless you're talking about some notion of "types of types" (which exists, but not in this way). You're still trying to hold onto some notion that `a` is flexible; but the compiler does not care about the kind of flexibility you want. You will need to let go of that "flexible" for Haskell's type system to make sense.

As an example of this, by the way: your function declaration admits only two possible definitions, ignoring nontermination. Both of them ignore `a` entirely, because you can't do *anything* with it. You don't get much more rigid than being unable to use it at all! -- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

Hi Vlatko, On Thu, Nov 14, 2013 at 11:33:15AM +0100, Vlatko Basic wrote:

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.

Can you recommend any resources that helped you in better understanding?

Did you understand what Brandon said, that 'a' has to be a 'String', because it's compared by an other string with '==' and the operator '==' demands, that both arguments have the same type? If you try to write the same function in C++ (the same may hold for Java Generics): template <typename A> bool f(A a) { return a == "x"; } Than the C++ compiler would happily read this function and wouldn't complain in any way. Only if you would use this function with a type that isn't comparable with a string, than it would complain. The problem with the C++ way is, that the function isn't telling you in any way the constraints of type 'A', only if you're using a type that doesn't fulfill all constraints, than the compiler will tell you that with some very indirect error messages. Haskell is very explicit about the constraints, you have to explicitly declare all the constraints of your type. So looking at the function 'f': f :: a -> Bool f a = let b = "x" in a == b The first thing is the usage of '==', which is an operator of the type class 'Eq', so only types having an instance of 'Eq' are allowed: f :: Eq a => a -> Bool f a = let b = "x" in a == b But you're comparing the 'a' against a variable of type 'String' and because the type of '==' is 'a -> a -> Bool' the type of 'a' also has to be 'String'. f :: String -> Bool f a = let b = "x" in a == b Greetings, Daniel

On Thu, Nov 14, 2013 at 5:33 AM, Vlatko Basic 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

On Fri, Nov 15, 2013 at 2:10 AM, Vlatko Basic 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

"It could be any type" has always been a truism. It has never been an issue of contention. The issue has always been "but who gets to choose". Teachers and tutorial writers still don't address that up front and head on; they spend 99 minutes harping on "any", watch students fail, and finally spend 1 minute to reveal "but you don't choose". As opposed to revealing that in the 1st minute so everyone can save the other 99 minutes. Perhaps they think that it is obvious to themselves, and need not be said to students. Perhaps they need to ensure a certain high variance in student marks. Less flexibility for the provider equals more flexibility for the user. Less cavalier power for the writer equals more predictive power for the reader. Cavalier power has previously been known as convenience, flexibility, and expressive power, for the writer; extreme examples include self-modifying code and performing list operations on complex numbers (let us call that type cavalierism, so that we have a judgmental name for the antithesis to type safety); mild examples include type-case and allowing effects everywhere. Programming is a dialectic class struggle between the user and the provider, between the reader and the writer. Given the type signature f :: a -> Bool and the restriction of "no type-case" and "no effect" such as in Haskell, if a simple test results in f () = True, then I know f 5 = True, f "hello" = True, universally f x = True. I need just one test case, f (), to complement the type. This is from the free theorems that Phil Wadler talks about in the article "theorems for free!". Perhaps f is a useless function. Here is a useful function: dpc :: a -> [a] If a simple test results in dpc () = [(), (), ()], then I know dpc x = [x, x, x] universally. replicate 3 is, certainly, a useful function, at least for glue code. And it is important to know that I will not be trolled by "you get a list of 4 if the type is Double, and you get random numbers in the list if the type is Int". The writer's loss of cavalier power is my gain of predictive power. Your freedom is my slavery. Your ignorance is my strength. Your war is my peace. Customers who like this article may also like the following from the same author: http://www.vex.net/~trebla/weblog/any-all-some.html http://www.vex.net/~trebla/haskell/prerequisite.xhtml#leibniz and this talk (50 minutes) from another author: http://www.youtube.com/watch?v=TS1lpKBMkgg

Can you recommend any resources that helped you in better understanding?

If you really like type theory, you may want to take at look at Types and Programming Languages by Benjamin C. Pierce. It goes from very simple concepts and builds up, getting into Typed Lambda Calculus and type systems for O.O. languages, for example. http://www.cis.upenn.edu/~bcpierce/tapl/

I think that more intuitive/understandable would be something like

'b' has too rigid type for 'a' ...

At least, that is what I have to tell myself when I encounter this issue

I don't think this is quite correct. As I'm a daily Java programmer, one thing that really troubled me was to think as `a' being something like `Object', but it is wrong. The `a' really means that the client of the function can define the type it wants, and be precise. I guess it's easier to see this in the value (result) of a function: "f :: a -> b" is a function that takes any value and produces any value the user wants, i.e. I can take an Int out of it, or a Double, or a String, or a Foo, or a Bar. That's a huge difference between Java's "Object f(Object a)" (a better comparison would be with " B f(A a);", I guess). I'm diverging a bit, but what I want to say is that there is no way to tell that the type of "b" is "too rigid" for the type `a' , because the `a' can be anything, even the exact type of "b".