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

Interview about Austral, a systems programming language with linear types

blog.lambdaclass.com

Post reply on HN
Print view View original

21–30 of 45 posts

Re: Interview about Austral, a systems programming language with linear types

#21

Post by _dain_ »

dgreensp wrote: post #2

As someone working on a language myself, I found this to be very high-quality material! It aligns with a lot of my thinking, and it’s educational. A random part of interest: I followed the link about how linear types and exceptions don’t mix: https://borretti.me/article/linear-types-exceptions In it, the author explains how linear types always need to be explicitly destroyed, and if you end up in a “catch” block, you…

>So why does Austral use linear types, not affine types?

Affine types give a safety guarantee: you can't use it more than once. The bad thing (double free, use after free) does not happen.

Linear types give that same safety guarantee, plus a liveness guarantee: you must use it, possibly in some nontrivial way.

A function that takes an affine value as an argument is enforcing a contract about the past behaviour of the caller, leading up to the call: having the affine value is proof that certain other functions were called in the right way to produce it. But returning an affine value gives you weaker guarantees about future behaviour, because you can use it zero times. At most you know that it will get Dropped. But maybe you want to enforce more interesting things than the Drop trait can express. Returning a linear value lets you do this: maybe the linear Foo you return can only be disposed of in conjunction with a linear Bar, like

    fn consume(x: Foo, y: Bar) -> Baz
And perhaps now Baz itself is linear, which has to be consumed in some other way ... at any rate, returning a linear value is proof that in the future, the program will advance through a particular state machine of function calls, where the states and transitions are defined by the available signatures. If Foo is linear but there's no simple function like

    fn drop(x: Foo) -> Unit
then buckle in, the compiler says you're not getting off the ride until it's over.

Re: Interview about Austral, a systems programming language with linear types

#23

Post by swsieber »

wredue wrote: post #18
mamcx wrote: post #4

Earlier quoted context omitted.

> So why does Austral use linear types, not affine types? Because linear types are simpler. The major reason here is that you don't need a "fancy" inference engine of lifetimes like the Rust borrow checker.

I very much doubt that linear types are simpler in a lot of cases. Do they look simpler in cheesy anecdotes? Sure. But again, graphs and linked structures come in the to fray and it’s immediately noticeable that there’s be some problems here. Or maybe I am crazy in thinking that “being forced to update every single link just cause one node updated” is a problem. Even if this is only superficial, I foresee there being…

My reading was that it is simpler to implement..

Re: Interview about Austral, a systems programming language with linear types

#25

Post by throwup238 »

_dain_ wrote: post #20
throwup238 wrote: post #16

Earlier quoted context omitted.

> One reason for linear types over automatic scope-based destruction is that the final destruction can take arguments and produce results in a more streamlined way. This is nice for e.g. handling errors on file close. Couldn't the language allow something like Zig's `defer` op except tie that explicit destructor to the type?

Because it doesn't have to be something you'd ordinarily think of as a "destructor". e.g. you might have multiple possible functions that consume the value, because you're modelling a state machine with several outgoing edges from the type-state. You get to choose the one you call.

`defer` allows for executing arbitrary expressions based on scope (the "destructor" called depends on the code path)

Re: Interview about Austral, a systems programming language with linear types

#26

Post by skybrian »

_dain_ wrote: post #21
dgreensp wrote: post #2

As someone working on a language myself, I found this to be very high-quality material! It aligns with a lot of my thinking, and it’s educational. A random part of interest: I followed the link about how linear types and exceptions don’t mix: https://borretti.me/article/linear-types-exceptions In it, the author explains how linear types always need to be explicitly destroyed, and if you end up in a “catch” block, you…

>So why does Austral use linear types, not affine types? Affine types give a safety guarantee: you can't use it more than once. The bad thing (double free, use after free) does not happen. Linear types give that same safety guarantee, plus a liveness guarantee: you must use it, possibly in some nontrivial way. A function that takes an affine value as an argument is enforcing a contract about the past behaviour of the…

