Vlatko Basic | 13 Nov 17:37 2013
Picon

Word rigid in "`a' is a rigid type variable..."

Hi Cafe,

in an example function

     f :: a -> Bool
     f a = let b = "x" in a == b

compiler complains with
   `a' is a rigid type variable bound by  the type signature for f :: a -> Bool

I'm puzzled with the choice of word 'rigid' here.
I see these types as
     - 'b' has "rigid/unchangeable" type (only String), and
     - 'a' has "soft/variable" type (any type, no constraints).

Why is it called rigid?
Where does the meaning (in this context) come from?

Best regards,

vlatko
Stijn van Drongelen | 13 Nov 17:52 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

On Wed, Nov 13, 2013 at 5:37 PM, Vlatko Basic <vlatko.basic <at> gmail.com> wrote:
Hi Cafe,

in an example function

    f :: a -> Bool
    f a = let b = "x" in a == b

compiler complains with
  `a' is a rigid type variable bound by  the type signature for f :: a -> Bool

I'm puzzled with the choice of word 'rigid' here.
I see these types as
    - 'b' has "rigid/unchangeable" type (only String), and
    - 'a' has "soft/variable" type (any type, no constraints).

Why is it called rigid?
Where does the meaning (in this context) come from?



Best regards,

vlatko

Hi Vlatko,

I suspect the nomenclature comes from SPJ et al.'s "Simple Unification-based Type Inference for GADTs" (even though you're not using GADTs). Here, 'rigid' is used as a more technical term for "user-supplied".

But I'm not sure.

Kind regards,

Stijn
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Vlatko Basic | 13 Nov 18:25 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

Yes, the "user-supplied" term has more meaning than rigid here.

-------- Original Message --------
Subject: Re: [Haskell-cafe] Word rigid in "`a' is a rigid type variable..."
From: Stijn van Drongelen <rhymoid <at> gmail.com>
To: vlatko.basic <at> gmail.com
Cc: Haskell-Cafe <haskell-cafe <at> haskell.org>
Date: 13.11.2013 17:52


On Wed, Nov 13, 2013 at 5:37 PM, Vlatko Basic <vlatko.basic <at> gmail.com> wrote:
Hi Cafe,

in an example function

    f :: a -> Bool
    f a = let b = "x" in a == b

compiler complains with
  `a' is a rigid type variable bound by  the type signature for f :: a -> Bool

I'm puzzled with the choice of word 'rigid' here.
I see these types as
    - 'b' has "rigid/unchangeable" type (only String), and
    - 'a' has "soft/variable" type (any type, no constraints).

Why is it called rigid?
Where does the meaning (in this context) come from?



Best regards,

vlatko

Hi Vlatko,

I suspect the nomenclature comes from SPJ et al.'s "Simple Unification-based Type Inference for GADTs" (even though you're not using GADTs). Here, 'rigid' is used as a more technical term for "user-supplied".

But I'm not sure.

Kind regards,

Stijn

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Brandon Allbery | 13 Nov 17:53 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

On Wed, Nov 13, 2013 at 11:37 AM, Vlatko Basic <vlatko.basic <at> gmail.com> wrote:
    f :: a -> Bool
    f a = let b = "x" in a == b

compiler complains with
  `a' is a rigid type variable bound by  the type signature for f :: a -> Bool

I'm puzzled with the choice of word 'rigid' here.
I see these types as
    - 'b' has "rigid/unchangeable" type (only String), and
    - 'a' has "soft/variable" type (any type, no constraints).

The type declaration is the final arbiter. Since it says "any type", it means exactly that: you are claiming your function is prepared to handle *any type* the caller wishes to specify. It is not "soft", nor "variable" in the sense you intend: it is a hard requirement that your function must be prepared to handle whatever type the caller wants there.

But instead your function requires that it be String, because both sides of (==) must be the same type. This violates the type signature'a assertion that the caller can specify any type.

--
brandon s allbery kf8nh                               sine nomine associates
allbery.b <at> gmail.com                                  ballbery <at> sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Vlatko Basic | 13 Nov 18:24 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

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' ...

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


vlatko
-------- Original Message --------
Subject: Re: [Haskell-cafe] Word rigid in "`a' is a rigid type variable..."
From: Brandon Allbery <allbery.b <at> gmail.com>
To: Vlatko Bašić <vlatko.basic <at> gmail.com>
Cc: Haskell-Cafe <haskell-cafe <at> haskell.org>
Date: 13.11.2013 17:53


