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 :)

[Twey]

Hmm, I'm not sure I buy that. (A, B) is equivalent to Σ(_ : A). B, but that doesn't make it a Σ-type either. More pertinently, there's no reflection of the dependency in the type system — if xs: &[T], you can get xs.len(), but you can't access anything of type [T; xs.len()].

[glaebhoerl]

Right. From the last time I was confused about this and researched it, I believe there are at least three superficially similar but different beasts in this space: existentials, weak sums, and strong sums. I think "sigma type" applies to both of the latter(?), but that it's usually used to mean strong sums. The difference is best discernible if you have a local variable or a top-level constant of the type, that is, whose definition is also in scope. If we think of each of the three as a pair where the type of the second component may refer to the 'value' of the first, then with existentials, the first component is always erased (even if it's "visible in the source"), and can only be used as an abstract (unknown) value; with weak sums, the first component gives back the same value you put in, but when accessing the second component, its type again refers to an abstract placeholder value in place of the first component; while with strong sums, when you access the second component, its type retains full knowledge of the first's value as well ("dependent elimination"). It's the last of these which is usually referred to as a "dependent pair".

So I believe Rust's trait objects correspond to existentials, and its slices to weak sums.

(Unfortunately I didn't save the links where I read about this, but if anyone's interested, hopefully googling should lead to the same results.)

[Centril]

Closing this issue since the associated RFCs have all been closed.

[mark-i-m]

Thanks again @ticki ! This was epic.

[YairHalberstadt]

This paper might be relevant:

https://www.google.co.uk/url?sa=t&source=web&rct=j&url=http://drops.dagstuhl.de/opus/volltexte/2018/9218/pdf/LIPIcs-ECOOP-2018-13.pdf&ved=2ahUKEwj27tHC9sveAhUpLsAKHRiwB4UQFjAAegQIBBAB&usg=AOvVaw3cUw88ELS2ROyQu34OJbJw

It proposes adding a subset of dependant types to a mutable Java-like language by tracking aliases and using move semantics.

It can be fully verified at compile time.

Any linear inequality over the integers is a valid constraint.

As such I think it could fit in with the Rust paradigm very well.