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
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: instance inference

[Simon Peyton-Jones]

Thank you Ross.

I've committed your patch, and added documentation.

Simon

| -Original Message-
| From: [EMAIL PROTECTED]
[mailto:glasgow-haskell-users-
| [EMAIL PROTECTED] On Behalf Of Ross Paterson
| Sent: 06 February 2006 11:36
| To: Simon Peyton-Jones; glasgow-haskell-users@haskell.org
| Subject: Re: instance inference
| 
| A patch implementing a relaxed termination constraint is at
| 
|   http://www.soi.city.ac.uk/~ross/instance-termination.patch
| 
| Here is the description:
| 
|  With -fglasgow-exts but not -fallow-undecidable-instances, GHC 6.4
|  requires that instances be of the following form:
| 
|   (1) each assertion in the context must constrain distinct variables
|   mentioned in the head, and
| 
|   (2) at least one argument of the head must be a non-variable type.
| 
|  This patch replaces these rules with the requirement that each
|  assertion in the context satisfy
| 
|   (1) no variable has more occurrences in the assertion than in the
|   head, and
| 
|   (2) the assertion has fewer constructors and variables (taken
together
|   and counting repetitions) than the head.
| 
|  This allows all instances permitted by the old rule, plus such
|  instances as
| 
| instance C a
| instance Show (s a) => Show (Sized s a)
| instance (Eq a, Show b) => C2 a b
| instance C2 Int a => C3 Bool [a]
| instance C2 Int a => C3 [a] b
| instance C4 a a => C4 [a] [a]
| 
|  but still ensures that under any substitution assertions in the
context
|  will be smaller than the head, so context reduction must terminate.
| 
|  This is probably the best we can do if we consider each instance in
|  isolation.
| 
| ___
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

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: [EMAIL PROTECTED]  /   |___\


___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

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

[Ben Rudiak-Gould]

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
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

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
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

newtype and rules

[John Meacham]

I am curious if rules pragmas are applied before or after newtype
desugaring? basically what I want to know is if I have a newtype of an
Int say, and make a rule acting on the newtype, will it be applied to
any Int as well?

John

-- 
John Meacham - ⑆repetae.net⑆john⑈
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

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

[David Menendez]

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 <[EMAIL PROTECTED]> | "In this house, we obey the laws
  |of thermodynamics!"
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

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

[David Menendez]

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 <[EMAIL PROTECTED]> | "In this house, we obey the laws
  |of thermodynamics!"
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users