6 ms·

Interview about Austral, a systems programming language with linear types

dgreensp 3y ago
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 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 can’t easily go back and destroy things that are now out of scope, which control flow got interrupted while doing things with. “Why not just destroy things when they go out of scope?” I thought. The author addresses this, saying that types that you have to “consume” “at most once” are called affine types, and the compiler can clean them up for you, and it solves the problem with exceptions. Rust has affine types, and you don’t have to explicitly “destruct” every string/object/resource using the appropriate destructor for that type, manually, as you do with linear types (of course, the compiler will make sure you do it, but you have to do it). So why does Austral use linear types, not affine types? The reasons given do not really resonate with me (but I’m not a systems programmer); it’s that the compiler would have to insert hidden function calls, and secondarily, for temporary/intermediate values, the order of invocation might not be obvious; plus, maybe the programmer not doing something with a value is a mistake. I’m really glad the reasons are written out, however. In other areas I feel very aligned with the author, such as on the value of required type annotations and local inference rather than global inference, and I’ve saved the link to refer back to the way the opinion is stated.
- mamcx 3y ago
  > 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.
  - Rusky 3y ago
    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 unrelated to the affine/linear distinction.) 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.
    - treyd 3y ago
      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.
      - crabmusket 3y ago
        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?
        Rusky 3y ago
        Rust certainly doesn't insert automatic cleanup in signal handlers. I don't think there's actually any meaningful difference between linear types and automatic drop here.
    - throwup238 3y ago
      > 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?
- deleted 3y ago
  [deleted]
- JonChesterfield 3y ago
  Linear types are more powerful than affine in terms of implementing code that cannot go wrong as enforced by the type system. State machines reified in application code. Affine is fine if there's a catch all operation available for when the value drops out of scope which the compiler inserts. You can call deallocate or similar when an exception comes through the call stack. If the final operation is some function that returns something significant, takes extra arguments, interacts with the rest of the program in some sort of must-happen sense, then calling a destructor implicitly doesn't cover it. There's some interesting ideas around associating handlers with functions to deal with exceptions passing through but I think I've only seen that in one language. The simple/easy approach is to accept that exceptions and linear types are inconsistent.
  - fdupress 3y ago
    Linear types and handlers are even more inconsistent, given the continuations could be run more than once if not careful.
    - alexisread 3y ago
      This is why, in Koka, there exists initially and finally blocks, to control resource cleanup https://koka-lang.github.io/koka/doc/book.html#sec-resource https://koka-lang.github.io/koka/doc/book.html#sec-resource I think linear types and exceptions can play well together if you use controlled effects like this.
  - Rusky 3y ago
    One way you can think of the exception unwinding stuff is that each call provides not just one continuation (the usual return address) but two (also one for the cleanup), and that these are combined using the & connective of linear logic. This means both paths must use the same set of resources, and exactly one of them must be invoked. Interestingly, in linear logic this is equivalent (using De Morgan dualities) to a single continuation that expects a sum type: A^⊥ & B^⊥ = (A ⊕ B)^⊥.
    - JonChesterfield 3y ago
- _dain_ 3y ago
  >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.
  - skybrian 3y ago
    It seems like a language could support both. That is, a type could either be automatically droppable or not.
    - dgreensp 3y ago
      Yes, this. The notable thing in Austral is not that linear types are used somewhere, it’s that it’s all linear, even when destruction is just deallocation and could easily be done by the compiler (even in the presence of exceptions).
      - _dain_ 3y ago
        You might want finer-grained control over when deallocation happens.
- seanmcdirmid 3y ago
  You can destroy them if you know they weren't destroyed in the try block. If they are destroyed in the the try block, then they would be in a dreaded "maybe destroyed" state. What you really want to do is somehow destroy resources in finally blocks. This is true if you are using linear types are not actually, and need to work with things that are explicitly destroyed.
