diff --git a/rfcs/unsealed-table-literals.md b/rfcs/unsealed-table-literals.md new file mode 100644 index 00000000..320bf7ca --- /dev/null +++ b/rfcs/unsealed-table-literals.md @@ -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. \ No newline at end of file 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 00000000..deecfdb3 --- /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. +