Void types with type parameters?


#1

Is there a way to express the idea of a void/never/uninhabited type with type parameters (also void) for doing type-level things? Is there a void equivalent of PhantomData? Is it even meaningful?

Maybe:

struct Void<T> {
    _never: !,
    _phantom: PhantomData<T>,
}

?


#2

#3

Yeah, that’s why I used it in my example :wink:

I guess I’m asking a theory question about whether a type containing ! and some other type is equiv to !. I guess it is because the ! prevents it from ever being instantiated, so the size doesn’t matter (ie, it need not be PhantomData).


#4

I still get 4 for mem::size_of::<(!, i32)>(), though who knows, I could see that changing to 0. It may come into effect for enums, like Result<T, !>. If that error type were something larger that happened to contain a !, it will currently still take up space.


#5

If I’m understanding you, I think the answer is no - they’re not equivalent. A type containing ! should not take up space for that field, so it’s like a ZST in that sense. What it does add over existing ZST is ability to cast ! to any other type, including traits (I believe). But I don’t think it makes a type containing ! and other types into a ! as a whole.

Curious what type level use case you have in mind for this?


#6

Curious why you think that should have 0 size?


#7

I’m carrying around a bunch of related types as associated types on a trait and some static methods. It’s used as a type parameter on a function, or in a phantom field of a non-void type. I don’t care about the type that implements the trait, but for cleanliness it shouldn’t ever be instantiated.

I’m in a prototyping stage and it could end up being a mistake, (ie I do need the type to be instantiated - the methods may need self).

In other words, I don’t need it to be equiv to ! in the sense of being Bottom.


#8

I think you could reasonably prune away types containing !, much like how LLVM may prune a bunch of code if it leads to something flagged unreachable. (Although type layout should be independent of optimization level.) So if a (!, u32) can never be instantiated, we could give it any size we want – might as well be zero.


#9

In fact I wonder if this layout refactoring will do pruning just like that:


#10

I was about to say that I would be surprised if there was any code that could possibly benefit from optimizing size_of::<VoidLike>()

but I suppose you can waste stack space with it on Debug mode.

enum Void {}
struct DeadBeef<T> {
    _void: Void,
    _value: T,
}

// constant fold THIS!!!
fn sum_of_primes_under(limit: i64) -> i64
{ (2..limit).filter(|&p| (2..p).all(|k| p % k != 0)).sum() }

fn main() {
    if sum_of_primes_under(100) != 1060 {
        // This branch is never entered.
        // The stack overflow actually occurs much earlier, upon entry to main.
        let x: DeadBeef<[i64; 1000000000000]> = unsafe { ::std::mem::uninitialized() };
    }
}
    Finished dev [unoptimized + debuginfo] target(s) in 0.52 secs
     Running `target/debug/playground`

thread 'main' has overflowed its stack
fatal runtime error: stack overflow

P.S. a common notion is that the size of a voidlike type should be −∞. I also remember somebody somewhere mentioning the max-plus algebra which seems to be a nice foundation to build upon. But it’s quite a special case to put into the type system for what would appear to be very little gain…


#11

Yes! I just tested pr45225 myself, and these all print 0!

    println!("{}", std::mem::size_of::< ! >());
    println!("{}", std::mem::size_of::< (!, u32) >());
    println!("{}", std::mem::size_of::< Option<!> >());
    println!("{}", std::mem::size_of::< Option<(!, u32)> >());

edit: @ExpHp your example also works fine on that branch!


#12

Amazing! I need to go high-five @eddyb some more!

I like the mental model that ! actually has size −∞ (since no matter what’s in a struct with it, the struct also has size −∞) and that mem::size_of is just saturating.


#13

Wow.

That PR covers like half of the optimizations mentioned in the exotic enum layouts issue. I had just assumed that pretty much none of this was ever going to happen.

This is incredible work! :clap:


#14

It wasn’t going to happen while we still had all the crufty old backend code around, rotting away very slowly.

LLVM is part of the problem as the way it handles a subset of C types and interactions with them, pointers, etc. is quite idiosyncratic, in self-defeating ways.

For good IR design (within the limits of SSA/CFG), Cretonne is pretty nice to look at, and all future developments should treat it as a first-class citizen (even without a rustc backend for it yet), instead of LLVM, which requires extra ad-hoc heuristics to lower to.


#15

Ah ok, so ! is “infectious” and taints (or saturates as @scottmcm phrased it) everything reachable from it. I don’t think I picked up on that previously.

So what does it do at the type level, going back to @jsgf’s question that I suspect I may have given the wrong answer to.


#16

I think your answer was fine. At the type level, ! and (!, T) are still distinct types, both uninhabited.


#17

Amazing! I need to go high-five @eddyb some more!

I like the mental model that ! actually has size −∞ (since no matter what’s in a struct with it, the struct also has size −∞) and that mem::size_of is just saturating.

For the curious, this is known as the max-plus algebra, max-plus semiring, tropical algebra, or tropical semiring.

In this model, the size of a type is calculated for sum types (enums, unions) using ⊕ (a.k.a. max) and for product types (tuples, structs) using ⊗ (a.k.a. plus).


#18

For the original question: I don’t suspect that void generic types are anything fantastically more interesting than just the sum of their parts.

  • There is an isomorphism between the set of all types and the set of all Void<_> types (with T <=> Void<T>), just like with any generic type.
  • Any monomorphized Void<T> has no values and effectively has size −∞, just like any void type.

maybe once there’s higher kinded types there might be fancy shiznitz that rustc could do by treating the higher kinded type Void<_> as a constant function in some limited respects. I dunno. Not a type theorist.


#19

So an associated type that can only be substituted with uninhabited types?


#20

Not quite. An associated type of a trait that’s only ever implemented with uninhabited types. The associated types can be inhabited.