Add spec for intersection types #5233
Conversation
| ## Syntax | ||
|
|
||
| Syntactically, an intersection type `S & T` is similar to an infix type, | ||
| where the infix operator is `&`. |
There was a problem hiding this comment.
Let's expand on this a little bit:
... where the infix operator is the identifier &. & is treated as a soft keyword. That is, it is a normal identifier with the usual precedence. But a type of the form A & B is always recognized as an intersection type, without trying to resolve &.
| ``` | ||
| Type ::= ...| InfixType | ||
| InfixType ::= RefinedType {id [nl] RefinedType} | ||
| RefinedType ::= WithType {[nl] Refinement} |
There was a problem hiding this comment.
I'd drop productions for RefinedType and WithType, since WithTypes will be removed, adding them here is confusing.
|
|
||
| The type of `children` in `A & B` is the intersection of `children`'s | ||
| type in `A` and its type in `B`, which is `List[A] & List[B]`. This | ||
| can be further simplified to `List[A & B]` because `List` is |
There was a problem hiding this comment.
By what rule? I think it would be good to specify the rule for this.
There was a problem hiding this comment.
I proposed a rule in the subtyping section
There was a problem hiding this comment.
It seems List[A & B] <: List[A] & List[B] can be derived by the normal subtyping rule for type constructors, no more rules required.
A <: A B <: B
---------- ---------
A & B <: A A & B < B
---------------------- ----------------------
List[A & B] <: List[A] List[A & B] <: List[B]
--------------------------------------------------
List[A & B] <: List[A] & List[B]
If C is contravariant:
A <: A B <: B
---------- ---------
A <: A | B B < A | B
---------------------- ----------------------
C[A | B] <: C[A] C[A | B] <: C[B]
--------------------------------------------------
C[A | B] <: C[A] & C[B]
I agree, it is good to document them.
| ---------------- | ||
| A & B <: T | ||
| ``` | ||
|
|
There was a problem hiding this comment.
If C is a type constructor, the join C[A] & C[B] is simplified by pulling the intersection inside the constructor, using the following rules:
- If
Cis covariant,C[A] & C[B] = C[A & B] - If
Cis contravariant,C[A] & C[B] = C[A | B]
There was a problem hiding this comment.
Ahh ... I think my comment above should have been a follow up to this ...
There was a problem hiding this comment.
Good catch. The derivation provides partial justification for the simplification, as we cannot derive in the other direction.
I tried to find examples where the rules are unsound, but failed. It seems the other direction can be justified informally. @odersky mentioned some theoretical work is needed here based on DOT.
|
|
||
| ## Type Checking | ||
|
|
||
| The type `S & T` represents values that are of the type `S` and `T` at the same time. |
There was a problem hiding this comment.
I would leave this material in the main page.
| class C extends A with B { | ||
| def children: List[A & B] = ??? | ||
| } | ||
| ``` |
There was a problem hiding this comment.
Integrate the whole type checking section in the main page.
|
|
||
| - If `C` is covariant, `C[A] & C[B] ~> C[A & B]` | ||
| - If `C` is contravariant, `C[A] & C[B] ~> C[A | B]` | ||
|
|
There was a problem hiding this comment.
Where does the "simplified" terminology and the ~> come from? Intuitively it makes sense, but seems redundant with the typing rules stating the same thing immediately below.
Add spec for intersection types