On Mon, 26 May 2008, Andrew Coppin wrote:

Thomas Davie wrote:

...

This is perhaps best explained with an example of something that can be typed with rank-2 types, but can't be typed otherwise:

main = f id 4

f g n = (g g) n

We note that the same instance of id must be made to have both the type (Int -> Int) and ((Int -> Int) -> (Int -> Int)) at the same time. Rank 2 types allows us to do this.

What a perplexing example! :-}

Well anyway, I was under the impression that id :: x -> x, so I'm not really sure why this wouldn't work without Rank-2 types...

Because f's type can't be written as a rank-1 type - its parameter g must be polymorphic (forall x. x->x). With rank-1 types, all the instantiation is done by the caller - the function can't require that it receive polymorphic parameters. -- flippa@flippac.org Sometimes you gotta fight fire with fire. Most of the time you just get burnt worse though.

On Tue, 2008-05-27 at 00:19 +0100, Eric Stansifer wrote:

Say, wouldn't a syntax like "(forall a => a -> a)" or "(a => a -> a)" or something similar to that be more consistent with syntax for contexts, e.g. "(Ord a => a -> a)"?

It's not remotely the same thing as a class constraint so why would we want it to be "consistent" with it?

On Tue, 2008-05-27 at 01:45 +0100, Eric Stansifer wrote:

...

...

Say, wouldn't a syntax like "(forall a => a -> a)" or "(a => a -> a)" or something similar to that be more consistent with syntax for contexts, e.g. "(Ord a => a -> a)"?

It's not remotely the same thing as a class constraint so why would we want it to be "consistent" with it?

Well, true; the idea come from when I read just now in the ghc manual that the following are equivalent:

...

data T = MkT (Ord a => a -> a) data U = MkU (forall a. Ord a => a -> a)

In other words, the context "Ord a" in the /T/ definition is implicitly carrying a "forall a" around with it. In a sense, one can think of "forall a" as a class constraint for /a/ that offers no constraints at all; i.e., "forall a" is satisfied by any type /a/, whereas "Ord a", for example, is satisfied by any type /a/ which has an instance for /Ord/.

It's not "carrying a forall" around with it. The fact that 'a' is otherwise unbound leads GHC to insert a 'forall a'. That's another way in which forall and class constraints aren't remotely the same. forall is a binding construct that introduces a new type variable, a class constraint is not a binding construct.

To be exact, here is the analogy I'm making.

Suppose we have:

...

class F a => C1 a class C2 a

Then: ((F a, C1 a) => a -> a) is to (C1 a => a -> a) as (forall a. C2 a => a -> a) is to (C2 a => a -> a)

That is, /forall a/ acts like a constraint that always succeeds (and is thus usually implicit -- e.g., in the line "class C2 a").

The analogy, of course, breaks down the moment one writes:

...

-- t :: (Ord a => a -> a) -> T -- t = MkT

u :: (forall a. Ord a => a -> a) -> U u = MkU

where for very good reasons the type signatures written for /t/ and /u/ above mean entirely different things.

