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

31–40 of 45 posts

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

#31

Post by seanmcdirmid »

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…

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.

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

#32

Post by tempodox »

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.

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.

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

#33

Post by aatd86 »

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…

Curious, aren't lifetimes and borrowing there in order to control aliasing that linear type preclude?

I was seeing linear types as a kind of: manual ssa + definite assignment analysis + unused variable analysis with the goal to facilitate some typestate analysis by the compiler.

I know barely anything on the subject, just wondering.

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

#34

Post by fdupress »

JonChesterfield wrote: post #12
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 tha…

Linear types and handlers are even more inconsistent, given the continuations could be run more than once if not careful.

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

#35

Post by alexisread »

fdupress wrote: post #34
JonChesterfield wrote: post #12

Earlier quoted context omitted.

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 tha…

Linear types and handlers are even more inconsistent, given the continuations could be run more than once if not careful.

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

I think linear types and exceptions can play well together if you use controlled effects like this.

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

#36

Post by dgreensp »

skybrian wrote: post #26
_dain_ wrote: post #21

Earlier quoted context omitted.

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

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

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

#37

Post by _dain_ »

dgreensp wrote: post #36
skybrian wrote: post #26

Earlier quoted context omitted.

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

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

You might want finer-grained control over when deallocation happens.

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

#38

Post by Rusky »

JonChesterfield wrote: post #12
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 tha…

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)^⊥.

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

#39

Post by Rusky »

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?

Sure, this would just desugar to normal control flow and be checked for linearity in the usual way.

I'm not sure what you mean exactly by "tie to the type," though? Just some kind of standard name for it? The benefit of linearity here is that you can change its signature while still getting the compiler to enforce its usage, so you probably wouldn't want it to look like e.g. Rust's Drop trait.

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

#40

Post by Rusky »

crabmusket wrote: post #27
treyd wrote: post #14

Earlier quoted context omitted.

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?

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.
Post reply on HN