Recent change to make exhaustiveness and uninhabited types play nicer together

[ahmedcharles]

Using a [u8;0] to make it 0 size is a nice trick.

I think it would be reasonable to have a way to declare a type which can only be used like *const T and *mut T, can’t be dereferenced and is `#[repr©] by default. This would allow having opaque pointers to something on the other side of the FFI boundary without any risk of Rust (or users) invoking UB, since the pointer can only be stored and passed through FFI to other code.

[arielb1]

That actually sounds like a hole in the improper_ctypes lint. Not a hole that I’ll like fixed, in any case.

That makes extern type a rather low priority feature.

[canndrew]

I slapped together an RFC for the extern type proposal: https://github.com/rust-lang/rfcs/pull/1861

That’s probably the best place to discuss this as this thread is getting a little off-topic.

[arielb1]

I’ve talked about the &mut issue with @nikomatsakis, and it seems that the following desirable properties are incompatible:

1. match exhaustiveness is identical between safe and unsafe code
2. &! is matchck-uninhabited in safe code
3. matches don’t assert deep validity in unsafe code
4. uninhabited types are not treated specially for UB
5. if a match is exhaustive, every arm you add to its end can never be reached

The problem is: Because of (2), you can write this code:

    let x: &! = get();
    match x {
    }

From (1), we also get

    unsafe {
        let x: &! = get();
        match x {
        }
    }

On the other hand, we also want this to be non-UB - aka (3)

    unsafe {
        let x: &Whatever = get();
        match x {
            y => println!("hi {:?}", y as *const _)
        }
    }

Because of (4), this is equivalent to

    unsafe {
        let x: &! = get();
        match x {
            y => println!("hi {:?}", y as *const _)
        }   
    }

Which contradicts (5)

[canndrew]

There’s a PR to roll-back and feature gate all the changes surrounding uninhabited types in matches here. I also just posted and RFC arguing that these changes should be re-instated here (before having seen @arielb1’s comment).

[canndrew]

@arielb1

There’s two ways out of this that I can see: One is to say that we hit UB as soon as we try to return a &!. A value returned by get() isn’t just invalid, it’s provably invalid, statically. This is different to trying to return a NULL &u32 - we may not be able to prove that this value is valid but can’t prove that it’s invalid either. We could make a distinction between safe and unsafe code where, in safe code, we need to be able to prove that all accessible data is valid to guarantee safety whereas, in unsafe code, we just need to not be able to prove that some accessible data is invalid.

The other is to recognize that (5) is true - unless your types are lying to you. We shouldn’t force people to consider that possibility. If they do want to consider that possibility, we can say they’re welcome to and this code will run fine:

unsafe {
    let x: &! = get();
    match x {
        y => println!("hi {:?}", y as *const _)
    }   
}

But the uninhabitedness changes also allow them to write this code:

unsafe {
    let x: &! = get();
    match x {
    }   
}

Why shouldn’t they be allowed to write this? Yes it’s broken but it’s broken because they fucked up using unsafe to create an impossible value and then matched on it. I mean, how much leeway to we need to give people, really? If this code shouldn’t be allowed then neither should exhaustively matching on a bool by testing for both true and false. What if they create a 42: bool and try to match on it? We don’t want their code to break! Better force them to match on every possible bit-pattern of a bool instead,

[arielb1]

The current consensus is that you can’t have a NULL: &u8 or a 42: bool any more than you can have a 256: u8 - any attempt to create such is instant UB.

[canndrew]

Yes, and you can’t have empty_vector_of_bits: ! either. So if you match on that it’s instant UB. This code:

unsafe {
    let x: &! = get();
    match x {
    }   
}

dereferences the pointer and matches on the contained !. That’s UB.

[arielb1]

That’s the !(5) position. Personally, I am split between !(5) and !(1).

[canndrew]

I’ve argued (sort-of) for !(5) in that RFC. Or at least !(5) when you have invalid data exposed and pattern-matchable through an enclosing piece of data that you’re matching on.

[gasche]

Loosely inspired by Agda’s absurd patterns, we can actually make a coherent policy out this by forcing one to get the value in a “match arm stub”, e.g.:

match void_ref_result {
    Err(e) => ... ,
    Ok(&_), // no arm needed
}

This would add clarity when the uninhabited type is deeply nested. I’d consider this an excellent compromise for everywhere, or convent sugar for unsafe code for

match void_ref_result {
    Err(e) => ... ,
    Ok(&r) => match r { },
}

Where one relies on UB to remove the extra branching instead of being explicit.

We added such a feature in OCaml in the last version, precisely for the purpose of better handling empty types appearing deeply nested (otherwise there is a termination issue, of how deep you do your case-analysis to test for inhabitation, and a practical issue of performance of exhaustivity checking). I think this is a very good construction because it both guides the implementation (of the exhaustiveness checker) and expresses programmer’s intent (“here is the reason why this case is dead”).

.

Regarding the larger discussion: it is very common in programming languages that support modularity to have a notion of “abstract type”, whose definition is not known. The client cannot build a value of such a type, but that does not mean that it is not inhabited (using an empty sum type for this is a very bad idea). Once you start reasoning on type equalities (for GADTs for example), the same phenomenon occurs, there are equalities that you can prove are true (from available definitions), equalities that you can prove are false (from available definitions), and equalities that you neither prove or disprove as they involve unknown/abstract types. In general it is important to carefully distinguish “I cannot prove X” and “I can prove not(X)”: the closed-world assumption that lets you confuse the two notions is anti-modular.

One of the good things with the ML module systems is that they force the language design to be honest with respect to abstract type: modules have an interface that is separated from the implementation. You need abstract types in the language as soon as you allow encapsulation, as they describe the interface of private types. Rust does not have an interface language, so it does not ask itself the question of “what is the interface of a type whose definition is private?” – the only natural answer would be “an abstract type”. If you add the extern type Foo; syntax to the language, it will be useful not only to think of types defined through the FFI, but also to think of types from other crates that are visible but whose definition are private.

[tupshin]

“abstract type”, whose definition is not known. The client cannot build a value of such a type, but that does not mean that it is not inhabited (using an empty sum type for this is a very bad idea).

Once you start reasoning on type equalities (for GADTs for example), the same phenomenon occurs, there are equalities that you can prove are true (from available definitions), equalities that you can prove are false (from available definitions), and equalities that you neither prove or disprove as they involve unknown/abstract types. In general it is important to carefully distinguish “I cannot prove X” and “I can prove not(X)”: the closed-world assumption that lets you confuse the two notions is anti-modular.

Can’t overstate how important this is to support very abstract approaches.

If one looks at the similarities between Scala’s underscore and Rust’s, it feels like Rust should be able to source some additional flexibility from there: http://stackoverflow.com/questions/8000903/what-are-all-the-uses-of-an-underscore-in-scala Existential types

def foo(l: List[Option[_]]) = ...

Higher kinded type parameters

case class A[K[_],T](a: K[T])

[canndrew]

otherwise there is a termination issue, of how deep you do your case-analysis to test for inhabitation, and a practical issue of performance of exhaustivity checking

Could you elaborate here? There’s no arbitrary recursion limits anywhere in the inhabitedness-checking code but I don’t see how it could go into an infinite loop. We also cache the result of the inhabitedness check but there hasn’t been any benchmarks comparing it with being disabled.

[gasche]

I did not participate in the performance measurements, but Jacques Garrigue reported his number in the relevant bugtracker entry, PR#6437. The costs seemed to be non-neglectible, see for example (Exh is for exhaustivity checking, while Unus for analysis of unused cases):

Here are a few more times, for make library on another machine. The number indicates the “exploding depth”, i.e. the number of nested GADTs one may explode for analysis. Exh(2)+Unus(2): 77.0s Exh(1)+Unus(1): 6.55s Exh(1)+Unus(0): 6.35s Exh(0)+Unus(0): 5.95s Exh(1): 6.19s Exh(0): 5.75s

Re. non-termination: a naive implementation of inhabitation will say that if the type is a tuple/product type, then it is inhabited if all components are inhabited, and if is a sum/enumeration type, then it is inhabited if at least one component is inhabited. If you have a recursive type, repeatedly applying this strategy can loop infinitely. For a regular recursive type (type nat = Z | S of nat), you can detect that you are looping (a subgoal is the same as the original goal), and terminate there (deciding inhabitedness or not depending on whether your language allows recursive values). But if the recursive type is parametrized and its definition instantiates its parameter in an non-regular way (say type 'a fulltree = Leaf of 'a | Node of ('a * 'a) fulltree), then there is no clear termination strategy. Your language design might forbid that (those types also make monomorphization difficult), so maybe the performance aspect will speak more to you.

[canndrew]

Ahh… yes it’s possible to make it go into an infinite loop then. In fact, that example just turned up at least three bugs:

This type should be uninhabited but isn’t: FullTree<!> where

enum FullTree<'a, T: 'a> {
    Leaf(T),
    Node(&'a FullTree<'a, (T, T)>),
}

I’m not even sure why this doesn’t go into an infinite loop, it seems like the inhabitedness here should be (niavely) undecidable.

This type gives a weird, spurious error message:

struct Foo<'a, T: 'a> {
    node: &'a Foo<'a, (T, T)>,
}

error[E0392]: parameter `T` is never used
 --> smeg.rs:3:18
  |
3 | struct Foo<'a, T: 'a> {
  |                ^ unused type parameter
  |
  = help: consider removing `T` or using a marker such as `std::marker::PhantomData`

error: aborting due to previous error

And this type causes rustc to stack overflow (in the uninhabitedness check):

struct Foo<'a, T: 'a> {
    _ph: PhantomData<T>,
    node: &'a Foo<'a, (T, T)>,
}

Damn.

Edit: The first bug isn’t really a problem and the second one is actually expected behaviour. I’ve filed a report for the third one and put it on my list of things to fix.

[gasche]

The idea of refutation clauses in that situation is that you do not unroll type definitions indefinitely, or at all: a pattern can be omitted only when its head constructor is “obviously” impossible in this context (if it is a GADT constructor that assumes an equality that is inconsistent in the current typing environment; empty enums would qualify as well, or !). If a pattern is impossible for a reason that is only visible in depth (for example it is of a tuple type T * U where T and U are “obviously” impossible), then the user has to write a refutation clause (_, _) -> . to explicitate the fact that this pattern is impossible. We asks the user to “prove” that the rest of the patterns are uninhabited, so they tell us exactly how deep we need to unroll the definitions.

(A nice side-effect of this feature is that while, in general, a non-exhaustive pattern matching emits a warning rather than an error, a refutation clause for which the type-checker cannot ensure that the pattern is indeed empty raises a hard error. So we can now use _ -> . after all patterns as a way to assert that the pattern-matching is exhaustive, and get a hard error if the datatype definitions change in a way that breaks this assertion.)

[comex]

Once you start reasoning on type equalities (for GADTs for example), the same phenomenon occurs, there are equalities that you can prove are true (from available definitions), equalities that you can prove are false (from available definitions), and equalities that you neither prove or disprove as they involve unknown/abstract types. In general it is important to carefully distinguish “I cannot prove X” and “I can prove not(X)”: the closed-world assumption that lets you confuse the two notions is anti-modular.

Doesn’t Rust already deal with “abstract types” in the form of type parameters in generic code?

[gasche]

Yes, type parameters are also abstract types, but there are use cases for abstract types (such as exporting a type to other crates without exporting its definition) that are not well-served by parametrization. This subtlety is, for example, at the key of module system design in the ML community: in principle universal and existential quantification suffice to express type abstraction, but in practice modular programming require code structures that they do not serve very well. (See also the discussions in the Scala community about “type members” versus “type parameters” and the fairly different code structures they make comfortable.)

If crate A exports an abstract type T that is used by crate B, to emulate the same pattern using a type parameter you would have to have B be parametrized over any signature of A using a type parameter T, and instantiate this parameter with A. To my knowledge the crate language does not allow such kind of crate-level parametrization and instantiation. (And even if it did, it would be very inconvenient to use in practice.)

(To exercise these type-checking situations using type parameters instead of a new construction for abstract types, you need a language construction that takes parameter, and can internally define new types and build new expressions. Is it possible to define a type locally to a parametrized function, or a struct or trait definition?)

[ahmedcharles]

it seems that the following desirable properties are incompatible:

1. match exhaustiveness is identical between safe and unsafe code
2. &! is matchck-uninhabited in safe code
3. matches don’t assert deep validity in unsafe code
4. uninhabited types are not treated specially for UB
5. if a match is exhaustive, every arm you add to its end can never be reached

I’m not entirely sure what &! being matchck-uninhabited means, but &! seems to be a violation of the requirements of a & in safe code, if ! represents something that doesn’t exist. Am I missing something?

[nikomatsakis]

This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.