Update pre-null-safety spec with new null safety sections

[eernstg]

This PR was created by deleting the sections from Subtypes to (but not including) Reference plus the appendix Algorithmic Subtyping, and inserting the section Subtypes from the null safety update branch plus all the following sections until (but not including) Reference, plus the new version of the appendix Algorithmic Subtyping.

The point is that this PR introduces a large chunk of the new material related to null safety which is introduced into the language specification, and it does not include all the small changes to sections that are mostly the same as before (those changes will be submitted as other PRs later on). In other words, the text before Subtyping is unchanged (apart from the fixes mentioned below), and references from the new material to any location before Subtyping may thus very well refer to obsolete language.

A couple of other updates were necessary in order to make the result LaTeX'able:

• dart.sty was updated to be the version used with the null safety PR (the new version includes a number of declarations that are used by the material about null safety).
• dartLangSpec.tex was updated to use \Delta rather than \Gamma to denote a type variable environment (that's the common notation; we previously used \Gamma, but that's typically a "term" variable environment, so \Delta would be less confusing for readers who also read research papers involving type systems).
• \RawFunctionTypeNamed was updated to allow for the required modifier; a couple of changes were necessary in sections before Subtyping in order to make dartLangSpec.tex LaTeX'able again, but this only involved adding the new LaTeX macro argument {r}, further updates will take place later on (this update just updates stuff from Subtyping and out).
• The symbol used to indicate that a word or phrase is being defined was changed from \diamond to \triangle, because \triangle is now also used over = in order to indicate that a certain term of the form A = B defines A.
• Compile-time errors are now also indicated in the margin (using an \ominus symbol, similar to the symbolic traffic sign meaning "No entrance"), this symbol is used in the new material, that is, nowhere before section Subtyping; for instance, it occurs in section Type Null.

Unfortunately, the diff algorithm in git (and, probably, almost any diff algorithm) does not quite understand that the operation performed here is "delete two big chunks of text and insert replacements that are mostly new material", but it does seem to get on track after a while.

[eernstg]

An update fixing a few issues with interface types is on the way, will upload in half an hour, approx. ;-)

[eernstg]

Done.

[github-actions]

Visit the preview URL for this PR (updated for commit 6cd9296):

https://dart-specification--pr2023-specify-null-safety-56htdccy.web.app

_{(expires Mon, 11 Jul 2022 14:42:40 GMT)}

_{🔥 via Firebase Hosting GitHub Action 🌎}

_{Sign: 6941ecd630c4f067ff3d02708a45ae0f0a42b88a}

[chloestefantsova]

I skimmed over the changes and created the following checklist. I plan to review the text in parts and cross them out here when I'm done. The checklist itself may change in the future in case I missed anything.

• Subtype algorithm.
  • Rules of inference.
  • Subsequent commentary.
• Type nullability.
• Top merge.
• IsTopType.
• Moretop, morebottom.
• Type normalization.
• Canonical syntax of types.
• Standard bounds.
• Closures of types.
• Specific kinds of types
  • Types bounded by types.
  • Class building types.
  • Interface types.
  • Intersection types.
  • Never.
  • Null.
  • Type.
  • Function.
  • dynamic.
• Type inference.
  • Flow analysis.
  • Type promotion.
• Appendix. Algorithmic subtyping.

[chloestefantsova]

I checked the part "Rules of Inference", in the green "after" column the lines range from 20728 to 20889. It looks good to me.

EDIT: In my review I assumed that the requirement for the bounds of two function types is to be in the mutual-subtypes relationship. After a conversation with Erik I realized that the spec needs to be updated to mean that.

[chloestefantsova]

I reviewed the part "Subsequent commentary" to the subtype algorithm, in the green "after" column the lines range from 20889 to 21291. I have two drive-by questions to the surrounding text. Otherwise, the part LGTM.

[chloestefantsova]

I checked the part "Type Nullability", in the green "after" column the lines range from 21291 to 21414. I have left some comments, but otherwise LGTM.

[chloestefantsova]

I checked the part "Top merge", in the green "after" column the lines range from 21414 to 21494. LGTM with one comment.

[chloestefantsova]

I checked the part "IsTopType", in the green "after" column the lines range from 21494 to 21539. It LGTM.

[chloestefantsova]

I checked the part "Moretop, morebottom", in the green "after" column the lines range from 21539 to 21582. LGTM.

[chloestefantsova]

I checked the part "Type normalization", in the green "after" column the lines range from 21582 to 21737. LGTM with one question.

[chloestefantsova]

I checked the part "Canonical syntax of types", in the green "after" column the lines range from 21737 to 21931. LGTM.

[chloestefantsova]

As I understand it, with the exception of a top type?

[eernstg]

This particular sentence refers to the real, mathematical least upper bound in a set (Dart types) with an ordering relation (subtyping). The usage of 'least upper bound' in older versions of the spec is misleading, because it was never a least upper bound.

So we're looking for a type which is a supertype of both A and B, and it must be the least element among all the types which are supertypes of both A and B. It can't be I because we don't have I <: J; similarly it can't be J. But it also can't be a top type, because we don't have Top <: I (or J, or a bunch of other types).

So I think the claim is correct.

[chloestefantsova]

But it also can't be a top type, because we don't have Top <: I (or J, or a bunch of other types).

I don't think I understand this argument. Shouldn't we have I <: Top and J <: Top (in the reverse order) in order to claim Top as the upper bound for both I and J?

Additionally, I think declarations class I {} and class J {} imply class I extends Object {} respectively class J extends Object {}, which makes Object an upper bound for A and B.

[eernstg]

True, Object is an upper bound for each of those classes, but that makes no difference: The least upper bound (mathematically speaking) of a set S of elements in an ordered set {v1, .. vk} is an element v from S that satisfies (1) vj <: v, for all j, and (v1 <: other && .. && vk <: other) => v <: other. It's the latter part that fails, so Top and Object aren't 'least', they are just upper bounds.

[eernstg]

The PR was rebased on the current master, that is, 3e99947.