4
$\begingroup$

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)

$\endgroup$
4
  • $\begingroup$ What is set-theoretic semantics? A denotational semantics in which types are interpreted as sets? Are we talking about intuitionistic set theory or classical set theory? $\endgroup$ Commented Nov 3, 2023 at 7:52
  • $\begingroup$ Yes I am talking about the semantic which interprets types as sets, my wording may not be very rigorous : ), and I'm talking about classical set theory (even perhaps naive set theory), because I can hardly conclude more from those intersection types/union types $\endgroup$
    – Dylech30th
    Commented Nov 3, 2023 at 8:51
  • $\begingroup$ One question is whether this would actually be useful. Are there situations in programming where you'd want to declare that a variable isn't an integer, while allowing the possibility that it might be any other type at all? $\endgroup$
    – N. Virgo
    Commented Nov 4, 2023 at 3:40
  • $\begingroup$ Well, this may sound weird but I am indeed talking about the theoretical part from a practical perspective.. so yes this may not be useful at all but consider it as a digression from those languages with intersection types/union types, like —— what will happen if we fulfill such set-theoretic notions, i.e., include the negation type $\endgroup$
    – Dylech30th
    Commented Nov 4, 2023 at 11:16

3 Answers 3

4
$\begingroup$
  1. Negation is certainly possible in these systems. It's discussed in the best introductory materials, in particular: https://www.irif.fr/~gc/papers/covcon-again.pdf https://pnwamk.github.io/sst-tutorial/ This however doesn't have anything to do with double negation elimination or classical logic.

  2. As to why these systems are not widely used, there are a few reasons. One is just that the type systems are more complex, and harder to learn about and implement. Additionally, important features such as polymorphism have only been developed recently (e.g., in the last 10 years). The necessary algorithms are also quite expensive, as required by the expressiveness of the type system. Finally, most such type systems rely on runtime type information, which is available in runtimes for e.g. Lua or Erlang but not in conventional typed languages like ML or C.

    But these type systems are becoming more common as these constraints get met. E.g., Luau in Roblox uses set-theoretic types, and the new proposals for Erlang and Elixir and Ballerina do as well (designed by the originator of these systems).

  3. Finally, true union and intersection types have become more common as well, even if they don't adopt the semantic subtyping perspective (often for performance reasons). See TypeScript, Flow, Typed Racket, and more.

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ Thanks for your answer! I'm aware that the normal way to define the negation of A intuitionistically is to define it with a function type from A to the absurdity $\endgroup$
    – Dylech30th
    Commented Nov 3, 2023 at 8:38
  • $\begingroup$ but I want to know if types are viewed as sets in (engineering perspectives, which means what makes type theory differs from set theory is not that important), then is any language or any possibility to define a type ¬A in a language as "any type that is not of type A", just like how complements are treated in the set theory, this kind of interpretation sounds "natural" (perhaps? I'm not sure) when discussing together with "set-theoretic types" such as intersection type and union type (which mostly appear in the general purpose language that is born for engineering purpose, like typescript $\endgroup$
    – Dylech30th
    Commented Nov 3, 2023 at 8:39
  • $\begingroup$ My problem concerning this mainly arises from the recently announced so-called "set-theoretic type system" of Erlang, see Set-theoretic Types for Erlang $\endgroup$
    – Dylech30th
    Commented Nov 3, 2023 at 8:42
  • $\begingroup$ Well, why not mention from the start that's what you're looking at? Section 3 of the paper explains what they're doing. It's not the standard set-theoretic semantics in which types are sets, but rather subset semantics in which types are subsets of a given set $M$ (the model). (They also explain that they restrict recursion so that the above problems do not arise.) Because every type is a subset of $M$, negation is just complement relative to $M$. You're worrying about the wrong thing. $\endgroup$ Commented Nov 4, 2023 at 12:05
2
$\begingroup$

Generally, and to build upon this discussion, there is plenty of work which describes types exactly as you'd like, that is as a collection of "values" of a certain shape, with natural set theoretic operations on them, like complement, union and intersection.

Worth remembering that union and intersection should be untagged if you want them to be "set-like", that is an element of Nat + Bool should look like 5 or true rather than Left(5) or Right(true), otherwise you're in "structural land", and it doesn't really matter whether you think of types as sets (though it's possible as Andrej points out).

As the infinitely knowledgeable Noam notes, you have to be very careful if you have union or intersection types in the presence of mutation though, or polymorphism, because the type system quickly becomes unsound!

The example given in Davies and Pfenning (Intersection Types and Computational Effects) is simply:

   let x : ref nat /\ ref pos = ref 1 in
   x := 0;
   let z : pos = x! in
   z

With union types and negation, you can even break subject reduction on open terms without mutation! An example is given by Castagna et al in On Type-Cases, Union Elimination, and Occurence Typing.

I'll let you draw your own conclusions, but it's pretty clear that

  1. Types as a set-theoretic concept is quite well-studied, so not quite as "relatively rare" as you suggest.
  2. There are subtleties with the computational content of (untagged) intersection and union types in the presence of effects or other constructs, beyond the simple lack of logical correspondence.
$\endgroup$
3
  • 1
    $\begingroup$ Thank you! I understand that interpreting types as set-theoretic notions have been well-studied for a long time, (well, still, my question is regarding the practical application of it in the engineering languages), as you said intersection types and union types should be untagged if you want them to be set-like, and indeed, does this kind of interpretation extends to the relationship between complement and negation? Is there any sense in interpreting negations as the complements of sets? $\endgroup$
    – Dylech30th
    Commented Nov 4, 2023 at 11:25
  • $\begingroup$ Regarding practical applications: Typescript has a flavor of union types (typescriptlang.org/docs/handbook/unions-and-intersections.html). Regarding the negation/complement relationship: the "On Type-Cases..." paper presents complements as negation exactly as you suggest. $\endgroup$
    – cody
    Commented Nov 4, 2023 at 16:58
  • $\begingroup$ Appreciate, I'll have a look $\endgroup$
    – Dylech30th
    Commented Nov 5, 2023 at 1:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.