A blend of intersection types and union types

authors: Baber Rehman
year: 2023
url: https://i.cs.hku.hk/~bruno/papers/Baber-thesis.pdf
publisher:
abstract:
notes:
Note the last premise in rule type-switch. It says that the branches of a switch expression must not have overlapping types. Therefore the following program does not type-check in λu because Int and ⊤ are overlapping types: switch (x : Int ∨ ⊤) {(x : Int) → true,(y : ⊤) → false} Whereas the following program type-checks because Int and Bool are non-overlapping or disjoint types: switch (x : Int ∨ Bool) {(x : Int) → true,(y : Bool) → false} Note that the disjointness in disjoint intersection types and disjoint switches diverge. Two types are disjoint in disjoint intersection types when they do not share a common supertype. Whereas two types are disjoint in disjoint switches when they do not share a common subtype.