Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

How to choose between Hindley-Milner and bidirectional typing

thunderseethe.dev

Post reply on HN
Print view View original

41–50 of 50 posts

Re: How to choose between Hindley-Milner and bidirectional typing

#41

Post by StopDisinfo910 »

thunderseethe wrote: post #39
StopDisinfo910 wrote: post #35

Earlier quoted context omitted.

Not really, no. You can get localised unification but bidir as a whole like in Rust but you lose most of the advantage of unification. Hybrid systems are bidir for parts, unification for others. But, I maintain that what the article calls HM is trully unification independantly of what's above. This is not about algorithm W. It's actually about the tension between solving types as a large constraint problem or using a…

> You can get localised unification but bidir as a whole like in Rust but you lose most of the advantage of unification. Could you expand on this? I do not follow. You can create a bidir system that never requires annotations and uses unification to infer all types in the style of Haskell or OCaml. It is not often done because people are coming around to the idea that global type inference causes spooky action at a d…

> You can create a bidir system that never requires annotations and uses unification to infer all types in the style of Haskell or OCaml.

There is no more bidir if you do that. It's just plain unification.

> In some sense I think HM == unification because you can't really implement HM without unification. The first time a type variable encounters another type you'd be stuck.

You can't implement HM without unification but you can do unification which is not HM. Actually a lot of what people call HM is not really HM but evolution of it and sometimes significant evolution.

Re: How to choose between Hindley-Milner and bidirectional typing

#42

Post by ufo »

Panzerschrek wrote: post #10

I have my own programming language (pretty advance), but I don't even know what these two typing approaches are. Is it problematic? Or I just have one of these two without knowing that?

If your language is typed it's good to know at least a bit, so you can do the type inference properly; there are many ways to shoot yourself in the foot when it's ad-hoc.

Bidirectional type inference is a type inference style where you traverse the syntax tree once. Sometimes the type info flows top to bottom and sometimes it flows bottom up. If your type inference algorithm works by traversing the syntax tree, I suggest reading more about bidirectional type inference to get a better idea of how to best coreograph when the type info goes up and when it goes down.

Hindley-Milner type inference works by solving constraints. First you go through the code and figure out all the type constraints (e.g. a function call f(x) introduces the constraint that x must have the same type as the argument of f). Then you solve the system of equations, as if you'd solve a sudoku puzzle. This sort of "global type inference" can sometimes figure out the types even if you don't have any type annotations at all. The catch is that some type system features introduce constraints that are hard to solve. For example, in object oriented languages the constraints are inequalities (instanceof) instead of equalities. If you plan to go this route it's worth learning how to make the algorithm efficient and which type system features would be difficult to infer.

Re: How to choose between Hindley-Milner and bidirectional typing

#43

Post by thunderseethe »

StopDisinfo910 wrote: post #41
thunderseethe wrote: post #39

Earlier quoted context omitted.

> You can get localised unification but bidir as a whole like in Rust but you lose most of the advantage of unification. Could you expand on this? I do not follow. You can create a bidir system that never requires annotations and uses unification to infer all types in the style of Haskell or OCaml. It is not often done because people are coming around to the idea that global type inference causes spooky action at a d…

> You can create a bidir system that never requires annotations and uses unification to infer all types in the style of Haskell or OCaml. There is no more bidir if you do that. It's just plain unification. > In some sense I think HM == unification because you can't really implement HM without unification. The first time a type variable encounters another type you'd be stuck. You can't implement HM without unification…

What are you calling bidir, if the introduction of unification means its no longer bidir?

Re: How to choose between Hindley-Milner and bidirectional typing

#44

Post by ux266478 »

ruuda wrote: post #37
Drup wrote: post #23

Earlier quoted context omitted.

HM is not complex type inference. In fact, among all the approaches you cite, it leads to the simplest type system and the simplest implementation. Moreover, there are lot's of courses, reference implementations, and reasonable extensions for a wide array of features (structural subtyping, qualified types, etc). There are even type-system libraries to make it easy to implement (like Inferno). When new programmer disc…

It's not complex, in the sense that the rules are simple, but simple rules can still lead to complicated emergent behavior that is difficult for humans to understand, even if each of the 153 steps that the typechecker took to arrive at the result were easy to understand individually.

It's not any different than having 153 steps in any other computational sense. Even limiting ourselves to elementary arithmetic, horrendous opaqueness arises with 153 operations spanning the whole set. Are we going to pretend like arithmetic is a systemically problematic because of this? Any non-trivial formal construct is potentially dangerous.

If you're having trouble reasoning about how variables are unified, it's either because you never actually built a strong gut intuition for it, or it's because you're writing Very Bad Code with major structural issues that just so happen to live in the type system. In this case it's the latter. For an HM type system, 153 choice points for an expression is ludicrous unless you're doing heavy HKT/HOM metaprogramming. The type system, and more broadly unification, is a system to solve constraints. Explosive choice indicates a major logical fault, and most probably someone naively trying to use a structural type system like a nominal one and/or a bit too much unsound metaprogramming.

Thankfully of course, you can simply just specify the type and tell the compiler exactly what it should be using. But that's not really resolving the issue, the code still sucks at the end of the day.

Now higher order unification? That's an entirely different matter.

Re: How to choose between Hindley-Milner and bidirectional typing

#45

Post by Panzerschrek »

ufo wrote: post #42
Panzerschrek wrote: post #10

I have my own programming language (pretty advance), but I don't even know what these two typing approaches are. Is it problematic? Or I just have one of these two without knowing that?

If your language is typed it's good to know at least a bit, so you can do the type inference properly; there are many ways to shoot yourself in the foot when it's ad-hoc. Bidirectional type inference is a type inference style where you traverse the syntax tree once. Sometimes the type info flows top to bottom and sometimes it flows bottom up. If your type inference algorithm works by traversing the syntax tree, I sug…

> Bidirectional type inference is a type inference style where you traverse the syntax tree once.

Yes, in my language I just build code directly from syntax tree in single pass (with a couple of minor exceptions). No complex machinery for type deduction is involved. So, now I assume it's called bidirectional type inference.

Personally I find what Rust does with possibility to avoid specifying types for variables isn't that great. It allows writing code which is hard to read, since no type information is present in source code. Also I suppose that it makes compilation slower, since solving all these equations isn't so easy and computationally-cheap.

Re: How to choose between Hindley-Milner and bidirectional typing

#46

Post by bossyTeacher »

copx wrote: post #12
Panzerschrek wrote: post #10

I have my own programming language (pretty advance), but I don't even know what these two typing approaches are. Is it problematic? Or I just have one of these two without knowing that?

Probably not. Most popular programming languages have messy - unsound and/or undecidable - type systems e.g. C++, C#, TypeScript, Java,.. ..because that is more practical.

No. Some of this are essentially products of their time. C# for example used to be very ceremonial and class heavy while now it keeps adding features from the functional world. If c# was made nowadays, it would likely be more like modern Swift than 2010s Java.

Re: How to choose between Hindley-Milner and bidirectional typing

#47

Post by ndriscoll »

cardanome wrote: post #30
pjc50 wrote: post #24

Earlier quoted context omitted.

Type inference saves typing on the keyboard. Ironically the language which needed this most was C++, which took ages to get the "auto" keyword and can still have a bit of a problem with fully expanded template names in error messages.

I don't think saving a few keyboard strokes is a worthwhile design goal for most languages. You have to keep the types in your head anyway so it just increases the mental burden when reading the code. At least with dynamic typing you might be in a flow state and care more about the shape of data than the types so it might be valid. But in static type land, not so sure. But yeah as I said, definitely infer trivial thi…

> You have to keep the types in your head anyway so it just increases the mental burden when reading the code.

It's the opposite! Type inference means you can rely on the compiler to check that everything is consistent while you just read what's in front of you. You don't need to think about types at all; the annotations would just be noise.

It simplifies reading (via not needing to care) and writing (via suggestions/auto-complete/jump-to-definition/better error messages).

Re: How to choose between Hindley-Milner and bidirectional typing

#48

Post by wk_end »

Panzerschrek wrote: post #45
ufo wrote: post #42

Earlier quoted context omitted.

If your language is typed it's good to know at least a bit, so you can do the type inference properly; there are many ways to shoot yourself in the foot when it's ad-hoc. Bidirectional type inference is a type inference style where you traverse the syntax tree once. Sometimes the type info flows top to bottom and sometimes it flows bottom up. If your type inference algorithm works by traversing the syntax tree, I sug…

> Bidirectional type inference is a type inference style where you traverse the syntax tree once. Yes, in my language I just build code directly from syntax tree in single pass (with a couple of minor exceptions). No complex machinery for type deduction is involved. So, now I assume it's called bidirectional type inference. Personally I find what Rust does with possibility to avoid specifying types for variables isn'…

It's unclear from your comment whether you inadvertently have bidirectional type inference or if you just...don't have type inference.

So, just to be clear, bidirectional type inference is a particular kind of machinery for type deduction (complexity is in the eye of the beholder). The defining characteristic of bidirectional type inference is that type information flows in both directions, not that it takes a single pass for type checking over the tree.

And that's, again, a single pass for type checking - the compiler as a whole can and usually does still take many passes to go from syntax tree to code. Pascal was famously designed to be compiled in a single pass, but it doesn't have any type inference to speak of.

Re: How to choose between Hindley-Milner and bidirectional typing

#49

Post by ufo »

wk_end wrote: post #48
Panzerschrek wrote: post #45

Earlier quoted context omitted.

> Bidirectional type inference is a type inference style where you traverse the syntax tree once. Yes, in my language I just build code directly from syntax tree in single pass (with a couple of minor exceptions). No complex machinery for type deduction is involved. So, now I assume it's called bidirectional type inference. Personally I find what Rust does with possibility to avoid specifying types for variables isn'…

It's unclear from your comment whether you inadvertently have bidirectional type inference or if you just...don't have type inference. So, just to be clear, bidirectional type inference is a particular kind of machinery for type deduction (complexity is in the eye of the beholder). The defining characteristic of bidirectional type inference is that type information flows in both directions, not that it takes a single…

Indeed. The point I was trying to make is that an ad-hoc type inference scheme that works by recursively traversing the tree will probably be most similar to unidirectional or bidirectional type inference.

Re: How to choose between Hindley-Milner and bidirectional typing

#50

Post by nextaccountic »

kccqzy wrote: post #36
nextaccountic wrote: post #19

Earlier quoted context omitted.

In this case do yourself a favor and use something like simple-sub https://github.com/LPTK/simple-sub https://www.reddit.com/r/ProgrammingLanguages/comments/hpi54... https://dl.acm.org/doi/10.1145/3409006

I have implemented simple-pub a few years ago in a toy project. And no, the type inference user experience is still way worse than what’s acceptable for a mainstream language.

That's interesting. Can you share some specifics? Like, what makes it worse?

Anyway I didn't mean that simple-sub makes subtyping inference great. It (and mlsub) seems to be just better than previous approaches

Post reply on HN