On Wed, Nov 13, 2013 at 11:37 AM, Vlatko Basic <vlatko.basic <at> gmail.com> wrote:
    f :: a -> Bool
    f a = let b = "x" in a == b

compiler complains with
  `a' is a rigid type variable bound by  the type signature for f :: a -> Bool

I'm puzzled with the choice of word 'rigid' here.
I see these types as
    - 'b' has "rigid/unchangeable" type (only String), and
    - 'a' has "soft/variable" type (any type, no constraints).

The type declaration is the final arbiter. Since it says "any type", it means exactly that: you are claiming your function is prepared to handle *any type* the caller wishes to specify. It is not "soft", nor "variable" in the sense you intend: it is a hard requirement that your function must be prepared to handle whatever type the caller wants there.

But instead your function requires that it be String, because both sides of (==) must be the same type. This violates the type signature'a assertion that the caller can specify any type.

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Brandon Allbery | 13 Nov 18:42 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

On Wed, Nov 13, 2013 at 12:24 PM, Vlatko Basic <vlatko.basic <at> gmail.com> 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.

(This will make more sense when you start using typeclasses. Or, at least once you've tried to use your notion of "flexible" with them, because it will lead you straight into a brick wall that is not flexible at all.)

--
brandon s allbery kf8nh                               sine nomine associates
allbery.b <at> gmail.com                                  ballbery <at> sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Brandon Allbery | 13 Nov 18:56 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

On Wed, Nov 13, 2013 at 12:42 PM, Brandon Allbery <allbery.b <at> gmail.com> wrote:
On Wed, Nov 13, 2013 at 12:24 PM, Vlatko Basic <vlatko.basic <at> gmail.com> 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 <at> gmail.com                                  ballbery <at> sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Vlatko Basic | 14 Nov 11:33 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

Hi Brandon,

-- 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.

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


vlatko

-------- Original Message --------
Subject: Re: [Haskell-cafe] Word rigid in "`a' is a rigid type variable..."
From: Brandon Allbery <allbery.b <at> gmail.com>
To: Vlatko Bašić <vlatko.basic <at> gmail.com>
Cc: Haskell-Cafe <haskell-cafe <at> haskell.org>
Date: 13.11.2013 18:42


On Wed, Nov 13, 2013 at 12:24 PM, Vlatko Basic <vlatko.basic <at> gmail.com> 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.

(This will make more sense when you start using typeclasses. Or, at least once you've tried to use your notion of "flexible" with them, because it will lead you straight into a brick wall that is not flexible at all.)

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

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Daniel Trstenjak | 14 Nov 12:08 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."


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
Vlatko Basic | 14 Nov 12:14 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

Hi Daniel,

Yes, I do understand all that. :-)
The function is the most trivial example to show my confusion with the word 
rigid, not the error itself.

I had a feeling Brandon was talking about some important differences in the way 
of thinking.

vlatko

-------- Original Message  --------
Subject: Re: [Haskell-cafe] Word rigid in "`a' is a rigid type variable..."
From: Daniel Trstenjak <daniel.trstenjak <at> gmail.com>
To: haskell-cafe <at> haskell.org
Date: 14.11.2013 12:08

>
> 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
Brandon Allbery | 14 Nov 15:17 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

On Thu, Nov 14, 2013 at 5:33 AM, Vlatko Basic <vlatko.basic <at> 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 <at> gmail.com                                  ballbery <at> sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Vlatko Basic | 14 Nov 20:10 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

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 <at> gmail.com>
To: Vlatko Bašić <vlatko.basic <at> gmail.com>
Cc: Haskell-Cafe <haskell-cafe <at> haskell.org>
Date: 14.11.2013 15:17


On Thu, Nov 14, 2013 at 5:33 AM, Vlatko Basic <vlatko.basic <at> 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 <at> gmail.com                                  ballbery <at> sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Kim-Ee Yeoh | 14 Nov 20:54 2013

Re: Word rigid in "`a' is a rigid type variable..."


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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Vlatko Basic | 15 Nov 10:50 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

Hi Kim-Ee,

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.

Exactly the point where I made the wrong turn in thinking. Unlike in OO, I think I can imagine that compiler creates new function for every 'a' type that is used, and check for that (mono)type. That's the difference in static type checking.

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.

Just when I got the feeling I'm getting somewhere with my Haskell skills, you're telling me I'm groping. :-)
I think you're probably right. I was so amazed with the language that I went coding as soon as possible, and in the way missed some theoretical background.

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).

