[HN Gopher] Interview about Austral, a systems programming langu...
___________________________________________________________________
Interview about Austral, a systems programming language with linear
types
Author : unbalancedparen
Score : 56 points
Date : 2023-12-24 20:01 UTC (1 days ago)
(HTM) web link (blog.lambdaclass.com)
(TXT) w3m dump (blog.lambdaclass.com)
| dgreensp wrote:
| 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 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 wrote:
| > 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 wrote:
| 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 wrote:
| 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.
| zozbot234 wrote:
| AIUI Rust is adding what is effectively linear types (i.e.
| types without auto-drop) to allow for better interaction with
| async programming.
| JonChesterfield wrote:
| 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.
| dang wrote:
| Related:
|
| _Austral Programming Language_ -
| https://news.ycombinator.com/item?id=36898612 - July 2023 (118
| comments)
|
| _What Austral proves_ -
| 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 - Dec 2022 (120
| comments)
| cyco130 wrote:
| 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
| Rusky wrote:
| 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
| cyco130 wrote:
| Very informative, thank you.
| smitty1e wrote:
| > 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 wrote:
| 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 wrote:
| Seems a bit of a paradox, no? Is it not pragmatic to go easy
| on the pragmatism when appropriate?
| Alifatisk wrote:
| It's exciting seeing new languages popup offering memory safety.
___________________________________________________________________
(page generated 2023-12-25 23:00 UTC)