> However, this is not the interpretation that leads to a straightforward correspondence between logic and programming. For example, we would like "A and B" to correspond to the type of pairs of elements of A with elements of B, which is not at all the set-theoretic intersection. And while "(A and B) implies A", we do not want to say a value of type "(A, B)" also has type "A". (E.g., if a function expects an "A" and receives an "(A, A)", we are at an impasse.)
Intersection types in TypeScript and Scala 3 do work like conventional intersections / conjunctions. Something of type A&B is of type A. For example, a Set&Iterable is a Set. This makes perfect sense and is coherent with how unions work. A&A is then obviously equivalent to A. I'm not sure where you see the problem.
Intersection types in TypeScript and Scala 3 do work like conventional intersections / conjunctions. Something of type A&B is of type A. For example, a Set&Iterable is a Set. This makes perfect sense and is coherent with how unions work. A&A is then obviously equivalent to A. I'm not sure where you see the problem.