mirror of
https://github.com/luau-lang/luau.git
synced 2024-12-13 13:30:40 +00:00
RFC: Fix an unsoundness issue around stripping optional properties (#276)
* Fix an unsoundness issue around stripping optional properties Co-authored-by: vegorov-rbx <75688451+vegorov-rbx@users.noreply.github.com>
This commit is contained in:
parent
73b7bcb2da
commit
82587bef29
2 changed files with 142 additions and 0 deletions
76
rfcs/unsealed-table-literals.md
Normal file
76
rfcs/unsealed-table-literals.md
Normal file
|
@ -0,0 +1,76 @@
|
||||||
|
# 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, in particular developers
|
||||||
|
may initialize properties but not methods:
|
||||||
|
```lua
|
||||||
|
local t = { p = 5 }
|
||||||
|
function t.f() return t.p end
|
||||||
|
```
|
||||||
|
|
||||||
|
## Design
|
||||||
|
|
||||||
|
The proposed change is straightforward: make all table literals unsealed.
|
||||||
|
|
||||||
|
## 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.
|
||||||
|
|
||||||
|
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
|
||||||
|
```
|
||||||
|
|
||||||
|
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 continue to treat array-like tables as sealed.
|
66
rfcs/unsealed-table-subtyping-strips-optional-properties.md
Normal file
66
rfcs/unsealed-table-subtyping-strips-optional-properties.md
Normal file
|
@ -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.
|
||||||
|
|
Loading…
Reference in a new issue