What does the Austral language bring to the table? Are there code examples?
By way of example: the borrow checker in the Rust compiler is 24.7k lines of code[1]. Austral's equivalent is 600 lines, because it's simply doing less. The linear type system is designed so that the rules fit in a page of text, and you learn them once and apply them everywhere, rather than fighting against an ever-changing, opaque pile of heuristics. It's much more like a normal type system and much less like static analysis.
There are a few example programs in the compiler repository[2] and the website[3].
[0]: https://www.stroustrup.com/P0977-remember-the-vasa.pdf
[1]: https://twitter.com/zetalyrae/status/1540883027743559682
[2]: https://github.com/austral/austral/tree/master/examples
In particular type inference (Rust has this, Austral does not) is a real quality of life improvement. If there's only one possible type X could be, what value is produced by insisting that I figure out how to spell that type to talk about X? This feels unimportant when X's type is an integer, but when it's an array of functions which return other functions that take an array of functions and return an integer, figuring out how to write what I'm doing is tiresome. The compiler knows, and I know, don't waste my time.
I presume that providing inference interferes with the ambition to have a small specification, because offering inference means either different implementations could have different inference rules, or else, those rules must be set out in full in the specification. However the quality of life improvement is real.
IDEs can add type annotations not present in the code, but there are many contexts (source control diffs, or code in a PDF, or code in a website) where that kind of software type annotation is not available.
I find that in OCaml, which has type inference for everything (function arguments, function return type, local variables, expressions) I end up writing the types almost everywhere, for two reasons. The first is documentation: it helps me to read and understand code I wrote ages ago.
But the second is that type inference often goes haywire, because the compiler doesn't know ahead of time whether the code you wrote is in error. So when you make a mistake, like forgetting to pass the right number of arguments to a curried function, the compiler will happily propagate that mistake around, even propagating the erroneously-inferred types to other functions. And you get these incomprehensible type error messages that come from places that are very separate from where the mistake actually happened.
And then I find myself taking a random walk through the code, adding type annotations to constrain the inference until I find my mistake. So why not skip the middle step, and require annotations?
Often, however, it isn't obvious what the type of an expression is going to be, and it's easier to construct the value level than the type level. For those cases you could simply force a type error to find out the type and write it in the text.
The simplicity reason is not that inference rules vary by compiler (the rules can be put in the spec), it's that type inference (as opposed to one-directional type propagation) can be complex to implement, and for simple extensions to an H-M type system it can become undecidable.
Never written any OCaml in anger, and it has been decades since I wrote more ML of any sort, so perhaps in OCaml I'd find there's too much inference for my taste.
I could easily modify the compiler to allow omitting types from `let` statements. Maybe for development you'd use annotation-free `let`s, and when publishing or otherwise finalizing code you have to write the type annotation.
I could be convinced to add this as a feature, but I tend to favor the strict and one-way-to-do-it approach.
So the easy win has my vote.
Widget w = new SpecialWidget (junk);
Java itself introduced syntax for eliding the type of simple variables, so this is an old complaint, but yeah: a little bit of inference goes a long way.
As a tangent, there is a third option (or a twist on the second), called "principle types": carefully design the type system so that there is only one possible type for each expression, or at least one "best" or "most general" type for each expression. The spec for this can be much smaller than a full type inference algorithm.
I haven't heard much from the usefulness of linear types in real world scenarios and would like to learn more from someone with a bit more experience.
- Is it enough to grow to do things like concurrency?
- Are non-linear types allowed?
- Are references possible?
- In which case, does it fall back to a GC? ref counting?
2. The set of types is divided into two universes: the Free universe (i.e. unrestricted) types like bool, int, records and unions containing other free types; and the Linear universe, containing linear types. So non-linear types are allowed and are the default for anything that's not a resource with a particular lifecycle (i.e., anything other than memory, file handles, socket handles, that kind of thing).
3. References are possible and they work like borrowing in Rust.
4. No refcounting or GC, it's done at compile time like in Rust.
The spec has some nice code snippets: