narrow type in else block of if (is...)

[gavinking]

Tako gives this example:

shared Integer q(Integer? x) {
    if (is Null x) {
        return 0;
    }
    else {
        return x; //compile error
    }
}

He argues, rather reasonably, that the compiler should be able to reason that x has type Integer where the error occurs.

I agree that it would be possible. This would not amount to supporting types like X~Y, which Ross says results in undecidability, if I recall correctly. It just means being able to utilize the identity X|Y~Y == X, which we already do utilize in certain places.

On the other hand:

1. This example is a bit contrived. It would be much more usual to reverse the condition to do if (is Integer x) or if (exists x).
2. For more complex cases, this is stepping on the turf of the switch statement.

So I'm not sure that this feature would really be especially practically useful. OTOH, it's easily doable.

[quintesse]

He argues, rather reasonably

Don't believe this guy, I never said any such thing! ;)

[ikasiuk]

For more complex cases, this is stepping on the turf of the switch statement.

So how would switch behave in that case?

shared Integer q(Integer? x) {
    switch (x) {
        case (is Null) {
            return 0;
        }
        else {
            return x;
        }
    }
}

In any case, the behavior in the two examples should be consistent.

[gavinking]

@ikasiuk

You could write:

Integer q(Integer? x) {
    switch (x)
    case (is Null) {
        return 0;
    }
    case (is Integer) {
        return x;
    }
}

[ikasiuk]

Obviously. I just wanted to point out that the question posed by this ticket applies to switch as well as to if.

[gavinking]

Obviously. I just wanted to point out that the question posed by this ticket applies to switch as well as to if.

OK, sure.

[gavinking]

This feature would be even more useful for the else of if (nonempty seq), where we could narrow to Empty.

[gavinking]

As mentioned in #170, I could now start work on this.

[FroMage]

I got a remark during my presentation that people expect this to be true:

void foo(Apple|Garbage box){
 if(is Apple box){
  box.eat();
 }else{
  box.throwAway(); // box is a Garbage here
 }
}

[gavinking]

@FroMage Yeah so I will work on it as one of the first things for M5, I suppose.

[gavinking]

I wonder if we need the same thing for the else block of switch?

[FroMage]

Sounds logical to me.

[matejonnet]

+1 for ^4 (#74 (comment))

[gavinking]

Note to self: Once we implement this feature, we should also add !exists and !nonempty conditions, as proposed by #170.

[gavinking]

Note that #170 proposed that flow-dependent typing should work together with definite return analysis, to allow the following:

shared Integer q(Integer? x) {
    if (is Null x) {
        return 0;
    }
    return x;
}

This would be much more difficult to implement.

[lucaswerkmeister]

flow-dependent typing should work together with definite return analysis

I think it should work together with some more general type of flow analysis, because this should totally work without an assert:

String? str = "abc";
print(str.uppercased); // method or attribute does not exist: uppercased in type String?

(In a real-world scenario, str might be declared outside an if statement and assigned and used inside.)

A more brutal scenario for that analysis would be:

Integer i = ...;
String? str;
if (i == 42) {
    str = "abc";
}
...
if (i == 42) {
    // since i isn’t variable, this block is entered iff the first if block is entered
    print(str.uppercased);
}

(Not sure how useful that would be)

[gavinking]

@lucaswerkmeister see #536, which is planned for Ceylon 1.2.

[lucaswerkmeister]

... I really should search before making comments. Thanks!

[gavinking]

I have implemented this in the typechecker for switch (but not yet for if) in the 74 branch.

[gavinking]

Ok, and you also think there's no need to warn people like we do for other useless narrowings?

Well, no, these are totally different things. In other "useless" narrowings the entire if construct becomes superfluous. That's not the case here.

[quintesse]

Ok, understood.

[quintesse]

@gavinking how can I actually obtain the type of the Variable as it is seen from the else-block? (For the then-block we use isDecl.getVariable().getType().getTypeModel())

[gavinking]

The ElseClause has a getVariable().

[chochos]

I think something else changed because a totally unrelated test fails when I typecheck with this branch... I get a weird error when refining methods in a subtype like this:

span = whatever.span;
measure = whatever.measure;

I had to change it to

shared actual List<[Integer+]> span(Integer from, Integer to) => whatever.span(from, to);
shared actual List<[Integer+]> measure(Integer a,Integer b) => whatever.measure(a,b);

[gavinking]

@chochos Please give me a simplified bit of code that reproduces the error.

[chochos]

JS backend is done: !nonempty, !exists, and narrowing in else of if and switch. It's on branch spec-74 so let me know when you merge branch 74.

[chochos]

@gavinking Something as simple as this won't compile with this typechecker:

class Bug(String s) {
  equals=s.equals;
}

But it's only with methods; attributes don't have this problem:

class Bug(String s) {
  hash=s.hash;
}

[quintesse]

@gavinking this branch doesn't compile anymore, I'm getting :

The method getVariable() is undefined for the type Tree.ElseClause
The method getNot() is undefined for the type Tree.NonemptyCondition

and things like that.

[quintesse]

F**k, forget it, all that branch switching has liquified my brain.

[quintesse]

@gavinking I can confirm @chochos ' problem with this branch, have had time to take a look at that?

[gavinking]

It isn't this branch. It's on main. And I already have a partial fix for it.

Sent from my iPhone

On 13 Nov 2014, at 14:13, Tako Schotanus notifications@github.com wrote:

@gavinking I can confirm @chochos ' problem with this branch, have had time to take a look at that?

—
Reply to this email directly or view it on GitHub.

[quintesse]

Ok! Thx

[gavinking]

It's fixed by @7e9103f60fa456aed7e9c7bc028674ed6754f39b.

[chochos]

Not really. I'll open a separate issue.

[quintesse]

@gavinking the branch doesn't apply cleanly to master, could you merge master again please?

[gavinking]

@quintesse done.

[gavinking]

Merged. Closing, finally!

[gavinking]

In 9 days time, this issue would have turned three years old :-/

[sgalles]

@gavinking I stumbled upon something minor that I think is related to this issue :
This code obviously does not compile but there is a funny type in the error message :

 String foo<Bar> 
            (String|Bar element){
        if (is String element){
            return element;
        }else{
            return element;
        }
    }

error: returned expression must be assignable to return type of 'foo': 'Bar&Object|Bar&null' is not assignable to 'String'.
(I can open an other issue if you don't want to reopen this one)

[gavinking]

@sgalles OK, I agree that this was worth improving. Not a bug precisely, but anyway I have improved the algorithm in ProducedType.minus() to be a little bit less aggressive.

[jvasileff]

Oh, cool, this also addresses #1238!