revise fn sig and ty representation so that bot is not a type.

[pnkfelix]

Spawned off from #13847: @nikomatsakis says:

My preferred fix is to remove ty_bot from the set of types and instead instantiate a fresh type variable. This may cause a slight change in the set of programs we accept, but not much of one, and it should simplify a number of bits of code that must currently consider bot, which rarely makes sense. It will require some changes to the representation here and there -- for example fn return types will need to be an enum rather just a ty::t.

[pnkfelix]

I would be willing to mentor this.

[gamazeps]

On it :)

[gamazeps]

@pnkfelix I've been looking around the code, and I have to admit that I don't really know by what to start, would you happen to have any advice ?
(I'm avaible on IRC if you are, with the same nick ;) )

[nikomatsakis]

This is roughly what I had in mind:

1. Remove the ty_bot variant.
2. Function return types become Option<ty::t> instead of ty::t -- this is because we used to use ty_bot to communicate ! return type, but now we would use None (or perhaps a custom enum would be clearer, but anyway you get the idea). You need an analogous change to the AST. (*)
3. Wherever we would create a ty_bot -- that is, call ty::mk_bot() -- we replace that with a new inference variable (fcx.new_inference_var()).

I'm not sure what the fallout will be -- I can imagine that some of those new inference variables will wind up being unconstrained, leading to type checking errors. We can tackle that problem when we come to it I guess. For one thing, at some point, we should probably allow unconstrained type variables anyway, since they don't really hurt anybody afaik. But even if we don't want to do that more generally, we could at least allow these type variables to be unconstrained (that is, unify them with ()). The defaulting mechanism proposed in rust-lang/rfcs#213 would be perfect for this (not yet implemented, of course).

(*) This is actually how the AST used to be structured. For all I know, it may still be structured that way.

[ghost]

I should say I investigated removing ty_bot from the type system in the past and found that it may be rather impractical.

Specifically, in the following program:

fn f(v: Vec<uint>) {
    for x in v.iter() {
        let y: uint = if x > 0 {
            break;
        } else {
            42u
        };
        println!("{}", y);
    }
}

there'd be no obvious way of unifying the two branches (if and else). Or rather, specifically, on what basis would the type of the first if block be unconstrained? If we defaulted to () for that block, the types wouldn't unify.

I think it'd be possible to make it so that inference would look for all "diverging" constructs to decide the types of which branches it needs to unify but that seems to defeat the purpose.

Thoughts, @nikomatsakis?

[nikomatsakis]

On Sat, Sep 20, 2014 at 10:43:08AM -0700, Jakub Wieczorek wrote:

I should say I investigated removing ty_bot from the type system in the past and found that it may be rather impractical.

Specifically, in the following program:

fn main(v: Vec<uint>) {
    for x in v.iter() {
        let x: uint = if true {
            break;
        } else {
            42u
        }
    }
}

there'd be no obvious way of unifying the two branches (if and else).

The usual way is to create a fresh type variable as the result of the if branch,
which will then unify with anything. Do you think that will not work?

[ghost]

The usual way is to create a fresh type variable as the result of the if branch,
which will then unify with anything. Do you think that will not work?

But there's ambiguity in whether a type variable originates in computation diverging or if it's truly unconstrained. For example, with your plan implemented the following two programs would type check the same way:

if x > 0 {
    Default::default();
    ()
} else {
    42u
}

if x > 0 {
    break;
} else {
    42u
}

Whereas it seems the first one should not type check.

Specifically, any time the type of a statement in a block is unconstrained, the block itself would unify with anything. That seems like it'd be way too permissive and dangerous.

I may be completely off here but it doesn't seem like type variables give us the sort of nice propagation rules that ty_bot has. Not that I'm particularly fond of ty_bot...

[gamazeps]

Soooooo ...
Is this considered doable or should I move to another issue ?

[pnkfelix]

@gamazeps it seems to me that if you understand the conversation above, and want to still look into following the path outlined by @nikomatsakis in the comments above, then you should feel free to try. I myself would not want to close this issue until I have a chance to look into @jakub- 's examples carefully (I do not yet see why he claims that his first example would type-check under the plan).

But nonetheless, feel free to move on to another issue, since this one clearly may be more difficult than I had anticipated.

[nikomatsakis]

@jakub- I do not understand why you say that this program would type check:

if x > 0 {
    Default::default();
    ()
} else {
    42u
}

Can you clarify? For one thing, there is no bottom type involved here?

[nikomatsakis]

Specifically, any time the type of a statement in a block is unconstrained, the block itself would unify with anything. That seems like it'd be way too permissive and dangerous.

I think there is some misunderstanding. The bottom type is only "created" in the following situations:

1. The type of a return, break, continue
2. Invoking a function declared as -> !

It reflects the fact that control flow will never reach that point. I am proposing that we use a fresh type variable in these situations.

The bottom type is already considered, well, the bottom of the type lattice. This means that it is assignable to any other type (that is, bottom <: T is true for all T). In a sense, this means it "unifies with all other types" just as a fresh type variable would. If anything, I expect there may be scenarios where a fresh type variable to be slightly less permissive, as it can only be unified once.

[ghost]

After an IRC discussion with @nikomatsakis I can happily say I've been proven wrong and that the plan is workable. One thing that remains to be seen is how the new rules will affect expressions such as { return 42; } or { fail!(":("); }, where the diverging expression appears in the trailing statement of the block as opposed to the trailing expression itself. It seems like the fall out from the discussed change will be that this class of programs will break and will have to be converted, respectively, to { return 42 } and { fail!(":(") } unless, as an ergonomic measure, we incorporate some sort of special treatment for trailing statements.

@gamazeps, I think this is definitely doable and my alarm was unwarranted. :) Please feel free to proceed if you're still interested in implementing this and I'm more than happy to assist.

[nikomatsakis]

I don't think there is any reason that those programs have to break, but it is perhaps more refactoring than I imagined initially to keep them working.

[nikomatsakis]

In particular, the type checker would potentially have to track whether something diverges or not separately from its type, though of course we could take a different approach like marking the type variables in question in some special way.