-
Notifications
You must be signed in to change notification settings - Fork 341
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Co-authored-by: vegorov-rbx <75688451+vegorov-rbx@users.noreply.github.com>
- Loading branch information
1 parent
f3a248d
commit 59c0492
Showing
1 changed file
with
179 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,179 @@ | ||
# Write-only properties | ||
|
||
## Summary | ||
|
||
Allow properties of classes and tables to be inferred as write-only. | ||
|
||
## Motivation | ||
|
||
This RFC is a follow-on to supporting read-only properties. | ||
|
||
Read-only properties have many obvious use-cases, but write-only properties | ||
are more technical. | ||
|
||
The reason for wanting write-only properties is that it means | ||
that we can infer a most specific type for functions, which we can't do if | ||
we only have read-write and read-only properties. | ||
|
||
For example, consider the function | ||
```lua | ||
function f(t) t.p = Dog.new() end | ||
``` | ||
|
||
The obvious type for this is | ||
```lua | ||
f : ({ p: Dog }) -> () | ||
``` | ||
|
||
but this is not the most specific type, since read-write properties | ||
are invariant, We could have inferred `f : ({ p: Animal }) -> ()`. | ||
These types are incomparable (neither is a subtype of the other) | ||
and there are uses of `f` that fail to typecheck depending which one choose. | ||
|
||
If `f : ({ p: Dog }) -> ()` then | ||
```lua | ||
local x : { p : Animal } = { p = Cat.new() } | ||
f(x) -- Fails to typecheck | ||
``` | ||
|
||
If `f : ({ p: Animal }) -> ()` then | ||
```lua | ||
local x : { p : Dog } = { p = Dog.new() } | ||
f(x) -- Fails to typecheck | ||
``` | ||
|
||
The reason for these failures is that neither of these is the most | ||
specific type. It is one which includes that `t.p` is written to, and | ||
not read from. | ||
```lua | ||
f : ({ set p: Dog }) -> () | ||
``` | ||
|
||
This allows both example uses of `f` to typecheck. To see that it is more specific than `({ p: Animal }) -> ()`: | ||
|
||
* `Dog` is a subtype of `Animal` | ||
* so (since write-only properties are contravariant) `{ set p: Dog }` is a supertype of `{ set p: Animal }` | ||
* and (since read-write properties are a subtype of write-only properties) `{ set p: Animal }` is a supertype of `{ p: Animal }` | ||
* so (by transitivity) `{ set p: Dog }` is a supertype of `{ set p: Animal }` is a supertype of `{ p: Animal }` | ||
* so (since function arguments are contravariant `({ set p: Dog }) -> ()` is a subtype of `({ p: Animal }) -> ()` | ||
|
||
and similarly `({ set p: Dog }) -> ()` is a subtype of `({ p: Dog }) -> ()`. | ||
|
||
Local type inference depends on the existence of most specific (and most general) types, | ||
so if we want to use it "off the shelf" we will need write-only properties. | ||
|
||
There are also some security reasons why properties should be | ||
write-only. If `t` is a shared table, and any security domain can | ||
write to `t.p`, then it may be possible to use this as a back-channel | ||
if `t.p` is readable. If there is a dynamic check that a property is | ||
write-only then we may wish to present a script analysis error if a | ||
user tries reading it. | ||
|
||
## Design | ||
|
||
### Properties | ||
|
||
Add a modifier to table properties indicating that they are write-only. | ||
|
||
This proposal is not about syntax, but it will be useful for examples to have some. Write: | ||
|
||
* `set p: T` for a write-only property of type `T`. | ||
|
||
For example: | ||
```lua | ||
function f(t) | ||
t.p = 1 + t.q | ||
end | ||
``` | ||
has inferred type: | ||
``` | ||
f: (t: { set p: number, get q: number }) -> () | ||
``` | ||
indicating that `p` is used write-only but `q` is used read-only. | ||
|
||
### Adding read-only and write-only properties | ||
|
||
There are various points where type inference adds properties to types, we now have to consider how to treat each of these. | ||
|
||
When reading a property from a free table, we should add a read-only | ||
property if there is no such property already. If there is already a | ||
write-only property, we should make it read-write. | ||
|
||
When writing a property to a free table, we should add a write-only | ||
property if there is no such property already. If there is already a | ||
read-only property, we should make it read-write. | ||
|
||
When writing a property to an unsealed table, we should add a read-write | ||
property if there is no such property already. | ||
|
||
When declaring a method in a table or class, we should add a read-only property for the method. | ||
|
||
### Subtyping | ||
|
||
Write-only properties are contravariant: | ||
|
||
* If `T` is a subtype of `U` then `{ set p: U }` is a subtype of `{ set p: T }`. | ||
|
||
Read-write properties are a subtype of write-only properties: | ||
|
||
* If `T` is a subtype of `U` then `{ p: U }` is a subtype of `{ set p: T }`. | ||
|
||
### Indexers | ||
|
||
Indexers can be marked write-only just like properties. In | ||
particular, this means there are write-only arrays `{set T}`, that are | ||
contravariant. These are sometimes useful, for example: | ||
|
||
```lua | ||
function move(src, tgt) | ||
for i,v in ipairs(src) do | ||
tgt[i] = src[i] | ||
src[i] = nil | ||
end | ||
end | ||
``` | ||
|
||
we can give this function the type | ||
``` | ||
move: <a>({a},{set a}) -> () | ||
``` | ||
|
||
and since write-only arrays are contravariant, we can call this with differently-typed | ||
arrays: | ||
```lua | ||
local dogs : {Dog} = {fido,rover} | ||
local animals : {Animal} = {tweety,sylvester} | ||
move (dogs,animals) | ||
``` | ||
|
||
This program does not type-check with read-write arrays. | ||
|
||
### Classes | ||
|
||
Classes can also have write-only properties and indexers. | ||
|
||
Some Roblox APIs which manipulate callbacks are write-only for security reasons. | ||
|
||
### Separate read and write types | ||
|
||
Once we have read-only properties and write-only properties, type intersection | ||
gives read-write properties with different types. | ||
|
||
```lua | ||
{ get p: T } & { set p : U } | ||
``` | ||
|
||
If we infer such types, we may wish to present them differently, for | ||
example TypeScript allows both a getter and a setter. | ||
|
||
## Drawbacks | ||
|
||
This is adding to the complexity budget for users, who will be faced | ||
with inferred set modifiers on many properties. There is a trade-off | ||
here about how to spend the user's complexity budget: on understanding | ||
inferred types with write-only properties, or debugging false positive | ||
type errors caused by variance issues). | ||
|
||
## Alternatives | ||
|
||
Just stick with read-only and read-write accesses. |