Promote ! to a type.

[canndrew]

Promote ! to be a full-fledged type equivalent to an enum with no variants.

Rendered

[edited to link to final version]

[eddyb]

It had to be handled everywhere to prevent all sorts of weird errors and crashes, and it eventually became unmanageable.
Right now we mark an inference variable as diverging, to default it to () if unconstrained.
But it otherwise is a regular inference variable, and I believe you could fully emulate it after defaulting is implemented, e.g:

fn give_up<T = ()>() -> T {
    panic!("I give up")
}

[canndrew]

What sort of weird errors and crashes and why don't we have the same problem with Never/Void? Am I right that ty_bot was a bottom type in the sense of it being a subtype of all types?

It's the defaulting to () that I don't like. If an expression doesn't return any value then it doesn't return the value (). So how does it make sense to pretend it has type ()?

[eddyb]

You might be able to find dozens of rust-lang/rust issues mentioning ty_bot.
Yes, it was a bottom type, that's what "bot" and the bang sign refer to ("!" is supposed to look like "⊥").
Void doesn't have significant issues because the compiler doesn't care: passing values of it around does not count as unreachable control-flow, nor can Void be used in lieu of any other type.

Defaulting to () only happens if nothing constraints the type.
I guess you do run into trouble if you have, e.g. panic!() + 0, as (): Add<i32> does not hold.

We could prune obligations that do not need to be satisfied due to diverging inference variables and remove those paths from the CFG to avoid attempts at translating code that doesn't otherwise type-check.
But you have to be extra careful there, and you'd likely just run into corner cases everywhere, like we used to, although there's more tests now to get feedback from.

[canndrew]

Yes, it was a bottom type, that's what "bot" and the bang sign refer to ("!" is supposed to look like "⊥").

