4 ms·
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
by ezyang 10y ago
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!