Specify null safety subtyping #3515

eernstg · 2023-12-14T16:32:56Z

This PR contains the null-safety updates from #2605 (the overall null-safety PR) that are concerned with subtyping. The intention is that we process and land this PR, and #2605 will then be made smaller when it is rebased over this one, thus allowing us to deal with the null-safety update in smaller portions.

lrhn

Can't really review this as source.
Do we still have a way to generate a rendering showing the changes?

lrhn · 2023-12-22T08:45:01Z

specification/dartLangSpec.tex

-which means that this seemingly expensive step can be confined to some extent.%
-}
+  \commentary{%
+    Note that this rule is admissible, and can be safely elided if desired.%


Define "admissible". It's a term of art not used elsewhere in the specification, so we cannot assume the reader to be familiar with it.

eernstg · 2024-10-17T14:24:58Z

dartLangSpec-3515.pdf

eernstg · 2024-10-18T10:30:36Z

Based on the output from git diff main..., here is an overview of the changes:

Front matter

Only comments.

@@ -21633,128 +21631,188 @@

Section 'Subtypes': Now mentions intersection types.

Figure 'Subtype rules': Changed a lot.

Subsection 'Meta-Variables': Slightly changes presentation of
metavariables.

Subsection 'Subtype Rules': Introduces the 'canonical syntax' of a
type. Controversial! An alternative could be to say that subtype rules
are not applicable to syntax, they are applicable to semantic
entities that are normalized in the same way as canonical syntax does
it. Extensively rewritten.

Subsection 'Being a Subtype': Extensively rewritten.

Subsubsection 'Informal subtype rule descriptions': Rewritten extensively.

Subsection 'Additional Subtyping Concepts': Extensively rewritten.

Section 'Function Types': Last paragraph modified.

Section 'Type Function': Rewritten.

@@ -22482,7 +22498,7 @@

Just the title of section 'Type dynamic' was adjusted, for consistency
(that is: titles do not use non-standard fonts).

Section 'Type FutureOr': Just adding missing \Error{} on static
errors, and updating Object to Object? in an example.

Section 'Type void': Removed commentary that reiterated an obsolete
definition of Type equality. Removed the item that enabled await expressionOfTypeVoid, because that rule that enabled this usage has
been removed from the language. Example at the end is updated.

Subsection 'Void Soundness': Example updated, plus body text about the
example.

@@ -23324,156 +23324,238 @@

Section 'Appendix: Algorithmic Subtyping': Updated to use the
NNBD-updated presentation of the subtype rules.

eernstg · 2024-10-18T11:36:10Z

specification/dartLangSpec.tex

+    if $T_1$ is \code{FutureOr<$S$>} for some $S$,
+    then the query is true if{}f \SubtypeNE{\code{Null}}{S}.
+  \item
+    if $T_1$ is \code{$S$?} for some $S$ then the query is true.


The case where $T_1$ is \code{Null} is already handled by reflexivity.

eernstg · 2024-10-18T11:50:32Z

specification/dartLangSpec.tex

+\item
+  \textbf{Left Top:}
+  if $T_0$ is \DYNAMIC{} or \VOID{}
+  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{\code{Object?}}{T_1}.


I think it should be 'iff' rather than 'if', so I changed it.

It could be implied that it works the same with 'if' because it was already stated that it is never necessary to try subsequent cases when a syntactic match has been determined, but many rules further down use 'iff' so it seems consistent to do it here as well.

eernstg · 2024-10-18T12:02:36Z

specification/dartLangSpec.tex

+\item
+  \textbf{Left Promoted Variable:}
+  If $T_0$ is a promoted type variable \code{$X_0$\,\&\,$S_0$}
+  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{S_0}{T_1}.


In 'subtyping.md' there is no 'If', and the second line is just 'and S0 <: T1'. However, that seems to make it less obvious that if T0 is a promoted type variable X0 & S0 but S0 <: T1 cannot be proven, then we do have a known false outcome, rather than a non-matching rule.

eernstg · 2024-10-18T12:02:49Z

specification/dartLangSpec.tex

+\item
+  \textbf{Left Type Variable Bound:}
+  $T_0$ is a type variable $X_0$ with bound $B_0$
+  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{B_0}{T_1}.


Similar to the previous rule. A few more rules below got the same treatment.

eernstg · 2024-10-18T12:08:52Z

specification/dartLangSpec.tex

+  $T_0$ is a function type and $T_1$ is \FUNCTION.
+\item
+  \textbf{Record Type/Record:}
+  $T_0$ is a record type and $T_1$ is \RECORD.


This one is far into the future (that is, it comes with a version which is much higher than 2.13), so perhaps we should omit it (comment it out)?

Note that records are only mentioned here in the appendix, they do not occur in the subtype rules figure.

eernstg · 2024-10-18T12:37:29Z

specification/dartLangSpec.tex

+\item
+  If $T_0$ is \code{($V_0$, \ldots, $V_n$, \{$V_{n+1} d_{n+1}$, \ldots, $V_m d_m$\})}
+  and $T_1$ is \code{($S_0$, \ldots, $S_n$, \{$S_{n+1} d_{n+1}$, \ldots, $S_m d_m$\})}
+  then \SubtypeNE{T_0}{T_1} if{}f \SubtypeNE{V_i}{S_i} for each $i \in 0 .. m$.  


Again a record type: Could be commented out for now.

eernstg · 2024-10-18T14:10:47Z

specification/dartLangSpec.tex

+    then the subtyping does not hold
+    (\commentary{%
+      i.e., the result of the subtyping query is known to be false%
+    }).


Like a few other rules, I believe 'Right Object' is admissible, but not required.

eernstg · 2024-10-21T11:25:55Z

I tried to use latexdiff to generate a PDF that shows the differences, but it doesn't handle "non-standard" LaTeX (which seems to be difficult to avoid). I can generate a PDF that shows some differences and stops at page 232, but it would take some more experimentation to produce something that shows the differences in a way that can be relied upon.

eernstg · 2024-11-01T17:39:50Z

I added a section about 'being the same type', and adjusted the text such that the thing previously known as 'canonical syntax' (now renamed to 'explicitly resolved syntax') is encapsulated in this section. Also, alpha equivalence has been made part of this 'being the same type' section.

eernstg force-pushed the specify_null_safety_subtyping_dec23 branch from 082c391 to a9f4886 Compare December 18, 2023 13:27

lrhn reviewed Dec 22, 2023

View reviewed changes

eernstg force-pushed the specify_null_safety_subtyping_dec23 branch from a9f4886 to 0fd9980 Compare February 9, 2024 13:53

eernstg force-pushed the specify_null_safety_subtyping_dec23 branch from 0fd9980 to 84e6d38 Compare August 13, 2024 17:18

eernstg force-pushed the specify_null_safety_subtyping_dec23 branch from 84e6d38 to 4fcf76e Compare September 2, 2024 16:13

eernstg force-pushed the specify_null_safety_subtyping_dec23 branch from 4fcf76e to b7cdb30 Compare September 23, 2024 09:56

eernstg force-pushed the specify_null_safety_subtyping_dec23 branch from b7cdb30 to bf98431 Compare October 11, 2024 13:38

eernstg requested a review from leafpetersen October 18, 2024 10:32

eernstg commented Oct 18, 2024

View reviewed changes

eernstg force-pushed the specify_null_safety_subtyping_dec23 branch from f28e000 to 54323ec Compare November 25, 2024 09:51

eernstg added 16 commits November 28, 2024 10:30

Integrate the null-safety subtyping rules into dartLangSpec.tex

ed1877b

Integrated null-safety into the appendix about subtyping

d04bf85

Fix a couple of typos

437ba96

Adjust dart.sty to change like specify_null_safety_sep21

7190129

WIP

2593067

Align this PR with specify_null_safety_sep21

bd830c5

WIP

c803490

WIP

e4153a0

WIP

7b5151f

WIP

1a5c146

WIP

c2bf4d9

WIP

3f40931

WIP

eaa61d5

WIP

1e3ffdc

WIP

698d8bd

WIP

64988c0

eernstg added 5 commits November 28, 2024 10:30

WIP

c070392

WIP

3732473

WIP

b9dd85c

WIP

ba4f777

Added section about explicitly resolved (fka canonical) syntax

d02466b

eernstg force-pushed the specify_null_safety_subtyping_dec23 branch from 54323ec to d02466b Compare November 28, 2024 09:30

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Specify null safety subtyping #3515

Specify null safety subtyping #3515

eernstg commented Dec 14, 2023

lrhn left a comment

lrhn Dec 22, 2023

eernstg commented Oct 17, 2024

eernstg commented Oct 18, 2024 •

edited

Loading

eernstg Oct 18, 2024

eernstg Oct 18, 2024

eernstg Oct 18, 2024

eernstg Oct 18, 2024

eernstg Oct 18, 2024

eernstg Oct 18, 2024

eernstg Oct 18, 2024

eernstg commented Oct 21, 2024

eernstg commented Nov 1, 2024 •

edited

Loading

Specify null safety subtyping #3515

Are you sure you want to change the base?

Specify null safety subtyping #3515

Conversation

eernstg commented Dec 14, 2023

lrhn left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eernstg commented Oct 17, 2024

eernstg commented Oct 18, 2024 • edited Loading

Front matter

@@ -21633,128 +21631,188 @@

@@ -22482,7 +22498,7 @@

@@ -23324,156 +23324,238 @@

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eernstg commented Oct 21, 2024

eernstg commented Nov 1, 2024 • edited Loading

eernstg commented Oct 18, 2024 •

edited

Loading

eernstg commented Nov 1, 2024 •

edited

Loading