If nothing else, Austral makes for a wonderful teaching language for linear types/regions/capabilities.
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.
https://github.com/bytecodealliance/cap-std
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.
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`.
No really I think you should use cap std maybe in a project and see if it meets your needs first
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.
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.
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.
[1]:https://wiki.clean.cs.ru.nl/download/html_report/CleanRep.2....
[2]:https://granule-project.github.io/papers/esop22-paper.pdf
>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.
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.
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.
> 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.
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?
https://se.cs.uni-tuebingen.de/publications/schuster19zero.p...
let file: File := openFile("test.txt");
writeString(file, "Hello, world!");
g(file);
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); foo = writeString(file, "Hello world!");
g(foo);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.
function closeFile (file : File) : Unit is
let { handle } := file; (* This consumes the file *)
fclose(handle);
return nil;
end;
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;
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;
record RootCapability: Linear is
value: Unit;
end;
function surrenderRoot(cap: RootCapability): Unit is
let { value: Unit } := cap;
return nil;
end;
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.
[0] https://borretti.me/article/second-class-references; [1] https://www.hylo-lang.org/
> 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.