The function to close a database connection has to take in a linear value for a database handle, but it returns nil. How do you actually get rid of the handle? And how does the compiler stop you from doing it incorrectly (or does it?)?
---
Oh and, if open file handles are a linear resource, how do we do print-debugging? Do we need to thread a stdout/stderr linear value through the whole program?
For example: you can define a record type that contains only free values, but tell the compiler you want it to be linear.
record Foo: Linear is
x: Int32; -- machine-sized ints are free
y: Int32; -- but `Foo` is declared to be linear
end;
Then instances of `Foo` behave like any other linear type. To destroy it, you'd destructure its contents: let foo: Foo := Foo(x => 10, y => 20);
let { x: Int32, y: Int32 } := foo;
So, how does this relate to safety? Because you can have something like: record File: Linear is
ptr: Pointer[Nat8];
end;
Where `File` is a linear record that contains a free (unsafe) file pointer. You can hide this behind an API, as an opaque type: module Filesystem is
type File: Linear; -- `File` is opaque
-- etc.
end module.
Opaque types can be imported from the outside, but clients don't know what they contain. So they can't construct them directly or destructure them or access record fields. Instead, you have to expose constructors and destructors in the API: module Filesystem is
type File: Linear;
function openFile(path: String): File;
function closeFile(file: File): Unit;
end module.
The implementation of `closeFile` would simply be: function closeFile(file: File): Unit is
let { ptr: Pointer[Nat8] } := file;
fclose(ptr); -- FFI-defined function
return nil;
end;
>Oh and, if open file handles are a linear resource, how do we do print-debugging? Do we need to thread a stdout/stderr linear value through the whole program?Borrowing allows you to relax the linearity constraints for some time: https://austral-lang.org/tutorial/borrowing
- we destroy a linear value either by destructuring it ourselves, or by calling a cleanup function that transitively destructures it
- we can make a type opaque to importers of our module, which precludes direct destructuring by the user
- the compiler forces the user to eventually destroy the linear value
- therefore the user must call our cleanup function
And it's our responsibility to ensure the function implements the correct cleanup logic.
>we destroy a linear value either by destructuring it ourselves, or by calling a cleanup function that transitively destructures it
I think I'll borrow this for the tutorial because it's very succinctly put.
I’m sure there’s a good answer. This is a really cool and impressive project.
EDIT: Ah, just got to the section on "The FFI Boundary". Makes sense!
Rust’s name shadowing is technically safe, but a massive footgun because humans are human and assume that in the same scope the same name refers to the same thing.
With name shadowing, you have to read through every line to make sure that the otherwise immutable value hasn’t been replaced with an impostor.
IMHO, it’s one of the worst Rust design decisions and shouldn’t be copied.
People will say they’re too lazy to come up with temporary variable names, meanwhile Rust doesn’t have multiple dispatch so every fn name has to be unique, which I personally find more irritating…
This is the painful approach, which is demonstrated in this very introductory document:
let f: File := openFile("test.txt");
let f1: File := writeString(f, "First line");
let f2: File := writeString(f1, "Another line");
...
Foo63 is one of those things I do not miss from Erlang.> IMHO, it’s one of the worst Rust design decisions and shouldn’t be copied.
100% disagree. It's even more valuable to rust because of things like capture clause patterns.
> People will say they’re too lazy to come up with temporary variable names
No, people will say that most of the time temporary variable names make no sense and add no information. When you have an input of `T: AsRef<U>` and literally the first thing you do is ref' it, there's no value whatsoever to having two different names.
let f: File := openFile("filename.txt");
writeString(&!f, "first line");
writeString(&!f, "second line");
writeString(&!f, "third line");
closeFile(f);The unsafe pragma seems like an ugly exception to the otherwise seamless capability-safe design.
One thought— not a full one— is that a functional module system would allow for a comptime unsafe capability root.
I’m guessing the rejected alternative was to pass an unsafe capability; but that would get awkward quick…