The pi type trilogy

[ticki]

This issue is reference issue for the upcomming pi type trilogy, dividing the old RFC into 3 parts.

1. RFC: Constant generics (restricted Π types) for Rust, core RFC (v2) #1931: Core proposal.
2. with bounds for pi types. #1932: with bounds on pi types.
3. Fully dependent pi types. #1933: Breaking runtime-compile time barrier.

[ticki]

First rfc up: #1931

[fottey]

Thank you very much @ticki for continuing to champion this feature proposal. I appreciate all your hard work.

[burdges]

@edwinb @david-christiansen

[clarfonthey]

Discussion from the first RFC that's worth noting here:

@rkruppe: As already pointed out in previous discussion, these really aren't dependent types or Pi-types, at least not until #1933 gets accepted. I had to carefully read both RFCs to come to this conclusion, so this should really be clarified to make this RFC precise and self-contained. A good term that has been used before is "const-dependent types".

@withoutboats: In addition to being inaccurate I think "pi types" is not a very explanatory choice of name for most users. Const parameters seems more obvious.

@eddyb: "const generics", "const generic parameters" and "const parameters" are all better (both user-facing, and even in implementation details) than Π IMO.

I personally agree that we should come up with a much better name than Π types for this. We're not gonna use that name in the Rust book, and while understanding type theory is necessary for implementation, I don't think it's necessary for the average user.

[clarfonthey]

We don't talk about Σ types at all when we're discussing Rust's type system and I think that talking about Π types is equally silly.

[ticki]

@clarcharr

I fully agree. Only the last proposal is true dependent types.

[Twey]

Well, that's because Rust doesn't have Σ-types either, surely?

[mark-i-m]

@ticki As I read through the RFCs, I continue to be amazed at how well-thought-out they are! Thanks for the effort 😄

[burdges]

I'll make time to read these in the next few weeks, but so far my reading beyond the first amounted to ctrl-F "lifetime", but..

I wondered if one could create a value type from a runtime value and lifetime, so that the value acted as basically an implicit parameter, while the lifetime dictates where the proof must resolve. As an example :

Imagine we've some crate that requires a struct Params with configuration parameters. Right now, we have roughly three choices :

1. We can pass &Params, or Params if small enough, but doing so requires runtime "type" checks for agreement between our different Params structs. And this agreement might not be simple equality, like say dimension checks in matrix multiplication.

2. We can pass a &'static Params thus constraining them to being defined at compile time, so maybe now debug_asserts suffice for verifying compatibility between our Params instances.

3. We could replace Params with a trait containing various associated constants and types that users must impl for a ZST. In this way, we do this our checks for agreement of our Params at compile time. We can even avoid some unsized types in this way, either by defining them as associated types, or by using a network of traits, like what the generic-array crate does. It's kinda hideous though.

I think 3 will become increasingly popular regardless, but const dependent types, or just a fragment there of, makes doing so clean and idiomatic, as opposed to a morass of trait hacks, and they let you avoid unsized types.

Now can we push this messy trait based Params back into runtime with trait objects? We actually do not want to anyways because we do not want to erase the type like that. Also, I'd imagine object safety rules forbid 3 in trait objects, presumably meaning no object safe generic arrays too.

You can nevertheless imagine an implicit parameter being set by a type, and the compiler being asked to prove its correctness, even if under the hood this parameter gets passed at runtime.

Can you return a [u8; n] on the stack where n is runtime? In principle sure, but the caller must know n to perform the alloca, well n is part of the type of the callee after all.

I think 2 actually provides a useful way to imagine these hypothetical "lifetime dependent types". There is some lifetime 't inside which we can define some 't types that depends only on immutable values from outside 't. In compilation, the compiler must prove the 't types check, almost as if it were inserting asserts everywhere and running only the value computations that happen inside the 't types. It's actually more complex than that however.

Apologies for rambling here.

[strega-nil]

sigma types are a part of rust, due to DSTs. &[T] is equivalent to &(sigma N: usize, [T; N]). Important to note :)