Can you give some examples of what it looks like to destroy a linear value? Elsewhere in the thread you said the compiler doesn't privilege destructor functions over anything else. I'm a bit confused how it works.

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?

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

Ah 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.

Yes, 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.

Trying 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!

I like that in rust one can reuse variable names, since they are dead anyway. Makes sense to ‘update’ the old name with the new value, sort of like a swap-and-kill. Does austral have this? Seems like no reason not to.

No, in fact variable shadowing is not allowed.

Any other mechanism for fixing the ephemeral name problem? I don’t like having to invent meaningless names.

No names, just function piping.

This is the safe approach.

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 safe approach.

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.

Borrowing exists to fix this problem, I believe you can do something like this?

    let f: File := openFile("filename.txt");
    writeString(&!f, "first line");
    writeString(&!f, "second line");
    writeString(&!f, "third line");
    closeFile(f);

What would it take for you to reconsider macros / compile time evaluation?

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…