RE: Rank-2 polymorphism & type inference
| < p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ []) | < q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f) | < | System CT accepts both. No type signature is required. | | The types inferred for p and q are, resp.: | | Forall a,b. [a] -> (b -> Bool, [a]) and | Forall a,b. [a] -> ([a], b -> Bool) That's not the type we wanted, though. We wanted Forall a. [a] -> (Forall b. b->Bool, [a]) and similarly the other one. That's the reason for the type signature on f, which is short for (forall c. c->Bool). If you leave out the type signature then all Haskell compilers are happy. (Of course, this isn't a very useful example, but it's the smallest one that shows up the problem.) Simon
On Thu 07 Dec, Simon Peyton-Jones wrote:
| < p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ []) | < q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f) | < | System CT accepts both. No type signature is required. | | The types inferred for p and q are, resp.: | | Forall a,b. [a] -> (b -> Bool, [a]) and | Forall a,b. [a] -> ([a], b -> Bool)
That's not the type we wanted, though. We wanted
Forall a. [a] -> (Forall b. b->Bool, [a])
I thought.. Forall a,b. [a] -> ( b -> Bool, [a]) Forall a. [a] -> Forall b.(b -> Bool, [a]) Forall a. [a] -> (Forall b. b -> Bool, [a]) All mean they same thing, or do they? Regards -- Adrian Hey
Adrian Hey writes:
On Thu 07 Dec, Simon Peyton-Jones wrote: [...]
| Forall a,b. [a] -> (b -> Bool, [a]) and [...] That's not the type we wanted, though. We wanted
Forall a. [a] -> (Forall b. b->Bool, [a])
I thought.. Forall a,b. [a] -> ( b -> Bool, [a]) Forall a. [a] -> Forall b.(b -> Bool, [a]) Forall a. [a] -> (Forall b. b -> Bool, [a]) All mean they same thing, or do they?
Section 7.3.2 of the Hugs user guide demonstrates the difference, using simpler examples. Among other things, it says "quantifiers can only appear in the types of function arguments, not in the results." So the second one (forall a. [a] -> forall b.(b -> Bool, [a])) may be invalid. Something to do with letting the locally quantified b escape, perhaps? I'm not sure. I'm also not sure whether Hugs will allow any function with the type (forall a. [a] -> (forall b. b -> Bool, [a])) to be applied, because "Any call to such a function must have at least as many arguments as are needed to include the rightmost argument with a quantified type." Regards, Tom
On Fri 08 Dec, Tom Pledger wrote:
Adrian Hey writes:
I thought.. Forall a,b. [a] -> ( b -> Bool, [a]) Forall a. [a] -> Forall b.(b -> Bool, [a]) Forall a. [a] -> (Forall b. b -> Bool, [a]) All mean they same thing, or do they?
Section 7.3.2 of the Hugs user guide demonstrates the difference, using simpler examples.
Thanks, I've had a look at the Hugs user guide you mentioned. I'm not convinced that it does explain the difference, but it certainly lists a lot of constraints. I don't really understand why nested quantifiers shouldn't be allowed, for example, or why quantifiers can't appear in function results. (or why partial application in the example (twice f) is illegal). Presumably there's some reason why the type of.. (twice (\x ->[x])) can't be infered as Forall a. a->[[a]] To me, pushing all quantifiers 'down the tree' (so to speak) as far as they can go without leaving a type variable occurence unquantified seems natural, but maybe my intuition is at fault here. Making the implicit quantification of a explicit, twice :: Forall a. (Forall b. b -> f b) -> a -> f (f a) Push Forall a 'down the tree'.. twice :: (Forall b. b -> f b) -> Forall a. a -> f (f a) seems to work (informally at least). Regards -- Adrian Hey
participants (3)
-
Adrian Hey -
Simon Peyton-Jones -
Tom Pledger