forall a (Ord a => a-> a) -> Int is an illegal type???

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

forall a (Ord a => a-> a) -> Int is an illegal type???

Brian Hulley
Hi -
I've been puzzling over section 7.4.9.3 of the ghc users manual for the past
few months (!) and still can't understand why the following is an illegal
type:

forall a. ((Ord a => a-> a) -> Int)

whereas

(forall a. Ord a => a->a) -> Int

is legal. I can understand why the second one *is* legal but I can't seem to
understand why the first syntax is not just exactly the same thing even
though the parse tree is different.

Can anyone shed some light on this?

Thanks, Brian.

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

Re: forall a (Ord a => a-> a) -> Int is an illegal type???

Brian Hulley
Brian Hulley wrote:

> Hi -
> I've been puzzling over section 7.4.9.3 of the ghc users manual for
> the past few months (!) and still can't understand why the following
> is an illegal type:
>
> forall a. ((Ord a => a-> a) -> Int)
>
> whereas
>
> (forall a. Ord a => a->a) -> Int
>
> is legal. I can understand why the second one *is* legal but I can't
> seem to understand why the first syntax is not just exactly the same
> thing even though the parse tree is different.
>
> Can anyone shed some light on this?
>
> Thanks, Brian.

A better way of putting the question is that I can't see the difference
between:

          forall a. ((Ord a => a->a) -> Int)

and

          forall a. Ord a => (a->a) -> Int


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

Re[2]: forall a (Ord a => a-> a) -> Int is an illegal type???

Bulat Ziganshin
Hello Brian,

Thursday, February 09, 2006, 9:38:35 AM, you wrote:

>> the past few months (!) and still can't understand why the following
>> is an illegal type:
>>
>> forall a. ((Ord a => a-> a) -> Int)

i don't know right answer burt may be because "Ord a" restriction and
"forall a" )"dseclaration" of type variable) should be at the same
"level". imagine the following declaration:

forall a. (Int -> (Ord a => a)) -> Int)

it is not good to write restriction on some deep level instead of
right together with "declaration"



--
Best regards,
 Bulat                            mailto:[hidden email]



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

Re: Re[2]: forall a (Ord a => a-> a) -> Int is an illegal type???

Brian Hulley
Bulat Ziganshin wrote:

> Hello Brian,
>
> Thursday, February 09, 2006, 9:38:35 AM, you wrote:
>
>>> the past few months (!) and still can't understand why the following
>>> is an illegal type:
>>>
>>> forall a. ((Ord a => a-> a) -> Int)
>
> i don't know right answer burt may be because "Ord a" restriction and
> "forall a" )"dseclaration" of type variable) should be at the same
> "level". imagine the following declaration:
>
> forall a. (Int -> (Ord a => a)) -> Int)
>
> it is not good to write restriction on some deep level instead of
> right together with "declaration"

Thanks! If I understand you correctly, I should think of the "Ord" as being
part of the "forall" quantifier, so that

       forall a. Ord a =>

is really to be thought of as something like:

      forall_that_is_Ord a =>

and of course quantifiers can't be split up into pieces that are distributed
all over the place...

If so, then I think I understand it all now, though I'm puzzled why GHC
chooses to create illegal types instead of finding the innermost
quantification point ie I would think that

         (Ord a=> a->a) -> Int

should then "obviously" be shorthand for

          (forall a. Ord a=> a->a) -> Int

and surely this could easily be implemented by just prepending "forall a b
c" onto any context restricting a b c... (?)

Regards, Brian.

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

Re: Re[2]: forall a (Ord a => a-> a) -> Int is an illegal type???

Atze Dijkstra
Hello,

for me it helps to think of "Ord a =>" as an obligation of the caller  
of the function with "Ord a =>" to pass a dictionary for Ord a (and  
satisfy the predicate). "forall a" allows the caller of the function  
to choose a type for "a". Then

f :: forall a. ((Ord a => a-> a) -> Int)
f g = ...

means that a caller of 'f' can choose the type of 'a', so the body of  
'f' cannot make any assumptions about it. However, in order to use  
'g' inside 'f', 'f' has to provide 'g' with a "Ord a", which it  
cannot, because no (dictionary for) "Ord a" is available (for all  
'a'). So the type may well be considered legal, but is fairly useless  
as no implementation can be given for 'f'. On the other hand:

f :: forall a . Ord a => (Ord a => a -> a) -> a -> a
f g i = g i

