Existential types in Rust

Posted Apr 24, 2024 16:04 UTC (Wed) by mb (subscriber, #50428)
Parent article: Existential types in Rust

>In 2018, Rust gained the ability to have impl Trait types as the argument to a function as well.
>However, these types still remain quite constrained compared to full existential types.

Is this case even an existential type at all?
I always thought this would be more or less syntactic sugar for the generics syntax.
The caller defines the type.

https://play.rust-lang.org/?version=stable&mode=debug...

to post comments

Existential types in Rust

Posted Apr 24, 2024 16:36 UTC (Wed) by tialaramex (subscriber, #21167) [Link] (1 responses)

Yes, that's not really an existential type, and we can tell because if we try to use it with different types it works - the compiler will just monomorphize your function again with the new type because this is just generics.

Here's a Jon Gjengset talk about all the places we can write "impl Trait" and they mean different things. Jon talks about the "Existential types" as Return Position Impl Trait, RPIT in 1.26. He literally says this is Existential Types about 3 minutes in.

https://www.youtube.com/watch?v=CWiz_RtA1Hw

The Argument Position Impl Trait APIT is really easy and so doesn't take long in the video - it's possible to watch the video distractedly and not realise Jon even mentioned APIT because it's like "Here's what this does, that was boring, it's just a generic with easy syntax", it is not an Existential.

Existential types in Rust

Posted Apr 24, 2024 16:48 UTC (Wed) by mb (subscriber, #50428) [Link]

>Return Position Impl Trait

Ah, yes. Thanks for explaining. I remember now that I heard that name before.

Existential types in Rust

Posted Apr 24, 2024 17:01 UTC (Wed) by starblue (guest, #5842) [Link]

It depends how you view it.
As an argument type the existential quantifier is in a contravariant position, which corresponds to logical negation. When you push the negation down over the quantifier you get a universal quantifier, which can be pushed all the way out, so it corresponds to the usual generics.
Defining a type alias for an existential type looks like it corresponds to skolemization, so that should go quite far. (Skolemization is used in first-order logic to remove existential quantifiers, by replacing them with a constant or function symbols).