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

11–20 of 45 posts

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

#11

Post by cyco130 »

Rusky wrote: post #8
cyco130 wrote: post #5

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

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…

Very informative, thank you.

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

#12

Post by JonChesterfield »

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…

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.

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

#13

Post by Avshalom »

smitty1e wrote: post #9

> 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.

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.

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

#14

Post by treyd »

Rusky wrote: post #6
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.

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.

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

#15

Post by smitty1e »

Avshalom wrote: post #13
smitty1e wrote: post #9

> 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.

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.

Seems a bit of a paradox, no? Is it not pragmatic to go easy on the pragmatism when appropriate?

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

#16

Post by throwup238 »

Rusky wrote: post #6
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.

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 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?

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

#17

Post by galangalalgol »

Rusky wrote: post #6
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.

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?

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

#18

Post by wredue »

mamcx wrote: post #4
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? 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 not insignificantly annoying issues in how one needs to manage graph and linked structures.

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

#20

Post by _dain_ »

throwup238 wrote: post #16
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 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.
Post reply on HN