4 ms·
The idea is: linear interface, free core. Free types are the opposite of linear: they're unrestricted and can be used any number of types. For example: you can
by zetalyrae 4y ago
The idea is: linear interface, free core. Free types are the opposite of linear: they're unrestricted and can be used any number of types.
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 https://austral-lang.org/tutorial/borrowing
- _dain_ 4y agoAh great! So to summarize: - 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.
- zetalyrae 4y agoYes, that's correct >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.
- all_factz 4y agoTrying to understand: what’s to prevent someone from calling an FFI-defined function on a free type without going through the whole linear types rigmarole? E.g. could I call `fopen` and `fclose` directly to circumvent the whole `File` interface? 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!