On Borrow Checking

[Richard (Rikki) Andrew Cattermole]

On 10/05/2025 4:21 PM, Walter Bright wrote:
> On 5/4/2025 3:49 PM, Richard (Rikki) Andrew Cattermole wrote:
>> On 05/05/2025 8:50 AM, Walter Bright wrote:
>>> The point of the borrow checker is to ensure there is exactly one 
>>> point of origin for a pointer and exactly one point of termination 
>>> for it.
>>
>> Hang on, that isn't the point of it at all.
>>
>> A borrow checker has got the _side effect_ of only having one entry 
>> and exit point for an object.
>>
>> But the _objective_ is to loosen the restrictions that an _ownership 
>> transfer system_ imposes on the type system whilst keeping its 
>> guarantees.
> 
> I don't see how that would be workable.

Okay that is interesting.

>> We do not have an ownership transfer system in D.
> 
> Yes we do, in @live code. That's exactly what it does. A pointer 
> assignment to another pointer transfers the ownership to the lvalue, and 
> the rvalue becomes "dead".

That is an owner state in the DFA.

Ownership transfer system operates at the type qualifier level and 
applies to a variable regardless of what function it is in.

See isolated from Midori, which was designed with D's type system in mind.

Currently people fake having one, by using a struct with a copy 
constructor that resets the old value.

>> herefore we cannnot have a borrow checker.
> 
> The implementation shows it works.
> 
> 
>> What we do have is a liveliness analysis with guaranteed modelability, 
>> and we do have a use for that, @restrict.
>>
>> Enforcing @restrict could be an incredibly useful tool to those who do 
>> data processing with simd, right now they are doing this by hand.
> 
> Restricted pointers in C are guaranteed only by the user, the compiler 
> does no checking.
> 
> You cannot vet restricted pointers without a borrow checker.

Exactly, so what I've been thinking is tying @live to @restrict, which 
would make it a very useful tool.

This is something it could shine at, given its current implementation 
details.

----------------------------------------------------------------------

I want to go back to an earlier example I did elsewhere, where I have 
this type qualifier ``unique``, that is for an ownership transfer system.

If you have an ownership transfer system without a borrow checker:

```d
void func(scope ref int*) {}

unique(int*) a = ...;
assert(a !is null);

unique(int*) b = a;
assert(a is null);
assert(b !is null);

func(b); // error
```

Very annoying, it is what we have today if we fake it with a struct, 
except people will use alias this... and no more compiler error.

When you have both an ownership transfer system with a borrow checker:

```d
void func(scope ref int*) {}

unique(int*) a = ...;
assert(a !is null);

unique(int*) b = a;
assert(a is null);
assert(b !is null);

func(b); // ok
```

You may notice that unique may implicitly be removed in the type system.
It is not the type systems job to care about it being removed.

It is the job of the borrow checker to enforce the guarantee the origin 
outliving the borrow.

This is what I mean by: "But the _objective_ is to loosen the 
restrictions that an _ownership  transfer system_ imposes on the type 
system whilst keeping its guarantees."

In practice it just means that the type system doesn't need to solve a 
problem that a DFA is going to later on.