Simple Bidirectional Type Inference
12 points by asb
12 points by asb
A few languages use Hindley-Milner type inference, such as Rust, Haskell, and F#.
Another algorithm which isn't used by any popular languages (to my knowledge) is called bidirectional type inference.
I don't know about F#, but I'm pretty sure both Rust and Haskell are using check/infer bidirectional schemes. They're definitely not just Hindley Milner. In fact, I think most modern languages have bidirectional schemes because the error reporting is much better.
For instance, see the difference in how Rust reports errors for if's with differently type arms depending on whether there's a type annotation and check mode is possible vs. it must infer. If it were just doing hindley Milner, it would've basically just inferred the type of the if and the second error would look just like the first.
Huh! That's really cool. I might need to update some of the docs of the rustc book to reflect what they're doing right now since it only mentions HM.
Bi-directional type inference is a simple concept: Instead of simply percolating types from leaf nodes upwards in an AST, bi-directional typing allows type information to flow downwards as well. ("AST" is used here only as a well-known example; there are many alternatives to represent source code and intermediate compilation forms.)
In reality, outside of rudimentary typing systems, bi-directional type inference becomes fairly complex, and introduces the potential for exponential complexity. (This may explain some of the Swift language compiler slow-downs that people have long complained about.) I think the benefits are well worth the complexity, but the complexity still exists.
Furthermore, global bidirectional type inference (potentially allowing entire programs to be fully typed at compile time, without requiring any type annotations whatsoever) tend to require dramatically larger compile contexts, preventing localization of compile state, and potentially making highly-desirable "language server" functionality quite expensive in larger projects due to type circularity and/or long dependency chains. I'm only aware of a few projects that have successfully pulled this off with reasonably useful type systems, but I'd expect to see this approach become fairly common in language groups that detest type annotations (a common trend, but one that I do not personally embrace).
FWIW the orchestration model that I found worked well to support bi-directional typing (whether a node is a basic block or an AST node etc.) is one that provides the following functionality:
Types getImplicitTypes(): without any down-flow type information, what type(s) does this node predict that it would emit?TypeFit testFit(Types): can this node emit the specified type(s), and if so, how simple vs convoluted ("TypeFit") is the necessary production?require(Types): lock in the types that this node must produceEach of these allows for recursive implementations. Interestingly, the traditional uni-directional typing can be implemented using this set of functions simply as: require(firstOf(getImplicitTypes()). It's always a nice bonus when you can express traditional models in simple forms using newer models.
In reality, outside of rudimentary typing systems, bi-directional type inference becomes fairly complex, and introduces the potential for exponential complexity.
Like more than HM does? I was under the impression that HM is also of exponential time complexity but in practice is efficient to check (because you have to write nonsense programs for it to explode like this one --- I'm assuming it explodes for this program at least).
HM definitely has exponential time complexity but for most "real" programs don't require this (see Mairson (1989) which shows this for (Standard) ML which uses HM). Something something, almost data is random, but we're almost always interested in the data that isn't.
I'm pretty sure that HM is the most widely used algorithm for bi-directional type inference, by a long shot. Different languages and type system designs will have different worst-case scenarios for inferencing, and the example you linked to is a reasonable example of "OMG that would be bad". Where I've hit it the worst in my own work has been in deeply nested lambdas without type annotations (or other type indications e.g. literals of a particular type), so it traverses back and forth across the nesting levels repeatedly as it narrows (decides) the potential solution set. Fortunately, each back and forth is shorter, as monotonic progress is required.