Hacker News Reader

> It's interesting because it's both important and hard.

Is it true that the problem (of type inference) is hard only in the presence of operations or expressions with types? In other words, if a language does not provide operations or expressions with types then it is more or less obvious how to infer types?

View on HN

It makes some things easier, but you give up principality: without things like intersection types, you end up with programs for which there isn't a "best" type to ascribe them. You can see this in the parent's example: without subtyping constraints or intersection types, there's no way to usefully express the subtyping that is possible in this example. It's generally considered a bad thing if your language infers a type which is incompatible with another type you could have manually written, e.g., (float -> int) -> float -> int, that is also a valid type for the expression. We like there to be a best choice for type inference to pick, but if the type language isn't expressive enough, there won't be one!

Reply on news.ycombinator.com