What is practically preventing us from applying set-theoretic types in engineering?

I know the title is sort of misleading because we do have set-theoretic types in several languages:) From a theoretic view, set-theoretic types such as intersection, union, and negation may bring some troubles, as the proof object they do not encode the derivation, thus making it hard to find a logical part through the C-H correspondence, moreover, negation is not able to be encoded at all because the normal semantic of complement in set theory contradicts the rejection of the non-existing of the double negation elimination in the intuitionistic logic (Question: is this viewpoint correct? that the set-theoretic approach contrast fundamentally with the central of the BHK interpretation of the intuitionistic logic). But from a practical view, it seems that there aren't so many obstacles, and we don't face that many problems we need to be concerned about in the theory: we are doing neither proof verifications nor automated reasoning, so my problems are:

• Why set-theoretic types are relatively rare in the languages?

• Can we define the negation type a: not A if a is not of type A (if we only consider the practical part of this problem)?

• Is subtyping also a set-theoretic definition? Since the subtyping also does not record the derivation, if this is true, then is subtyping some meta-theoretic level notation, and we need to put intersection/union/negation types at the same level as the subtyping relation.

Postscriptum: I've read MLTT and some topology & category theory, not yet started reading the HoTT Book (I want to do this after I've read algebraic topology and some higher category theory, though I might be aware of the fact that the HoTT book does not require so many preliminaries)

Let me first answer the easy part. The negation sign in the judgement a : ¬ A does not modify : but A. In particular, the standard way to define ¬ A is to equate it with A → ∅.

A major obstacle to using set-theoretic semantics for a programming language is general recursion. Concretely, the fixed-point operator

fix : {A : Set} → (A → A) → A
fix f = f (fix f)

can be defined in general-purpose programming languages. (The above definition works for a functional language, but the same kind of problem arises in any language with general recursion).

If we interpret fix in set theory, it says that for every set A and every map f : A → A there is a ∈ A such that f a = a. Indeed, just take a := fix f. However, if A has at least two elements, say a₁ and a₂, then the map g x := (if x = a₁ then a₂ else a₁) does not have a fixed point. So sets cannot be used to interpret general recursive functions.

If we remove general recursion, but keep structural recursion (which is always guaranteed to terminate), then we can use set-theoretic semantics. For example Martin-Löf type theory can be interpreted in set theory, and so can Coq's calculus of inductive constructions, and Agda's type theory with inductive-recursive defintions. All of these languages strictly control what form of recursion is allowed (namely structural recursion), so as to prevent existence of fix.

Another obstacle to set-theoretic semantics is polymorphism, see John Reynold's classic paper Polymorphism is not set-theoretic.

If you are willing to switch to intuitionistic set theory, then set-theoretic semantics can be recovered. See Andy Pitt's Polymorphism is set-theoretic, constructively and Alex Simpon's Computational adequacy for recursive types in models of intuitionistic set theory.

StackExchange Computer Science Q#162744, answer score: 4