dang 3y ago
Related: Austral Programming Language - https://news.ycombinator.com/item?id=36898612 https://news.ycombinator.com/item?id=36898612 - July 2023 (118 comments) What Austral proves - https://news.ycombinator.com/item?id=34845895 https://news.ycombinator.com/item?id=34845895 - Feb 2023 (21 comments) Austral: A systems language with linear types and capabilities - https://news.ycombinator.com/item?id=34168452 https://news.ycombinator.com/item?id=34168452 - Dec 2022 (120 comments)
cyco130 3y ago
I thought the concept of "linear types" as defined here was simply another name for "uniqueness types"[1]. But the Wikipedia article claims there's a difference. [1] https://en.wikipedia.org/wiki/Uniqueness_type https://en.wikipedia.org/wiki/Uniqueness_type
- Rusky 3y ago
  Linear and uniqueness types sort of collapse into the same thing when an object is required to stay linear or unique for its entire life cycle. They become distinct, and sort of dual to each other, when you relax this restriction: linearity ensures that no copies or aliases are produced going forward, while uniqueness ensures that no copies or aliases have ever been produced in the past. In other words, if you call a function that is linear in its parameter, you know it won't form any additional copies of the argument, but the function can't assume it has the only reference to that argument, so it can't e.g. update it destructively. Conversely, a function that takes a unique parameter can make that assumption, but its caller can no longer assume that the argument it passed in is unique. See also this recent paper on the two: https://granule-project.github.io/papers/esop22-paper.pdf https://granule-project.github.io/papers/esop22-paper.pdf
  - cyco130 3y ago
    Very informative, thank you.
smitty1e 3y ago
> But Rust is a very pragmatic language, and the problem with pragmatism is that it never ends* I'll bite: why can't pragmatism feel when it's hitting the diminishing returns curve and, you know, fight for a modicum of principle? That is: pragmatic pragmatism should fall short of dogmatism.
- Avshalom 3y ago
  You can absolutely stop being pragmatic when it's hitting diminishing returns, but that means that you stop being pragmatic not that pragmatism has ended.
  - smitty1e 3y ago
    Seems a bit of a paradox, no? Is it not pragmatic to go easy on the pragmatism when appropriate?
- tempodox 3y ago
  I think what he means is that there will always be new special interests and use cases that could get pragmatic language support. If you're invested in a culture that provides this support, it will never end.
Alifatisk 3y ago
It’s exciting seeing new languages popup offering memory safety.
pjmlp 3y ago
> Just as Pascal introduced modules This is wrong, the notion of modules predated the units from UCSD Pascal units. https://en.m.wikipedia.org/wiki/Modular_programming https://en.m.wikipedia.org/wiki/Modular_programming I would assume an interview would do proper fact checking.
hollerith 3y ago
The main thing I want from a language with a borrow checker is faster compilation time than Rust's.
FrustratedMonky 3y ago
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?
- epage 3y ago
  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.

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 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 can’t easily go back and destroy things that are now out of scope, which control flow got interrupted while doing things with. “Why not just destroy things when they go out of scope?” I thought. The author addresses this, saying that types that you have to “consume” “at most once” are called affine types, and the compiler can clean them up for you, and it solves the problem with exceptions. Rust has affine types, and you don’t have to explicitly “destruct” every string/object/resource using the appropriate destructor for that type, manually, as you do with linear types (of course, the compiler will make sure you do it, but you have to do it). So why does Austral use linear types, not affine types? The reasons given do not really resonate with me (but I’m not a systems programmer); it’s that the compiler would have to insert hidden function calls, and secondarily, for temporary/intermediate values, the order of invocation might not be obvious; plus, maybe the programmer not doing something with a value is a mistake. I’m really glad the reasons are written out, however. In other areas I feel very aligned with the author, such as on the value of required type annotations and local inference rather than global inference, and I’ve saved the link to refer back to the way the opinion is stated.

mamcx 3y ago
> 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.
- Rusky 3y ago
  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 unrelated to the affine/linear distinction.) 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.
  - treyd 3y ago
    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.
    - crabmusket 3y ago
      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?
      - Rusky 3y ago
        Rust certainly doesn't insert automatic cleanup in signal handlers. I don't think there's actually any meaningful difference between linear types and automatic drop here.
  - throwup238 3y ago
    > 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?
deleted 3y ago
[deleted]
JonChesterfield 3y ago
Linear types are more powerful than affine in terms of implementing code that cannot go wrong as enforced by the type system. State machines reified in application code. Affine is fine if there's a catch all operation available for when the value drops out of scope which the compiler inserts. You can call deallocate or similar when an exception comes through the call stack. If the final operation is some function that returns something significant, takes extra arguments, interacts with the rest of the program in some sort of must-happen sense, then calling a destructor implicitly doesn't cover it. There's some interesting ideas around associating handlers with functions to deal with exceptions passing through but I think I've only seen that in one language. The simple/easy approach is to accept that exceptions and linear types are inconsistent.
- fdupress 3y ago
  Linear types and handlers are even more inconsistent, given the continuations could be run more than once if not careful.
  - alexisread 3y ago
    This is why, in Koka, there exists initially and finally blocks, to control resource cleanup https://koka-lang.github.io/koka/doc/book.html#sec-resource https://koka-lang.github.io/koka/doc/book.html#sec-resource I think linear types and exceptions can play well together if you use controlled effects like this.
