Fix quantification order for a op b and a %m -> b

[int-index]

This proposal changes the order of implicit quantification for type variables occurring (1) as type operators a `op` b, (2) in multiplicity annotations a %m -> b.

It is essentially a bugfix. However, it is also a breaking change, so we wish to bring the attention of the committee to it in order to discuss the appropriate migration strategy.

Rendered

[aspiwack]

Thank you for taking this on. Let's move quickly and submit in a couple of days.

[aspiwack]

Alternative 1.5: do only the fix for %m, because it only affects experimental code, and the other has been here for a long time and we would bite that particular bullet.

[int-index]

Added it as a third alternative.

[maralorn]

I am wondering how we would even warn about this sensibly and how people could act on that. I don’t see a way to use type applications that works before and after this change. So by warning first we would kinda force people into not using type applications on type operators for a while or removing the warning. I agree that this is all probably a moot point since this likely happens nowhere.

Question for the implementation: Can we maybe inform people about this change when they run into a type error in the context of a type application to a type operator?

[int-index]

Can we maybe inform people about this change when they run into a type error in the context of a type application to a type operator?

This would mean tracking, for each implicitly quantified type variable, whether it's used as a type operator or not. Type applications can be used with definitions coming from other modules, so we'd also have to store this information in interface files. It's not impossible but the complexity quickly adds up.

[int-index]

Let's move quickly and submit in a couple of days.

I agree. Not sure if there's much to discuss here, only a judgement call to make. @adamgundry let's get the committee involved?

[adamgundry]

This proposal doesn't feel right to me, and I've been trying to work out why. I think of a `op` b and op a b as having different parse trees that represent the same abstract syntax tree, and it seems strange to make a type inference property differ based on the parse tree. Conceptually op comes before its arguments, regardless of the use of infix syntax.

If we take the rule to be "leftmost outermost first" rather than "strictly left-to-right", does that correctly describe the current behaviour, or are there still inconsistencies? Because if that is always the current behaviour, I would be inclined to accept it as the correct specification and update the docs accordingly. Or are there more compelling motivations for the change than a desire for tidiness?

[int-index]

I think of a op b and op a b as having different parse trees that represent the same abstract syntax tree, and it seems strange to make a type inference property differ based on the parse tree.

OK, perhaps it's not very elegant, but I don't think we can use the abstract syntax tree to guide us either. Its nodes don't have an inherent ordering at all. There isn't any reason to say that in an application f a the order is [f, a] rather than [a, f], it's only an artifact of the concrete syntax. (Thought experiment: imagine a dialect of Haskell where we write applications right-to-left, i.e. Int Maybe instead of Maybe Int. It would work just as well).

As far as the abstract syntax is concerned, I tend to think of f a as an unordered record { fn: "f", arg: "a" }, which is conceptually equal to { arg: "a", fn: "f" }.

Of course we could pick an arbitrary ordering and stick to it, e.g. we could postulate that function applications are ordered [fn, arg] (which matches the concrete syntax of Haskell), but then we'd have to specify the ordering for every possible AST node. It's much easier (although perhaps not as principled) to simply take the ordering from concrete syntax.

If we take the rule to be "leftmost outermost first" rather than "strictly left-to-right", does that correctly describe the current behaviour, or are there still inconsistencies?

Well, what about a %m -> b? At the moment the ordering is [a, b, m]. I don't know if it fits your proposed scheme. (My opinion, as I've explained, is that the AST does not have an inherent ordering, so we could theoretically pick any permutation of [a, m, b]).

Or are there more compelling motivations for the change than a desire for tidiness?

It's mostly a desire for tidiness. We were in the process of a major refactor of implicit quantification and spotted this inconsistency.

[goldfirere]

I agree this is a bugfix. (I do think it's appropriate for the committee to consider, because of the backward-compatibility impact.) Let's do it. Authors of code that care can always explicitly quantify, though admittedly consumers of such code have no good way to fix the problem if they are hit by it.

[simonpj]

This proposal doesn't feel right to me, and I've been trying to work out why. I think of a op b and op a b as having different parse trees that represent the same abstract syntax tree, and it seems strange to make a type inference property differ based on the parse tree.

I sympathise with this, but any specification amounts to specify some linearisation of the tree. Your mental linearisation puts the function of (a op b) first; and mine does to. BUT I don't want us to have to specify a linearisation function, because we already have one: it's called "look at the left to right order of what the user wrote". It may not be a great linearisation function, but it is simple, easy to specify, no further explanation needed.

If you want another order, use explicit forall.

Back-compat:

• Linear Haskell is experimental anyway. I'm not concerned about breaking these programs.
• Types with infix operators where the infix function is itself a type variable are pretty rare; add implicit quantificaton; and visible type application; and now we are in a very small population.

Moreover, deprecation would be a pain to implement.

I think we should just do this.

[maralorn]

Ah, I just realized that I forgot to ping here.

I am the sheperd for this RFC and I suggested acceptance as is to the committee. I will wait for another few days to collect opinions.

[maralorn]

This proposal has been accepted by the committee. Thank you @int-index!