Difference between returning dyn Box<Trait> and impl Trait

I’m convinced: T -> Anything<T> is the way to think about “for all T” in a where clause. This holds converting T to a borrow: T -> &T. My thinking T -> T was wrong.

It depends on what you mean with Anything<T>.

Note, that where clauses describing existentials usually don't land in where clauses describing the parametrized function/type.

Example:

fn function<T>(x:dyn Trait,y:T) where T:Equatable

Is the same as:

fn function<T>(x:(S where S:Trait),y:T) where T:equatable

but not the same as:

fn function<S,T>(x:S, y:T) where S:Trait, T:Equatable

Type parameter S for the function in the middle could be named T because the where clause is in its own nested scope.
The function in the middle is however not directly expressible in Rust.

1 Like

I'm running into an incongruency in how I think about traits.

My dominant view (starting point) of traits is their ability to solve problems such as how to implement addition. The concept of addition exists for many types, but not all types: Traits. I liked the term "ad hoc" polymorphism because it's a "separate" way to deal with concerns across different types. "ad hoc" also implies a sequence of how to design my types: Traits come after my "other" types.

What this view translates to is: addition is not applicable for all T, so

fn add(input1: T, input2: T) -> T

... is too generic. But,

fn add<T: Add>(input1: T, input2: T) -> T

... draws a useful, type-safe boundary. I went from "any T" to "some T".

Where I need to do some more work, is rectifying this view with how the community discusses the concept of "some/existential", and "any/universal" when discussing impl Trait. The target/subject for the descriptor is slightly different. For instance, from one of the RFC's that proposes adding impl Trait in the argument position:

There are basically two ways to talk about an "unknown type" in something like a function signature:

  • Universal quantification , i.e. "for any type T", i.e. "caller chooses". This is how generics work today. When you write fn foo<T>(t: T) , you're saying that the function will work for any choice of T , and leaving it to your caller to choose the T .
  • Existential quantification , i.e. "for some type T", i.e. "callee chooses". This is how impl Trait works today (which is in return position only). When you write fn foo() -> impl Iterator , you're saying that the function will produce some type T that implements Iterator , but the caller is not allowed to assume anything else about that type.

When it comes to functions, we usually want any T for arguments, and some T for return values.

Thus in fn f(x: impl Foo) -> impl Bar, the caller picks the value of x and so picks the type for impl Foo, but the function picks the return value, so it (the callee) picks the type for impl Bar.

These quotes may not exactly capture my point, but they seem to skip an important starting point: by definition of using a trait to qualify the argument T, we have entered the realm of "some" types i.e., those those types T that implement the trait. With this qualifier in place I can use the trait methods in the body of my function. This is not

Furthermore, for the most part, if I want to actually do something with T (e.g., not just wrap it), I need to know something about T. So again, "some".

Do you see what I mean?

Here's an excerpt from my thesis draft that attempts to explain this:

When reasoning about Rust code, it is often helpful to think in terms of typeclasses , sets of types that all share some common properties. Rust has several different mechanisms to describe typeclasses, depending on the nature of the properties that they share:

  • The class of types with a particular memory layout is represented by a generic datatype .
  • The class of types which exhibit a particular behavior is represented by a trait .
  • The class of types which are valid for a particular period of time is represented by a lifetime annotation .

In generic code, an externally-specified type is represented by a type parameter. This parameter is a local identifier that acts in all ways like a concrete type name. The types that are allowed to bind to a particular parameter are specified by a special kind of expression, a type bound. Each type bound specifies one or more typeclasses; any type that is a member of all the listed typeclasses is valid.

Within the scope of a type parameter, it may only be used in a way that will be valid for all possible type bindings. This analysis is completely local: The compiler rejects code that attempts to use any property that is not provided by one of the typeclasses in corresponding bound expression.

What I describe here is the behavior of universally-quantified types. Existential types behave almost exactly opposite to this.

