[HN Gopher] Austral: A Systems Language with Linear Types and Ca...
___________________________________________________________________
Austral: A Systems Language with Linear Types and Capabilities
(2022)
Author : yamrzou
Score : 133 points
Date : 2025-03-20 04:37 UTC (18 hours ago)
(HTM) web link (borretti.me)
(TXT) w3m dump (borretti.me)
| zdragnar wrote:
| 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.
| adastra22 wrote:
| He's still working on it AFAIK.
| ofalkaed wrote:
| 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.
| rybosome wrote:
| 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.
| yellowapple wrote:
| Same. Feels like a precocious lovechild between Erlang and
| Pascal.
| toastal wrote:
| ATS2 would give you all the FP + linear types + a proof system.
| No "capabilities" tho.
| nerdponx wrote:
| Idris 2 has some really interesting stuff with linear types. IO
| is implemented using a linear "world" token. Every I/O
| operation consumes the current state of the world and returns a
| new state of the world. Each state of the world must be used
| exactly once. And the IO monad ends up just being syntactic
| sugar around this. See https://github.com/stefan-
| hoeck/idris2-tutorial/blob/main/sr...
| pieterr wrote:
| Earlier discussion:
|
| https://news.ycombinator.com/item?id=34168452
| nicoty wrote:
| 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 wrote:
| 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.
| sirwhinesalot wrote:
| 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.
| choeger wrote:
| 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.
| rixed wrote:
| 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 wrote:
| 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...
| aiono wrote:
| 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?
| conaclos wrote:
| 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/
| jamii wrote:
| I don't think Austral uses second-class references. Even the
| page you linked says:
|
| > But is it worth it? Again, the tradeoff is expressivity vs.
| simplicity... Austral's linear types and borrowing is already
| so simple. Austral's equivalent of a borrow checker is ~700
| lines of OCaml. The only downside of Austral is right now you
| have to write the lifetimes of the references you pass to
| functions, but I will probably implement lifetime (region)
| elision.
| skavi wrote:
| 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.
| beders wrote:
| I'm missing something on the discussion of correctness for Linear
| types: let file: File := openFile("test.txt");
| writeString(file, "Hello, world!"); g(file);
|
| If I have any other function 'g' that takes a File and returns
| Unit, wouldn't the compiler be ok with that. Now I have a
| dangling file pointer.
| tupshin wrote:
| Linear typed are "use exactly once". In this case you consume
| "file" when you pass it into writeString and then it is
| (compile time) unavailable to be used with g, afterwards.
| nine_k wrote:
| AFAICT the compiler would forbid to use `file` after the
| `writeString(file)` line, because it has been consumed.
|
| You can get something like affine types out of the linear types
| constructed this way, by returning new one-time value every
| time when operations on an object can continue:
| let file_1: File := openFile("test.txt"); let file_2 :=
| writeString(file_1, "Hello, world!"); g(file_2);
| beders wrote:
| yes, I mistyped. I wanted to take the File object from
| writeString foo = writeString(file, "Hello
| world!"); g(foo);
| sweeter wrote:
| looks like if Zig and Golang had a child. But I would expect
| something like file.writeString()
| assbuttbuttass wrote:
| g also has to use file exactly once
| randomNumber7 wrote:
| Its very interesting but i disagree with the operator precedence.
|
| > but programming languages have many categories of binary
| operators--arithmetic, comparison, bitwise, Boolean--and mixing
| them together creates room for error
|
| I think an expert should be able to remember the operator
| precedence of C and s.th. like
|
| a < x && b >= y
|
| is easier for a human to read than this
|
| (a < x) && (b >= y)
|
| Edit: Besides that it looks pretty promising. They even got it
| right to call the void type unit.
___________________________________________________________________
(page generated 2025-03-20 23:01 UTC)