TMI: More typechecker refactoring

[tim]

Almost finished with the big typechecker refactor. Or the typechecker refactor of moderate size, anyway. Getting libcore to compile with the refactored typechecker was painful, but once I got there, I got all the way through building stage1 and most of the run-pass tests! The first round of tests that failed were:

failures:
    [run-pass] /Users/tchevalier/rust3/src/test/run-pass/unreachable-code-1.rs
    [run-pass] /Users/tchevalier/rust3/src/test/run-pass/unreachable-code.rs
    [run-pass] /Users/tchevalier/rust3/src/test/run-pass/weird-exprs.rs

There was something satisfying about that. Little weird-exprs tests doing their job.

As for why the unreachable-code tests failed: trans (the part of rustc that translates Rust to LLVM) tries to use type information to avoid generating code for unreachable Rust expressions. This is all pretty ad hoc, but since we have the _|_ type in the type system, why not use it?

The expression in this case looks like return + 1. In the old typechecker, if you looked up the type for this instance of 1, it would have been int or uint. But return always returns and arguments to + in Rust are always evaluated left to right, so we know that the 1 is unreachable here. So the new typechecker says 1 has type _|_ in this context.

That caused the code to translate int literals to complain, since it's not expecting an int to have type _|_. Why would anyone write code like this, you ask? They probably wouldn't, but macros could.)

So I'll just make trans more consistent in when it avoids generating code for unreachable expressions. Arguably it might be better to make trans not approximate what code is unreachable and just treat _|_-typed things as if they are reachable and generate code for them, but that's a change for another day.

Comments

[cxcvi]

It's at this point that I feel somewhat compelled to ask what exactly the _|_ type means. And how it's supposed to be pronounced.

[tim]

Sure! _|_ is pronounced "bottom" and at least here, it means the type of values whose evaluation never returns to the caller (immediate context). So return has type _|_ because it returns immediately to the callee -- and fail!() expands to code using a primitive operation with type _|_, because it halts the program. Keep in mind that this is different from the type () (nil) -- let x = (); binds x to a value of type nil, whereas let x = return; pops the current stack frame before x has a chance to get bound.

We care because currently, the Rust typechecker looks for unreachable expressions -- ones that would have to be preceded by evaluating a value of type _|_ in the same context -- and warns about them. Though this should really be done outside the typechecker anyway.

The term comes from the theory of lattices and partial orders, and I guess Wikipedia is as good for the background on that as anything, though you don't have to understand all the math to understand how it works in programming languages (as usual).

[sanxiyn]

http://en.wikipedia.org/wiki/Bottom_type is probably a better Wikipedia reference.

[etb]

(Disclaimer: I don't actually know anything about Rust.)

I think all you need to know about partial orders is that ⊥ is below everything in the subtyping relation (which is a partial order). And ⊥ is below everything because it's uninhabited; the empty set is a subset of every set.

(I guess you mean the type of expressions (statements?) whose evaluation never returns? Values should be already evaluated, and you'll never actually get a value of type ⊥.)

[tim]

Whoops, yes -- expressions. (In Rust, almost everything is an expression and a statement is just an expression with a semicolon after it, or a let-binding.)