would be ok, because 'f' gets passed a dictionary for "Ord a" which  
can be passed on to 'g'. (this is not accepted by GHC).

The type

f :: (forall a . Ord a => a->a) -> Int
f g = g 3

differs from the previous in the higher-rank forall quantifier. Now  
no caller of 'f' can choose the type of 'a', but the body of 'f' can,  
for 'g', for example by passing '3' to 'g' and implicitly also the  
dictionary for "Ord Int".

On  9 Feb, 2006, at 09:22 , Brian Hulley wrote:

> Bulat Ziganshin wrote:
>> Hello Brian,
>>
>> Thursday, February 09, 2006, 9:38:35 AM, you wrote:
>>
>>>> the past few months (!) and still can't understand why the  
>>>> following
>>>> is an illegal type:
>>>>
>>>> forall a. ((Ord a => a-> a) -> Int)
>>
>> i don't know right answer burt may be because "Ord a" restriction and
>> "forall a" )"dseclaration" of type variable) should be at the same
>> "level". imagine the following declaration:
>>
>> forall a. (Int -> (Ord a => a)) -> Int)
>>
>> it is not good to write restriction on some deep level instead of
>> right together with "declaration"
>
> Thanks! If I understand you correctly, I should think of the "Ord"  
> as being part of the "forall" quantifier, so that
>
>       forall a. Ord a =>
>
> is really to be thought of as something like:
>
>      forall_that_is_Ord a =>
>
> and of course quantifiers can't be split up into pieces that are  
> distributed all over the place...
>
> If so, then I think I understand it all now, though I'm puzzled why  
> GHC chooses to create illegal types instead of finding the  
> innermost quantification point ie I would think that
>
>         (Ord a=> a->a) -> Int
>
> should then "obviously" be shorthand for
>
>          (forall a. Ord a=> a->a) -> Int

See http://www.cs.uu.nl/wiki/Ehc/WebHome where we did experiment with  
this and the above.


regards,

                 - Atze -

Atze Dijkstra, Department of Information and Computing Sciences. /|\
Utrecht University, PO Box 80089, 3508 TB Utrecht, Netherlands. / | \
Tel.: +31-30-2534093/1454 | WWW  : http://www.cs.uu.nl/~atze . /--|  \
Fax : +31-30-2513971 .... | Email: [hidden email] ............ /   |___\


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

Re: forall a (Ord a => a-> a) -> Int is an illegal type???

Ben Rudiak-Gould
In reply to this post by Brian Hulley
Brian Hulley wrote:

> I'm puzzled why GHC chooses to create illegal types instead  of
> finding the innermost quantification point ie I would think that
>
>         (Ord a=> a->a) -> Int
>
> should then "obviously" be shorthand for
>
>          (forall a. Ord a=> a->a) -> Int
>
> and surely this could easily be implemented by just prepending "forall a
> b c" onto any context restricting a b c... (?)

I agree that it's strange to add an implicit quantifier and then complain
that it's in the wrong place. I suspect Simon would change this behavior if
you complained about it. My preferred behavior, though, would be to reject
any type that has a forall-less type class constraint anywhere but at the
very beginning. I don't think it's a good idea to expand implicit
quantification. Also, the rule would not be quite as simple as you make it
out to be, since

     forall a. (forall b. Foo a b => a -> b) -> Int

is a legal type, for example.

-- Ben

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

Re: forall a (Ord a => a-> a) -> Int is an illegal type???

Brian Hulley
Ben Rudiak-Gould wrote:

> Brian Hulley wrote:
>> I'm puzzled why GHC chooses to create illegal types instead  of
>> finding the innermost quantification point ie I would think that
>>
>>         (Ord a=> a->a) -> Int
>>
>> should then "obviously" be shorthand for
>>
>>          (forall a. Ord a=> a->a) -> Int
>>
>> and surely this could easily be implemented by just prepending
>> "forall a b c" onto any context restricting a b c... (?)
>
> I agree that it's strange to add an implicit quantifier and then
> complain that it's in the wrong place. I suspect Simon would change
> this behavior if you complained about it. My preferred behavior,
> though, would be to reject any type that has a forall-less type class
> constraint anywhere but at the very beginning. I don't think it's a
> good idea to expand implicit quantification. Also, the rule would not
> be quite as simple as you make it out to be, since
>
>     forall a. (forall b. Foo a b => a -> b) -> Int
>
> is a legal type, for example.

This is what I still don't understand: how the above could be a legal type.
Surely it introduces 'a' to be anything, and then later retricts 'a' to be
related to 'b' via the typeclass 'Foo' ?

I would have thought only the following would be legal:

        f :: (forall a b. Foo a b => a->b) -> Int

In other words, in:

       f :: forall a. (forall b. Foo a b => a->b) -> Int
       f g = ...

how can 'f' pass the dictionary 'Foo a b' to g when 'f' can only choose 'b'
but doesn't know anything about 'a'? Where does it get this dictionary from?

Regards, Brian.

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

Re: forall a (Ord a => a-> a) -> Int is an illegal type???

David Menendez
In reply to this post by Brian Hulley
Brian Hulley writes:

> I've been puzzling over section 7.4.9.3 of the ghc users manual for
> the past few months (!) and still can't understand why the following
> is an illegal type:
>
> forall a. ((Ord a => a-> a) -> Int)
>
> whereas
>
> (forall a. Ord a => a->a) -> Int
>
> is legal. I can understand why the second one *is* legal but I can't
> seem to understand why the first syntax is not just exactly the same
> thing even though the parse tree is different.

I see you already clarified this, but I'd like to point out that

    forall a. (a -> a) -> Int

and

    (forall a. a -> a) -> Int

are very different. The first essentially takes two arguments, a type
|a| and a value of type |a -> a|. The second takes a single argument of
type |forall a. a -> a|.
 
There are some type systems (like JHC core, IIRC) which treat "forall"
and "->" as special cases of the dependent product. That is, "T -> U" is
short for "Pi _:T. U" and "forall a. T" is short for "Pi a:*. T". Using
that syntax, the types above become:

    Pi a:*. Pi _:(Pi _:a. a). Int

and

    Pi _:(Pi a:*. Pi _:a. a). Int
--
David Menendez <[hidden email]> | "In this house, we obey the laws
<http://www.eyrie.org/~zednenem>      |        of thermodynamics!"
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: forall a (Ord a => a-> a) -> Int is an illegal type???

David Menendez
In reply to this post by Ben Rudiak-Gould
Ben Rudiak-Gould writes:

| Also, the rule would not be quite as simple as you make it out to be,
| since
|
|      forall a. (forall b. Foo a b => a -> b) -> Int
|
| is a legal type, for example.

Is it? GHCi gives me an error if I try typing a function like that.

