This sounds awesome! One question I have is around runtime semantics: is the idea that VRTs can only be constructed from within matches? Or is the SAT solver able to understand things like if (value != 0) { value <: usize != 0 }?
1 Like
I think to start, Rust wouldn't support that kind of type narrowing. With subtyping, it can always be added later, in a backward-compatible way.
Makes sense. 
(I don't really like supertype <: subtype, as that feels backwards to me; supertype is "larger" than subtype.)
I quite like "pattern types" as the way to express this functionality.
I think it would be a reasonable enough choice (though kind of a cop-out one) to say that it is not possible to implement traits on refined Pattern Types. IOW, you still only have the unrefined type for the purpose of any trait implementations and using refinement types in generics always collapses the type to the unrefined type unless the only generic bounds are Sized or lifetimes.
TBQH I don't really like this solution, but it is a potentially valid one. It essentially says that if you want to use the Pattern Type refinement as a full type, you should define a newtype and give it a name; that the refinement is in fact purely a type system fiction[1] for convenience and you still just have the unrefined type plus a bit of metadata allowing you to elide some unreachable arms.
Not about variance
Suggestion: the root way to refine to a pattern type should probably be by pattern matching providing type refinement, i.e.
fn takes(_: i32 in 1..3) {}
fn example(x: i32) {
match x {
val @ 1..3 => takes(val),
_ => {}
}
}
This is imho a fairly straightforward refinement of pattern @ bindings, in that the resulting type is now a Pattern Type restricted to the pattern it was bound to. A nice property of refinement types is that because they can transparently be used in place of the unrefined type (assuming variance works out), it's (modulo variance) always fair game for the compiler to refine more accurately.
More involved refinement could of course thus be added later, such as in-place refinement without needing rebinding and using ==/!= for StructuralEq type refinement.
One thing I wonder is if Pattern Types is (or can be) a superset of Enum Variant Types, and if so, that would allow us to use enums with refinement typing fairly simply:
enum Expr {
Array {
attrs: Vec<Attribute>,
..
},
Assign {
attrs: Vec<Attribute>,
..
},
..
}
fn example(expr: &Expr) -> &[Attribute] {
match expr {
expr @ Expr::Array { .. } => &expr.attrs,
expr @ Expr::Assign { .. } => &expr.attrs,
_ => &[],
}
}
This isn't the perfect syntax[2], but it's imho very clear and obvious how this functions as an extension to current semantics.
-
moreso than the type system usually is even ↩︎
-
The return of type ascription! There's no ambiguity if it's allowed as part of top-level patterns, I think; the ugly placement is
Struct { field: binding: Type }which despite the ugliness should've used.binding @ fieldsyntax to be consistent
↩︎match expr { expr: Expr::Array => &expr.attrs, expr: Expr::Assign => &expr.attrs, _ => &[], }
3 Likes
Yeah, I got the notation wrong 
. Will edit to fix (Edit: done)
Side note: I typoed type is pat syntax as in. The in only really makes sense to me for ranges, not other patterns, especially if you think about it as reverse let syntax: if x is pat instead of if let pat = x
Aaanyway. My hope was we could create an MVP where pattern subtypes implement no traits and are basically invariant everywhere, making the only way to create values of these types be pattern matching
I guess that's a matter of perspective: Putting aside the wrinkle of things like collections, if we were to go by the size of values of each type, then the subtype values would be larger. So viewed that way, subtype has a larger footprint than supertype.
All that said, I really like neither :> nor <: for subtyping relations, because knowing what I said above coupled with what you wrote above only leads to the realization that neither has a superior mnemonic to remember it by w.r.t. the other. And syntax that you constantly need to look up is just bad syntax IMO.
They'll likely have to implement Sized at least… (except for slice patterns, where only references to them can implement Sized).
I don't really get that perspective? A type is essentially a set of values that are of that type. A supertype then is a set which is a superset of the subtype; a larger set of values.
There's no "size" to a value. In terms of physical size_of, they're by definition the same. The only way I can get to values being "larger" is to consider the type some fixed size, and values each taking an equal part of the value, thus removing some values from a type make the others expand to take up the missing space. But that's explicitly not how Rust types work, at all; removing a value from a type produces an empty space "niche" for the values which are not valid for that type.
2 Likes
If by "being a subtype" you mean "can be silently used wherever the supertype is, and the values should automatically coerce between the two", then I don't think we should do anything like this. Hidden automatic conversions are a really huge bag of worms, and it's really easy to get the language into an intractable state with them.
There should be some explicit conversion. A refinement type must have a canonical projection to the supertype. This canoncail projection could be a coercion, but a safer and more flexible choice is to make it an explicit map, e.g. via the as cast:
inj: T as pat -> T
inj t = t as T
This eliminates the Option<usize in 1..> --> Option<usize> issue, because an explicit map of contained types can be extended to the explicit map of options using s
The refinement types should definitely not implement the traits of the supertype. It is impossible to do in a sane and sound way.
trait Zero {
fn zero() -> Self;
}
impl Zero for usize {
fn zero() -> Self { 0 }
}
impl Zero for (usize in 1..) {
fn zero() -> Self { ???? }
}
Similar counterexamples are easy to provide with any other kinds of methods, even if they don't return Self.
Now, there may be specific cases where, for specific types, specific refinements and specific traits, there is a sane way to give an automatic trait implementation, but that would be special cases which should be invidiually considered for addition, on their own merit.
By the variance argument, the only slightly common case where the trait could be automatically implemented is if it consists only of the functions
fn(&self, *args) -> ret;
fn(self, *args) -> ret;
provided that the refinement type is not present in the return type (and likely not in arguments, because that would make the analysis even more complex). This doesn't sound like a very strong case for automatic trait impls, and it's likely that it will have semantic issues of its own (e.g. if the trait makes some compiler-unchecked guarantees about the implementing type, like various marker traits commonly do, or if the impl would try to use the refined type in an incompatible way).
One extra issue is how one could construct an instance of T in pat, i.e. how can one provide the inverse map T -> Option<T in pat>. Imho that would need support for flow typing of match expressions, because we would need to be able to match t on pat and use the matched value to construct the refined type, even if there are intermediate operations on the matched value.
On the other hand, refinement types are already a component of flow typing, so we could do something like this:
match (t: T) {
t_ @ pat => {
// The captured binding is automatically of the refined type.
// We assert it here for clarity.
let t_: T as pat = t_;
/* do stuff */
Some(_t)
}
_ => None,
}: Option<T as pat>
This would also allow e.g. to construct T as (pat1 | pat2) by separately matching on pat1 and pat2, doing the required extra checks & side effects, and coercing the captured T as pat1 or T as pat2 to the desired supertype T as (pat1 | pat2).
Since coercion is transitive and ! coerces to any type, this would mean that T as ! coerces to any U. This sounds hugely problematic, and I don't see a good reason to coerce silently between the subtypes of different types. This may also cause layout issues: in principle, in the cases where we don't support niches T as pat can be layout-equivalent to T, but with compiler-enforced guarantees on the contained value. Different T and U would thus have very different layouts even for empty patters: the size and alignment of T as ! is the same as T, even if there are no values.
If at a certain point we would want to add runtime-dependent refinement, then discerning between empty and non-empty dynamic refinements of the type would be entirely impossible.
By "being a subtype," I mean that there's no coercion, because a i32 in 1..3 already is an i32, just like a &'static str is a &'a str.
Currently, A <: B implies that A implements all traits that B implements. You are correct that that would have to change somehow for this feature to be viable. I'm still thinking about whether that's possible and how to do it if so. (My current thought is that if you model every trait as taking an implicit Self type parameter, then you could say that A implements some of B's traits with Self = B instead of Self = A. But I haven't worked that out.)
Yeah, this is what I (and @CAD97) had in mind.
No T as ! can ever soundly be produced, any code that tries to is either dead code or UB. And if & or &mut references to uninhabited types remain uninhabited as they are now, then those will also be freely coercible to one another. Given these facts, I don't think the difference in size_of or align_of matters. But maybe you have a counterexample?
1 Like
Doesn't the compiler already implement a way to check whether a function pointer is contravariant with respect to a specific type (Self in this case)? This seems fairly general and easy to support.
However Rust already has subtyping coercion, meaning that being a subtype implies a coercion to the supertype. This would have to change if you don't want a coercion.
This is already not true for HRTB subtyping. for<'a> fn(&'a T) is a subtype of fn(&'static T), but it doesn't inherit its traits.
That said, it feels weird to me that i32 in 1.. is a subtype of i32,. because it's i32 that's extending the capabilities of i32 in 1.., not the other way around... But at the same time i32 being a subtype of i32 in 1.. can't possibly work because a i32 is not a i32 in 1..
3 Likes
On variance: Rust traits had variance before 1.0. RFC 738 and the rustc dev guide document how it used to work. But trait variance required extra annotation for little benefit, and so was removed. I am thinking about whether and how it could be brought back.
That makes things easier, I think. Thanks!
No, a value of type i32 in 1.. is strictly more capable than a value of type i32; knowing more about its contents allows you to do more stuff with it. (A function that needs an i32 in 1.. is less useful than one taking any i32, hence why functions are contravariant with respect to their arguments.)
2 Likes
trait Test {}
impl Test for fn(&'static u8) {}
impl Test for for<'a> fn(&'a u8) {}
Interestingly, the above code triggers a future-compatibility lint.
It's one that lies about the intention to make it a hard error, though. Unless direction has changed again. More on the topic.
(There's at least one other such misleading future-compatibility lint, but I can't recall which off the top of my head.)
1 Like
Some thoughts on type inference with subtyping coercion.
In current Rust:
trait Trait {}
impl Trait for fn(&'static u8) {}
fn takes_concrete_supertype(_: fn(&'static u8)) {}
fn takes_impl_trait(_: impl Trait) {}
fn to_ptr<'a>(_: &'a u8) {}
fn main() {
let fn_ptr: for<'a> fn(&'a u8) = to_ptr;
// This works fine. Rust realizes it needs to convert `fn_ptr`
// from a `for<'a> fn(&'a u8)` to the supertype `fn(&'static u8)`.
takes_concrete_supertype(fn_ptr);
// This doesn't compile today :(
// Rust doesn't manage to coerce `fn_ptr` to supertype.
takes_impl_trait(fn_ptr);
}
If a u32 in 1.. is to be as useful as a u32, code like the last line in the above example needs to compile. For Rust to be able to infer what to do, there needs to be a unique "best" supertype to coerce to to satisfy trait bounds. I would propose something like the following rules:
For any type
Tand traitTrait, one of the following two cases must hold:
TimplementsTrait. In this case, if any ofT's supertypes or subtypes also implementTrait, those impls must come from the sameimplblock as the impl ofTraitforT.Additionally, ifIf any of these rules is violated, it's a coherence error.Uis a supertype ofT, andUdoes not implementTrait, then none ofU's supertypes may implementTrait.
Tdoes not implementTrait. In this case, consider the set{U}of all supertypes ofTthat do implementTrait. One of the following must hold (otherwise, it's a coherence error):a) The described set
{U}is emptyb) All of the elements of
{U}share a common subtypeS, that itself implementsTrait, and is a member of{U}.In case 2b, when a value of type
Tis provided but a value of a type implementingTraitis expected, the value of typeTis coerced toS.
I don't believe it's possible to write impls that would conflict with these rules in Rust today, without triggering the coherence_leak_check future-compat lint. But maybe I am wrong about that, please tell me if so!
You're right, sorry for the noise.