-
Notifications
You must be signed in to change notification settings - Fork 94
RFC: Unique types #173
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
athar-adv
wants to merge
35
commits into
luau-lang:master
Choose a base branch
from
athar-adv:master
base: master
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Open
RFC: Unique types #173
Changes from 28 commits
Commits
Show all changes
35 commits
Select commit
Hold shift + click to select a range
73d879d
Introduce RFC for unique types in Luau
athar-adv 72ca62c
Improve clarity on unique types and intersections
athar-adv 9d995d6
added a period (#1)
athar-adv cad3cd0
Refactor unique type definitions in unique-types.md
athar-adv cbde0b6
Added export semantics
athar-adv b8cb27e
Added type function semantics
athar-adv f5b1f7c
Added no other language has done this drawback
athar-adv 4c45324
Changed semantics and syntax to work with subtypes instead of carryin…
athar-adv 02cd7fd
Added generic semantics & changed casting to be explicit
athar-adv f205498
Added function call examples to behavior with literals
athar-adv 691a992
Clarified no-intersection semantics
athar-adv 1266f5a
Added clarification to no-implicit-cast statement
athar-adv 1a3d99c
Added better examples for no-inter-unique-type-casts
athar-adv 6fc728a
Clarified casting semantics
athar-adv 3a17a8f
Added examples where generics define the supertype
athar-adv d5ecde8
Added tostring example to generic examples
athar-adv 2b2aca5
Made motivation clearer
athar-adv 28d2daa
Added clarification to design summary and changed generics example
athar-adv aa4d207
Fixed invalid casts in casting semantics example
athar-adv 08c45a1
Amended type function semantics
athar-adv 9a215b5
Amended intersection behavior to work with refinements
athar-adv 68069d1
Amended incorrect usage of the word subtype
athar-adv 19730ed
Replaced a stray } with ]
athar-adv d42cb64
Added #123 nominal typing rfc as one of the alternatives to this rfc
athar-adv e0184ba
Amended casting semantics section
athar-adv f42e1c9
Fixed an incorrect statement regarding casts
athar-adv 01118fc
Amended casting semantics vector example being wrong
athar-adv 288bff8
Unique types that are used in type functions instead of unique types …
athar-adv 89c39d1
Amended motivation for alternative rfc
athar-adv 04119de
Amended redundant summary information
athar-adv e5b363e
Amended operations & interface section
athar-adv b13ff3a
Amended amended operations & interface of a unique type
athar-adv a6d7bea
Amended operations & interface of a unique type section to be more sp…
athar-adv 6c1d9c4
Made example of aliases being interchangeable clearer that its talkin…
athar-adv d2cc0ce
Fixed grammar mistakes
athar-adv File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or 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,265 @@ | ||
| # Unique Types | ||
| --- | ||
| ## Summary | ||
| --- | ||
| This RFC proposes adding support for unique types to luau. | ||
|
|
||
| Unique types are an extension to the type checker, and make no changes to runtime semantics. | ||
|
|
||
| ## Motivation | ||
| --- | ||
| Since Luau uses structural typing, there is no way to make a primitive distinct. If there are two types PlayerId and AssetId and they are both strings, the type checker allows a PlayerId to be passed into a function expecting AssetId because they are both just string. | ||
|
|
||
| Current workarounds like tagging (string & { _tag: "PlayerId" }) are messy and confuse autocomplete. | ||
|
|
||
| Unique types solve this by being completely unique from any other type, therefor allowing programmers to bar casts between different unique types. | ||
| A supertype and a list of generics can be assigned to a unique type to alter its subtyping behavior, making it easier to inter-operate between unique types and normal Luau structural types. | ||
| A unique type will be able to be cast to its supertype, but not to other unique types or types that are not its supertype. | ||
|
|
||
| ## Design | ||
| --- | ||
| The proposed syntax to create a unique type is to define it using `type TypeName: Supertype`, the unique type `TypeName` will be defined as having a supertype `Supertype`, defined after the colon. A unique type with no supertype is not allowed as that type would never exist and is "uninhabited". | ||
|
|
||
| A unique type is allowed to have other unique types as its supertype | ||
|
|
||
| ### Behavior with autocomplete | ||
|
|
||
| The autocomplete of a unique type should inherit from its defined supertype, as the unique type is gauranteed to have everything that the supertype has. | ||
|
|
||
| ### Casting semantics | ||
|
|
||
| When assigning a value to a variable, a cast will NOT be implicitly performed. An explicit cast must be done first, because unique types are different types from types such as literals and primitives. | ||
|
|
||
| A unique type cannot be cast to another unique type, however can be cast to types it is subtype of (defined by the type expression after the : in the unique types declaration) | ||
| Illustrated in code: | ||
|
|
||
| ```luau | ||
| type UserId: number | ||
| type PlaceId: number | ||
|
|
||
| local user1: UserId = 2 -- Doesnt work, must cast first | ||
| local user2 = 2 :: UserId -- Works! UserId is a subtype of number and its being typecast | ||
| local user3 = "2" :: UserId -- Doesnt work, string is not a supertype of UserId | ||
| local user4: UserId = 12323 :: PlaceId -- Doesnt work, could not convert PlaceId into UserId | ||
| local user5 = 1234 :: PlaceId | ||
| local user6 = user5 :: UserId -- Doesnt work, could not convert PlaceId into UserId | ||
|
|
||
| local function getPlaceData(id: PlaceId) | ||
|
|
||
| local data = getPlaceData(1234) -- Doesnt work, must explicitly cast number to PlaceId | ||
| local data = getPlaceData(1234 :: PlaceId) -- Works! | ||
|
|
||
| local a = 10 | ||
| local moredata = getPlaceData(a) -- Again, doesnt work | ||
| local moreadaatatata = getPlaceData(a :: PlaceId) -- Works! | ||
| ``` | ||
|
|
||
| Unique types can be casted to other structural types provided the types are compatible in a structural manner and vice versa. That is to say: | ||
|
|
||
| ```luau | ||
| type Vec2: { x: number, y: number } | ||
| type Vec3: { x: number, y: number, z: number } | ||
|
|
||
| local vec2_1 = { x=1, y=1 } | ||
| local vec3_1 = { x=1, y=1, z=2 } | ||
|
|
||
| local vec2_2 = vec3_1 :: Vec2 -- Works, "x" and "y" are present, which is all that's required | ||
| local vec3_2 = vec2_1 :: Vec3 -- Doesnt work, "z" is missing from the type | ||
| local vec3_3 = vec3_2 :: Vec2 -- Doesnt work, Vec3 cannot be cast into Vec2 despite the fact that Vec2 is a valid subtype of Vec3 | ||
|
|
||
| local vec2_3 = vec2_2 :: {x: number, y: number} -- This works because {x: number, y: number} is a subtype of {x: number, y: number} (itself) | ||
| ``` | ||
|
|
||
| ### Behavior with intersections | ||
|
|
||
| Using a unique type in an intersection would simply intersect with the supertype of the unique type, for example: | ||
| ```luau | ||
| type Thing: {a: string} | ||
| type ExtendedThing = Thing & {b: number} -- Aliases still work with unique types! | ||
| -- The supertype of ExtendedThing has been expanded, and since in the case of intersections, wider = subtype, that means ExtendedThing is now a subtype of {a: string} which is the supertype of Thing. | ||
|
|
||
| local thing = {a: string, b: number} :: ExpandedThing -- Works! | ||
| local thing2 = thing :: Thing -- This works! Since thing is actually the same unique type, just with the expanded supertype of ExtendedThing, and ExtendedThing is a subtype of {a: string} which is the supertype of Thing, that means this cast is valid. | ||
| ``` | ||
|
|
||
| ### Behavior with unions | ||
|
|
||
| Using a unique type in a union would work, illustrated in something like: | ||
|
|
||
| ```luau | ||
| type UserIdNumber: number | ||
| type UserIdString: string | ||
|
|
||
| local function getData(id: UserIdNumber | UserIdString) -- This makes sense, UserIdNumber | UserIdString reads as "UserIdNumber, a type that is a subtype of number, or UserIdString, a type that is a subtype of string". | ||
| local function getDataStringy(id: string | UserIdString) -- This also makes sense, string | UserIdString reads as "A string, or UserIdString, a type that is a subtype of string". | ||
|
|
||
| local data = getData(1234 :: UserIdNumber) | ||
| ``` | ||
|
|
||
| ### Refinement behavior | ||
|
|
||
| Unique types can be refined through type guards and pattern matching based on their supertype. | ||
|
|
||
| ```luau | ||
| type ItemId: string | ||
| type ItemData: {data: ItemId, name: string} | ||
|
|
||
| local function processItem(item: ItemId | ItemData) | ||
| if type(item) == "string" then | ||
| -- item is refined to ItemId as the only type that is a subtype of string is ItemId, and to satisfy type(item) == "string" the type must be a subtype of string | ||
| print("Item ID: " .. item) | ||
| else | ||
| -- item is refined to ItemData as that's the only other member of the union that's not a subtype of string | ||
| print("Item: " .. item.name) | ||
| end | ||
| end | ||
| ``` | ||
|
|
||
| Unique types work with discriminated unions, however if a unique type itself is a discriminated union, it will not be able to be decomposed into the correct component as unique types due to the "atomic" nature of nominal types: | ||
|
|
||
| ```luau | ||
| type ClickEvent: {kind: "click", x: number, y: number} | ||
| type KeyEvent: {kind: "key", code: string} | ||
| type UEvent: ClickEvent | KeyEvent | ||
| type Event = ClickEvent | KeyEvent | ||
|
|
||
| local function handleEvent(event: Event) | ||
| if event.kind == "click" then | ||
| -- event is refined to ClickEvent | ||
| print("Click at", event.x, event.y) | ||
| end | ||
| end | ||
|
|
||
| local function handleUEvent(event: UEvent) | ||
| if event.kind == "click" then | ||
| -- UEvent is a subtype of ClickEvent | KeyEvent, which means UEvent is either one of these. | ||
| -- However, UEvent is a unique type, which means it cannot be decomposed any further | ||
| -- Due to this, this means that the "event" variable will have 0 autocomplete (opaque) because it's unclear which one it's supposed to be | ||
| -- So here, no refinement occurs and event remains as UEvent | ||
| end | ||
| end | ||
| ``` | ||
|
|
||
| However, if a member of a unique type was to be refined like so: | ||
|
|
||
| ```luau | ||
| type Proxy: {inst: Instance?, metadata: {[string]: any}} | ||
|
|
||
| local function modify(p: Proxy) | ||
| if p.inst then | ||
| -- The supertype of p would be refined to Proxy & {inst: ~(false?) & Instance, metadata: {[string]: any}}, narrowing the type and becoming a subtype of the original supertype. | ||
| end | ||
| end | ||
| ``` | ||
|
|
||
| ### Generic arguments semantics | ||
|
|
||
| To accomodate usage of generics, unique types are able to declare a list of generic arguments using the `type TypeName<Arg1, Arg2, Arg3, ...Tuple>: Supertype` syntax, or alternatively `type TypeName<Arg1 = A, Arg2 = B, Arg3 = C, ...Tuple = D...>: Supertype` for generics with default values.. | ||
|
|
||
| Whenever a unique type is instantiated with a list of generics, these generics become part of the instantiated type and will not be discarded even if the generics aren't used in the supertype, acting sort of like metadata for the instantiated unique type. | ||
|
|
||
| It's important to note that an instantiated generic unique type T of unique type A will only be able to be cast to another instatiated generic unique type U of unique type A if the generic values of T are all subtypes of the generic values of U (for instance, `A<string> -> A<"hello">` is invalid as `string` is not a subtype of "hello", however `A<"hello"> -> A<string>` is valid, and so is `A<"hello"> -> A<any>`) | ||
|
|
||
| An example of usage: | ||
|
|
||
| ```luau | ||
| type i53: number | ||
| type Component<T>: i53 | ||
| type Entity: i53 | ||
|
|
||
| local function newEntity(): Entity | ||
| local function newComponent<T>(): Component<T> | ||
| local function get<T>(entity: Entity, component: Component<T>): T | ||
|
|
||
| local entity = newEntity() | ||
| local component = newComponent<<string>>() | ||
|
|
||
| local value = get(entity, component) -- value is string! | ||
| ``` | ||
|
|
||
| Generic arguments can also be used to define the supertype, for example: | ||
|
|
||
| ```luau | ||
| type UserId<ValueType = any>: ValueType | ||
|
|
||
| local function getUserId(): UserId | ||
| local function saveUserId(id: UserId<string>) | ||
|
|
||
| local id: UserId<number> = getUserId() | ||
| saveUserId(id) -- Does not work! number is not a subtype of string | ||
| saveUserId(id :: UserId<string>) -- Does not work! number is not a subtype of string in the generics list | ||
| saveUserId(tostring(id) :: UserId<string>) -- Works! The type signature for tostring is tostring(...any) -> string, and since we now have a string it's able to be converted into UserId<string>. | ||
| ``` | ||
|
|
||
| ### Type function semantics | ||
|
|
||
| Due to the nature of unique types, there would be no way to construct unique types in type functions. | ||
|
|
||
| However, since you should be able to input unique types into type functions, or use it as an upvalue, the following are some semantic rules for unique `type` objects: | ||
|
|
||
| - Using `type:__eq()` on a unique `type` object on any type other than itself or the type it was instantiated from should return `false` (for example, where T is instantiated from UniqueType and passed as a parameter, `T == UniqueType` -> `true`, `T == T` -> `true`, `UniqueType == types.number` -> `false`, `T == types.string` -> `false`). | ||
| - There should be a new valid string input to `type:is()`, which is `"unique"`. Illustrated in code: | ||
| ```luau | ||
| type function hi(T) | ||
| if T:is("unique") then | ||
| print("t is unique!") | ||
| else | ||
| print("t is normal :(") | ||
| end | ||
| return T | ||
| end | ||
| ``` | ||
| - Unique types that are used in type functions should have a `.tag` property set to `"unique"` too. | ||
| - Implement a new method to `type`, which is `type:generics() -> {type}`. This will return the list of instantiated generic values bound to the unique type. | ||
| - Implement a new method to `type`, which is `type:setgenerics({type}) -> ()`. This will set the list of instantiated generic values bound to the unique type. | ||
| - `type:is()` will work if you try to check the supertype of a unique type, so for example: | ||
| ```luau | ||
| type PlayerId<T>: T | ||
|
|
||
| type function playerIdToString(t: type) | ||
| assert(t:is("number") and t == PlayerId) | ||
| local newid = PlayerId(types.string) | ||
| return newid | ||
| end | ||
|
|
||
| local a: PlayerId<number> | ||
| local b: playerIdToString<typeof(a)> = tostring(a) | ||
| ``` | ||
| - `type:issubtypeof(T)` should return true if T is defined as a supertype of the unique type, false if otherwise. | ||
|
|
||
| # Drawbacks | ||
| --- | ||
|
|
||
| - Values need to be explicitly cast to the unique type before being able to be assigned to an annotated variable of a unique type | ||
|
|
||
| # Alternatives | ||
| --- | ||
|
|
||
| ### The nominal typing rfc | ||
| There is an alternative nominal typing rfc that proposes encapsulating structural types inside of nominal types instead: | ||
| [#123](https://github.com/luau-lang/rfcs/pull/123) | ||
|
|
||
| ### Just use tables | ||
| My example of distinct UserId and AssetId types could instead be written as | ||
|
|
||
| ```luau | ||
| type UserId = { userId: number } | ||
| type AssetId = { assetId: number } | ||
| ``` | ||
|
|
||
| This works in the current system and makes these types incompatible. For the vectors example, the following snippet would produce the required incompatible types: | ||
|
|
||
| ```luau | ||
| type Vec2 = { x: number, y: number, __isVec2: number } | ||
| type Vec3 = { x: number, y: number, z: number, __isVec3: number } | ||
| ``` | ||
|
|
||
| A helper type could be used to perform this automatically, such as the following: | ||
|
|
||
| ```luau | ||
| type Tagged<T, Tag> = T & { __tag: Tag } | ||
| type UserId = Tagged<number, "UserId"> | ||
| type AssetId = Tagged<number, "AssetId"> | ||
| ``` | ||
|
|
||
| In all of these cases, the types are no longer zero-cost at runtime, and in the cases where casting between "nominal" types is desired, it also incurs a runtime cost. The Tagged option does allow runtime introspection, however nothing in this RFC would disallow use of that existing pattern when desired. | ||
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.