RFC: Sealed table subtyping

[AmaranthineCodices]

Rendered link.

[zeux]

Alternative syntax for tables open for extension: ... postfix inside the table (similarly to runtime syntax for varargs).

[zeux]

What do we infer as the type of

function foo(t)
return t.field
end

right now?

[andyfriesen]

We don't have surface syntax for generic tables, but if we did, it would be something like

foo : <T>{field: T, ...} -> T

[zeux]

Aha - generic tables is what I was looking for. After this change, would sealed and generic tables be different?

[tiffany352]

Does going with unsealed as the default for table types imply we'll need to add a syntax for sealed tables later? Sort of like the inverse of the interface {} alternative.

It seems like this proposal will make it impossible to declare sealed tables except via typeof.

[AmaranthineCodices]

@zeux

Aha - generic tables is what I was looking for. After this change, would sealed and generic tables be different?

Generic tables will stick around for a bit longer. Constrained generics will probably replace the generic table state entirely, but for right now they have some subtle behavioral differences that we want to keep around.

@tiffany352

Does going with unsealed as the default for table types imply we'll need to add a syntax for sealed tables later? Sort of like the inverse of the interface {} alternative.

It seems like this proposal will make it impossible to declare sealed tables except via typeof.

This proposal doesn't change the semantics of sealed tables; they will still occur in the same places. Unsealed tables are sealed when they leave the scope they were created in, so e.g. this function returns a sealed table, not an unsealed one:

local function x()
    return {
        a = 1,
    }
end

This subtyping mechanic is actually unsound for unsealed tables without flow analysis:

local x = {
    a = 1,
}

local y = {
    a = 1,
    b = 2,
}

-- both x and y are unsealed in this scope

local z: typeof(x) = y -- y is said to be a subtype of x for this to work
x.c = 3 -- now x has a "c" property, which y does not. accessing z.c is nil.

This introduces some somewhat awkward semantics for cases where type annotations aren't involved, unfortunately. Using type annotations can force a table to be sealed; for example, in this code:

type Foo = {
    a: number,
}

local x: Foo = {
    a = 123,
}

x is a sealed table, not an unsealed one.

[asajeffrey]

At some point we'd want to replace generic tables b bounds on type parameters, e.g.

function foo(x)
  x.p = 5
  return x
end

would get inferred as having type

foo : <t : {p : number}>(t) -> t

[asajeffrey]

LGTM!

[zeux]

I feel like long term this can make the type system easier to understand if we stop using the words "sealed table"; instead this purely becomes a table, generic tables go away in lieu of generic constraints, and unsealed tables are just a transient state that happens during type checking. Short term we should consider rewording the manual (and error messages if we have any) to refer to sealed tables as tables while keeping the other types...

[andyfriesen]

One thought I had was that we could just convert sealed tables in function arguments to generic tables during quantification. I think this would mostly get us what we want with minimal changes.

It seems to be very rare that anyone ever actually wants a sealed table as an argument.

If we ever actually do run into that use case, we could do what Flow does and offer explicit syntax for a sealed table type.