Relationship between Higher Kinded Polymorphism, type inference, and Currying

Question

On Hacker News there is an interesting exchange about the async\await RFC for Rust.

The author of the proposal withoutboats is responding to a comment about the usage of async-await construct vs a monadic implementation in Rust. He notes three problems, the first one I am having some trouble parsing:

Higher kinded polymorphism results in trivially undecidable type inferences without something like currying; the restrictions needed to support it would be arbitrary and weird given that Rust does not have currying (essentially some rules to reconstruct the restrictions of currying in type operator context).

I have a decent understanding of higher-kinded polymorphism, type inference, and currying (or so I naively assert), and I even see why currying is useful for higher-kinded polymorphism, i.e. type constructors of the form * -> * -> *, a type which takes a type and produces a third.

But what I don't understand is why currying is necessary to avoid "trivially undecideable type inferences." Can someone provide an example of a such an undecideable inference, and why currying helps?

Answer 1

I imagine what the comment writer is referring to is this...

Consider type inference in Haskell. At some point, we may be asked to solve the unification problem f a = Maybe Int. This is very easy to solve (f = Maybe, a = Int), but only because we have restricted the allowable solutions. The solution to f may only be built out of (partial) applications of type 'constructors' (like Maybe) and variables. Another example is f a = (b, a) with solution f = (,) b. I suspect this partial application is what is meant by "currying". Note that f Int = (Int, Double) just fails.

Now consider (until somewhat recently) Scala. For one, there was no inherent notion of left-to-right partial application like the above. To even write a partially applied type required giving it a name via some rather baroque syntax. But more importantly, it made no commitment to the restrictions that made things easy in the last paragraph. This has the 'advantage' that you can make f Int = (Int, Double) work. A solution is f = λa. (a, Double). However, note that we had to solve for f with a lambda term. This means inference must solve a problem called, "higher-order unification," which is bad, because it's undecidable.

Another (related, I think) problem is that my last solution above wasn't actually unique. Another solution is f = λ_. (Int, Double). Neither of these solutions is more general than the other, they're simply different. So, I suspect it's also the case that higher-order unification doesn't have most-general solutions. This means (I think) that even if it were a solvable problem, the 'right' solution would not be a local property, and would depend on the rest of the program (because some of the multiple possible solutions might not be compatible with other parts of the program where the solution is used).

So, to avoid these problems, it is much easier to restrict the solution space the way Haskell does. It isn't terribly inconvenient to organize things according to this discipline such that you get good inference most of the time. And when unification fails, it's obvious what the problem was, whereas it can get complicated to figure out how to guide the system using higher-order unification with the right annotations.

However, I've heard that newer versions of Scala actually have adopted this type inference methodology. But I still don't think their type functions look "curried" exactly like Haskell's do (i.e. they still look like F[A,B]). So it's probably not essential to do that. The left-to-right partial application rule is the essential part.