The general issue with subtype relations

#1

Subtype relations are known to be a hurdle for type inference in that them require more advanced algorithms than classic unification, where instead of a system of equations a system of inequalities has to be solved. Now such relations apparently appear in Rust at essential points. For example, &'a mut T is a subtype of &'a T for each 'a and T. So I wondered how far Rust is able to handle this.

To my understanding it is induced naturally that [&mut 'a T; N] is a subtype of [&'a T; N] for all 'a, T, N. At first it seems that Rust is able to handle it:

fn f(_a: [&i32; 2]) {}

fn main() {
    f([&mut 1, &mut 2]);
}

It's bogus, however. This program does not compile:

fn main() {
    let a: [&mut i32; 2] = [&mut 1, &mut 2];
    f(a);
}

Can you think of any programs, not too long, that would be nice to have but are not expressible? It seems, in many cases one can write manual conversions.

1 Like
Type-checking ! vs i32
#2

Rust only has subtyping of lifetimes, not types. Going from &mut T to &T is a coercion, not subtyping.

(and &'static T is a subtype of &'a T for any lifetime 'a, but not the other way around)

The reason your program fails to compile is simply that there is no coercion from [T; 2] to [U; 2] even if there is a coercion from T to U. Subtyping is not involved.

11 Likes
#3

I mean, in this example:

fn f(_a: [&i32; 2]) {}

fn main() {
    f([&mut 1, &mut 2]);
}

The compiler sees that you are building an array of type [&i32; 2] and putting mutable references into it. However mutable references can be automatically reborrowed into immutable references, so it inserts a conversion automatically.

#4

Well, in further consideration one would like to gain a broader meaning of subtyping. We attain then to a view in which the essential point is not whether a coercion is present or not, but that this coercion should be safe and natural. An additional optional requirement is that it should be zero cost.

From this point of view it seems strange that f([a[0],a[1]]) is allowed, but f(a) is not. Would richness and depth of the type system be the maxim, one would rate this as half-baked. In the desire for minimalism there is certainly not much need.

To further shine light on this consideration, here is a similar concept from mathematics that I recall I brought up before in another thread. Given two objects X, Y, and a monomorphism φ: X→Y, one may consider X to be a subobject of Y. At least for a natural monomorphism, this is also illustrative. In particular, when the objects are plain sets, then φ is nothing else than an injection and one may consider X to be a subset of Y in a generalized sense.

#5

This sentence doesn't make much sense to me, but if what you're saying is that the distinction between subtyping and coercion is meaningless, I disagree.

Sure, you can make up whatever terms you want, but at the end of the day there is still a distinction between subtyping and coercion. Calling things "subobjects" doesn't lend any clarity here.

Coercion is a thing that happens to a value of type A when you try to put it into a "slot" of type B, and the value can be automatically converted in some way to a new value of the right type for the slot.

Subtyping is a relationship between types in which one is a subset of the other. One important thing about subtyping is that subtypes participate in variance. Another important thing is that no conversion is necessary to treat a value as a subtype of its type. This is what makes it possible for Box<&'static i32> to be a subtype of Box<&'a i32> for any 'a: because Box<T> is covariant in T, you don't need to convert the inner value to be able to treat the Box as its subtype.

You can coerce a &[i32; 10] to a &[i32] -- that's an unsized coercion. You can't coerce a &&[i32; 10] to a &&[i32], because it doesn't make sense; coercions are shallow and there's no &[i32] around for the result to reference. [&mut i32; 2] can't be coerced to [&i32; 2] for basically the same reason.

Now you may argue that the compiler should recognize that &mut i32 and &i32 have the same layout, and implicitly reborrow the elements of a. And maybe that would be nice to have! But it'd still be a coercion, not subtyping, because [&mut i32; 2] is not and can never be a subtype of [&i32; 2].

7 Likes
#6

To expand on this, one reason that &mut T cannot be a subtype of &T is that it would violate the Liskov substitution principle:

in a computer program, if S is a subtype of T, then objects of type T may be replaced with objects of type S without altering any of the desirable properties of the program (correctness, task performed, etc.).

In particular, &T implements Copy and &mut T can never implement Copy due to its non-aliasing rules, so it's invalid to treat &mut T as &T.

For similar reasons, the substitution doesn't work in reverse either: The existence of an &mut T blocks all access to the referent through any other path. This property would be lost if you attempted to use an &T where an &mut T is expected.

Thus, neither &T nor &mut T can be properly considered a subtype of the other.

2 Likes
#7

Oh, it seems I've stumbled into a problem area. I skimmed the literature on this, and found that it is indeed a delicate question. Interestingly, the very question, how much coercions are different from subtypes, has already been discussed before:

Moreover, surprisingly, even my specific consideration has already been discussed. In the book "Funktionale Programmierung. Sprachdesign und Programmiertechnik" by Pepper and Hofstedt, in chapter seven, "Subtypen (Vererbung)", there is a relevant passage I want to quote, emphasis as in original:

Before we look at the individual constructions by which subtypes can be introduced and used, let us consider some general aspects.

Basically, what kinds of subtype formation one allows in a language is a design decision. How this decision is made has a massive impact on the expressive power of the language and on the complexity of the compiler. Even if – as for all design questions – the judgement cannot be made according to right/wrong, but rather according to criteria such as successful/corky or elegant/overloaded, there are nevertheless guidelines which one can orient oneself with the design. Of particular importance here is the context criterion.

Definition (Context Criterion)
The context criterion says: The subtype can occur everywhere where the supertype is expected. More precisely: Let S be a subtype of T. Then in every context c[. . .], in which elements of the type T are expected, elements of the subtype S can occur.

As we shall see, this criterion can help us whenever the "correct" definition of subtype is not immediately evident.

A second guideline is compatibility with the other typing aspects. The subtype relation should fit as "naturally" as possible into the world of type constructions. This has a particular effect on the relation to sum types.

As a consequence of this approach, we get an answer to an old controversial question: are subtypes (in the mathematical sense) true subsets or just subsets modulo a homomorphic embedding? In interaction with our other type constructions, the answer is: subtypes are subsets modulo homomorphic embedding.

Note: So as not to be misunderstood: This statement holds in the context of our general treatment of the typing idea. For languages that follow a different type philosophy, the answer may accordingly be different.

2 Likes
#8

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.