RFC: Write-only properties (#79)

Co-authored-by: vegorov-rbx <75688451+vegorov-rbx@users.noreply.github.com>

rfcs/property-writeonly.md

@@ -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.