Skip to content(if available)orjump to list(if available)

Austral: A Systems Language with Linear Types and Capabilities (2022)

sirwhinesalot

The explicit regions make it really clear what "borrowing" is actually doing. Rust tries to do as much as possible implicitly, which is convenient 90% of the time but when it doesn't work as you expect you're left scratching your head.

If nothing else, Austral makes for a wonderful teaching language for linear types/regions/capabilities.

rybosome

Linear types are an interesting idea.

I really liked the way that each transformation of the file was a separate File object, reminded me of functional style immutable data structures where each transformation returns a new structure.

toastal

ATS2 would give you all the FP + linear types + a proof system. No “capabilities” tho.

yellowapple

Same. Feels like a precocious lovechild between Erlang and Pascal.

skavi

Really love the principles set out here. Love the concessions made in order to keep the language simpler.

I've been idly considering building an alternative Rust std lib with a shape that reminds me of the capabilities system laid out here. In my case that was less out of a desire for supply chain security (impossible if I'm just swapping the std lib) and more to discourage side effects from being produced deep within the core of program logic.

WRT the rejection of async, has there been any consideration of a more general feature like generators or coroutines? Resumable functions are a really nice way to write state machines. I don't expect those to go out of style.

conaclos

An interesting design choice of Austral is the use of second-class references [0] in place of first-class references like Rust does. This makes the implementation of a borrow checker simpler at the cost of reduced expressiveness. Hylo (previously Val) [1] tries also to find a way of avoiding first-class references using value semantic and subscripts.

[0] https://borretti.me/article/second-class-references; [1] https://www.hylo-lang.org/

rixed

I love this project and particularly its documentation.

But:

> Design Goals

> - Simplicity (...) is the amount of information it takes to describe a system.

> (...)

>

> Anti-Features

> - There are no exceptions

>

> (Error handling etc. omitted for clarity.)

At first sight, error handling is going to be laborious in this language. I wonder what's the state of the art in PL theory regarding error handling in a context without automatic resource management. Anything better than manual bubbling up of errors up the chain of callers until one takes responsibility?

finiteparadox

A combination of staging and effects might be a candidate. Any other candidate will probably be staging + X.

https://se.cs.uni-tuebingen.de/publications/schuster19zero.p...

zdragnar

It's a shame the last release was 2023 and the status was planning and expanding the standard library. I find myself rather enjoying both the syntax and stated philosophy. Unfortunately, I'm not really in a position to contribute anything myself to keep it going.

ofalkaed

Someone opened an issue on the Austral github asking about the status, his response:

>Regrettably I have not had the time/energy to work on this for the past year or so. But that might change since I'm going to be funemployed soon.

adastra22

He's still working on it AFAIK.

choeger

Lovely. It is well written and has a design I can 100% agree with.

I am curious, though: How will separate compilation work? I think it's an important practical feature but polymorphism (which I simply assume from the presence of type classes) and flexible file/module mappings make it extremely difficult to implement.

aiono

Very cool! This is exactly the topic I will probably be working in my Masters thesis. I am curious if you done anything about linearity and concurrency in the type system. Can one send files across threads for example?

nicoty

If the author/someone with knowledge of the language lurks here, there's these unanswered questions from the previous discussions that I'd interested about: https://news.ycombinator.com/item?id=34205220

isaacimagine

Not the author, but both of those features seem unlikely to fit well with the rest of the language. I believe Borretti has commented on partial application in OCaml being a big pain because it can lead to weird type inference errors, and this was one of the motivations for not having type inference in Austral. Ditto pipeline operator, but I might be able to see unified function call syntax, maybe? f(a, b) == a.f(b). Would be curious to hear Fernando's thoughts on this.