Hacker News Reader

Comment by iitalics | Hacker News Reader

Hindley-Milner is cool, but if you're planning on implementing a language with type inference, I strongly suggest you take inspiration from bidirectional type inference, notably Pierce-Turner[1] and subsequently Dunfield-Krishnaswami[2]. These algorithms are capable of inferring much more complex types and generally produce better error messages. Typically, there are very few programs which can't be typed when you combine Dunfield-Krishnaswami type inference and have the user place annotations on major function definitions.

[1] http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf

[2] https://arxiv.org/pdf/1306.6032.pdf

View on HN

Why are they capable of inferring much more complex types? Which sort of types can Hindley-Milner infer – what sort of types can Pierce-Turner and Dunfield-Krishnaswami respectively infer? Which programs still can't be typed using the latter method?

Dunfield-Krishnaswami handles higher ranked polymorphism but is probably most famous for just being a very nice presentation of bidirectional typechecking. Algorithm W (Hindley-Milner) is only able to infer first-order polymorphism occurring at generalization points (usually "let"s).

What does "bidirectional" mean in this context?

Here is what they say in the introduction of the second paper:

Bidirectional propagation of type information allows the types of parameters of anonymous functions to be inferred. When an anonymous function appears as an argument to another function, the expected domain type is used as the expected type for the anonymous abstraction, allowing the type annotations on its parameters to be omitted. A similar, but even simpler, technique infers type annotations on local variable bindings.

From this I gather it means syntactically bidirectional. (But I don't understand this really, so someone should correct me :P)

The algorithm is split into two mutual components the "inference" and the "checking" (upward and downward) which run together. This turns out to be a really flexible setting for playing with language and type features as it's often possible to figure out how to extend a bidirectional typer/inferrer with new features.

It means check both ways

    Gamma |- e => t

Given Gamma (the environment) and e, you want to derive the type t (bog standard type inference).

The other direction also holds:

    Gamma |- e <= t

Now we want to ensure that e conforms to type t.

Consider for example, a function:

    func foo(a) b

and an expression that we know the type of already:

    e <= a

Therefore we can say when we apply `foo` onto `e`, we'll yield something of type `b`

In effect, you perform 2 passes: forwards inference, and then backwards inference.

p/s: I'm not actually a PL person. This is from my casual reading, so my understanding is highly probably very wrong

I don’t fully understand it myself, but this seems like a good introduction:

https://people.mpi-sws.org/~joshua/bitype.pdf

edit: but it’s incomplete: it never gets around to discussing subtyping and thus helping justify its existence. I think the main point is that due to subtyping and other complexities, we may not be able to synthesize the type of an expression just by looking at it, but if its type has been determined by other constraints, we can still check that that type is valid for the expression.

Reply on news.ycombinator.com