6
$\begingroup$

This question asks why union and intersection types are the "opposite" of the mathematical union and intersection operations when considering the types' sets of properties.

Such questions are related to language design and implementation insofar as type theory itself is. On the other hand, questions about type theory are on-topic on CS SE and CS Theory SE, and many are also on-topic on Stack Overflow (and indeed, this specific question already has answers there), so there is the potential for duplicating a lot of content across sites if we allow them here.

I can see arguments for and against allowing questions like this, and I don't have a strong view either way but I would lean towards allowing them. What is the community's view?

$\endgroup$

2 Answers 2

11
$\begingroup$

I think type-theory questions should be allowed here, since they’re certainly on-topic. The siloing of Stack Exchange sites inherently creates some overlap and duplication of questions, and requires some allowance for it. So in such cases, I think our responsibility is to clarify where it’s better to ask. For example:

  1. CS and TCSpure type theory questions from students and practitioners, especially questions about language-agnostic concepts, algorithms, and proofs, for their own sake.

    • Does my type system have the properties I expect?
    • Is typechecking in this system decidable?
  2. Stack Overflowtype-theoretic literacy questions from users of type systems, wanting to build understanding, for the purpose of programming.

    • I’m trying to write a Scala program and I expected it to infer this type, how come it can’t?
    • My Haskell code gives me an error message with some type-theory jargon in it. What does it mean?
  3. Hereapplied type theory questions from implementors of type systems, wanting to build understanding for the purpose of langdev.

    • Should I include this type-system feature in my language?
    • Why is this property a consequence of this type system?
    • How do I implement this rule of this type system?

There are close analogies with other scientific fields like mathematics, physics, or chemistry:

  1. Students and theorists — people whose intention is to make research results

  2. Users and enthusiasts — by far the majority, who may have an interest in the subject for work or entertainment, but aren’t experts, and don’t do research

  3. Engineers and tinkerers — downstream of researchers (1) and upstream of end-users (2)


So by the above groupings, I think the question you link is not a great fit, but still a good one. I will highlight these quotes which I think are telling:

Why intersection types have more fields and union types have fewer fields?

[…]

I even implemented it backwards when I implemented the type system for my language.

To me, these show that this is an example of a “why” question that an implementor needs to understand in order to implement the system correctly. A user doesn’t necessarily need this knowledge: if they use a meet when they need a join or vice versa, a correctly-implemented typechecker will reject their program.

$\endgroup$
2
  • 2
    $\begingroup$ I broadly agree with this answer, but I wonder how many "pure type theory" questions are not also practical questions that implementors could have. For example, decidability seems like something a language designer would want to ensure about their language's type system, since an undecidable type system cannot practically be implemented. $\endgroup$
    – kaya3
    Commented Jun 20, 2023 at 10:24
  • $\begingroup$ Another possible place to ask type theory questions, depending on the question, is proofassistants.SE. $\endgroup$
    – Pseudonym
    Commented Jun 21, 2023 at 13:47
3
$\begingroup$

Only when they affect implementation/design of the language

For example, in Typescript the existence of a type theory feature leads to having to check for the fields of an object at compile time instead of a (potentially quicker and simpler) type equals or subclasses check.

The particular question we're talking about seems to be less language-specific in that it asks about what ends up being available when you use type intersection/unions, which is very much a trait of type theory itself and not something a language might be interested in affecting.

A question along the lines of

How should I implement attribute access in a compiled language that supports type intersection/union?

or

What are the disadvantages of including type theory in my language?

Might be more suited for this site.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .