What does "no global type inference" mean regarding Scala?

Question

I have read that Scala's type inference is not global so that is why people must place type annotations on the methods. (Would this be "local" type inference?)

I only a little understand that the reason is from its object-oriented nature, but clarity eludes me. Is there an explanation for "global type inference" and why Scala cannot have it that a beginner might understand?

Polygnotus

Answer 1

The typical example for a global type inference is Hindley-Milner: It takes a given program and "calculates" all the necessary types. However in order to achieve this, the given language needs to have some properties (there are extensions to HM, which try to overcome some of these restrictions). Two things HM doesn't like are inheritance and method overloading. As far as I understand these are the main obstacles for Scala to adopt HM or some variant of it. Note that in practice even languages which heavily rely on HM never reach a 100% inference, e.g. even in Haskell you need a type annotation from time to time.

So Scala uses a more limited (as you say "local") form of type inference, which is still better than nothing. As far as I can tell the Scala team tries to improve the type inference from release to release when it is possible, but so far I've seen only smaller steps. The gap to a HM style type inferencer is still huge, and can't be closed completely.

Uro

Answer 2

The problem is that HM type inference is undecidable in general in a language with subtyping, overloading or similar features.^Ref This means more and more stuff could be added to the inferencer to make it infer more special cases, but there will always be code where it will fail.

Scala has made the decision to make type annotations in method arguments and some other places mandatory. This might seem like a hassle first, but consider that this helps to document the code and provides the compiler with information it can understand in one place. Additionally, languages with HM inference often suffer from the problem that programming errors are sometimes detected in code far away from the original mistake, because the HM algorithm just went along and happened (by chance) to infer other parts of the code with the faulty type it inferred before it failed.

Scala's inference basically works from the outside (method definition) to the inside (code inside the method) and therefore limits the impact of a wrong type annotation.

Languages with HM inference work from the inside to the outside (ignoring the possibility to add type annotations) which means there is a chance that a small code change in one single method can change the meaning of the whole program. This can be good or bad.

---

Ref: Lower bounds on type inference with subtypes

Bhagavadgita

@Bhagavadgita Could you link a paper stating that HM inference is undecidable with subtyping? I'm having trouble finding anything on it. – Broussard

"Lower bounds on type inference with subtypes" dl.acm.org/citation.cfm?id=199481 – Bailiff