Indeed, and I have read a lot. But one first has to understand the problem, to understand the solution. Maybe it's time for a re-read.


vlatko
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Albert Y. C. Lai | 15 Nov 23:25 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

"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
James ‘Twey’ Kay | 14 Nov 15:39 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

On 2013-11-14 10:33, Vlatko Basic wrote:

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

I generally find it easier to think in terms of type functions: a type 
function is a function that takes a type and returns a type, written 
perhaps Λa → E (where a is a type, and bound in E).

The type of a Haskell function with a type variable a is a type function 
whose parameter just happens to be automatically filled in by the type 
checker at the call site:

   id ∷ Λa → a → a
   id _ x = x

That makes it quite clear (to me, at least) where the type gets passed 
in.  It's also pretty similar to a Java generic, which just has slightly 
different syntax for the type parameter:

   <A> A id(A x) { return x; }

In Java, you'd call that function (if I remember my Java syntax 
correctly) like

   <Integer>id(3);

the Haskell-with-type-functions version looks the same, except perhaps 
without the pointy brackets:

   id Integer 0

where

   id Integer            ∷ Integer          → Integer
   id Char               ∷ Char             → Char
   id (Either Char Bool) ∷ Either Char Bool → Either Char Bool

et cetera.

   HTH,
     — Twey
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Thiago Negri | 14 Nov 16:02 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

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.


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Adam Gundry | 13 Nov 18:52 2013

Re: Word rigid in "`a' is a rigid type variable..."

Hi Vlatko,

On 13/11/13 17:24, Vlatko Basic wrote:
> Thanks for explanation. If I understood correctly, 'rigid' refers  the
> requirement, not the type itself.

It refers to the type *variable*. This is a standard term [1] from
unification theory, where variables are divided into two kinds:

* rigid variables, which may not be filled in by the unifier; and
* flexible variables, which may be filled in to solve a constraint.

As Brandon says, a variable in a type declaration means "any type", so
it is rigid. Flexible variables are introduced when you use a
polymorphic definition, and the type inference algorithm must solve for
them.

Sometimes one speaks of a "rigid type", meaning a type that is either
constant (like String) or a rigid variable.

> 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

You may well be right that this error message could be easier to
understand, but in suggesting an alternative, be careful to be
consistent with the existing meaning of "rigid".

Adam

[1] Which is to say, I can't remember where it originates.

>> -------- Original Message --------
>> Subject: Re: [Haskell-cafe] Word rigid in "`a' is a rigid type
>> variable..."
>> From: Brandon Allbery <allbery.b <at> gmail.com>
>> To: Vlatko Bašić <vlatko.basic <at> gmail.com>
>> Cc: Haskell-Cafe <haskell-cafe <at> haskell.org>
>> Date: 13.11.2013 17:53
>>
>>
>> On Wed, Nov 13, 2013 at 11:37 AM, Vlatko Basic <vlatko.basic <at> gmail.com
>> <mailto:vlatko.basic <at> gmail.com>> wrote:
>>
>>         f :: a -> Bool
>>         f a = let b = "x" in a == b
>>
>>     compiler complains with
>>       `a' is a rigid type variable bound by  the type signature for f
>>     :: a -> Bool
>>
>>     I'm puzzled with the choice of word 'rigid' here.
>>     I see these types as
>>         - 'b' has "rigid/unchangeable" type (only String), and
>>         - 'a' has "soft/variable" type (any type, no constraints).
>>
>>
>> The type declaration is the final arbiter. Since it says "any type",
>> it means exactly that: you are claiming your function is prepared to
>> handle *any type* the caller wishes to specify. It is not "soft", nor
>> "variable" in the sense you intend: it is a hard requirement that your
>> function must be prepared to handle whatever type the caller wants there.
>>
>> But instead your function requires that it be String, because both
>> sides of (==) must be the same type. This violates the type
>> signature'a assertion that the caller can specify any type.
>>
>> -- 
>> brandon s allbery kf8nh                               sine nomine
>> associates
>> allbery.b <at> gmail.com <mailto:allbery.b <at> gmail.com>                      
>>            ballbery <at> sinenomine.net <mailto:ballbery <at> sinenomine.net>
>> unix, openafs, kerberos, infrastructure, xmonad      
>>  http://sinenomine.net

--

-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Thiago Negri | 13 Nov 18:52 2013
Picon

Re: Word rigid in "`a' is a rigid type variable..."

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 "<A, B> 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".

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane