Comment by Panzerschrek
2 days ago
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?
2 days ago
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.
> 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.
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.
1 reply →
I'm going to be contrarian: Yes, you should learn about type systems if you want to design a programming language, and decide in full conscience what you need. At the very least, it will give you a concrete idea of what safety means for a programming language.
It doesn't mean you have to use an advanced one, but your choice choose be based on knowledge, not ignorance.
A lot of harm; including the billion dollar mistake, has been done by badly designed type systems from the Java/C/C++ family.
Java also has covariant mutable arrays. I can't believe they created the whole language and didnt realize that covariant arrays are unsound? Or didn't care?
They didn’t care about preventing all unsoundness at type check time. As long as JVM can detect it and throw an exception, it’s good enough for Java.
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.
You suggest that the programming language developers made a conscious choice to implement "messy" type systems. That's not at all how it came about. These messy type systems are generally a result of trying to work with earlier language design mistakes. Typescript is an obvious example. The type system was designed to able to type a reasonable subset of the mess of existing Javascript. There is no need to make the same mistakes in a new language.
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?
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.
Can you make an example of TypeScript's unsoundness that cannot be fixed with better encodings?