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 stris 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.)
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?
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..
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.)
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 T and trait Trait, one of the following two cases must hold:
T implements Trait. In this case, if any of T's supertypes or subtypes also implement Trait, those impls must come from the same impl block as the impl of Trait for T. Additionally, if U is a supertype of T, and U does not implement Trait, then none of U's supertypes may implement Trait. If any of these rules is violated, it's a coherence error.
T does not implement Trait. In this case, consider the set {U} of all supertypes of T that do implement Trait. One of the following must hold (otherwise, it's a coherence error):
a) The described set {U} is empty
b) All of the elements of {U} share a common subtype S, that itself implements Trait, and is a member of {U}.
In case 2b, when a value of type T is provided but a value of a type implementing Trait is expected, the value of type T is coerced to S.
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!
I have a question about arithmetic operators.
Let we have this code:
let a: (i32 in 1..3) = foo();
let b: (i32 in 1..3) = bar();
let c = a+b;
Which is the type of result? Logically we can predict that result will have bounds [2..5), so would result have the same type as operands (i32 in 1..3), or bounds will be widened (i32 in 2..5)?
Also the next example:
let a: (i32 in 1..3) = foo();
let b: (i32 in 2..5) = bar();
let c = a+b;
Is this code valid? Operands have different bounds, but the same super-type, can we add them?
My hope is that yes. There are two approaches to making it work:
One possibility is that neither of the pattern types implement Add, and they get converted to their supertype as described in this comment. In this case, the result of the addition has type i32. This is the less powerful option, but also the simpler one with fewer issues to resolve.
The second possibility is that i32 in 1..3 does implement Add directly. I have no idea what the impl block would look like, haven't thought about that. <i32 in 1..3 as Add>::Output would have to be i32 in 2..6, or some supertype of that, as you say.
This is where I worry the lack of variance on traits may become a problem. Ideally, for S <: T, you would want <S as Add>::Output <: <T as Add>::Output. But Rust doesn't guarantee that today, and there might already be impls of Add out there that don't adhere to it. Maybe that kind of trait variance isn't actually needed to make this feature work, though? I'm not sure.
In any case, option 2 should be backwards compatible to introduce on top of option 1, so option 1 makes sense for an MVP.
nitpick: the syntax is u32 is 2..6 not u32 in 2..6, every time this feature has been discussed over the past ~1+ year has been using is not in unfortunately the initial version of oli's post messed this up. Option<u32> in None doesnt really make any sense, but Option<u32> is None imo does.
why do you prefer in?. Option<u32> in None doesnt make sense to me, how is it "inside of None". is however reads naturally "this Option is a None" "this Option is a Some"
An Option<i32> in None is a value of type Option<i32> that is contained in the subset of values that matches the pattern None. I get the equivalcence between let _ = and is, but I'm not sure that's really a good thing, because it makes stuff like let foo: Option<i32> is None = None; confusing imo.
(none of this is a deeply held belief, just my initial impression)
matches or matching was what I was using in my private musings before reading oli's post, but it's long and once I read the post in seemed superior.
It wasn't about the size of each set, but about the size of a value from each set.
Thr interpretation I'm using here is that of the original usage of subtyping i.e. not for lifetimes but for class-like inheritance.
Using that interpretation, given an inheritance/subtype relation B subtype of A for types A and B, each value of B is necessarily also a value of A (the Liskov Substitution Principle at work).
In addition B may or may not extend As definition by adding fields.
If it does, that means a value of B will be a value of Aand more. That implies a value of B is larger than a value of A.
But again, that excludes collections as their usage can easily distort that picture.
It's also not necessarily meant to apply to Rust types, or to Rust lifetimes for that matter, but rather a musing that the originally stated POV was somewhat arbitrary.
The thing is – the inheritance relationship in OOP languages is not subtyping in the type theoretic sense! OOP did not invent the subtype relationship, but languages such as Java that adopted the subclass/superclass terminology, which in turn confused people into thinking that subclasses are subtypes and superclasses supertypes. (The C++ terms "base class" and "derived class" are, at least, less confusing.)
If one wants to think of OOP class hierarchies from the sub/supertype perspective, then the important thing to understand is that if B extends A in Java, then B is not a subtype of A-in-itself. What it is, is a subtype of the transitive closure of every possible A (in the LSP sense) – that is, a subtype of the unbounded set of all possible subclasses of A including A itself. This agrees with the type theoretic definition of a subtype, and it is easy to see that indeed the inhabitants of B are necessarily a subset of the set of all inhabitants of A, just like the inhabitants of the refinement type i32 in 1..4 are a subset of the entire i32.
Yes, and this "extension of definition", or "implementation inheritance", is frowned upon even by OOP proponents, as evinced by the often repeated mantra "prefer composition to inheritance". Indeed, when B extends A in Java, what B actually is not a subtype of A at all, but rather the product typeA × B' (where B' denotes the "extra" fields of B), just with some syntactic sugar added. And this is abundantly clear when you consider how the base class part is actually stored in a derived class instance. Thus inheritance is composition, not subtyping.
Finally, it should be noted that the way that implementation inheritance breaks the "nice" rules of type theoretic subtyping has made it necessary to invent all kinds of rules and patterns to ensure better code quality and avoid rampant violation of invariants, such as:
the LSP itself ("if you do this you'll break things, so please don't")
the template method pattern ("we're trying to guide you not to break this important thing")
final methods ("ok, we're done asking nicely, this part you cannot break"), and
final classes ("…maybe this whole inheritance thing wasn't so good idea after all").
Re: the last part, it's not a coincidence that some critical vocabulary classes of Java, such as String (or, shudder, Integer), have always been final, since the beginning.
Actually, this rule has to go; it conflicts with the current behavior of 'static bounds. It wasn't essential to the scheme, so removing it shouldn't be an issue.
unfortunately the initial version of oli's post messed this up.