First cut at analyzer preferred subtyping algorithm #388
Conversation
| the syntactic criterion that `T` is any of: | ||
| - `Null` | ||
| - `S?` for some `S` | ||
| - `S*` for some `S` where `S` is nullable |
There was a problem hiding this comment.
note that we don't have to cover this case ourselves in the analyzer; we definite [S/S'?]S* = S'?.
| nullable then the subtyping does not hold (return false) | ||
| | ||
| - **Left Nullable 2**: otherwise, if `T0` is `S0?` then the subtyping holds iff | ||
| `S0 <: T1` (return true or false) |
There was a problem hiding this comment.
I think ideally we wouldn't have to extract S0 from S0?, because it requires a copy of S0 which may be a moderately complex type like a function type.
That said, I think we are mostly worried about extracting S0 from S0*, since legacy types will be much more common than nullable types for a long time. So unwrapping S0? may be totally doable.
MichaelRFairhurst left a comment
MichaelRFairhurst left a comment There was a problem hiding this comment.
Thanks for getting on this so quickly Leaf! Definitely some differences between what we've come up with, which tells me that your approach of refactoring the existing rules gives us a really really important sense of confidence once we have the right rules.
| apply that `T1` is nullable. | ||
| | ||
| - **Left Legacy** if `T0` is `S0*` then: | ||
| - `T0 <: T1` iff `S0 <: T1` (return true or false) |
There was a problem hiding this comment.
Yeah so this rule is a potential performance problem for us.
Do we need to redo all the prior steps if we don't allow representation of T?* etc?
| - `T0 <: T1` iff `T0 <: S1?` (return true or false) | ||
| | ||
| - **Right Nullable**: if `T1` is `S1?` then `T0 <: T1` if: | ||
| - `T0` is nullable |
There was a problem hiding this comment.
I think maybe there's a missing negative here somewhere or something. Am I correct in reading that these rules currently say FuureOr<int?> <: String??
There was a problem hiding this comment.
This is equivalent to Null <: T0, but I think the correct condition is
| - `T0` is nullable | |
| - `T0 <: Null` |
4 participants
Just exploration right now. The analyzer folks wanted to explore re-factoring the algorithmic subtyping to make it easier to share code between the legacy and new type systems, here's my attempt at working their suggestions into a version of the rules.
cc @MichaelRFairhurst @stereotype441