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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
19 messages Options
Reply | Threaded
Open this post in threaded view
|

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

Vlatko Basic
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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Stijn van Drongelen
On Wed, Nov 13, 2013 at 5:37 PM, Vlatko Basic <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Brandon Allbery
In reply to this post by Vlatko Basic
On Wed, Nov 13, 2013 at 11:37 AM, Vlatko Basic <[hidden email]> 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
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Vlatko Basic
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 [hidden email]
To: Vlatko Bašić [hidden email]
Cc: Haskell-Cafe [hidden email]
Date: 13.11.2013 17:53


On Wed, Nov 13, 2013 at 11:37 AM, Vlatko Basic <[hidden email]> 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
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Vlatko Basic
In reply to this post by Stijn van Drongelen
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 [hidden email]
To: [hidden email]
Cc: Haskell-Cafe [hidden email]
Date: 13.11.2013 17:52


On Wed, Nov 13, 2013 at 5:37 PM, Vlatko Basic <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Brandon Allbery
In reply to this post by Vlatko Basic
On Wed, Nov 13, 2013 at 12:24 PM, Vlatko Basic <[hidden email]> 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
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Adam Gundry-2
In reply to this post by Vlatko Basic
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 <[hidden email]>
>> To: Vlatko Bašić <[hidden email]>
>> Cc: Haskell-Cafe <[hidden email]>
>> Date: 13.11.2013 17:53
>>
>>
>> On Wed, Nov 13, 2013 at 11:37 AM, Vlatko Basic <[hidden email]
>> <mailto:[hidden email]>> 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
>> [hidden email] <mailto:[hidden email]>                      
>>            [hidden email] <mailto:[hidden email]>
>> unix, openafs, kerberos, infrastructure, xmonad      
>>  http://sinenomine.net

--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Thiago Negri
In reply to this post by Vlatko Basic
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Brandon Allbery
In reply to this post by Brandon Allbery
On Wed, Nov 13, 2013 at 12:42 PM, Brandon Allbery <[hidden email]> wrote:
On Wed, Nov 13, 2013 at 12:24 PM, Vlatko Basic <[hidden email]> 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
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Vlatko Basic
In reply to this post by Brandon Allbery
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 [hidden email]
To: Vlatko Bašić [hidden email]
Cc: Haskell-Cafe [hidden email]
Date: 13.11.2013 18:42


On Wed, Nov 13, 2013 at 12:24 PM, Vlatko Basic <[hidden email]> 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
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Daniel Trstenjak-2

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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Vlatko Basic
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 <[hidden email]>
To: [hidden email]
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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Brandon Allbery
In reply to this post by Vlatko Basic
On Thu, Nov 14, 2013 at 5:33 AM, Vlatko Basic <[hidden email]> 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
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

James ‘Twey’ Kay
In reply to this post by Vlatko Basic
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Thiago Negri
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Vlatko Basic
In reply to this post by Brandon Allbery
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 [hidden email]
To: Vlatko Bašić [hidden email]
Cc: Haskell-Cafe [hidden email]
Date: 14.11.2013 15:17


On Thu, Nov 14, 2013 at 5:33 AM, Vlatko Basic <[hidden email]> 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
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Kim-Ee Yeoh
Administrator

On Fri, Nov 15, 2013 at 2:10 AM, Vlatko Basic <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Vlatko Basic
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

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

Albert Y. C. Lai
In reply to this post by Brandon Allbery
"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
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe