4 ms·

I think it depends on the algorithm & implementation, but in at least some cases type inference adds very little code over type checking. (To some degree, both

I think it depends on the algorithm & implementation, but in at least some cases type inference adds very little code over type checking. (To some degree, both are propagating and unifying types through the program and throwing an error when trying to unify two things that aren't the same. And depending on the language, you've got to have some non-trivial machinery for handling function overloads, which can require inference-y reasoning anyway (like calling an overloaded function immediately with the result of another overloaded function).) On the other hand, non-local inference can make things more complicated in some situations, depending on how hard you try. For instance, Rust gives up if you don't know the type of a variable and you try to accesses a member of it, where I once wrote a more complicated iterative solver that would see if it could infer the type of the variable from later context and return to the member access later. For example, consider the following Rust code where the compiler could figure out the types with some additional complexity but doesn't bother: fn main() { let a = (1..10).collect(); println!("{:?}", a.len()); let b: Vec<i32> = a; } error[E0282]: type annotations needed

IggleSniggle 6y ago
Your comment has me feeling quite bullish on TypeScript type inference
chriswarbo 6y ago
> To some degree, both are propagating and unifying types through the program and throwing an error when trying to unify two things that aren't the same In fact they're so similar that they can be combined to give 'bidirectional typing'. This is mostly useful for systems that are more expressive than Hindley Milner. For example, dependently-typed languages like Agda and Idris require type annotations for top-level definitions (local definitions can sometimes be inferred). Bidirectional typing is a neater approach to such hit-or-miss inference approaches, and also allows values to be inferred (your function-overloading example is a case of value inference: using the types to figure out which particular function to call).
frank2 6y ago
>Rust gives up if you don't know the type of a variable and you try to accesses a member of it, where I once wrote a more complicated iterative solver that would see if it could infer the type of the variable from later context My guess is that Rust's designers would reply that their compiler is slow enough without the complication you describe.

IggleSniggle 6y ago

Your comment has me feeling quite bullish on TypeScript type inference

chriswarbo 6y ago

> To some degree, both are propagating and unifying types through the program and throwing an error when trying to unify two things that aren't the same In fact they're so similar that they can be combined to give 'bidirectional typing'. This is mostly useful for systems that are more expressive than Hindley Milner. For example, dependently-typed languages like Agda and Idris require type annotations for top-level definitions (local definitions can sometimes be inferred). Bidirectional typing is a neater approach to such hit-or-miss inference approaches, and also allows values to be inferred (your function-overloading example is a case of value inference: using the types to figure out which particular function to call).

frank2 6y ago

>Rust gives up if you don't know the type of a variable and you try to accesses a member of it, where I once wrote a more complicated iterative solver that would see if it could infer the type of the variable from later context My guess is that Rust's designers would reply that their compiler is slow enough without the complication you describe.