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.
withoutblogs
?) $\endgroup$withoutboats
$\endgroup$