Spec: Rewrite the type system fundamentals. #17447

sjrd · 2023-05-09T16:09:14Z

There are two fundamental differences between the type sytems of Scala 2 and 3, which made a fundamental rewrite desirable:

Scala 2 defines path-dependent types in terms of type projections, whereas Scala 3 is path-dependent first, and has not general type projects.
Scala 2 has ad hoc higher-kinded type parameters and polymorphic type aliases, whereas Scala 3 has first-class type lambdas and is fundamentally higher kinded.

We therefore rewrite the entire type system section of the spec to be higher-kinded and path-dependent first. In the process, we also revise refined types to better fit the path-dependent nature.

I (sjrd) took the liberty to add myself as a contributor in the index page of the spec, as I believe this constitutes a fundamental contribution to the language specification.

The rendered version of the Types chapter can be seen here:
~~Types Scala 3.pdf~~ (old version)
Types Scala 3.pdf

There are two fundamental differences between the type sytems of Scala 2 and 3, which made a fundamental rewrite desirable: - Scala 2 defines path-dependent types in terms of type projections, whereas Scala 3 is path-dependent first, and has not general type projects. - Scala 2 has ad hod higher-kinded type parameters and polymorphic type aliases, whereas Scala 3 has first-class type lambdas and is fundamentally higher order. We therefore rewrite the entire type system section of the spec to be higher-kinded and path-dependent first. In the process, we also revise refined types to better fit the path-dependent nature. I (sjrd) took the liberty to add myself as a contributor in the index page of the spec, as I believe this constitutes a fundamental contribution to the language specification.

And better define what a "type definition" is.

To align with the rest of the spec, which is syntax-first.

sjrd · 2023-05-30T10:00:48Z

@odersky I have updated the spec according to what we discussed last week. In particular, its starts with the concrete syntax of types now, and the desugaring of type lambdas and refined types is more explicit.

odersky

I like the new structure. It's a great improvement to what we had before.

odersky · 2023-05-24T10:28:17Z

docs/_spec/03-types.md

-## Paths
+In this specification, we specify and use types in terms of the following _abstract syntax_.
+The abstract syntax does not directly correspond to concrete syntax.
+It abstracts away irrelevant details such as precedence and grouping, and contains shapes of types that cannot be directly expressed using the concrete syntax.


