Difference between returning dyn Box<Trait> and impl Trait

42

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
43

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
44

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
45

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
46

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.

47

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

48

I'm not sure; we're reaching the limits of the logic manipulations I'm comfortable with.

The closest I can think of is trying to formulate the view from inside the function, which might be something like this, but I'm not sure:

∀T. fn() -> T ⇒ (T ∈ Foo)

"For every type T, if get_foo returns T, then T implements Foo"

I don't know if this is always equivalent to the existential quantification of T or if it relies on some other axiom of the type system as well.

49

I think we killed it :)) Thank you.

1 Like
50

To gain deeper understanding, at some point it would make sense to introduce the Curry–Howard isomorphism and the calculus arising from it.

Let us consider the proposition A∧B. It corresponds to the type A×B, i.e. (A, B). Now let M:={A,B,C,D} be a finite set of types, then

∀T∈M.T = A∧B∧C∧D.

Thus ∀T∈M.T corresponds to (A, B, C, D). Let (a, b, c, d) be a term of this type. It may be considered as the function

{0↦a, 1↦b, 2↦c, 3↦d}.

But the elements of a set, in this case M, are unique! Thus we can use the types itself as arguments, hence the term is

{A↦a, B↦b, C↦c, D↦d}.

Now, by analogy, ∀T∈M.P(T) corresponds to the product ∏T∈M.P(T). Terms of this type are functions T↦y, where y: P(T). It will work even when M is infinite.

Say, we want to prove ∀A.∀B.(A∧B → A).

The corresponding type is ∏A.∏B.(A×B → A).

We find a term of this type, the left projection

A ↦ B ↦ (a,b): A×B ↦ a.

It's a pure and total function, thus the type must be inhabited. This proves the initial proposition.

If we uncurry a bit, we get

left_proj := (A,B) ↦ (a,b): A×B ↦ a,

or equivalently

left_proj(A,B)((a,b): A×B) := a.

In Rust:

fn left_proj<A, B>((a, _b): (A, B)) -> A {a}

And what about A∨B? It's the disjoint sum A+B, i.e. Either<A,B>, where Either is defined by enum Either<A,B> {Left(A), Right(B)}. The elements of this sum are pairs (Tag,value), i.e. (Left,a) and (Right,b), where a: A and b: B. The type of the value depends on the tag.

Then ∃T∈M.P(T) corresponds to ∑T∈M.P(T), i.e. a potentially infinite enumeration. Said again, the elements of a set, in this case M, are unique. Thus we can use the types itself as tags! The type ∑T∈M.P(T) consists of pairs (T,value), where value: P(T).

1 Like
51

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.