It seems like a language could support both. That is, a type could either be automatically droppable or not.

Re: Interview about Austral, a systems programming language with linear types

#27

Post by crabmusket »

treyd wrote: post #14
Rusky wrote: post #6

Earlier quoted context omitted.

You don't need lifetimes or lifetime inference for affine types, either. Lifetimes/regions/borrowing are an orthogonal extension that you can add on top of either affine or linear types. (In fact Austral includes a region/borrowing system as well! It is a bit more explicit than Rust, along the lines of Rust's pre-NLL borrow checker, and with concrete binding forms instead of inference for regions, but this is also un…

One thing with explicit drops that Rust is having is that the thread can get SIGKILLed at any point without running destructors, which can complicate sync primitives and cause deadlocks in other threads if RAII is used for that. People do use it for that effectively but even if you have support for explicit drops it's really hard to ensure they actually run.

I can't quite parse your first line or two. Are you saying that explicit drops make SIGKILL a problem because the compiler can't automatically add in the right cleanups? Whereas if the compiler is in charge of adding all the drops, it can insert those into a signal handler?

Re: Interview about Austral, a systems programming language with linear types

#28

Post by crabmusket »

galangalalgol wrote: post #17
Rusky wrote: post #6

Earlier quoted context omitted.

You don't need lifetimes or lifetime inference for affine types, either. Lifetimes/regions/borrowing are an orthogonal extension that you can add on top of either affine or linear types. (In fact Austral includes a region/borrowing system as well! It is a bit more explicit than Rust, along the lines of Rust's pre-NLL borrow checker, and with concrete binding forms instead of inference for regions, but this is also un…

I believe I read australs borrow checker is rusts old version, possibly verbatim?

I haven't seen anything like that. I don't think Rust ever had linear types. This blog post has an explanation of Austral's linear type checking:

https://borretti.me/article/how-australs-linear-type-checker...

Re: Interview about Austral, a systems programming language with linear types

#29

Post by crabmusket »

wredue wrote: post #18
mamcx wrote: post #4

Earlier quoted context omitted.

> So why does Austral use linear types, not affine types? Because linear types are simpler. The major reason here is that you don't need a "fancy" inference engine of lifetimes like the Rust borrow checker.

I very much doubt that linear types are simpler in a lot of cases. Do they look simpler in cheesy anecdotes? Sure. But again, graphs and linked structures come in the to fray and it’s immediately noticeable that there’s be some problems here. Or maybe I am crazy in thinking that “being forced to update every single link just cause one node updated” is a problem. Even if this is only superficial, I foresee there being…

I think the point is they're simpler to specify and implement, and easier for the programmer to understand- not that they result in simpler code necessarily. From the language rationale:

> Is it simple? Yes: the type system rules fit in a napkin. There’s no need to use an SMT solver, or to prove theorems about the code, or do symbolic execution and explore the state space of the program. The linearity checks are simple: we go over the code and count the number of times a variable appears, taking care to handle loops and if statements correctly. And also we ensure that linear values can’t be discarded silently.

https://austral-lang.org/spec/spec.html#rationale-linear-typ...

Re: Interview about Austral, a systems programming language with linear types

#30

Post by epage »

FrustratedMonky wrote: post #24

Wasn't Rust created for systems programming, and strict types. Can I get a cliff notes on what this is doing to solve some pinch point that Rust isn't?

Async drop is a problematic case in Rust. Somehow grafting in linear types is one of the ideas that has been floated to solve this.

There is also a subset of developers (typically those used to the control of C and/or in the extremes of fault taulerance) that don't want the hiden control flow of implicit Drop / RAII so Linear types offers an alternative.

Personally, I'd also like a best-effort linear types so I can catch errors from closing file handles open for write. I can manually close to get the error but I want help to ensure I do it.

Post reply on HN