When writing a generic function, you have to assume that universally-quantified type parameters may be any type drawn from the identified class (i.e. you can only use operations that are valid for every type in the class). For existentially-quantified type parameters, you are free to choose any particular member of the class that suits your needs.

When calling a generic function, the roles are reversed. You are free to choose any types which satisfy the given bounds for universal parameters. But the existential parameters are out of your control: you may only use them in ways that would be valid for all types that meet the given bounds.


In other words:

  • Universal quantification restricts the types a caller can use and the behaviors the implementation can use.
  • Existential quantification restricts the types an implementation can use and the behaviors the caller can use.
2 Likes

I think, if still not clarified, your question is interesting for its own right.
From time to time, this or related questions about existentials seem to popup, I was one of them.
I think it's worth to post your concern in a new thread attracting the right people to answer.

1 Like

@EdmundsEcho,

This might be related to your point.

2 Likes

This is not the way "some" is used in mathematical logic. It may be a bit confusing because English uses the word "some" in both ways, e.g.

Rust's mascot is a crab for some reason.

There is one particular reason for Rust's mascot being a crab, but the speaker doesn't know or care what it is.

The borrow checker is confusing for some people.

There is a nonspecific number of people who find the borrow checker confusing.

Both of these are standard English meanings. But only the first one is used in formal logic and is what people mean when they define existential types as being "for some".

In logic fn add<T: Add>(input1: T, input2: T) -> T is not a "for some". It's still a "for all" because it applies to all T such that T: Add.

1 Like

Great post. Thank you.

Before responding to this post, I did some digging I reviewed a paper that first introduced me to type classes and re-read a chapter or two from "Types and Programming Languages" by Benjamin C. Pierce. Some consider it a definitive resource. All that said, there is lots of room for interpretation on my part. However, I was motivated as the terminology used to describe various aspects of abstract data types and other related concepts is seemingly pointing me in different directions.

My hypothesis: using T to mean anything other than "all types" as the starting point, introduces an inconsistent logic

When a type must implement a trait(s) in order to be admitted (i.e., pass the type-checker) it is an existential quantification. This is in contrast to universal quantification where the function must admit any and all types. T on its own means "all types". Finally, it is only partly correct to associate the quantification with caller vs callee control of the types admitted by a function.

So what

Without consistently holding T to represent all types we introduce multiple possible interpretations in a context where both universal and existential quantifications are required.

Where I see contradictions

Perhaps I'm misunderstanding, but I would suggest these statement are better described as an "existential" quantification of the type T, not "universal". The idea of "universal" and "restricts" seem contradictory; as are "any" and "part-of" etc..

Type parameter, e.g., T that "acts in all ways like a concrete type"... "the types that are allowed to bind" seems to me "existential" by definition of the possibility of rejection (so subset).

Example of correct use "universal" quantification

The following makes sense...

∀a ∈ ℕ

... because the starting point is literally anything. So, the expression now describes "for all values a that are members of the set of natural numbers...".

However, this is not what we are dealing with when we talk about T. So, the following:

∀T ∈ Trait

... strictly speaking is not what we mean given our the use and understanding of T as representing "any" type. Unless all types implement Trait, the statement is either wrong, or needs more interpretation (i.e., is unclear).

If we take the position that the whole point of the where clause is to specify what T is "in the first place" (i.e., ignoring that T already had meaning), then the statements make more sense.