Suggestion: Mark shapes that cannot be expressed in syntax specially (maybe in Italics? or else in a comment at the line's end.)

odersky · 2023-05-24T10:32:18Z

docs/_spec/03-types.md

+
+### Type Constructors
+
+To each type constructor corresponds an _inferred type parameter clause_ which is computed as follow:


Suggested change

To each type constructor corresponds an _inferred type parameter clause_ which is computed as follow:

To each type constructor corresponds an _inferred type parameter clause_ which is computed as follows:

odersky · 2023-05-25T14:21:33Z

docs/_spec/03-types.md

+```ebnf
+Type              ::=  FunctionArgTypes ‘=>’ Type
+FunctionArgTypes  ::=  InfixType
+                    |  ‘(’ [ ParamType {‘,’ ParamType } ] ‘)’


Dependent function types are missing here. The reference syntax is actually:

FunTypeArgs ::= InfixType | ‘(’ [ FunArgTypes ] ‘)’ | FunParamClause FunParamClause ::= ‘(’ TypedFunParam {‘,’ TypedFunParam } ‘)’ TypedFunParam ::= id ‘:’ Type

odersky · 2023-06-05T10:53:10Z

docs/_spec/03-types.md

+                        |  TypeLambdaParams '=>' Type
+FunctionArgTypes      ::=  InfixType
+                        |  ‘(’ [ FunArgTypes ] ‘)’
+                        |  FunParamClause


FunParamClause is not further explained. We need to explain that , e.g.

(x: T) => x.M

expands to

Function1[T, U] { def apply(x: T): x.M }

assuming that U is the least supertype of x.M that does not mention x.

Aside: This encoding might change. We'd really like it to be something like

DependentFunction1 { def apply(x: T): x.M }

instead.

odersky · 2023-06-05T10:54:41Z

docs/_spec/03-types.md

-SimpleType  ::=  Path ‘.’ ‘type’
+Type              ::=  FunctionArgTypes ‘=>’ Type
+FunctionArgTypes  ::=  InfixType
+                    |  ‘(’ [ ParamType {‘,’ ParamType } ] ‘)’


The syntax summary gives a different expansion for FunctionArgTypes. These need to be aligned.

odersky · 2023-06-06T10:30:51Z

docs/_spec/03-types.md

+- Otherwise, if either ´M_1´ or ´M_2´ is a class result, the result is that one.
+- Otherwise, ´M_1´ and ´M_2´ must either both be term results or both be type results.
+  - If they are term results with underlying types ´U_1´ and ´U_2´ and stable flags ´s_1´ and ´s_2´, the result is a term result whose underlying type is `meet(´U_1´, ´U_2´)` and whose stable flag is ´s_1 \lor s_2´.
+  - If they are type results with underlying type definitions ´D_1´ and ´D_2´, the result is a type result whose underlying type definition is `intersect(´D_1´, ´D_2´)`.

 ## Relations between types


Equivalence meaning "interchangeable in all contexts" is prone to mislead. Also because of its triple equals sign. It's definitely not structural equivalence. So in the table below I would put conformance first, and then define equivalence as mutual conformance. Also, if possible use another symbol like =:= or and = with a ~ on top.

odersky · 2023-06-06T11:30:09Z

docs/_spec/03-types.md

+      - ´\sigma (>: M_i <: G_i)´ is contained in ´>: L_i <: H_i´ (i.e., ´L_i <: \sigma M_i´ and ´\sigma G_i <: H_i´).
+- ´S = p.X´ and `´T = [\pm b_1 >: M_1 <: G_1, ..., \pm b_n >: M_n <: G_n]´ =>> ´T_1´` and ´S´ is a type constructor with ´n´ type parameters and:
+  - `´([\pm a_1 >: L_1 <: H_1, ..., \pm a_n >: L_n <: H_n]´ =>> ´S[a_1, ..., a_n]) <: T´` where the ´a_i´ are copies of the type parameters of ´S´ (i.e., we can eta-expand ´S´ to compare it to a type lambda).
+- `´T = T_1´ { ´R´ }` and ´S <: T´ and ´S´ is a stable type ´p´ (TODO: what if it is not stable?) and:


I think we solve that by skolemization. What happens is that we compute the member type of R in T_1. That goes through an asSeenFrom. The asSeenFrom will skolemize when we have to replace a C.this type with a non-stable prefix. So maybe we should add that case to the definition of asSeenFrom.

Compare with the treatment of QualSkolemType in TypeOps.asSeenFrom.

odersky · 2023-06-06T11:31:42Z

docs/_spec/03-types.md

+  - ´p´ is ´S´ if ´S´ is a stable type and ´∃ \alpha : S´ otherwise, and
+  - ´p'´ is the result of replacing any top-level recursive type `{ ´\gamma´ => ´Z´ }` in ´p´ with ´[\gamma := p]Z´ (TODO specify this better).
+- `´S = (´=> ´S_1)´` and `´T = (´=> ´T_1)´` and ´S_1 <: T_1´.
+- `´S =´ scala.Null` and:


I think it would be good to also say what happens under -YexplicitNulls here.

odersky · 2023-06-06T11:37:04Z

docs/_spec/03-types.md

+
+We define `matches(´S´, ´T´)` where ´S´ and ´T´ are types or methodic types as:
+
+<!-- TODO We should mention parameter substitution here. -->


Yes, we should do that.

odersky · 2023-06-06T11:38:24Z

docs/_spec/03-types.md

- A type alias `type ´t´[´T_1´, ..., ´T_n´] = ´T´` subsumes a type alias `type ´t´[´T_1´, ..., ´T_n´] = ´T'´` if ´T \equiv T'´.
- A type declaration `type ´t´[´T_1´, ..., ´T_n´] >: ´L´ <: ´U´` subsumes a type declaration `type ´t´[´T_1´, ..., ´T_n´] >: ´L'´ <: ´U'´` if ´L' <: L´ and ´U <: U'´.
- A type or class definition that binds a type name ´t´ subsumes an abstract type declaration `type t[´T_1´, ..., ´T_n´] >: L <: U` if ´L <: t <: U´.
-


Further below: I think we should drop the "Weak Conformance" section 3.6.3. Then in 3.6.4 we should refer to numeric widening as an implicit conversion.

The section on Volatile types should be dropped. It is replaced by a notion of realizability.

The section on Erasure should be updated to the new rules.

Generally, all usages of compound types (using with) should be dropped.

Weak conformance will be the subject of a separate PR that introduces harmonization, so I would rather not touch it now.

I updated erasure. For the volatile types I'll have to investigate how realizability affects that section.

odersky

I like the new structure. It's a great improvement to what we had before.

sjrd · 2023-06-06T15:36:34Z

I think I have addressed everything so far except the Volatile Types -> Realizable comment.

sjrd · 2023-06-07T08:32:20Z

Volatility now replaced by realizability as well. (also updated the PDF)

odersky

Looks all good now.

[Cherry-picked 8e65a2c] [Cherry-picked 978d4e4] [Cherry-picked 6f21d93] [Cherry-picked 8657620] [Cherry-picked 6021b7b] [Cherry-picked a99f0b6] [Cherry-picked 254f23e]

Backports #17447 to the LTS branch. This PR was initially erroneously skipped. It also includes changes form #17940. [skip ci]

sjrd requested a review from odersky May 9, 2023 16:09

sjrd assigned odersky May 9, 2023

sjrd added 5 commits May 30, 2023 11:16

Spec tweak: redefine designator types in terms of memberType.

978d4e4

And better define what a "type definition" is.

Spec: Specify the desugaring of concrete refined types.

6f21d93

Move the concrete syntax of types to the beginning.

8657620

To align with the rest of the spec, which is syntax-first.

Make it clear that variance in concrete type lambdas are inferred.

6021b7b

sjrd force-pushed the spec-type-system-fundamentals branch from d7ea469 to 6021b7b Compare May 30, 2023 09:58

odersky requested changes Jun 6, 2023

View reviewed changes

odersky assigned sjrd and unassigned odersky Jun 6, 2023

Spec: Address review comments except volatility.

a99f0b6

Spec: Replace volatility of types by the realizability concept.

254f23e

sjrd requested a review from odersky June 7, 2023 08:32

sjrd assigned odersky and unassigned sjrd Jun 7, 2023

odersky approved these changes Jun 7, 2023

View reviewed changes

odersky assigned sjrd and unassigned odersky Jun 7, 2023

sjrd merged commit 482dfeb into scala:main Jun 7, 2023

sjrd deleted the spec-type-system-fundamentals branch June 7, 2023 12:35

Kordyjan added a commit that referenced this pull request Nov 23, 2023

Backports #17447 to lts

27ab06e

[Cherry-picked 8e65a2c] [Cherry-picked 978d4e4] [Cherry-picked 6f21d93] [Cherry-picked 8657620] [Cherry-picked 6021b7b] [Cherry-picked a99f0b6] [Cherry-picked 254f23e]

Kordyjan mentioned this pull request Nov 23, 2023

Backport "Spec: Rewrite the type system fundamentals." to LTS #19034

Merged

Kordyjan added a commit that referenced this pull request Nov 29, 2023

Backports #17447 to lts

6368622

[Cherry-picked 8e65a2c] [Cherry-picked 978d4e4] [Cherry-picked 6f21d93] [Cherry-picked 8657620] [Cherry-picked 6021b7b] [Cherry-picked a99f0b6] [Cherry-picked 254f23e]

Kordyjan added a commit that referenced this pull request Dec 8, 2023

Backport "Spec: Rewrite the type system fundamentals." to LTS (#19034)

a04b90f

Backports #17447 to the LTS branch. This PR was initially erroneously skipped. It also includes changes form #17940. [skip ci]

Kordyjan added this to the 3.3.2 milestone Dec 14, 2023


		### Type Constructors

		To each type constructor corresponds an _inferred type parameter clause_ which is computed as follow:


		We define `matches(´S´, ´T´)` where ´S´ and ´T´ are types or methodic types as:

		<!-- TODO We should mention parameter substitution here. -->

Spec: Rewrite the type system fundamentals. #17447

Spec: Rewrite the type system fundamentals. #17447

Uh oh!

Conversation

sjrd commented May 9, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sjrd commented May 30, 2023

Uh oh!

odersky left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

odersky left a comment

Choose a reason for hiding this comment

Uh oh!

sjrd commented Jun 6, 2023

Uh oh!

sjrd commented Jun 7, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

odersky left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

sjrd commented May 9, 2023 •

edited

Loading

sjrd commented Jun 7, 2023 •

edited

Loading