It's important to note that the ! I'm advocating here is not a bottom type. It behaves exactly like Void except that it can be silently cast to any other type (which IMHO is still ugly but it's necessary for backwards-compatibility). I can only imagine a bottom type being a pain in the ass. You'd need to have Vec<!> <: Vec<i32>, fn() -> ! <: fn() -> i32 etc.

Void doesn't have significant issues because the compiler doesn't care: passing values of it around does not count as unreachable control-flow,

It probably should. If we know code is dead it would be good to be able to prune it.

Defaulting to () only happens if nothing constraints the type.

Well it shouldn't, that doesn't make sense. It should default to an empty type like Void or !.

I guess you do run into trouble if you have, e.g. panic!() + 0, as (): Add<i32> does not hold.

With this RFC you could implement !: Add<i32>. More generally:

impl<T> Add<T> for ! {
    type Output = !;
    fn add(self, rhs: T) -> ! {
        self
    }
}

and panic!() + 0 would compile fine.

[eddyb]

The subtyping was the easiest part of it all, just fwiw. It's like one line in the right type-relating match block.
Your magical silent cast cannot be achieved through coercion because coercions cannot be triggered in every possible corner case.
You're left with subtyping, either directly or through inference variables.

But really, what is the value in having unreachable code type-check?

[eddyb]

@Ericson2314 Resolution is not "propagated", inference variables are being created and updated during the traversal of a function, and then the types of all the nodes and side-table miscellanea are resolved (which queries the state of the inference variables where necessary).

I don't understand why <rvalue> as _ is necessary, when just creating a new diverging inference variable would have the same effect, if diverging inference variables are always defaulted to ! instead of ().

However, that might be backwards-incompatible if any code is depending on the current default of () (via trait impls).
This is testable: create an enum BottomDefault {} lang item with no impls and use that as the default instead of ().
Optionally, modify rustc::middle::traits::select to consider BottomDefault: Trait as ambiguous (because unconstrained blanket impls would otherwise match).
That is a pretty small change. Once you've made it, ask @brson to do a crater run to evaluate the impact on the ecosystem.

[eddyb]

@canndrew "Keep track of where every ! came from" - types don't carry around any such identifiable information, except for inference variables.
Also, the type of nodes cannot change after they've been type-checked, again due to information loss and a need for efficiency: you can't re-evaluate every constraint in the function to ensure nothing broke due to an introduced coercion.
Most constraints are transient, resulting from the expressions being checked, and thus are not kept anywhere.
Maybe a MIR desugaring would have an easier time with after-the-fact mutations, but they still would be quite inefficient.

What you are describing is almost exactly the current implementation using inference variables, but with defaulting to !. See my above comment for more on that scheme.

[Ericson2314]

@eddyb

Resolution is not "propagated", inference variables are being created and updated during the traversal of a function, and then the types of all the nodes and side-table miscellanea are resolved (which queries the state of the inference variables where necessary).

Ah, so quasi-unification in a side table as the traverse happens.

I don't understand why <rvalue> as _ is necessary, when just creating a new diverging inference variable would have the same effect, if diverging inference variables are always defaulted to ! instead of ().

There is two things going on here. The first is limiting whatever magic we do to rvalues, which I think is good idea no matter what:

struct Baz;
struct Foo { bar: Baz }
fn asdf() {
    let x: ! = panic();
    x.bar = Baz; // WTF
}

The second is adding this coercion under the hood. I agree that is not necessary, and basically an implementation strategy that shouldn't be noticeable. But I suspect it might actually help with the implementation: as opposed to have seemingly normal expressions be type checked rather oddly, we associated all the magic with one AST/IR node (the conversion).

Also, I'd immediately like to immediately deprecate the coercion once ! becomes a real type. Perhaps if panic! and friends can be changed to be for<T> fn() -> T, there ergonomic fallout will be acceptable. Pruning the no-op ! -> ! conversions from the AST/IR, and then warning on the others seems like the easiest way to do this.

[eddyb]

How would x.bar = Baz; compile, given that x has an undetermined type?
Maybe you could create such an example with a trait that has only one impl, as we assume that impl applies unconditionally.
Again, I don't see the point of introducing conversions to inference variables instead of instantiating ! as inference variables that default to !.

[Ericson2314]

Ok, didn't realize it wouldn't default to Foo, but remain unconstrained. How about this?

struct Baz;
fn foo(_: &Baz) { }
fn bar(_: Baz) { }
fn asdf() {
    let x: ! = panic!();
    foo(&x) // WTF
    bar(x) // still arguably WTF, but needed for back-compat
}

[Ericson2314]

Overall I'm super for this! One thing to keep in mind:

let x = SOMETHING as *mut !;
let y = unsafe { *x };

I suppose it's UB, but this could be some especially bad UB if the code is considered unreachable.

[canndrew]

@Ericson2314 It would be more like

let x = unsafe { SOMETHING } as *mut !;
let y = *x;

If you have a &! you wouldn't need an unsafe block to dereference it. Just like you don't need an unsafe block to dereference a &Void today. However there isn't a safe way to create a &! because there isn't a safe way to create a ! for it to point to. If you have a ! then you're definitely dealing in undefined behaviour.

You could write something like:

let x: () = ();
let y: !  = unsafe { mem::transmute(x) };
match y { // undefined behaviour! Where are we executing now!?
}

(Assuming rust continues to treat empty types as having size 0). But you can already do that with Void. You can also do an equivalent thing with non-empty enums:

enum Wub {
    A = 0,
    B = 1,
}

let x: u8 = 123;
let y: Void = unsafe { mem::transmute(x) };
match y { // undefined behaviour! Where are we executing now!?
    Wub::A => ...
    Wub::B => ...
}

[glaebhoerl]

@canndrew I think @Ericson2314's *mut example is more correct: dereferencing a *mut (of any type) is unsafe, casting to one with as is not. Whereas &'a T is a type that's statically guaranteed to be safe to dereference, because it cannot live longer than the value it refers to, this is explicitly not true of *mut T, where the burden is on the programmer to dereference it only when it is dynamically safe to do so (when it actually points to a live T) - and to state her belief that it is so with an unsafe { }. The times when it is safe to dereference a *mut ! just happens to be "never" (because there is never a live !), but precisely because *mut ! doesn't guarantee liveness, it is safe to create values of that type. (Indeed it's a common pattern in FFI bindings to encode abstract C types which are only handled through pointers as empty enum types on the Rust side.)

I'm also +1000 for this proposal, presuming we can achieve some clarity on what the actual problems with the old ty_bot were, why they don't manifest with enum Never { }, and where the new ! would fall in between.

[canndrew]

Sorry, that was careless reading. I saw *mut ! and thought "pointer".

[RalfJung]

From a type-theoretic perspective, I absolutely agree Rust should have an empty type just like it has a singleton type. It should also be consistent about not calling () "empty type", because it really is not. It has an element, also written (). C started this bad habit by saying "void is an type empty, so it's for functions not returning anything" - which is just plain wrong, "void" is a singleton type (whose only element we cannot name), it's for functions that don't return any information - because you already know which element of () you will get. It would be a shame for Rust to inherit this flaw, in particular considering how much it learned otherwise from functional languages.

[eddyb]

@RalfJung Where is () called "empty"? It's official name is "unit", and it's technically a 0-tuple.
struct Foo; types are called "unit structs", not "empty structs".

[RalfJung]

@eddyb : Certainly above someone wrote "Currently empty types are represented as ()". I did not check the documentation, and if Rust is already consistent about this, and it's just about doing more education, even better!

[pnkfelix]

@RalfJung Ah, that explains the confusion. The phrase "X is represented as Y" is not the same as "X is synonymous with Y".

In particular, it is a particular implementation artifact that empty types are represented as having zero-size (and thus have the same quote-unquote 'representation in memory" (which is a bit of a joke since they do not actually have any bits in the memory at all)).

This means for example that:

1. one cannot assign from an empty enum to a variable of zero-sized type.
2. but, one can (today) do an unsafe mem::transmute from zero-sized value to a variable that has the type of an empty enum. This leads to all kinds of "fun" -- there is a reason that transmute is unsafe.

Update: see also for examples of such "fun":
rust-lang/rust#4499
rust-lang/rust#12609
rust-lang/rust#24590

[RalfJung]

I would say that the phrase "representation in memory" is pretty much meaningless for empty types. A representation says for each value of the type how it is stored (a function from values to lists of bytes, for example). If there is no value, there's not much to talk about (a function from the empty set to something, there is exactly one unique function like that).

In particular, () and ! do not have the same "representation function": The former maps the only value (unit) to the empty list of bytes, while the latter doesn't map anything since its domain is empty. So arguably, the "representation of the empty type" is very different from the one of ().

A transmute to an empty type should always be UB, nothing else can make any sense. Thus the only remaining question here is what size_of says. The correctness statement of size_of is: Any list returned by the representation function, must have that length. For the empty type, there is no list returned by the representation function, so it really doesn't matter. size_of can return anything, so 0 is just fine.
In particular, any match on an empty type can never be executed, so there's nothing to say about its run-time semantics.

If this is all done consistently, there shouldn't be any problems. In fact, there's an entire class of languages that crucially relies on this kind of behavior for empty types, namely proof systems like Coq or Agda. These languages don't have unsafe operations, but by making the creation of an inhabitant of the empty type UB, that part is taken care of.

[nikomatsakis]

I think the sentiment of this RFC is reasonable, but it is underspecified and not a particularly pressing problem. I agree with the idea that a bottom type might be an interesting extension, but reasoning thoroughly about it seems to add significant complexity, with relatively little benefit -- particularly since one can model it using your own enum. Moreover, the coercion/subtyping semantics from the RFC seem quite underspecified. In general, the code for our coercion and subtyping is too complex as it is, and I am very reluctant to try adding extensions for this use case, at least until we done a better job of formalizing and isolating the coercions we already do.

[canndrew]

I don't understand the details of the compiler well enough to specify how the coercion/subtyping stuff could work. Either someone who knows more would have to expand the RFC or I'll have to have a crack at implementing it myself and see what I can come up with - but I'll need help with that.

Also, from my (probably niave) point of view I'm not convinced that this makes things more complicated. Rust already has empty types but it also this ! psuedo-type that can only be used as a function return type and it has this division between converging and diverging expressions being treated as two different kinds of things. We can use the first thing to eliminate the other two things.

[Ericson2314]

@nikomatsakis

• While there is some nuance as this thread shows, I feel like the complexity is the "fault" of our existing coercions, not having ! as a real type.
• @eddyb's solution is exactly just keeping the treatment of ! we have today, and not doing any coercions with types including/parametrized-with !. Conceptually it wasn't immediately obvious given the discussion, but code-wise it is keeping the precisely coercions we have today and thus ought to have little impact on the code complexity.

[Virtlink]

My understanding of type theory is limited, but it seems to me you're confusing the bottom type and the void type. The bottom type is for functions that never return, thus where ! is used today. The void type is for functions that return no meaningful value, thus where () is used today. Then there are unit types, types with only one value, thus an empty struct. The void type is a special unit type that has no associated operations, which is what makes () the void type and struct Foo; not.

The return type of break type should be the void type () (not the bottom type !) because it returns no meaningful value, but the return type of panic should be the bottom type ! because it can't return at all.

---

I see the value of your proposal to allow ! as a type. It would allow you to pass a diverging function around. But since there exists no value of type !, you can't do let x: ! = exit(0) or Result<String, !>, or implement functions for values of type !.

[RalfJung]

The void type is for functions that return no meaningful value, thus where () is used today. Then there are unit types, types with only one value, thus an empty struct.

I would argue that the void type and the unit type are both the same: They are inhabited (functions returning it can return), but there's no information to be gained from an inhabitant of the type. (The Void type is not a common term in type theory, but the empty type and the unit type are.)

The bottom type is the type that has every type as a subtype, whereas the top type is the type that is a subtype of every type. A priori, both of these terms are only about the subtyping relation, and not at all about how or whether the type is inhabited.
Once Rust has an empty type, it would be possible to make it the bottom type (by extending the subtyping relation appropriately), but discussion above suggested to me that that will probably create more problems than it solves.

The return type of break type should be the void type () (not the bottom type !) because it returns no meaningful value

break never returns to its caller, so it should have return type !. If you have a piece of code break; do_something(), then you know that do_something will never be run, just like if you have code after panic. That justifies giving break the empty type as return type. The same applies to continue. (And goto, if Rust had it.)

EDIT:

But since there exists no value of type !, you can't do let x: ! = exit(0) or Result<String, !>. Also, by definition, you can't implement functions for values of type !. A function returning ! such as exit() can't return, as there is no value of type !.

Well, actually, both of these are fine. The point is, the code will never come to the point where x is used, or where the function that takes ! as argument is run. It's perfectly fine to allow such code to be written, and there's no need to ever compile it. In the case of generic functions, adding extra checks that the arguments are not ! would be a pointless complication.

[canndrew]

The same applies to continue. (And goto, if Rust had it.)

And return which is also an expression in Rust.

Also it's worth noting that the type proposed in this RFC is not the bottom type. The bottom type is a subtype of all types so making ! bottom would mean making, eg. Vec<!> <: Vec<i32>. What's proposed here is a canonical empty type (like () is a canonical unit type), albeit one that can be silently coerced to any other type.

[nikomatsakis]

While there is some nuance as this thread shows, I feel like the complexity is the "fault" of our existing coercions, not having ! as a real type.

Regardless of where the "fault" lies, it seems clear that adding further coercions to the existing system will increase complexity. At the end of the day, I don't think there is sufficient motivation for such a change at this time -- particularly as we are unsatisfied with the existing coercion code and rules today, which are not capable of inferring all the coercions we would like. This matter of inference is relevant to this RFC as well: in particular, this change would be a breaking change unless we can reliably infer the necessary coercions, which I am pretty sure we would not. Therefore, I am inclined to close this RFC until we have improved the inference situation around coercions and/or a stronger motivation arises.

[canndrew]

it seems clear that adding further coercions to the existing system will increase complexity

This doesn't seem clear at all. The whole point of this RFC is to simplify the type system. Being able to write stuff like Result<T, !> is just an added bonus.

The fact that let x: i32 = break; compiles but let x: i32 = break as i32; doesn't isn't bad because people frequently want to write code like this, it's bad because it's weird and weirdness is usually a sign that something is wrong. What's wrong here is that Rust doesn't have a type to assign to diverging expressions. Any empty type will do. But Void isn't a lang item and we already have the ! syntax for diverging functions. Assigning type () here doesn't make any sense. Whoever decided that rule was thinking "I need a dummy type to put here. () is the trivial type so I'll use that." The correct answer was the other trivial type but that wasn't available.

Is there a reason that ! hasn't been a type since the beginning? I'm talking about the empty type ! not the subtype-of-everything type ! that got removed for being too painful. Any arguments against the usefulness of ! can be made about () aswell. () is pointless as a function argument, it's pointless as a variable, it's pointless in a struct or tuple and if you really want something like () you can always just define your own struct Void;. It could've been left out entirely except for as a way to express functions that don't return any data. Blocks that are now typed () could have been handled outside of the type system altogether. Do you think that would have made the language less complicated or more complicated? If more so then why?

That's not rhetorical. The guys who made C kept their language simple by not making void a type. They were wrong. And all the arguments in favor of having () as a type can be made for ! as well. Rust's current ! is a type in disguise. If you just take off it's disguise you'll have a natural way to talk about diverging expressions within the type system and a bunch of weird and generic-code-breaking things in the corners of the language will evaporate. Implementing it would mean removing a bunch of divergence-related types and checks in the compiler as most of it would be obsoleted by the type-checking machinery you've already got (eg. you don't need to check that a diverging function doesn't return, just check that a function that returns ! does in fact return !). All of the divergence-handling code could be subsumed by type-level checks if it already handled typed and untypeable diverging expressions consistently (eg. if code that handles a Void was detected as unreachable, if Void-returning functions were marked with llvm's NoReturn etc.).

particularly as we are unsatisfied with the existing coercion code and rules today, which are not capable of inferring all the coercions we would like.

If you're thinking about adding more inference then that's all the more reason to think about adding ! now while it still might be possible. The deeper the change to the language, the earlier it needs to happen.

this change would be a breaking change unless we can reliably infer the necessary coercions, which I am pretty sure we would not.

I hope you're wrong. Can you give a concrete example where we couldn't?

[canndrew]

TL;DR If you think this RFC is about adding super-useful features at the expense of more complexity then you've got everything backwards.

[Virtlink]

The fact that let x: i32 = break; compiles but let x: i32 = break as i32; doesn't isn't bad because people frequently want to write code like this.

Why would anyone want to write let x: i32 = break as i32;?

break never returns to its caller, so it should have return type !.

Yes, break doesn't return to its caller but it does return, and I believe ! is for functions that don't return at all. If you where to replace a break (or continue) with a function that performs the same operation, what would that function's return type be? Surely not !. There is no function type (or operation) that you could use in place of break, and therefore I consider break and continue to be special language constructs with special behaviors. There is no sane way to assign a sound type to such a language construct, and I believe the semantics of () are fine for break.

I'm talking about the empty type ! not the subtype-of-everything type ! that got removed for being too painful.

Empty type, bottom type, zero type, all refer to the bottom type which by definition is the subtype of all types. The empty type is theoretically any type you want it to be, by the same logic that on an empty set you can make any statement true.

---

I just reread your RFC and I'm still failing to understand the advantages of ! as a full-fledged type. It's probably correct and beautiful on a type theory level, but all I see is a way to write dead code. Is there practical code that your RFC allows me to write that I currently can't write, or not as concise?

[RalfJung]

Yes, break doesn't return to its caller but it does return, and I
believe ! is for functions that don't return at all. If you where
to replace a break (or continue) with a function that performs
the same operation, what would that function's return type be? Surely
not !. There is no function type (or operation) that you could use
in place of break, and therefore I consider break and continue
to be special language constructs with special behaviors. There is no
sane way to assign a sound type to such a language construct, and I
believe the semantics of () are fine for break.

I am sorry, but you are wrong here. Assigning the empty type to "break",
"continue" (and "return") is a perfectly well-established practice in
type theory and programming language theory. There's an entire style of
writing programs (continuation-passing style, CPS) that's built around
"things that one can call that don't come back to you". A function that
diverges is such a thing, as is "break". One nice way of modeling such
continuations is as functions that return "!".
CPS is, in some way, pretty close to assembly: Think of "jmp

"
as "calling , without ever returning here". This analogy is
known to work perfectly, one can build compilers using CPS internally
and translating that to assembly pretty easily.
Clearly, "break" and "continue" are jumps in assembly, and indeed on
CPS, they become continuations. So their natural return type is "!".

Actually, if you use CPS, then all these high-level language features
(break, continue, goto, return - and even exceptions) unify and they are
all reduced to the same, underlying idea. This turns out to be a very
sane way to formally talk about such features.

Empty type, bottom type, zero type, all refer to the bottom
type which by definition
is the subtype of all types. The empty type is theoretically any
type you want it to be, by the same logic that on an empty set you
can make any statement true.

There is no reason to add "! <= T" to the subtyping relationship. The
empty type can be the bottom type, but it does not have to be. The
subtyping relationship is a syntactic property, we define what is part
of it. If you want to think of types as sets, and "subtyping" is not
the same as "subset": "subtyping" is a relation of our choice. Now, for
it to make any sense, we are going to make sure that if "T1 subtype of
T2", then "T1 subset of T2". However, the converse does in no way have
to hold.

[canndrew]

Why would anyone want to write let x: i32 = break as i32;?

They almost never would. They might want to write macro code that expands to something like that.

Yes, break doesn't return to its caller but it does return, and I believe ! is for functions that don't return at all.

break doesn't return at all to it's caller. That's why it makes sense to be able to write let x: i32 = break. Not because break has type i32, but because an expression that doesn't return can be treated as any type. (or as a type that is a subtype of or can be coerced to any type).

[main--]

@Virtlink If I understand your reasoning correctly, you're arguing that break shouldn't be an expression. However, that's beyond the scope of this RFC. Right now, break is an expression and as such needs a type. The current choice of () is not totally wrong as the code after a break never runs and therefore receives this (or any other type) in all cases due to there being none.

@canndrew mentions that let x: i32 = break; is valid today and indeed it should be as the same reasoning applies. let x: i32 = break as i32; should definitely be allowed for exactly the same reasons but it's not. "Why would anyone do this?" is a question one can close virtually any bug report with. Why would anyone leak the guard they received from thread::scoped?

This outlines in what a weird state break's type (using this to represent all similar expressions as well) really is right now: The choice of () is obviously arbitrary and not even consistently applied. The RFC proposes clearly defining the type to be !.

The way I understand it, the coercion mechanics proposed are merely a simplification. I think the compiler's existing special treatment of diverging expression could be kept entirely instead (the coercions would make it obsolete). This could address @nikomatsakis's concerns about the problems regarding correct inference of the required coercions, but I'm not nearly familiar enough with the compiler to assess this.

Edit: Spent a few minutes writing this, so sorry for the overlap with those who were faster than me.

[main--]

By the way, how would this interact with return? A block ending with a statement is () and the diverging return can't affect this (because it can't affect the type of nested blocks either). So while { return 42 } would be !, { return 42; } is still () and therefore incompatible with the return type (i32 in this example).

I probably misunderstood what exactly the coercions are supposed to achieve.

[flying-sheep]

maybe @RalfJung and @alexbool can voice their concers with the name. if there are serious arguments beyond simple preference, we could rethink, else it’s really safe to call it winner.

[alexbool]

Well, I'm not sure if my argument is strong, but here it is. Never is not a noun, so it is an answer to the question "How?" and not "What?". In this sense I like scala's Nothing a lot more.

[eddyb]

@alexbool But "fn main() {} returns nothing" is already in our vocabulary.

[ExpHP]

Never is not a noun

Oddly enough, I consider this to be the best argument in favor of Never.

It makes many of those "poor questions" (from recent Mu discussion) impossible to ask to begin with.

[eternaleye]

Oddly enough, I consider this to be the best argument in favor of Never.

Agreed - fundamentally, a function marked with ! in return position is incapable of returning any noun at all.

[alexbool]

@eddyb @ExpHP as with any topic relying on personal preference, this decision will be a matter of some compromise :)

[comex]

@alexbool Nothing is also Haskell's name for None (i.e. the empty variant of the optional type).

[canndrew]

You can now play with this on rust nightly! Just add #![feature(never_type)] to your crate and you're good to go.

It still has bugs, so please find them and report them.