ceylon / ceylon-spec

DEPRECATED
Apache License 2.0
108 stars 34 forks source link

flow-based type inference #536

Open gavinking opened 11 years ago

gavinking commented 11 years ago

A nice feature that it looks like Groovy now has is, if I'm understanding correctly, is the following:

value xy;
if (something) {
    xy = X();
    xy.x(); //xy has type X
}
else {
    xy = Y():
    xy.y(); //xy has type Y
}
print(xy.string); //xy has type X|Y

Currently we don't let you use type inference with "forward" specified values. So it would be very easy to make it mean flow-based typing.

Another example:

value x = X();
//x has type X
if (something) {
    x = Y();
    //x has type Y
}
//x has type X|Y

(This feature would fit nicely with the proposal to do type narrowing in else blocks.)

RossTate commented 11 years ago

This seems cool to me. Loops will be a little more restrictive, though.

quintesse commented 11 years ago

Loops will be a little more restrictive, though.

Out of curiosity: why?

RossTate commented 11 years ago

Loop-invariant inference is a big challenge in the analysis community, so we don't want to do that. We can have types be refined within the body of the loop, but by the end of the body of the loop that type needs to be a subtype of the type coming into the loop.

gavinking commented 11 years ago

When I finally get round to implementing this - and I'm looking forward to it, for 1.1 - what I probably need to do is get rid of the new sub-Scope every time the type of something changes and instead maintain a map inside ExpressionVisitor that keeps the "current" type (a stack of current types, I suppose) for each value, and copy that type on the MemberOrTypeExpression so the backend can get it from there.

lahwran commented 10 years ago

would make this simpler if I could just do if(!is ComponentName obj) - though I recognize that I'm doing it somewhat wrong anyway:

https://github.com/lahwran/sleeplocker/blob/427d14f2145398a17d08080d6f75e22091c8ca54/src/main/java/lahwran/androidlocker/locker.ceylon#L31

gavinking commented 10 years ago

@lahwran yes, this is part of #74, as mentioned in this comment https://github.com/ceylon/ceylon-spec/issues/74#issuecomment-11896085.

PhiLhoSoft commented 9 years ago

I wonder if the following fits in this feature, and if it is even possible.... Instead of:

class FlowBased()
{
    variable String? notDefinedYet = null;

    shared void doStuff()
    {
        notDefinedYet = "Now it is defined";
        doMoreStuff();
    }

    void doMoreStuff()
    {
        if (exists ndy = notDefinedYet)
        {
            print(ndy + "!");
        }
    }
}

we could write:

class FlowBased()
{
    variable String? notDefinedYet = null;

    shared void doStuff()
    {
        notDefinedYet = "Now it is defined";
        doMoreStuff();
    }

    void doMoreStuff()
    {
        print(notDefinedYet + "!");
    }
}

Ie. the compiler will find out that doMoreStuff() is always called after notDefinedYet is defined, so there is no need to check it in this function. Of course, if a path is added that risks to call doMoreStuff() without setting notDefinedYet first, the code would no longer compile...

The use case I frequently encounter (in Java) is in GUI applications where some data cannot be available at component creation time, so it is set later, then displayed. But we are sure it is displayed only after it is set, so the check for nullity is a bit redundant.

I am not sure the case is worth the effort of implementing it (if possible at all), but I had to ask... :-)

gavinking commented 9 years ago

@PhiLhoSoft No, compilers don't generally try to do stuff which involves tracing paths through multiple functions. That bumps up against circularities and nontermination etc, etc.

RossTate commented 9 years ago

The relevant term is "typestate". It's surprisingly difficult, though there is research on it from an analysis perspective and from a language-design perspective. The Wikipedia article seems to be a decent start with the key links I could think of.

On Tue, Oct 21, 2014 at 9:56 AM, Gavin King notifications@github.com wrote:

@PhiLhoSoft https://github.com/PhiLhoSoft No, compilers don't generally try to do stuff which involves tracing paths through multiple functions. That bumps up against circularities and nontermination etc, etc.

— Reply to this email directly or view it on GitHub https://github.com/ceylon/ceylon-spec/issues/536#issuecomment-59930748.