luau/rfcs/property-writeonly.md

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

  function f(t) t.p = Dog.new() end

The obvious type for this is

  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

  local x : { p : Animal } = { p = Cat.new() }
  f(x) -- Fails to typecheck

If f : ({ p: Animal }) -> () then

  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.

  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:

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:

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:

  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.

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