[jonlong]

I suppose I erroneously assumed some familiarity with the correspondence between product types (i.e., types of pairs) and the constructive logical interpretation of "and".

Suffice it to say for now: there is an interpretation of logic that gives a tighter correspondence to programming than the set-theoretic one, under the name "Curry-Howard" or "propositions as types, proofs as programs", and which has been known and cherished by logicians, programming language theorists, and also category theorists for a long time. The logic is constructive as it must be: a program of type A tells us how to build a value of type A, a proof of proposition A tells us how to construct evidence for A. From here we get things like "a proof of A and B is a proof of A together with a proof of B" (the "BHK interpretation"), which connects "and" to product types...

I spoke up because I could not leave untouched the idea that "tagged unions are illogical". On the contrary, tagged unions (aka "disjoint unions", "sum types", "coproducts", etc.) arise forthwith from an interpretation of logic that is not the set-theoretical one, but is a more fruitful one from which programming language theory begins. You are not wrong that there is also a correspondence between (untagged) union and intersection types and a set-theoretical interpretation of propositional logic, and that union and intersection types can also be used in programming, but you are missing a much bigger and very beautiful picture (which you will find described in most any introductory course or text on PL theory).

[cubefox]

But I'm pretty sure that even in intuitionistic logic, "A" implies "A or B". Which is not the case with tagged unions (as I said, because of wrapping).

[jonlong]

It's true that in intuitionistic logic "A implies (A or B)"; the usual computational interpretation of that is that "there is a function taking a value of type A and returning a value of type A + B", where + is the tagged union, and, per above, that function is exactly the one which tags its input as belonging to the left disjunct.

I suspect you are still reading "A implies B" as "A is a subtype of B", derived from a set-theoretic interpretation of propositional logic. But the constructive interpretation is that a proof of "A implies B" is a method to take a proof of A and transform it into a proof of B. Computationally, a value of type "A implies B" (typically rewritten "A -> B") is a function that takes values of type A and returns values of type B.

Well, everything I've said here is standard and widely-taught; go forth and check if you're inclined to. A good introduction is the one by Philip Wadler, https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as... (tagged unions appear in Section 3, though it's all worth reading). A much more to-the-point and programming-focused account is in this OCaml book: https://cs3110.github.io/textbook/chapters/adv/curry-howard.... (very little OCaml syntax is used). You can find countless more.

[cubefox]

Thanks. I think in the end the question will be: which is better, an algebraic or a set-theoretic type system? Which is more practical to use? Which is more elegant? Should both be mixed?

(One complicating aspect is that there doesn't yet exist a mainstream language with full set-theoretic type system. TypeScript and Scala 3 currently only support intersections and unions, but no complements, making certain complex types not definable. E.g. "Int & ~0", integers without zero.)