Lifetime tracking

[Timon Gehr via Digitalmars-d]

On 03.06.2016 01:12, tsbockman wrote:
> On Thursday, 2 June 2016 at 23:05:40 UTC, Timon Gehr wrote:
>> Whenever the type checker is using a certain piece of information to
>> check validity of a program, there should be a way to pass that kind
>> of information across function boundaries. Otherwise the type system
>> is not modular. This is a serious defect.
>
> Would you mind giving a brief example of how that applies to `scope`?
>
> (I'm asking for my own education; I have no personal opinion as to the
> right implementation at the moment.)

The simplest example is this [1]:

void foo(scope int* k){
     void bar(){
         scope int* x;
         x = k; // ok: lifetime of x ends not after lifetime of k
     }
}

Now we factor out the assignment:

// need to know that lifetime of a ends not after lifetime of b
void assign(S,T)(ref S a, T b){ a = b; }

void foo(scope int* k){
     void bar(){
         scope int* x;
         // need to check that lifetime of x ends not after lifetime of k
         assign(x,k);
     }
}

I.e. now we need a way to annotate 'assign' in order to specify the 
contract I have written down in the comments.

Note that it is tempting to come up with ad-hoc solutions that make some 
small finite set of examples work. This is not how well-designed type 
systems usually come about. You need to think about what information the 
type checker requires, and how to pass it across function boundaries 
(i.e. how to encode that information in types). Transfer of information 
must be lossless, so one should resist the temptation to use more 
information than can be passed across function boundaries in case it is 
accidentally available.



[1] It might be possible to get that example to pass the type checker 
with 'return' annotations only if I change 'ref' to 'out', but often 
more than two lifetimes are involved, and then it falls flat on its face.