- Rusky 3y ago
  One way you can think of the exception unwinding stuff is that each call provides not just one continuation (the usual return address) but two (also one for the cleanup), and that these are combined using the & connective of linear logic. This means both paths must use the same set of resources, and exactly one of them must be invoked. Interestingly, in linear logic this is equivalent (using De Morgan dualities) to a single continuation that expects a sum type: A^⊥ & B^⊥ = (A ⊕ B)^⊥.
  - JonChesterfield 3y ago
_dain_ 3y ago
>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.
- skybrian 3y ago
  It seems like a language could support both. That is, a type could either be automatically droppable or not.
  - dgreensp 3y ago
    Yes, this. The notable thing in Austral is not that linear types are used somewhere, it’s that it’s all linear, even when destruction is just deallocation and could easily be done by the compiler (even in the presence of exceptions).
    - _dain_ 3y ago
      You might want finer-grained control over when deallocation happens.
seanmcdirmid 3y ago
You can destroy them if you know they weren't destroyed in the try block. If they are destroyed in the the try block, then they would be in a dreaded "maybe destroyed" state. What you really want to do is somehow destroy resources in finally blocks. This is true if you are using linear types are not actually, and need to work with things that are explicitly destroyed.

dang 3y ago

Related: Austral Programming Language - https://news.ycombinator.com/item?id=36898612 https://news.ycombinator.com/item?id=36898612 - July 2023 (118 comments) What Austral proves - https://news.ycombinator.com/item?id=34845895 https://news.ycombinator.com/item?id=34845895 - Feb 2023 (21 comments) Austral: A systems language with linear types and capabilities - https://news.ycombinator.com/item?id=34168452 https://news.ycombinator.com/item?id=34168452 - Dec 2022 (120 comments)

cyco130 3y ago

I thought the concept of "linear types" as defined here was simply another name for "uniqueness types"[1]. But the Wikipedia article claims there's a difference. [1] https://en.wikipedia.org/wiki/Uniqueness_type https://en.wikipedia.org/wiki/Uniqueness_type

Rusky 3y ago
Linear and uniqueness types sort of collapse into the same thing when an object is required to stay linear or unique for its entire life cycle. They become distinct, and sort of dual to each other, when you relax this restriction: linearity ensures that no copies or aliases are produced going forward, while uniqueness ensures that no copies or aliases have ever been produced in the past. In other words, if you call a function that is linear in its parameter, you know it won't form any additional copies of the argument, but the function can't assume it has the only reference to that argument, so it can't e.g. update it destructively. Conversely, a function that takes a unique parameter can make that assumption, but its caller can no longer assume that the argument it passed in is unique. See also this recent paper on the two: https://granule-project.github.io/papers/esop22-paper.pdf https://granule-project.github.io/papers/esop22-paper.pdf
- cyco130 3y ago
  Very informative, thank you.

smitty1e 3y ago

> But Rust is a very pragmatic language, and the problem with pragmatism is that it never ends* I'll bite: why can't pragmatism feel when it's hitting the diminishing returns curve and, you know, fight for a modicum of principle? That is: pragmatic pragmatism should fall short of dogmatism.

Avshalom 3y ago
You can absolutely stop being pragmatic when it's hitting diminishing returns, but that means that you stop being pragmatic not that pragmatism has ended.
- smitty1e 3y ago
  Seems a bit of a paradox, no? Is it not pragmatic to go easy on the pragmatism when appropriate?
tempodox 3y ago
I think what he means is that there will always be new special interests and use cases that could get pragmatic language support. If you're invested in a culture that provides this support, it will never end.

Alifatisk 3y ago

It’s exciting seeing new languages popup offering memory safety.

pjmlp 3y ago

> Just as Pascal introduced modules This is wrong, the notion of modules predated the units from UCSD Pascal units. https://en.m.wikipedia.org/wiki/Modular_programming https://en.m.wikipedia.org/wiki/Modular_programming I would assume an interview would do proper fact checking.

hollerith 3y ago

The main thing I want from a language with a borrow checker is faster compilation time than Rust's.

FrustratedMonky 3y ago

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?

epage 3y ago
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.