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

11–20 of 50 posts

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

#11

Post by mietek »

laksjhdlka wrote: post #4
piinbinary wrote: post #3

> friends don’t just bring up type inference in casual conversation I wonder if this is a reference to "I need you to understand that people don't have conversations where they randomly recommend operating systems to one another" But to the actual point of the article: my understanding is that there are areas where you can use bidirectional typing (e.g. languages that have subclasses) where HM style type inference mi…

I once studied proof theory for a summer at a school in Paris and we talked about type inference and theorem proving all the time in casual conversation, over beers, in the park. It was glorious. Being a student is so much fun, and we often waste it, or at least don't value it as much as we ought. 20 years later I'd love to go back.

Join us in ##dependent on Libera IRC. We continue to talk about this stuff all the time, with a focus on Martin-Löf intuitionistic type theory.

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

#12

Post by copx »

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.

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

#13

Post by bboreham »

piinbinary wrote: post #3

> friends don’t just bring up type inference in casual conversation I wonder if this is a reference to "I need you to understand that people don't have conversations where they randomly recommend operating systems to one another" But to the actual point of the article: my understanding is that there are areas where you can use bidirectional typing (e.g. languages that have subclasses) where HM style type inference mi…

The subject does sometimes come up in my casual conversations, since Robin Milner was my first CS lecturer.

He never actually spoke about type inference in my presence. He did teach me CCS (pi-calculus predecessor) a couple of years later, by which time I could appreciate him.

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

#14

Post by js8 »

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.

I don't think it's more practical, being able to do things like type inference on return value is actually really cool. Maybe more practical for the programming language developer (less learning about type systems) than for the user.. but then you have to ask why build another language?

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

#15

Post by tonyg »

derriz wrote: post #9
kccqzy wrote: post #5

> What folks should actually be asking is “Does my language need generics?”. You should also ask “Does my language need subtyping such as subclasses?” And if the answer to both is yes, you should probably forget about Hindley Milner, or at least pick something far away from it on the spectrum.

HM handles sub-typing just fine? Numerous approaches have been known since the 1980s - Michael Wand’s row polymorphism is one such approach. https://en.wikipedia.org/wiki/Row_polymorphism

*Mitchell Wand

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

#16

Post by epolanski »

derriz wrote: post #9
kccqzy wrote: post #5

> What folks should actually be asking is “Does my language need generics?”. You should also ask “Does my language need subtyping such as subclasses?” And if the answer to both is yes, you should probably forget about Hindley Milner, or at least pick something far away from it on the spectrum.

HM handles sub-typing just fine? Numerous approaches have been known since the 1980s - Michael Wand’s row polymorphism is one such approach. https://en.wikipedia.org/wiki/Row_polymorphism

I've been implementing row polymorphism in my fork of Elm in order to support proper sum and substraction operations on unions, and it's far from trivial.

Example usecase: an Effect may fail with 2 types, but actually you have handled one/catched one so you want to remove it.

Elm-like HM systems handle fine, as you say it, row polymorphism mostly over records.

I'm not an expert in all of this, started studying this recently, so take my words with a grain of salt.

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

#17

Post by whizzter »

derriz wrote: post #9
kccqzy wrote: post #5

> What folks should actually be asking is “Does my language need generics?”. You should also ask “Does my language need subtyping such as subclasses?” And if the answer to both is yes, you should probably forget about Hindley Milner, or at least pick something far away from it on the spectrum.

HM handles sub-typing just fine? Numerous approaches have been known since the 1980s - Michael Wand’s row polymorphism is one such approach. https://en.wikipedia.org/wiki/Row_polymorphism

Structural subtyping yes, nominal subtyping is a bit pricklier.

As a developer I personally prefer structural subtyping, but structural subtyping is harder for a compiler to optimize runtime performance for.

Nominal sub-type hierarchies allows for members to be laid out linearly and member accesses becomes just an offset whereas a structural system always has the "diamond problem" to solve (it's hidden from users so not a "problem" but will still haunt compiler/runtime developers).

Now the kicker though, in practice nominal subtype polymorphism has other issues for performance on _modern_ computers since they create variable sized objects and cannot be packed linearly like monomorphic structures.

In the 90s when languages settled on nominal typing memory speeds weren't really an huge issue, but today we know that we should rather compose data to achieve data-polymorphic effects and singular types should be directed to packing.

Thus, most performance benefits of a nominal type system over a structural don't help much in real-life code and maintenance wise we would probably have been better off using structural types (iirc Go went there and interfaces in Java/C# achieves mostly the same effect in practice).

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

#18

Post by epolanski »

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.

Can you make an example of TypeScript's unsoundness that cannot be fixed with better encodings?

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

#19

Post by nextaccountic »

kccqzy wrote: post #5

> What folks should actually be asking is “Does my language need generics?”. You should also ask “Does my language need subtyping such as subclasses?” And if the answer to both is yes, you should probably forget about Hindley Milner, or at least pick something far away from it on the spectrum.

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

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

#20

Post by cardanome »

Does your language even need (complex) type inference?

Personally I am a bit skeptical about whether complex type inference doesn't do more harm than good in some cases. A valid alternative approach is to just make type declarations required. Sure infer trivial types like when doing variable assignment but other than that just expect types to be provided. This drastically cuts down on complexity and enforces more readable programs. And it gives you much better error messages.

Or go the opposite way: If you want a language that feels dynamic and leads to prototyping, well a type system that is total and complete might be too heavy. Instead of only allowing programs that are proven to be typed correctly you might want to allow all programs that you can not proved to be wrong. Lean into gradual typing. Everything goes at first and the typing becomes as strict as the programmer decides based on how much type information they add.

Those are both very valid approach. Not every language needs that level of type inference.

Post reply on HN