however... if only by convention (that's a lemma on my part) the community continues to use "universal" as all types that implement a set of Traits, that would be unique to Rust.

Abstract data types are inherently "existential"

Only to level-set, traits are by definition, an abstract data type. This is true because a trait is a type that hides the underlying type. So, in impl Display for i32, i32 represents a hidden type. Depending on the context, the type system is aware of either:

  • i32
  • i32 as Display (hiding i32)

Caller vs callee control over the type is somewhat an artifact of the limited capacity of impl Trait (as of now)

In a generic function, where any (∀) type T is permitted, the caller determines the type.

In an existentially quantified function, where only the subset of T, specifically those types that implement Trait (∃), AND when the impl Trait specifies the return value, the callee determines the type.

In an existentially quantified function, where only the subset of T, specifically those types that implement Trait (∃), AND when the impl Trait specifies the input argument value, the caller determines the type (not yet possible, but does not change the logic)

The hook that "universal" => caller control is true, but the same can be said for "existential" in the input argument position (logically speaking). So the contrast is tactically useful right now, but not strictly based on quantification.

All in all

I can see how "universal" can make sense to describe all types that implement a set of traits. However, it requires a new understanding for what T is supposed to represent in a context where generics exist (i.e., where T already has meaning representing any and "for all types"). As such, presents a contradiction when used otherwise. This is reason enough to support the hypothesis. To the degree "it's all relative", by definition of what's being described, abstract data types, they are "existential". So why not "go with the flow" and use "existential" when describing which Ts separate from all Ts qualify?

We could be in a universe that recognizes ℝ too. It's not literally anything, it's anything in the set described. You could have ∀a ∈ {ℝ - ℕ} or any other sort of set restrictions...

...just like here the starting point is ∀T ∈ {TraitBound1 ∩ TraitBound2 ∩ etc}.

No. Type parameters (generics) are universally quantified whether or not they have trait bounds. Adding trait bounds limits the universe, so to speak, but it doesn't change the nature of the quantifier, i.e. it is still ∀ T: Trait and not ∃ T: Trait (again playing it a bit loose with the notation as I never learned any logic to do with type classes).

Consider this piece of code:

trait Foo {
    fn foo(&self);
}
trait Bar {
    fn bar(&self);
}

fn foo_and_bar<T: Foo + Bar>(arg: T) {
    arg.foo();
    arg.bar();
}

foo_and_bar is universally quantified over all T such that T: Foo + Bar. That doesn't mean that any T actually implements both Foo and Bar -- maybe no such T exists at all! But for any T: Foo + Bar that does happen to exist, you can call foo_and_bar::<T>. Even though that so-called universe of discourse, "the set of all types T such that T: Foo + Bar", isn't as big as "the set of all types", the quantification of T in the definition of foo_and_bar is still a universal quantification within that subset.

Existential quantification is a completely different thing. Suppose you wrote a function like this:

fn get_foo() -> impl Foo {
    /* suppose we return something here */
}

impl Foo is existentially quantified: there definitely exists some particular type that implements Foo, and the proof of its existence is that foo returns it.

This is a perfectly reasonable conclusion (although not the only reasonable conclusion) if you just take these words at their standard English face values. But they're not being used as standard English; they're part of a jargon of formal logic where "universal" has a specific meaning and makes perfect sense to apply to a restricted subset of some other set.

Nope, as already discussed, the possibility of things existing outside the universe of discourse does not make the universal quantification existential.

It's not "literally anything", though. It's "just the things that are natural numbers". That's the universe of discourse. You can have statements like "for all a greater than 4" or "for all composite a" and those are still universal, just with a smaller "universe".

Again, no... that's pretty much the common formal-logic definition of "universal" that I learned in my freshman college Discrete Mathematics course. It might not be the only standard English definition of "universal" but it's definitely not just Rust being weird.

I think you are touching on an important point here. Namely, there is a degree of perspective to whether you consider a type existential or universal. What's existential to the caller ("this function returns something that implements Foo") is universal to the callee ("I can return anything so long as it implements Foo"). And what's universal to the caller ("I can give this function anything that implements Bar") is existential to the callee ("the caller will give me something that implements Bar"). Your apparent rejection of this principle is based on a nonstandard definition of "existential".

Traits are not types. They're more like sets of types, or maybe relations on types... I'll have to leave this one for somebody else to pick up.

The type system can easily be aware of both, and often is. Consider fn id<T: Display>(a: T) -> T {a}. id(10_i32) is still an expression of type i32, not of (some opaque type that implements Display), because T is universally quantified even though it appears both in argument and return positions.

Only because you're using a nonstandard definition of "existential".

Because that deprives the word "existential" of its conventional and useful meaning.

2 Likes

Thank you.

Solid food for thought. This is where I suspect the nuance and perspective explains the difference. It depends on the starting point/reference.

I think I can agree with much of what you point out whilst still holding that it might make sense to call out when T is not something that represents all types. Where T represents all types is irrefutably “universal”, so good for “level-setting”. How to qualify the quantification from that point on could be made more explicit somehow.

Why so? Without clarification, hooks taking on lore relating quantification to other things become non-sensual guess work. No?

Yes, however my point is that that can’t be true at the same time we agree that T represents all types. Somewhere “along the way” universal means what you stated (for all that impl Trait). However, this happened “without notice” and when we are in a context where there are now two legitimate interpretations of “universal”. I argue that no matter from the caller or callee perspectives: all types is all imaginable types. Changing that meaning seems to be a problem... because folks are using the terms as absolutes to explain other things. The quantifies have relative meanings and thus always “it depends”.

You can always translate one of these bounded universal quantifications to an unbounded one by introducing an implication. These two formulations are entirely equivalent:

“For every x in the set S, proposition P(x) holds”
∀(x ∈ S). P(x)

“For every x, if x is in the set S, then proposition P(x) holds”
∀x. (x ∈ S) ⇒ P(x)

Applying this principle to the type assertions made by a generic function definition, you get a formulation like this:

fn foo<T:Trait1>(T)->impl Trait2;
T. (TTrait1) ⇒ ∃U. (UTrait2) ∧ (fn(T)->Ufoo)

For every T, if T implements Trait1, there is some type U where both U implements Trait2 and fn(T)->U is a concrete signature of the generic function foo.

All of the quantifiers in this formulation are operating on the universal set, and we reach the same result. The alternative notation is really just a shorthand because ‘all elements of a given set’ and ‘some unspecified member of a given set’ are extremely useful concepts.

5 Likes

The trait bounds are the notice given, or in logic theory, the set inclusion notation or "such that"s. (You could argue that implicit bounds like Sized happen without notice, in Rust.) Since you found the set of natural numbers version intuitive, I tried to show that it is the same thing. In a universe of real numbers, that quantifier over the natural numbers is still completely valid. And in a universe of types, a quantifier over the set of types which meet the stated bounds is just as valid. In some of the links below, this is called "the range of qualification". Only being able to make statements where the range is the entire universe is pretty limiting, as you pointed out yourself earlier in this thread. So given a universe of types, we specify subsets by setting trait bounds.

I think the real disconnect, though, is that "universal" and "existential" in these discussions are referring to the quantifier operators from formal logic, and not their informal english meanings. If you really want to dig into why that is relevant, you could read Niko's blogposts on Chalk:

Even then though, I should point out that some familiarity on the topic is assumed. I wish I had a good reference to give here (anyone else?), but depending on how much formal logic you've been exposed to, if you want to follow closely along I recommend:

Or you could skip all that and just read the blog posts with formal logic in the back of your mind to get the gist -- the real point is, these formal logic systems, including the universal and existential operators, are how the type system actually works, in a mathematically rigorous sense. From that starting point, intuition or interpretation of the words in their english sense doesn't really enter into it.

4 Likes

Not exactly, the (nth) caller of the caller determines the type, i.e.

∃ In argument position:

∃S∀T fun:(S,T)=>Void

means the caller can choose T but S was bound before and the choice is independent for T

∀T∃S fun:(T)=>S

means the callee bounds S which may depend on T, hence for every T exists an S.

It depends on what you mean with abstract type, but usually it's some type stealing/borrowing literals from another (abstract) type.
And the opposite is a base type who owns literals like i8 (owning 1i8 for example).
So yes, an existential type is literally an abstract data type, but this resembles a more set theoretic meaning of Traits (Traits as types) which is expressed by dyn Trait/impl Trait causing a subtype relationship.

Whereas the Trait itself is considered to be a predicate over types which brings us to:

Indeed, it is what we mean with "forall types T". The universe of T is the set of all types (commonly denoted as Type) so we can rewrite the statement above to:

∀T:Types ∈ Trait //we refine T implicitly with the bound/predicate Trait

and further to:

∀T:Type where T ∈ Trait

such that:

impl/dyn Trait = ⋃_{T isa Type and T conforms to predicate Trait} T

whereas

Trait = {T|T provides implementations for all required methods of Trait} 

As said before, dyn/imp Trait is the same existential type, but the implementation is different. To refine it a bit, dyn Trait is what we usually see as an existential type, and impl Trait is a restriction of dyn Trait to be statically determinable (by compiler reasoning).

I think part of the confusion stems from the overloaded meaning of : == memberOf + conformsTo + equalsTo (in case of struct fields).

2 Likes

For the people who are still discussing this, the answer to the OQ is in post by Cerberuser:

And by H2CO3, marked as a solution.

1 Like

Thank you to all for these solid responses. They are both illuminating and convincing.

In the following juxtaposition:

I agree. The way you have stated it makes complete sense. I'm also seeing how the use of the universal vs existential terms is not determined by set, subset necessarily. But rather, the limits of what can be inferred. Your juxtaposition made that clear to me.

Using the following form

∀x. (x ∈ S) ⇒ P(x)
fn foo_and_bar<T: Foo + Bar>(arg: T) -> ()
// could be quantified as
∀T. (T ∈ Foo ⋀ T ∈ Bar) ⇒ fn(T) -> () 
// compared to
fn get_foo() -> impl Foo
// could be quantified as
∃T. (T ∈ Foo) ⋀ fn() -> T
Notes
  • impl Trait and dyn Trait are two ways to implement a function that returns an existential type.
  • dyn Trait is a trait object that came to be from a trait with object safety, placed in a context where a trait object is required
  • dyn trait is a single standalone type (the underlying type is “forgotten”); the single type can be cast from many types simultaneously
  • dyn trait uses dynamic dispatch; impl Trait is static
  • impl Trait is an abstract data type (shares methods across instances?); dyn Trait is more like a traditional object (each instance has its own methods and state)

I'm getting the additional meaning of the quantifiers. The existential vs universal qualifiers are not in relation to a fixed meaning T, but rather what can be said (what can be inferred) about the set of types.

For instance, when I went through the logic associated with the following, it was clear that T describes the types "I need to include" for the logic to hold. That approach can be applied consistently as many have pointed out.

Caller vs Callee control over type


From the external, caller perspective

fn foo_and_bar,

  • scope of the control: function input
  • input type: any T that implements Foo and Bar
    => "this function accepts any T that implements Foo and Bar"
    universal: I know all the underlying types it accepts
    T: a subset of all types

fn get_foo,

  • scope of the control: function output
  • output type: any T that implements Foo
    => "this function returns a type that implements Foo" or,
    => "the underlying type could be anything that implements Foo"
    existential; I don't know the underlying type, I only know the type exists in the subset of types that implement Foo
    T: all types

From the internal, callee perspective

From the internal, callee perspective

foo_and_bar,

  • scope of the control is the function input
  • input type: T that implements Foo and Bar
    => "the underlying type could be anything that implements Foo and Bar"
    existential; I only know the type is a subset of any type
    T: all types

get_foo,

  • scope of the control is the function output
  • output type: any T that implements Foo
    => "this function returns any T that implements Foo"
    universal: I know all the underlying types it returns
    T: a subset of all types
2 Likes

It sounds like you've gotten a good handle on how all of this fits together. There's one small error that I spotted:

The identity for existential quantifiers is a little different than for universal ones. This should be:

∃T. (T ∈ Foo) ⋀ fn() -> T

The existence of the function guarantees that the type T exists, and that it implements Foo. Your quantification would allow choosing a T that doesn't implement Foo, as long as it's not returned by get_foo.

Thank you. I updated the post with your suggested correction. Is there a form that is consistent with: ∀x. (x ∈ S) ⇒ P(x)?