Second draft

This commit is contained in:
ajeffrey@roblox.com 2023-03-14 11:39:57 -05:00
parent 0a84f94634
commit 5470f2a264

View file

@ -40,9 +40,6 @@ For example, `Point` class can be simulated using metatables:
function Point:abs()
return math.sqrt(self:getX() * self:getX() + self:getY() * self:getY())
end
type PointMT = typeof(Point)
type Point = typeof(Point.new())
```
Currently, this code is problematic, since there is no connection between the types
@ -65,6 +62,7 @@ for overloaded operators, the inferred type would be something like:
type Point = {
x : number,
y : number,
@metatable PointMT
}
```
@ -111,8 +109,6 @@ end
function Set:contains(el)
return self.elements[el] != nil
end
type SetMT = typeof(Set)
```
In this case, the expected type would be something like:
@ -125,8 +121,8 @@ In this case, the expected type would be something like:
contains : <E>(Set<E>, E) -> boolean
}
type Set<E> = {
elements : { [E] : boolean },
@metatable SetMT
elements : { [E] : boolean }
}
```
@ -141,29 +137,38 @@ in this case:
contains : (Set, unknown) -> boolean
}
type Set = {
elements : { [unknown] : boolean },
@metatable SetMT
elements : { [unknown] : boolean }
}
```
and propose allowing explicit syntax for declaring the shared self type:
and propose allowing explicit declaration of the shared self type,
following the common practice of naming the self type after the metatable:
```lua
type Set:self<E> = { [E] : boolean }
type Set<E> = { [E] : boolean }
```
This type (and its generic type parameters) are used as the type of
`self` in methods declared using `function Set:m()` declarations.
This type (and its generic type parameters) are used to derive the
type of `self` in methods declared using `function Set:m()`
declarations:
```lua
type SetSelf<E> = {
[E] : boolean,
@metatable SetMT
}
```
In cases where shared self types are just getting in the way, there
are two work-arounds. The shared self type can be declared to be
`any`, which will silence type errors:
are two work-arounds. Firstly, the shared self type can be declared to
be `any`, which will silence type errors:
```lua
type Foo:self = any
type Foo = any
```
The self type can be declared explicitly:
Secondly, the self type can be declared explicitly:
```lua
function Foo.m(self : Bar) ... end
@ -171,96 +176,98 @@ The self type can be declared explicitly:
## Design
For each table type `T`, intoduce:
### Self types
* the self type parameters of `T`, a sequence of generic type and typepack variables,
* the self type definition of `T`, a type which can use the type parameters of `T:self`, and
* the self type of `T`, which is the self type definition of `T` extended with `@metatable T`.
For each table `t`, introduce:
* the self type parameters of `t`, a sequence of generic type and typepack variables,
* the self type definition of `t`, a type which can use the type parameters of `t`, and
* the self type of `t`, a type which can use the type parameters of `t`.
These can be declared explicitly:
```lua
type t:self<As> = U
type t<As> = U
```
which defines (when `t` has type `T`):
which defines, when `t` has type `T`:
* the self type parameters of `T` to be `As`,
* the self type definition of `T` to be `U`, and
* the self type of `T` to be `U` extended with `@metatable T`.
* the self type parameters of `t` to be `As`,
* the self type definition of `t` to be `U`, and
* the self type of `t` to be `U` extended with `@metatable T`.
For example,
```lua
type SetMT = typeof(Set)
type Set:self<E> = { [E] : boolean }
type Set<E> = { [E] : boolean }
```
declares:
declares, when `Set` has type `SetMT`:
* the self type parameters of `SetMT` to be `E`,
* the self type definition of `SetMT` to be `{ [E] : boolean }`, and
* the self type of `SetMT` to be `{ [E] : boolean, @metatable SetMT }`.
* the self type parameters of `Set` to be `E`,
* the self type definition of `Set` to be `{ [E] : boolean }`, and
* the self type of `Set` to be `{ [E] : boolean, @metatable SetMT }`.
If there is no explicit declaration of the self type of `T`, then
If there is no explicit declaration of the self type of `t`, then, when `t` has type `T`:
* the self type parameters of `T` are empty,
* the self type definition of `T` is a free table type `U`,
* the self type of `T` is a metatable type, whose metatable is `T`, and whose table is `U`.
* the self type parameters of `t` are empty,
* the self type definition of `t` is a free table type `U`,
* if `t` has an `__index` property of type `MT`, then the self type of `t` is
a metatable type, whose metatable is `MT`, and whose table is `U`, and
* if `t` does not have an `__index` property, then the self type of `t` is `U`.
Then free table type is inferred in the usual fashion.
The free table type is unified in the usual fashion.
Self types are used in two ways: in calls to `setmetatable`, and in metamethod declarations.
### `setmetatable`
In calls to `setmetatable(t, mt)`:
* if `mt` has type `MT`,
* and `MT` has self type parameters `As`, self type definition `T` and self type `S`,
* if `mt` has self type parameters `As`, self type definition `T` and self type `S`,
* and `T` has (final) type `T [ Ts/As ]`
* then `setmetatable(t, mt)` has type `S [ Ts/As ]`.
As currently, this has a side-effect of updating the type state of `t` from
'T [ Ts/As ]` to `S [ Ts/As ]`.
For example, in `setmetatable(Set, { elements = {} }`, we have:
For example, in `setmetatable({ elements = {} }, Set)`, we have:
* `Set` has type `SetMT`
* and `SetMT` has self type parameter `E`, self type definition` { elements : { [E] : boolean } }`, and self type `{ elements : { [E] : boolean }, @metatable SetMT }`,
* `Set` has type `SetMT`, self type parameter `E`, self type definition` { elements : { [E] : boolean } }`, and self type `{ elements : { [E] : boolean }, @metatable SetMT }`,
* and `{ elements = {} }` has type `{ elements : { [X] : boolean } }` for a free `X`,
* so `setmetatable(Set, { elements = {} }` has type `{ elements : { [X] : boolean }, @metatable SetMT }`.
* so `setmetatable({ elements = {} }, Set)` has type `{ elements : { [X] : boolean }, @metatable SetMT }`.
as a result `Set.new` has type `<a>() -> { elements : { [a] : boolean }, @metatable SetMT }`.
As another example, in `setmetatable(Point, result)`:
* `Point` has type `PointMT`,
* and `PointMT` has no self type parameters, a free self type definition (call it `T`), and a self type whose table type is `T` and whose metatable is `PointMT`,
* `Point` has type `PointMT`, no self type parameters, a free self type definition (call it `T`), and a self type whose table type is `T` and whose metatable is `PointMT`,
* and `result` has final type `{ x : number, y : number }`,
* so (by unifying `T` with `{ x : number, y : number }`) `setmetatable(Point, result)` has type `{ x : number, y : number, @metatable PointMT }`.
As a side-effect, the type state of `result` is updated to be `{ x : number, y : number, @metatable PointMT }`,
and unification causes the self type of `PointMT` to be `{ x : number, y : number, @metatable PointMT }`.
and unification causes the self type of `Point` to be `{ x : number, y : number, @metatable PointMT }`.
Note that this relies on the type of `result` being `{ x : number, y : number }`, which is why we use the final
long-lived type of `t` rather than its current type state.
### Method declarations
In method declarations `function mt:m`:
* if `mt` has type `MT`,
* and `MT` has self type parameters `As` and self type `S`,
* if `mt` has self type parameters `As` and self type `S`,
* then give the `self` parameter to `MT.m` the type `S [ Xs/As ]` for fresh free Xs (these types are quantified as all other free types are).
For example, in the method `Set:add(el)`:
* `Set` has type `SetMT`,
* and `SetMT` has self type parameter `E`, and self type `{ elements : { [E] : boolean }, @metatable SetMT }`,
* `Set` has self type parameter `E`, and self type `{ elements : { [E] : boolean }, @metatable SetMT }`,
* so `self` has type `{ elements : { [X] : boolean }, @metatable SetMT }` when type checking the body of `Set:add(el)`.
At this point, type inference proceeds as usual:
* `el` id given fresh free type `Y`,
* the statement `self.elements[el] = true` will unify `X` and `Y`,
* quantifying will result in type `<a>({ elements : { [X] : boolean }, @metatable SetMT }) -> ()`.
* `el` is given fresh free type `Y`,
* the statement `self.elements[el] = true` will unifies `X` and `Y`, and
* quantifying results in type `<a>({ elements : { [a] : boolean }, @metatable SetMT }) -> ()`.
## Drawbacks
@ -328,7 +335,7 @@ resulting in:
}
```
or can switch off type checking `self` by declaring `type Point:self = any`.
or can switch off type checking `self` by declaring `type Point = any`.
### Methods called on both tables and metatables.
@ -338,8 +345,10 @@ result in inferring that both `x` and `y` are optional,
## Alternatives
There are the usual bike shedding opportunities for new syntax.
We could use new syntax for declaring self types, rather than using
the convention that they have the same name as the metatable.
We could do nothing, but at a performance and ergonomics cost.
We could introduce special syntax for classes or records, though this doesn't address type checking current code.
We could introduce special syntax for classes or records, though this
doesn't address type checking current code.