From 164dc1d5753ab8460b690228ebb01c09c281c5aa Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Fri, 3 Dec 2021 11:36:58 -0600 Subject: [PATCH 1/5] Fix an unsoundness issue around stripping optional properties --- rfcs/unsealed-table-literals.md | 74 +++++++++++++++++++ ...le-subtyping-strips-optional-properties.md | 66 +++++++++++++++++ 2 files changed, 140 insertions(+) create mode 100644 rfcs/unsealed-table-literals.md create mode 100644 rfcs/unsealed-table-subtyping-strips-optional-properties.md diff --git a/rfcs/unsealed-table-literals.md b/rfcs/unsealed-table-literals.md new file mode 100644 index 000000000..970aefd25 --- /dev/null +++ b/rfcs/unsealed-table-literals.md @@ -0,0 +1,74 @@ +# Unsealed table literals + +## Summary + +Currently the only way to create an unsealed table is as an empty table literal `{}`. +This RFC proposes making all table literals unsealed. + +## Motivation + +Table types can be *sealed* or *unsealed*. These are different in that: + +* Unsealed table types are *precise*: if a table has unsealed type `{ p: number, q: string }` + then it is guaranteed to have only properties `p` and `q`. + +* Sealed tables support *width subtyping*: if a table has sealed type `{ p: number }` + then it is guaranteed to have at least property `p`, so we allow `{ p: number, q: string }` + to be treated as a subtype of `{ p: number }` + +* Unsealed tables can have properties added to them: if `t` has unsealed type + `{ p: number }` then after the assignment `t.q = "hi"`, `t`'s type is updated to be + `{ p: number, q: string }`. + +* Unsealed tables are subtypes of sealed tables. + +Currently the only way to create an unsealed table is using an empty table literal, so +```lua + local t = {} + t.p = 5 + t.q = "hi" +``` +typechecks, but +```lua + local t = { p = 5 } + t.q = "hi" +``` +does not. + +This causes problems in examples, for example +```lua + local t : { p: number, q: string? } = { p = 5, q = "hi" } + t = { p = 7 } +``` +typechecks because we allow subtyping to strip away optional +properties, so `{ p : number }` is a subtype of +`{ p : number, q : string? }`. Unfortunately this is not sound, +since sealed tables support width subtyping: +```lua + local t : { p: number, q: string? } = { p = 5, q = "hi" } + local u : { p: number } = { p = 5, q = false } + t = u +``` + +## Design + +The fix for this source of unsoundness is twofold: + +1. make all table literals unsealed, and +2. only allow stripping optional properties from when the + supertype is sealed and the subtype is unsealed. + +This RFC is for (1). There is a [separate RFC](unsealed-table-subtyping-strips-optional-properties.md) for (2). + +## Drawbacks + +Making all table literals unsealed is a conservative change, it only removes type errors. + +It does encourage developers to add new properties to tables during initialization, which +may be considered poor style. + +## Alternatives + +We could introduce a new table state for unsealed-but-precise +tables. The trade-off is that that would be more precise, at the cost +of adding user-visible complexity to the type system. diff --git a/rfcs/unsealed-table-subtyping-strips-optional-properties.md b/rfcs/unsealed-table-subtyping-strips-optional-properties.md new file mode 100644 index 000000000..deecfdb3a --- /dev/null +++ b/rfcs/unsealed-table-subtyping-strips-optional-properties.md @@ -0,0 +1,66 @@ +# Only strip optional properties from unsealed tables during subtyping + +## Summary + +Currently subtyping allows optional properties to be stripped from table types during subtyping. +This RFC proposes only allowing that when the subtype is unsealed and the supertype is sealed. + +## Motivation + +Table types can be *sealed* or *unsealed*. These are different in that: + +* Unsealed table types are *precise*: if a table has unsealed type `{ p: number, q: string }` + then it is guaranteed to have only properties `p` and `q`. + +* Sealed tables support *width subtyping*: if a table has sealed type `{ p: number }` + then it is guaranteed to have at least property `p`, so we allow `{ p: number, q: string }` + to be treated as a subtype of `{ p: number }` + +* Unsealed tables can have properties added to them: if `t` has unsealed type + `{ p: number }` then after the assignment `t.q = "hi"`, `t`'s type is updated to be + `{ p: number, q: string }`. + +* Unsealed tables are subtypes of sealed tables. + +Currently we allow subtyping to strip away optional fields +as long as the supertype is sealed. +This is necessary for examples, for instance: +```lua + local t : { p: number, q: string? } = { p = 5, q = "hi" } + t = { p = 7 } +``` +typechecks because `{ p : number }` is a subtype of +`{ p : number, q : string? }`. Unfortunately this is not sound, +since sealed tables support width subtyping: +```lua + local t : { p: number, q: string? } = { p = 5, q = "hi" } + local u : { p: number } = { p = 5, q = false } + t = u +``` + +## Design + +The fix for this source of unsoundness is twofold: + +1. make all table literals unsealed, and +2. only allow stripping optional properties from when the + supertype is sealed and the subtype is unsealed. + +This RFC is for (2). There is a [separate RFC](unsealed-table-literals.md) for (1). + +## Drawbacks + +This introduces new type errors (it has to, since it is fixing a source of +unsoundness). This means that there are now false positives such as: +```lua + local t : { p: number, q: string? } = { p = 5, q = "hi" } + local u : { p: number } = { p = 5, q = "lo" } + t = u +``` +These false positives are so similar to sources of unsoundness +that it is difficult to see how to allow them soundly. + +## Alternatives + +We could just live with unsoundness. + From c9c1a53e688af47e859873e5394bb9a6109d1ae3 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Mon, 6 Dec 2021 12:23:01 -0600 Subject: [PATCH 2/5] Wordsmithing --- rfcs/unsealed-table-literals.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rfcs/unsealed-table-literals.md b/rfcs/unsealed-table-literals.md index 970aefd25..da6e7db16 100644 --- a/rfcs/unsealed-table-literals.md +++ b/rfcs/unsealed-table-literals.md @@ -35,7 +35,7 @@ typechecks, but ``` does not. -This causes problems in examples, for example +This causes problems in examples, for instance ```lua local t : { p: number, q: string? } = { p = 5, q = "hi" } t = { p = 7 } From 9472479666528395eaedee4459a5769f17f8cf39 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Tue, 4 Jan 2022 16:03:24 -0600 Subject: [PATCH 3/5] Responding to review comments --- rfcs/unsealed-table-literals.md | 32 +++++++++++++------------------- 1 file changed, 13 insertions(+), 19 deletions(-) diff --git a/rfcs/unsealed-table-literals.md b/rfcs/unsealed-table-literals.md index da6e7db16..f220f632a 100644 --- a/rfcs/unsealed-table-literals.md +++ b/rfcs/unsealed-table-literals.md @@ -35,30 +35,16 @@ typechecks, but ``` does not. -This causes problems in examples, for instance +This causes problems in examples, in particular developers +may initialize properties but not methods: ```lua - local t : { p: number, q: string? } = { p = 5, q = "hi" } - t = { p = 7 } -``` -typechecks because we allow subtyping to strip away optional -properties, so `{ p : number }` is a subtype of -`{ p : number, q : string? }`. Unfortunately this is not sound, -since sealed tables support width subtyping: -```lua - local t : { p: number, q: string? } = { p = 5, q = "hi" } - local u : { p: number } = { p = 5, q = false } - t = u + local t = { p = 5 } + function t.f() return t.p end ``` ## Design -The fix for this source of unsoundness is twofold: - -1. make all table literals unsealed, and -2. only allow stripping optional properties from when the - supertype is sealed and the subtype is unsealed. - -This RFC is for (1). There is a [separate RFC](unsealed-table-subtyping-strips-optional-properties.md) for (2). +The proposed change is straightforward: make all table literals unsealed. ## Drawbacks @@ -67,6 +53,14 @@ Making all table literals unsealed is a conservative change, it only removes typ It does encourage developers to add new properties to tables during initialization, which may be considered poor style. +It does mean that some spelling mistakes will not be caught, for example +```lua +local t = {x = 1, y = 2} +if foo then + t.z = 3 -- is z a typo or intentional 2-vs-3 choice? +end +``` + ## Alternatives We could introduce a new table state for unsealed-but-precise From 8d3f485d14fae38898530b4680afe9cfbbfdfae5 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Wed, 5 Jan 2022 12:00:46 -0600 Subject: [PATCH 4/5] Added discussion of array-like tables --- rfcs/unsealed-table-literals.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/rfcs/unsealed-table-literals.md b/rfcs/unsealed-table-literals.md index f220f632a..3a3365fc6 100644 --- a/rfcs/unsealed-table-literals.md +++ b/rfcs/unsealed-table-literals.md @@ -61,8 +61,16 @@ if foo then end ``` +In particular, we no longer warn about adding properties to array-like tables. +```lua +local a = {1,2,3} +a.p = 5 +``` + ## Alternatives We could introduce a new table state for unsealed-but-precise tables. The trade-off is that that would be more precise, at the cost of adding user-visible complexity to the type system. + +We could contine to treat array-like tables as sealed. \ No newline at end of file From 9392a3cc38c538ff4140553ac08891f3ea7f5688 Mon Sep 17 00:00:00 2001 From: Alan Jeffrey <403333+asajeffrey@users.noreply.github.com> Date: Thu, 6 Jan 2022 12:47:44 -0600 Subject: [PATCH 5/5] Update rfcs/unsealed-table-literals.md Co-authored-by: vegorov-rbx <75688451+vegorov-rbx@users.noreply.github.com> --- rfcs/unsealed-table-literals.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rfcs/unsealed-table-literals.md b/rfcs/unsealed-table-literals.md index 3a3365fc6..320bf7ca9 100644 --- a/rfcs/unsealed-table-literals.md +++ b/rfcs/unsealed-table-literals.md @@ -73,4 +73,4 @@ We could introduce a new table state for unsealed-but-precise tables. The trade-off is that that would be more precise, at the cost of adding user-visible complexity to the type system. -We could contine to treat array-like tables as sealed. \ No newline at end of file +We could continue to treat array-like tables as sealed. \ No newline at end of file