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.
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.
Or if it's deficient in some way, contribute to it perhaps
The idea behind cap-std is being a stdlib for wasm runtimes in the backend. Wasm is supposed to give us sandboxing for free. It would suck to squander that by not having granular capabilities.
This work eschews practicality. The API will be super annoying and no one will want to use it but me. For example, the IO god object is passed to main as a reference rather than by value. I don't think there's any risk of splitting the ecosystem and I don't expect the cap_std project to really be interested in my BS.
That said, I did not know about cap_std until you mentioned it. I might steal the thing where all fs functionality is provided as methods on a `Dir`.
> 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.
Although I like capabilities for both purposes, I imagine the latter in isolation is less approachable and marketable. Do you also count heap allocations as side effects to be externalized?
> 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.
Async/await in Rust is just stackless coroutines (which are just glorified state machines) with some async IO-specific conventions on top, so if we get "just" coroutines it will be more than enough.
> Do you also count heap allocations as side effects to be externalized?
I’ve gone back and forth on heap. I admire Zig’s handling of allocation failures, but I’d also like to use Rust’s alloc lib. I’m currently leaning towards allocation and printing to stderr being available under any context.
> Async/await in Rust is just stackless coroutines
Yup, it was actually through Rust’s async that I learned about stackless coroutines. There’s a really fun rust crate [0] that implements effects with Rust’s nightly coroutine feature.
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.
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...
The same technique is also done with uniqueness types, which Clean[1] implements.
They look very similar on the surface and are sometimes confused. The paper Linearity and Uniqueness: An Entente Cordiale[2] goes into depth on the differences - but it basically boils down to - Uniqueness is about the history of some value - a contract that asserts it has not been aliased in the past. Linearity is about the future of the value - a contract that it must be consumed exactly once, from this point onward.
The benefit of uniqueness types is that it enables us to perform in-place mutation, because we know that nowhere else is this value aliased. The benefit of linear types is to guarantee proper cleanup. The two systems complement each other, and we can have types which are both unique and linear - steadfast types.
Austral doesn't have uniqueness types as such, but Capabilities are used to fulfil the same purpose. Because capabilities must be created from other capabilities, they're unforgeable - so we can design types that encapsulate a capability which in effect, ensures their uniqueness, but it's a bit more cumbersome than having uniqueness as a property of the language. Granule has both systems built in - uniqueness and linearity - but it doesn't support types which are both - they have to begin unique and be made into linear values.
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.
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.
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
You would need first-class functions (closures). This might work for the example you've given where we pass in a string - a non-linear value.
However, consider the case where we might partially apply a linear value - the value will be consumed and stored as part of the closure object - but linear values can only be contained in linear types - which would mean that the function itself must also become linear - and then you would only be able to use it once. These would be "one-shot" functions - because calling them would consume them. You would only be able to use them once - and if you wanted to reuse them, you would have to return a new function to replace the old one each time you call it.
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.
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.
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?
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);
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.
`g` still has to make `foo`, the new handle for `file` disappear.
I guess the question is around. If the File library can implement `fn CloseFile(f: File) -> ()`, why can't I implement `fn g(f: File) -> ()`?
At least I should be able to do so using `File::CloseFile` underneath, but what guarantees that only the module defining a type can define sinks for it?
I guess this is an implicit restriction that isn't talked in depth. It should be fine to add sources and sinks to a linear type, but only if they are implemented through the module's own sources and sinks.
A function like `closeFile` will consume the linear value but not produce a new linear value - it returns `Unit`. It does this via a destructuring assignment (For example, File would be a record type with a field named handle).
function closeFile (file : File) : Unit is
let { handle } := file; (* This consumes the file *)
fclose(handle);
return nil;
end;
A module will usually provide opaque types, with the actual definitions encapsulated by an implementation file, similar to how C and C++ do it. Users of this library don't know what is in the type `File`, so they're unable to use the destructuring assignment themselves - so their only option is to call `closeFile`, or the compiler will complain that the linear value is not consumed.
You can of course, call `closeFile` from `g`, and then it's fine to make `g` return Unit.
function g (file : File) : Unit is
let file0 := (* do something with file *);
return closeFile(file0);
end;
The compiler actually enforces this. If g takes a `file` argument and returns Unit, then it MUST call `closeFile`. Failure to do so won't compile.
For a real example, check how the RootCapability type is defined in `builtin/Pervasive`[1]. It's declared as an opaque type in the .aui file, along with `surrenderRoot`. This is all the user of the type knows about it.
type RootCapability : Linear;
function surrenderRoot(cap: RootCapability): Unit;
In the .aum file both the type and surrenderRoot are actually defined.
record RootCapability: Linear is
value: Unit;
end;
function surrenderRoot(cap: RootCapability): Unit is
let { value: Unit } := cap;
return nil;
end;
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?
Linear types can only really be used in a single-threaded manner. If multiple threads could access the same linear value, you would lose all compile time linearity guarantees, since it's out of your control in which order the threads will run.
You can transfer a linear value to another thread, but it will consume it (no longer be available) in the thread which transferred it.
If you want something with a bit more flexibility, look into Relevant types. Relevant types behave in some ways like a linear type - they disallow weakening - which means for example, if you consume it in any branch of a selection, it must be consumed in all branches. Relevant types allow contraction - unlike linear types, which means you can use them more than once - you just have to use them at least once - ie, you must ultimately consume them like you would a linear type.
You can treat Relevant types as subtypes of Linear types. If you have a value that disallows weakening, but allows contraction, you can say at any point that you are going to forbid contraction from this point onward - effectively turning it into a linear type via an upcast.
Affine types are the opposite - they allow weakening (so for example, you can use them in some branches, but not all), and in return, you are not forced to consume them - but they also cannot be used multiple times because they disallow contraction. They're use at most once. They can also be considered subtypes of Linear types - but they're a disjoint set from Relevant types.
Have a look at Granule[0], which supports these types and their interaction via a system of graded modes.
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.
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.
If nothing else, Austral makes for a wonderful teaching language for linear types/regions/capabilities.