Existential types in Rust
Existential types in Rust
Posted Apr 24, 2024 17:01 UTC (Wed) by starblue (guest, #5842)In reply to: Existential types in Rust by mb
Parent article: Existential types in Rust
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).
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).