Ability to assert over shared attributes

[FroMage]

I'm trying to do this:

shared class Foo(X val){
   shared Y y;
   assert(exists y = val.possiblyY());
}

And well, it's not allowed, so I have to do this stupid code:

shared class Foo(X val){
   assert(exists y_ = val.possiblyY());
   shared Y y = y_;
}

Is it something we could allow or is there another way to do this?

[FroMage]

I suppose that's mostly a question for @gavinking ;)

[jvasileff]

:+1: I've run into this several times.

Also, other cases where the declaration is split from an asserted definition, like:

shared class Foo(X val) {
    Y y;
    Z z;
    if (val.hasYZ) {
        assert(exists y = val.possiblyY());
        assert(exists z = val.possiblyZ());
    }
    else {
        y = ...;
        z = ...;
    }
    ...
}

and the same with destructuring.

[gavinking]

I don't particularly see an obvious solution to this problem.

[quintesse]

What if the exists is not really narrowing the type of the resulting expression as in this case? The Y is the same type before and after the assert.

[gavinking]

@quintesse well in that case the problem simply doesn't exist.

[quintesse]

I'm not sure I understand. What I'm saying is that it seems it could work for the case where y has the type Y both before and after the assert and that it's just used to test the type of the expression that gets assigned to y. I don't know which problem doesn't exist in that case.

[lucaswerkmeister]

The problem in code like

shared Y y;
assert(exists y = val.possiblyY());

is that normally, an is, exists or nonempty condition always introduces a new variable. In this case, we want it to refer to an existing, definitely uninitialized variable instead.

EDIT: To clarify my comment: I don’t yet see what’s being proposed here. Under which conditions do we allow the is condition to refer to an existing variable instead of a new one?

• Only definitely uninitialized variables?
• Only not variable “variables”?
• Only in asserts?
• …?

[quintesse]

@lucaswerkmeister I'd say "yes", "no" (we still need the assurance variables don't get changed) and "no" (it would work everywhere we have type narrowing exist and is)

[gavinking]

Actually I have changed my mind. In fact there's nothing wrong with:

Y y;
assert(exists y = val.possiblyY());

Since we actually accept this:

assert(exists Y y = val.possiblyY());

So in fact we could simply eliminate the error in this case.

[gavinking]

The thing that would be new here would be the idea that a condition can be used to initialize an uninitialized but pre-declared variable, which is not currently possible. I'm not sure if that would be unacceptably confusing. Perhaps it would be.

An alternative would be to let you write:

assert(exists shared Y y = val.possiblyY());

But that's probably even worse.

[lucaswerkmeister]

An alternative would be to let you write:

assert(exists shared Y y = val.possiblyY());

But that's probably even worse.

Agreed, on both counts (it’s an alternative, but a horrible one). You really don’t want to fit a long docstring in there.

[jvasileff]

If the type of the variable y must remain the same, the condition is redundant information. But I think it would be better and more natural to allow narrowing. So, a condition on an uninitialized value would initialize and (if necessary) narrow.

Instead of:

Y y;
if (...) {
    assert(is Y y = val.possiblyY());
    assert(is YSub y);
    y.doYSubStuff();
}

You'd have:

Y y;
if (...) {
    assert(is YSub y = val.possiblyY());
    y.doYSubStuff();
}

[FroMage]

Or a stef expression:

shared Y y = stef(exists x = f()) x;

Where stef has the same powers as assert but with a cooler name. Ties in well with my other issue about assert in comprehensions...

[ncorai]

Bumped into this issue today