Comment by zetalyrae | Hacker News Reader

Comment by zetalyrae | Hacker News Reader

Parent Full thread

You can think of it as either "Rust: The Good Parts" or "Modern Ada". It's a minimal language with linear types, capability-based security, an Ada-inspired module system, and strong typing. And it's designed with simplicity as the overriding goal: it's small enough that it fits in your head, and avoids becoming the Vasa[0].

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

[3]: https://austral.github.io/examples/

Linear types are interesting, however I don't buy "Rust: The Good Parts".

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.

It's about readability. You write the types for documentation, and to make it easier for people doing a code walkthrough to simulate what is happening in their heads.

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.

Coming from mostly C and Java (where I didn't have inference) and Python (dynamic types, no real annotation when I was writing it) I found Rust's degree of inference (Constants, function signatures, structures must spell their types, but other types can be inferred if unambiguous) very satisfying, and I don't fancy going back.

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 think the widespread consensus view is that function signatures should have type annotations. Local variables are more contentious, but even then, you don't strictly need type inference to omit the type annotation in local variables (except for disambiguation).

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.

I will say that I find the Java-style `Widget widget = new Widget(junk);` infuriating, this barely counts as inference, it's more like lookahead. `my widget = Widget(junk)` is easier to look at and shorter to type, while conveying the same information.

So the easy win has my vote.

Quite often it is:

    Widget w = new SpecialWidget (junk);

though. I kinda like verbosity. There is less magic to reason about in the language overall.

Languages which use only inference have been written, but it's just not ergonomic, no one wants to use that. So the Widget is always available as an annotation (although I can't read your intent out of one line of Java clearly, and depending on what that is, a cleaner type system than Java's might take care of covariance well enough that we still wouldn't care), or as a cast.

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.

I really like Golang’s inference which is much dumber than Rust (left type = right type)

> offering inference means either different implementations could have different inference rules, or else, those rules must be set out in full in the specification

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.

It's really similar to the language I'm writing a compiler for atm :). (I also like the syntax and choice of keywords.)

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?

1. I think it's good enough for concurrency. A big selling point of linear types is that, since there can only be a single reference to a linear value at any time, concurrency is trivial. You just send linear values through other threads on a channel, and they're consumed (from the point of view of the sending thread).

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.

Reply on news.ycombinator.com