So, the similarity is rather tenuous, and is further diminished because the "forall a" construct and the "Ord a" construct are used for entirely different things in practice, regardless of some nice, abstract connection that I see between them. But I hope you see why I feel that "forall a" is in some ways closely related to "Ord a". [Incidentally, I also don't like introducing new syntax (though introducing new syntax is better than abusing existing syntax).]

On another note: the ghc 6.6.1 manual says (as does the latest manual, but I have version 6.6.1, so that's what matters here) in section 7.4.8.1 that the following are equivalent:

...

data T a = MkT (Either a b) (b -> b) data T a = MkT (forall b. Either a b) (forall b. b -> b)

but for me, the first line does not compile with -fglasgow-exts (I get: "Not in scope: type variable `b'"), but the second line does compile. Am I missing something here?

Doesn't work for me either which kind of relieves me as I don't particularly like that interpretation.

Gleb Alexeyev wrote:

foo :: (forall a . a -> a) -> (Bool, String) foo g = (g True, g "bzzt")

So, after an entire day of boggling my mind over this, I have brought it down to one simple example: (id 'J', id True) -- Works perfectly. \f -> (f 'J', f True) -- Fails miserably. Both expressions are obviously perfectly type-safe, and yet the type checker stubbornly rejects the second example. Clearly this is a flaw in the type checker. So what is the type of that second expression? You would think that (x -> x) -> (Char, Bool) as a valid type for it. But alas, this is not correct. The CALLER is allowed to choose ANY type for x - and most of possible choices wouldn't be type-safe. So that's no good at all! In a nutshell, the function being passed MAY accept any type - but we want a function that MUST accept any type. This excusiatingly subtle distinction appears to be the source of all the trouble. Interestingly, if you throw in the undocumented "forall" keyword, everything magically works: (forall x. x -> x) -> (Char, Bool) Obviously, the syntax is fairly untidy. And the program is now not valid Haskell according to the written standard. And best of all, the compiler seems unable to deduce this type automatically either. At this point, I still haven't worked out exactly why this hack works. Indeed, I've spent all day puzzling over this, to the point that my head hurts! I have gone through several theories, all of which turned out to be self-contradictory. So far, the only really plausible theory I have been able to come up with is this: - A function starts out with a polymorphic type, such as 'x -> x'. - Each time the function is called, all the type variables have to be locked down to real types such as 'Int' or 'Either (Maybe (IO Int)) String' or something. - By the above, any function passed to a high-order function has to have all its type variables locked down, yielding a completely monomorphic function. - In the exotic case above, we specifically WANT a polymorphic function, hence the problem. - The "forall" hack somehow convinces the type checker to not lock down some of the type variables. In this way, the type variables relating to a function can remain unlocked until we reach each of the call sites. This allows the variables to be locked to different types at each site [exactly as they would be if the function were top-level rather than an argument]. This is a plausible hypothesis for what this language feature actually does. [It is of course frustrating that I have to hypothesise rather than read a definition.] However, this still leaves a large number of questions unanswered... - Why are top-level variables and function arguments treated differently by the type system? - Why do I have to manually tell the type checker something that should be self-evident? - Why do all type variables need to be locked down at each call site in the first place? - Why is this virtually never a problem in real Haskell programs? - Is there ever a situation where the unhacked type system behaviour is actually desirably? - Why can't the type system automatically detect where polymorphism is required? - Does the existence of these anomolies indicate that Haskell's entire type system is fundamentally flawed and needs to be radically altered - or completely redesigned? Unfortunately, the GHC manual doesn't have a lot to say on the matter. Reading section 8.7.4 ("Arbitrary-rank polymorphism"), we find the following: - "The type 'x -> x' is equivilent to 'forall x. x -> x'." [Um... OK, that's nice?] - "GHC also allows you to do things like 'forall x. x -> (forall y. y -> y)'." [Fascinating, but what does that MEAN?] - "The forall makes explicit the universal quantification that is implicitly added by Haskell." [Wuh??] - "You can control this feature using the following language options..." [Useful to know, but I still don't get what this feature IS.] The examples don't help much either, because (for reasons I haven't figured out yet) you apparently only need this feature in fairly obscure cases. The key problem seems to be that the GHC manual assumes that anybody reading it will know what "universal quantification" actually means. Unfortunately, neither I nor any other human being I'm aware of has the slightest clue what that means. A quick search on that infallable reference [sic] Wikipedia yields several articles full of dense logic theory. Trying to learn brand new concepts from an encyclopedia is more or less doomed from the start. As far as I can comprehend it, we have existential quantification = "this is true for SOMETHING" universal quantification = "this is true for EVERYTHING" Quite how that is relevant to the current discussion eludes me. I have complete confidence that whoever wrote the GHC manual knew exactly what they meant. I am also fairly confident that this was the same person who implemented and even designed this particular feature. And that they probably have an advanced degree in type system theory. I, however, do not. So if in future the GHC manual could explain this in less opaque language, that would be most appreciated. :-} For example, the above statements indicate that '(x -> x) -> (Char, Bool)' is equivilent to 'forall x. (x -> x) -> (Char, Bool)', and we already know that this is NOT the same as '(forall x. x -> x) -> (Char, Bool)'. So clearly my theory above is incomplete, because it fails to explain why this difference exists. My head hurts... (Of course, I could just sit back and pretend that rank-N types don't exist. But I'd prefer to comprehend them if possible...)

2008/5/27 Andrew Coppin :

Gleb Alexeyev wrote:

...

foo :: (forall a . a -> a) -> (Bool, String) foo g = (g True, g "bzzt")

So, after an entire day of boggling my mind over this, I have brought it down to one simple example:

(id 'J', id True) -- Works perfectly.

\f -> (f 'J', f True) -- Fails miserably.

Both expressions are obviously perfectly type-safe, and yet the type checker stubbornly rejects the second example. Clearly this is a flaw in the type checker.

No, this is a flaw in the type inferencer, but simply adding the Rank-N type to our type system makes type inference undecidable. I would argue against the "obviously perfectly type-safe" too since most type system don't even allow for the second case.

So what is the type of that second expression? You would think that

(x -> x) -> (Char, Bool)

as a valid type for it. But alas, this is not correct. The CALLER is allowed to choose ANY type for x - and most of possible choices wouldn't be type-safe. So that's no good at all!

None of the possible choice would be type-safe. This type means : whatever the type a, function of type (a -> a) to a pair (Char, Bool) But the type a is unique while in the body of your function, a would need to be two different types.

Interestingly, if you throw in the undocumented "forall" keyword, everything magically works:

(forall x. x -> x) -> (Char, Bool)

Obviously, the syntax is fairly untidy. And the program is now not valid Haskell according to the written standard. And best of all, the compiler seems unable to deduce this type automatically either.

As I said, the compiler can't deduce this type automatically because it would make type inference undecidable.

At this point, I still haven't worked out exactly why this hack works. Indeed, I've spent all day puzzling over this, to the point that my head hurts! I have gone through several theories, all of which turned out to be self-contradictory. So far, the only really plausible theory I have been able to come up with is this:

Rank-N type aren't a "hack", they're perfectly understood and fit nicely into the type system, their only problem is type inference.

yada yada, complicated theory... cut

What you don't seem to understand is that "(x -> x) -> (Char, Bool)" and "(forall x. x -> x) -> (Char, Bool)" are two very different beasts, they aren't the same type at all ! Taking a real world situation to illustrate the difference : Imagine you have different kind of automatic washer, some can wash only wool while others can wash only cotton and finally some can wash every kind of fabric... You want to do business in the washing field but you don't have a washer so you publish an announce : If your announce say "whatever the type of fabric x, give me a machine that can wash x and all you clothes and I'll give you back all your clothes washed", the customer won't be happy when you will give him back his wool clothes that the cotton washing machine he gave you torn to shreds... What you really want to say is "give me a machine that can wash any type of fabric and your clothes and I'll give you back your clothes washed". The first announce correspond to "(x -> x) -> (Char, Bool)", the second to "(forall x. x -> x) -> (Char, Bool)"

- Why are top-level variables and function arguments treated differently by the type system?

They aren't (except if you're speaking about the monomorphism restriction and that's another subject entirely).

- Why do I have to manually tell the type checker something that should be self-evident?

Because it isn't in all cases to a machine, keep in mind you're an human and we don't have real IA just yet.

- Why is this virtually never a problem in real Haskell programs?

Because we seldom needs Rank-2 polymorphism.

- Is there ever a situation where the unhacked type system behaviour is actually desirably?

Almost everytime. Taking a simple example : map If the type of map was "(forall x. x -> x) -> [a] -> [a]", you could only pass it "id" as argument, if it was "(forall x y. x -> y) -> [a] -> [b]", you couldn't find a function to pass to it... (No function has the type "a -> b")

- Why can't the type system automatically detect where polymorphism is required?

It can and does, it can't detect Rank-N (N > 1) polymorphism because it would be undecidable but it is fine with Rank-1 polymorphism (which is what most people call polymorphism).

- Does the existence of these anomolies indicate that Haskell's entire type system is fundamentally flawed and needs to be radically altered - or completely redesigned?

Maybe this should suggest to you that it is rather your understanding of the question that is flawed... Haskell's type system is a fine meshed mechanism that is soundly grounded in logic and mathematics, it is rather unlikely that nobody would have noted the problem if it was so important... -- Jedaï

Andrew Coppin wrote:

So, after an entire day of boggling my mind over this, I have brought it down to one simple example:

(id 'J', id True) -- Works perfectly. \f -> (f 'J', f True) -- Fails miserably.

Both expressions are obviously perfectly type-safe, and yet the type checker stubbornly rejects the second example. Clearly this is a flaw in the type checker.

So what is the type of that second expression? You would think that (x -> x) -> (Char, Bool) as a valid type for it. But alas, this is not correct. The CALLER is allowed to choose ANY type for x - and most of possible choices wouldn't be type-safe. So that's no good at all!

In a nutshell, the function being passed MAY accept any type - but we want a function that MUST accept any type. This excusiatingly subtle distinction appears to be the source of all the trouble.

Let's fill in the type variable: (x -> x) -> (Char, Bool) ==> forall x. (x -> x) -> (Char, Bool) ==> x_t -> (x -> x) -> (Char, Bool), where x_t is the hidden type-variable, not unlike the reader monad. As you've pointed out, callER chooses x_t, say Int when passing in (+1) :: Int -> Int, which obviously would break \f -> (f 'J', f True). What we want is the callEE to choose x_t since callEE needs to instantiate x_t to Char and Bool. What we want is (x_t -> x -> x) -> (Char, Bool). But that's just (forall x. x -> x) -> (Char, Bool). For completeness' sake, let me just state that if universal quantification is like (x_t -> ...), then existential quantification is like (x_t, ...). Andrew Coppin wrote:

At this point, I still haven't worked out exactly why this hack works. Indeed, I've spent all day puzzling over this, to the point that my head hurts! I have gone through several theories, all of which turned out to be self-contradictory.

My sympathies. You may find the haskell-cafe archive to be as useful as I have (search Ben Rudiak-Gould or Dan Licata). Having said that, I think you've done pretty well on your own. Andrew Coppin wrote:

- Why can't the type system automatically detect where polymorphism is required? - Does the existence of these anomolies indicate that Haskell's entire type system is fundamentally flawed and needs to be radically altered - or completely redesigned?

Well, give it a try! I'm sure I'm not the only one interested in your type inference experiments. Warning: they're addictive and may lead to advanced degrees and other undesirable side-effects. -- Kim-Ee -- View this message in context: http://www.nabble.com/Aren%27t-type-system-extensions-fun--tp17479349p174983... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

Darrin Thompson wrote:

On Tue, May 27, 2008 at 3:40 PM, Kim-Ee Yeoh wrote:

...

Let's fill in the type variable: (x -> x) -> (Char, Bool) ==> forall x. (x -> x) -> (Char, Bool) ==> x_t -> (x -> x) -> (Char, Bool), where x_t is the hidden type-variable, not unlike the reader monad.

As you've pointed out, callER chooses x_t, say Int when passing in (+1) :: Int -> Int, which obviously would break \f -> (f 'J', f True).

What we want is the callEE to choose x_t since callEE needs to instantiate x_t to Char and Bool. What we want is (x_t -> x -> x) -> (Char, Bool). But that's just (forall x. x -> x) -> (Char, Bool).

Nice. That's the first time any of this really made sense to me. Is it possible to construct valid argument for that function?

agree, the types-are-arguments-too makes thinking about how it works A LOT clearer... and it's actually what GHC's intermediate Core language does. It's too bad there's no way in the language syntax to make that interpretation clearer. (That's a subset of explicit dependent types -- explicitness is opposite type inference, not static vs. dependentness.) -Isaac

Andrew Coppin wrote:

So, after an entire day of boggling my mind over this, I have brought it down to one simple example:

(id 'J', id True) -- Works perfectly.

\f -> (f 'J', f True) -- Fails miserably.

Both expressions are obviously perfectly type-safe, and yet the type checker stubbornly rejects the second example. Clearly this is a flaw in the type checker.

So what is the type of that second expression? You would think that

(x -> x) -> (Char, Bool)

as a valid type for it. But alas, this is not correct. The CALLER is allowed to choose ANY type for x - and most of possible choices wouldn't be type-safe. So that's no good at all!

All possible choices wouldn't be type-safe, so its even worse.

In a nutshell, the function being passed MAY accept any type - but we want a function that MUST accept any type. This excusiatingly subtle distinction appears to be the source of all the trouble.

Interestingly, if you throw in the undocumented "forall" keyword, everything magically works:

(forall x. x -> x) -> (Char, Bool)

But you have to do it right. forall x . (x -> x) -> (Char, Bool) is equivalent to the version without forall, and does you no good. (Note the parentheses to see why these two types are different). So there lies no magic in mentioning forall, but art in putting it in the correct position.

The key problem seems to be that the GHC manual assumes that anybody reading it will know what "universal quantification" actually means. Unfortunately, neither I nor any other human being I'm aware of has the slightest clue what that means. A quick search on that infallable reference [sic] Wikipedia yields several articles full of dense logic theory. Trying to learn brand new concepts from an encyclopedia is more or less doomed from the start. As far as I can comprehend it, we have

existential quantification = "this is true for SOMETHING" universal quantification = "this is true for EVERYTHING"

Quite how that is relevant to the current discussion eludes me.

Your "MUST accept any type" is related to universal quantification, and your "MAY accept any type" is related to existential quantification: This works for EVERYTHING, so it MUST accept any type. This works for SOMETHING, so it accepts some unknown type. Quantification is the logic word for "abstracting by introducing a name to filled with content later". For example, in your above paragraph you wanted to tell us that no human being you are aware of has the slightest clue what "universal quantification" means. You could have done so by enumerating all human beings you are aware of. Instead, you used universal quantification: for all HUMAN BEING, HUMAN BEING has no clue. (shortened to not overcomplicate things, HUMAN BEING is the name here). Tillmann

On Tue, May 27, 2008 at 5:55 PM, Andrew Coppin wrote:

Gleb Alexeyev wrote:

...

foo :: (forall a . a -> a) -> (Bool, String) foo g = (g True, g "bzzt")

So, after an entire day of boggling my mind over this, I have brought it down to one simple example:

(id 'J', id True) -- Works perfectly.

\f -> (f 'J', f True) -- Fails miserably.

Both expressions are obviously perfectly type-safe, and yet the type checker stubbornly rejects the second example. Clearly this is a flaw in the type checker.

So what is the type of that second expression? You would think that

(x -> x) -> (Char, Bool)

When you're reasoning about this, I think it would help you greatly to explicitly put in *all* the foralls. In haskell, when you write, say: map :: (a -> b) -> [a] -> [b] All the free variables are *implicitly* quantified at the top level. That is, when you write the above, the compiler sees: map :: forall a b. (a -> b) -> [a] -> [b] (forall has low precedence, so this is the same as: map :: forall a b. ((a -> b) -> [a] -> [b]) ) And the type you mention above for the strange expression is: forall x. (x -> x) -> (Char, Bool) Which indicates that the caller gets to choose. That is, if a caller sees a 'forall' at the top level, it is allowed to instantiate it with whatever type it likes. Whereas the type you want has the forall in a different place than the implicit quantifiaction: (forall x. x -> x) -> (Char, Bool) Here the caller does not have a forall at the top level, it is hidden inside a function type so the caller cannot instantiate the type. However, when implementing this function, the argument will now have type forall x. x -> x And the implementation can instantiate x to be whatever type it likes. But my strongest advice is, when you're thinking through this, remember that: x -> x Is not by itself a type, because x is meaningless. Instead it is Haskell shorthand for forall x. x -> x Luke

as a valid type for it. But alas, this is not correct. The CALLER is allowed to choose ANY type for x - and most of possible choices wouldn't be type-safe. So that's no good at all!

In a nutshell, the function being passed MAY accept any type - but we want a function that MUST accept any type. This excusiatingly subtle distinction appears to be the source of all the trouble.

Interestingly, if you throw in the undocumented "forall" keyword, everything magically works:

(forall x. x -> x) -> (Char, Bool)

Obviously, the syntax is fairly untidy. And the program is now not valid Haskell according to the written standard. And best of all, the compiler seems unable to deduce this type automatically either.

At this point, I still haven't worked out exactly why this hack works. Indeed, I've spent all day puzzling over this, to the point that my head hurts! I have gone through several theories, all of which turned out to be self-contradictory. So far, the only really plausible theory I have been able to come up with is this:

- A function starts out with a polymorphic type, such as 'x -> x'.

- Each time the function is called, all the type variables have to be locked down to real types such as 'Int' or 'Either (Maybe (IO Int)) String' or something.

- By the above, any function passed to a high-order function has to have all its type variables locked down, yielding a completely monomorphic function.

- In the exotic case above, we specifically WANT a polymorphic function, hence the problem.

- The "forall" hack somehow convinces the type checker to not lock down some of the type variables. In this way, the type variables relating to a function can remain unlocked until we reach each of the call sites. This allows the variables to be locked to different types at each site [exactly as they would be if the function were top-level rather than an argument].

This is a plausible hypothesis for what this language feature actually does. [It is of course frustrating that I have to hypothesise rather than read a definition.] However, this still leaves a large number of questions unanswered...

- Why are top-level variables and function arguments treated differently by the type system? - Why do I have to manually tell the type checker something that should be self-evident? - Why do all type variables need to be locked down at each call site in the first place? - Why is this virtually never a problem in real Haskell programs? - Is there ever a situation where the unhacked type system behaviour is actually desirably? - Why can't the type system automatically detect where polymorphism is required? - Does the existence of these anomolies indicate that Haskell's entire type system is fundamentally flawed and needs to be radically altered - or completely redesigned?

Unfortunately, the GHC manual doesn't have a lot to say on the matter. Reading section 8.7.4 ("Arbitrary-rank polymorphism"), we find the following:

- "The type 'x -> x' is equivilent to 'forall x. x -> x'." [Um... OK, that's nice?]

- "GHC also allows you to do things like 'forall x. x -> (forall y. y -> y)'." [Fascinating, but what does that MEAN?]

- "The forall makes explicit the universal quantification that is implicitly added by Haskell." [Wuh??]

- "You can control this feature using the following language options..." [Useful to know, but I still don't get what this feature IS.]

The examples don't help much either, because (for reasons I haven't figured out yet) you apparently only need this feature in fairly obscure cases.

The key problem seems to be that the GHC manual assumes that anybody reading it will know what "universal quantification" actually means. Unfortunately, neither I nor any other human being I'm aware of has the slightest clue what that means. A quick search on that infallable reference [sic] Wikipedia yields several articles full of dense logic theory. Trying to learn brand new concepts from an encyclopedia is more or less doomed from the start. As far as I can comprehend it, we have

existential quantification = "this is true for SOMETHING" universal quantification = "this is true for EVERYTHING"

Quite how that is relevant to the current discussion eludes me.

I have complete confidence that whoever wrote the GHC manual knew exactly what they meant. I am also fairly confident that this was the same person who implemented and even designed this particular feature. And that they probably have an advanced degree in type system theory. I, however, do not. So if in future the GHC manual could explain this in less opaque language, that would be most appreciated. :-}

For example, the above statements indicate that '(x -> x) -> (Char, Bool)' is equivilent to 'forall x. (x -> x) -> (Char, Bool)', and we already know that this is NOT the same as '(forall x. x -> x) -> (Char, Bool)'. So clearly my theory above is incomplete, because it fails to explain why this difference exists. My head hurts...

(Of course, I could just sit back and pretend that rank-N types don't exist. But I'd prefer to comprehend them if possible...) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Andrew Coppin wrote:

Finally, that seems to make actual sense. I have one final question though:

forall x, y. x -> y -> Z forall x. x -> (forall y. y -> Z)

Are these two types the same or different? [Ignoring for a moment the obvious fact that you'll have one hell of a job writing a total function with such a type!]

they're the same type: foralls in function *results* can be moved to the outside with no change in meaning. They don't make it a higher rank type. (though some definitions in typically-uncurried languages like to call it higher rank, that's not relevant to us). (modulo GHC issues with impredicative polymorphism, which ideally shouldn't even come into the picture here, because you're only using/exploring RankNTypes) -Isaac

These things become easier if you are explicit about type applications (which Haskell isn't). Phillippa mentioned it in an earlier post, but here it is again. First the old stuff, if you have a term of type (S->T) then the (normal form of) term must be (\ x -> e), where x has type S and e has type T. When using a function it's the caller that decided the actual value of the x, and the callee decides the value to return. OK, now forall. If a term is of type (forall a . T) then the (normal form of) term must be (/\ a -> e), where /\ is a capital lambda, and it means it's a function that takes a type as the argument instead of a term. For type application I'll write f@T, meaning that f is /\ function and we give it type argument T. Let's try it on some functions. What's the real type id? It's id :: forall a . a-> a since the type is a forall, the body of the function must start with a /\ id = /\ b -> \ x -> x (or if you want to be explicit about types id= /\ b -> \ (x::b) -> x) It's quite clear that the caller gets to pick both the type argument and the value argument, and the id function only gets to pick the return value, e.g., (id@Int 5) or (id@Bool True). Another example const :: forall a . forall b . a -> b -> a const = /\ a -> /\ b -> \ x -> \ y -> x or, alternatively const' :: forall a . a -> forall b . b -> a const' = /\ a -> \ x -> /\ b -> \ y -> x It's obvious that the caller gets to pick both types and both values. The placement of the foralls only affect the type application order (const@Int@Bool 5 True) resp (const'@Int 5 @Bool True). All right, so let's do rank 2. f :: (forall a . a -> a) -> (Int, Bool) What's the body of the function? The top level type is -> so it must start with a \, e.g., \ g -> When using g it must be used correctly. The type of g starts with a forall, so using it must start with a type application followed by a normal application. f = \ g -> (g@Int 5, g@Bool True) So it's again clear the the caller of f doesn't get to pick the type a, it must be supplied by the callee. The caller of f must supply a value of type (forall a . a->a), i.e., (f id). So you can see that depending on the forall's position with respect to the -> the role of it changes from a type being picked by the caller or callee. (If it's under an odd number of arrows the callee picks.) If you remove all the explicit type abstractions and applications above then you have Haskell (+ RankN). As other have pointed out, you can't remove the nested foralls because in general they cannot be inferred. Hope this helps. -- Lennart On Wed, May 28, 2008 at 7:51 PM, Andrew Coppin wrote:

Luke Palmer wrote:

...

When you're reasoning about this, I think it would help you greatly to explicitly put in *all* the foralls. In haskell, when you write, say:

map :: (a -> b) -> [a] -> [b]

All the free variables are *implicitly* quantified at the top level. That is, when you write the above, the compiler sees:

map :: forall a b. (a -> b) -> [a] -> [b]

And the type you mention above for the strange expression is:

forall x. (x -> x) -> (Char, Bool)

Which indicates that the caller gets to choose. That is, if a caller sees a 'forall' at the top level, it is allowed to instantiate it with whatever type it likes. Whereas the type you want has the forall in a different place than the implicit quantifiaction:

(forall x. x -> x) -> (Char, Bool)

Here the caller does not have a forall at the top level, it is hidden inside a function type so the caller cannot instantiate the type. However, when implementing this function, the argument will now have type

forall x. x -> x

And the implementation can instantiate x to be whatever type it likes.

Hmm. Right. So you're saying that the exact position of the "forall" indicates the exact time when the variable(s) get specific types assigned to them?

So... the deeper you nest the foralls, the longer those variables stay unbound? [And the higher the "rank" of the type?]

Finally, that seems to make actual sense. I have one final question though:

forall x, y. x -> y -> Z forall x. x -> (forall y. y -> Z)

Are these two types the same or different? [Ignoring for a moment the obvious fact that you'll have one hell of a job writing a total function with such a type!] After all, ignoring the quantification, we have

x -> y -> Z x -> (y -> Z)

which are both the same type. So does that mean you can move the forall to the left but not to the right? Or are the types actually different?

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

Andrew Coppin wrote:

(id 'J', id True) -- Works perfectly.

\f -> (f 'J', f True) -- Fails miserably.

Both expressions are obviously perfectly type-safe, and yet the type checker stubbornly rejects the second example. Clearly this is a flaw in the type checker.

When you type some expression such as \x -> x you have to choose among an infinite number of valid types for it: Int -> Int Char -> Char forall a . a -> a forall a b . (a,b) -> (a,b) ... Yet the type inference is smart enough to choose the "best" one: forall a. a -> a because this is the "most general" type. Alas, for code like yours: foo = \f -> (f 'J', f True) there are infinite valid types too: (forall a. a -> Int) -> (Int, Int) (forall a. a -> Char)-> (Char, Char) (forall a. a -> (a,a)) -> ((Char,Char),(Bool,Bool)) ... and it is much less clear if a "best", most general type exists at all. You might have a preference to type it so that foo :: (forall a . a->a) -> (Char,Bool) foo id ==> ('J',True) :: (Char,Bool) but one could also require the following, similarly reasonable code to work: foo :: (forall a. a -> (a,a)) -> ((Char,Char),(Bool,Bool)) foo (\y -> (y,y)) ==> (('J','J'),(True,True)) :: ((Char,Char),(Bool,Bool)) And devising a type inference system allowing both seems to be quite hard. Requiring a type annotation for these not-so-common code snippets seems to be a fair compromise, at least to me. Regards, Zun.

Andrew writes | I have complete confidence that whoever wrote the GHC manual knew | exactly what they meant. I am also fairly confident that this was the | same person who implemented and even designed this particular feature. | And that they probably have an advanced degree in type system theory. I, | however, do not. So if in future the GHC manual could explain this in | less opaque language, that would be most appreciated. :-} As the person who wrote the offending section of the GHC user manual (albeit lacking a qualification of any sort in type theory), I am painfully aware of its shortcomings. Much of the manual is imprecise, and explains things only by examples. The wonder is that it apparently serves the purpose for many people. Nevertheless, the fact is that it didn't do the job for Andrew, at least not first time around. After some useful replies to his email, he wrote | Thank you for coming up with a clear and comprehensible answer. I would very much welcome anyone who felt able to improve on the text in the manual, even if it's only a paragraph or two. If you stub your toe on the manual, once you find the solution, take a few minutes to write the words you wish you had read to begin with, and send them to me. Meanwhile, Andrew, I recommend the paper "Practical type inference for arbitrary rank types", which is, compared to the user manual at least, rather carefully written. Simon

On Thu, May 29, 2008 at 9:51 AM, Kim-Ee Yeoh wrote:

Roberto Zunino-2 wrote:

...

Alas, for code like yours: foo = \f -> (f 'J', f True)

there are infinite valid types too: (forall a. a -> Int) -> (Int, Int) (forall a. a -> Char)-> (Char, Char) (forall a. a -> (a,a)) -> ((Char,Char),(Bool,Bool)) ...

and it is much less clear if a "best", most general type exists at all.

How about foo :: (exists. m :: * -> *. forall a. a -> m a) -> (m Char, m Bool)

Not quite Haskell, but seems to cover all of the examples you gave.

You have now introduced a first-class type function a la dependent types, which I believe makes the type system turing complete. This does not help the decidability of inference :-) Luke

Kim-Ee Yeoh wrote:

Luke Palmer-2 wrote:

...

You have now introduced a first-class type function a la dependent types, which I believe makes the type system turing complete. This does not help the decidability of inference :-)

God does not care about our computational difficulties. He infers types emp^H^H^H ... uh, as He pleases.

This begs the question: Can God come up with a type He doesn't understand? The answer, it seems, is Mu. -- (c) this sig last receiving data processing entity. Inspect headers for past copyright information. All rights reserved. Unauthorised copying, hiring, renting, public performance and/or broadcasting of this signature prohibited.

On Thu, May 29, 2008 at 01:44:24PM +0200, Roberto Zunino wrote:

Kim-Ee Yeoh wrote:

...

How about foo :: (exists. m :: * -> *. forall a. a -> m a) -> (m Char, m Bool)

Thank you: I had actually thought about something like that.

First, the exists above should actually span over the whole type, so it becomes a forall because (->) is contravariant on its 1st argument:

foo :: forall m :: * -> * . (forall a. a -> m a) -> (m Char, m Bool)

This seems to be Haskell+extensions, but note that m above is meant to be an arbitrary type-level function, and not a type constructor (in general). So, I am not surprised if undecidability issues arise in type checking/inference. :-)

Type *checking* is still decidable (System Fw is sufficiently powerful to model these types) but type inference now needs higher order unification, which indeed is undecidable.

Another valid type for foo can be done AFAICS with intersection types:

foo :: (Char -> a /\ Bool -> b) -> (a,b)

But I can not comment about their inference, or usefulness in practice.

Again, undecidable :) In fact, I believe that an inference algorithm for intersection types is equivalent to solving the halting problem. Type checking however is decidable, but expensive. Edsko

Isaac Dupree wrote:

...

...

foo :: (Char -> a /\ Bool -> b) -> (a,b)

a.k.a. find some value that matches both Char->a and Bool->b for some a and b. Could use type-classes to do it.

Uhmm... you mean something like (neglecting TC-related issues here) class C a b where fromChar :: Char -> a fromBool :: Bool -> b or some more clever thing? If this can be encoded with method-less classes, I would be quite interested in knowing how.

But why, when we can just use standard tuples instead? foo :: (Char -> a , Bool -> b) -> (a,b)

This makes the class dictionary explicit. Alas, IIUC we lost type erasure (does that still hold with intersection types?) in this "implementation". Zun.

...

...

...

foo :: (Char -> a /\ Bool -> b) -> (a,b)

a.k.a. find some value that matches both Char->a and Bool->b for some a and b. Could use type-classes to do it.

...

Uhmm... you mean something like (neglecting TC-related issues here)

class C a b where fromChar :: Char -> a fromBool :: Bool -> b

Oops: i meant something like

class C x a b | x -> a,b where fromChar :: x -> Char -> a fromBool :: x -> Bool -> b

no... let me figure out what I meant. Just somehow to have a single function that takes an argument of two different types without completely ignoring it. class Arg a where whatYouPass :: a -> Something instance Arg Char where whatYouPass = ... instance Arg Bool where whatYouPass = ... Then (foo whatYouPass) :: (Something, Something). Or if it was class Arg a where whatYouPass :: a -> a then (foo whatYouPass) :: (Char, Bool). And I'm sure there are ways to make the return type different if you want to think about FDs etc.

Zun.