> {-# OPTIONS -fglasgow-exts #-}
> class Foo a b
>
> f :: forall a. (forall b. Foo a b => a -> b) -> Int
> f = undefined

    No instance for (Foo a b)
      arising from instantiating a type signature at x.hs:5:4-12
    Probable fix: add (Foo a b) to the type signature(s) for `f'
      Expected type: (forall b1. (Foo a b1) => a -> b1) -> Int
      Inferred type: (a -> b) -> Int
    In the definition of `f': f = undefined

I think there would need to be a top-level constraint on |a| to
guarantee that an instance of |Foo a b| exists, like

    forall a. (exists c. Foo a c) =>
        (forall b. Foo a b => a -> b) -> Int
--
David Menendez <[hidden email]> | "In this house, we obey the laws
<http://www.eyrie.org/~zednenem>      |        of thermodynamics!"
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: forall a (Ord a => a-> a) -> Int is an illegal type???

Brian Hulley
David Menendez wrote:

> Ben Rudiak-Gould writes:
>
>> Also, the rule would not be quite as simple as you make it out to be,
>> since
>>
>>      forall a. (forall b. Foo a b => a -> b) -> Int
>>
>> is a legal type, for example.
>
> Is it? GHCi gives me an error if I try typing a function like that.
>
>> {-# OPTIONS -fglasgow-exts #-}
>> class Foo a b
>>
>> f :: forall a. (forall b. Foo a b => a -> b) -> Int
>> f = undefined
>
>     No instance for (Foo a b)
>       arising from instantiating a type signature at x.hs:5:4-12
>     Probable fix: add (Foo a b) to the type signature(s) for `f'
>       Expected type: (forall b1. (Foo a b1) => a -> b1) -> Int
>       Inferred type: (a -> b) -> Int
>     In the definition of `f': f = undefined
>
> I think there would need to be a top-level constraint on |a| to
> guarantee that an instance of |Foo a b| exists, like
>
>     forall a. (exists c. Foo a c) =>
>         (forall b. Foo a b => a -> b) -> Int

Is "exists" enough to ensure that 'f' is given a dictionary that will work
with all possible choices for 'b'?
I'd have thought it would need:

        forall a. (forall c. Foo a c) =>
            (forall b. Foo a b=> a->b)->Int

Regards, Brian.

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

Re: forall a (Ord a => a-> a) -> Int is an illegal type???

Stefan Holdermans
Brian,


>>> Also, the rule would not be quite as simple as you make it out to  
>>> be,
>>> since
>>>
>>>      forall a. (forall b. Foo a b => a -> b) -> Int
>>>
>>> is a legal type, for example.
>>
>> Is it? GHCi gives me an error if I try typing a function like that.
>>
>>> {-# OPTIONS -fglasgow-exts #-}
>>> class Foo a b
>>>
>>> f :: forall a. (forall b. Foo a b => a -> b) -> Int
>>> f = undefined
>>
>>     No instance for (Foo a b)
>>       arising from instantiating a type signature at x.hs:5:4-12
>>     Probable fix: add (Foo a b) to the type signature(s) for `f'
>>       Expected type: (forall b1. (Foo a b1) => a -> b1) -> Int
>>       Inferred type: (a -> b) -> Int
>>     In the definition of `f': f = undefined

Short answer: forall a. a -> a cannot be instantiated to the type of  
f. Try:

   {-# OPTIONS -fglasgow-exts #-}
   class Foo a b
   f   :: forall a. (forall b. Foo a b => a -> b) -> Int
   f _ =  undefined


Now, you should be fine.

HTH,

   Stefan

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

Re: forall a (Ord a => a-> a) -> Int is an illegal type???

Ben Rudiak-Gould
In reply to this post by David Menendez
David Menendez wrote:
> Ben Rudiak-Gould writes:
> |      forall a. (forall b. Foo a b => a -> b) -> Int
> |
> | is a legal type, for example.
>
> Is it? GHCi gives me an error if I try typing a function like that.

This works:

     f :: forall a. (forall b. Foo a b => a -> b) -> Int
     f _ = 3

I interpret this type as meaning that you can call the argument provided you
can come up with an appropriate b. If you can't come up with one then you
can't call the argument, but you can still ignore it and type check.

If you had, for example,

     instance Foo a Char
     instance Foo a Int

then you would be able to use the argument polymorphically at b=Char and b=Int.

f = undefined also works if you have "instance Foo a b" (which is only
allowed with -fallow-undecidable-instances). I think it's because of
predicativity that it fails without it.

Presumably forall a. (Ord a => a-> a) -> Int could be allowed as well, but
if you're called with a = IO () then you can't call your argument, therefore
you can never call your argument, therefore it's not a useful type in practice.

-- Ben

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

Re: forall a (Ord a => a-> a) -> Int is an illegal type???

Brian Hulley
Ben Rudiak-Gould wrote:

> David Menendez wrote:
>> Ben Rudiak-Gould writes:
>>>      forall a. (forall b. Foo a b => a -> b) -> Int
>>>
>>> is a legal type, for example.
>>
>> Is it? GHCi gives me an error if I try typing a function like that.
>
> This works:
>
>     f :: forall a. (forall b. Foo a b => a -> b) -> Int
>     f _ = 3
>
> I interpret this type as meaning that you can call the argument
> provided you can come up with an appropriate b. If you can't come up
> with one then you can't call the argument, but you can still ignore
> it and type check.
> If you had, for example,
>
>     instance Foo a Char
>     instance Foo a Int
>
> then you would be able to use the argument polymorphically at b=Char
> and b=Int.
> f = undefined also works if you have "instance Foo a b" (which is only
> allowed with -fallow-undecidable-instances). I think it's because of
> predicativity that it fails without it.
>
> Presumably forall a. (Ord a => a-> a) -> Int could be allowed as
> well, but if you're called with a = IO () then you can't call your
> argument,
> therefore you can never call your argument, therefore it's not a
> useful type in practice.


Thanks (also to Stefan) for clarifying that f's type is indeed legal.
However I still think that there is a bit of confusion about what the syntax
is supposed to mean, because:

           f :: forall a. (forall b. Foo a b => a -> b) -> Int

is effectively being used as a shorthand for (the illegal syntax):

           f :: forall a. (forall c. Foo a c) => (forall b. Foo a b =>
a->b)->Int

whereas

           g :: forall a. (Ord a => a->a)->Int

is *not* being seen as a quick way of writing:

          g :: forall a. Ord a => (Ord a => a->a)->Int

(which would further reduce to g:: forall a. Ord a=> (a->a)->Int because
there's no need for the constraint on 'a' to be written twice)

In both cases, for the argument to be useable, 'a' needs to be constrained
in the general case. The fact that all instances of Foo may happen to be
polymorphic in the 'a' argument is surely just a special case, which would
still be covered by the (forall c. Foo a c) constraint.

I think a question for the syntax is: are we to understand quantifiers and
class constraints in terms of logic, or are they supposed to only be
understood in terms of some specific implementation eg passing a dictionary?

If we are to understand them in terms of logic alone, I would suggest a
general rule that all types could be (internally) converted into a normal
form by propagating all constraints back to the relevant quantifier and
eliminating any redundant constraints that are left, so that we would get
the advantage of the existing "shorthand" while still allowing a simple way
of understanding what's going on even in the presence of multi-param type
classes.

Regards, Brian.


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

Re: forall a (Ord a => a-> a) -> Int is an illegal type???

Brian Hulley
Brian Hulley wrote:

> Thanks (also to Stefan) for clarifying that f's type is indeed legal.
> However I still think that there is a bit of confusion about what the
> syntax is supposed to mean, because:
>
>           f :: forall a. (forall b. Foo a b => a -> b) -> Int
>
> is effectively being used as a shorthand for (the illegal syntax):
>
>           f :: forall a. (forall c. Foo a c) => (forall b. Foo a b =>
> a->b)->Int
>
> whereas
>
>           g :: forall a. (Ord a => a->a)->Int
>
> is *not* being seen as a quick way of writing:
>
>          g :: forall a. Ord a => (Ord a => a->a)->Int
>
> (which would further reduce to g:: forall a. Ord a=> (a->a)->Int
> because there's no need for the constraint on 'a' to be written twice)
>
> In both cases, for the argument to be useable, 'a' needs to be
> constrained in the general case. The fact that all instances of Foo
> may happen to be polymorphic in the 'a' argument is surely just a
> special case, which would still be covered by the (forall c. Foo a c)
> constraint.
> I think a question for the syntax is: are we to understand
> quantifiers and class constraints in terms of logic, or are they
> supposed to only be understood in terms of some specific
> implementation eg passing a dictionary?
> If we are to understand them in terms of logic alone, I would suggest
> a general rule that all types could be (internally) converted into a
> normal form by propagating all constraints back to the relevant
> quantifier and eliminating any redundant constraints that are left,
> so that we would get the advantage of the existing "shorthand" while
> still allowing a simple way of understanding what's going on even in
> the presence of multi-param type classes.
>

Actually please ignore the above! :-)
I see now that all these things have useful meanings as they stand at the
moment, and that there would never be any need for a constraint such as
(forall c. Foo a c), because that actual 'c's used in the function body
could all be explicitly enumerated by a series of constraints in the case
where the relevant instances were not polymorphic in 'a' eg

         f :: forall a. (Foo a Char, Foo a Int) => (forall b. Foo a b =>
a->b) -> Int
         h :: forall a b c. (Foo a b, Foo a c) =>(forall d. Foo a d =>
a->d) -> a -> (b,c)
         h g x = (g x, g x)

Thanks to all who helped further my understanding of the interaction between
constraints and arbitrary rank polymorphism! :-)

Brian.

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

Re: forall a (Ord a => a-> a) -> Int is an illegal type???

John Meacham
In reply to this post by David Menendez
On Fri, Feb 10, 2006 at 01:41:03AM -0500, David Menendez wrote:

> are very different. The first essentially takes two arguments, a type
> |a| and a value of type |a -> a|. The second takes a single argument of
> type |forall a. a -> a|.
>  
> There are some type systems (like JHC core, IIRC) which treat "forall"
> and "->" as special cases of the dependent product. That is, "T -> U" is
> short for "Pi _:T. U" and "forall a. T" is short for "Pi a:*. T". Using
> that syntax, the types above become:
>
>     Pi a:*. Pi _:(Pi _:a. a). Int
>
> and
>
>     Pi _:(Pi a:*. Pi _:a. a). Int


Yup. that is exactly right. when pretty printing I show the pi's in a
more human digestable form (foralls and function arrows), but internally
they are all represented as Pi's.

        John

--
John Meacham - ⑆repetae.net⑆john⑈
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users