luau-lang/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2025-05-04 10:33:46 +01:00
Code Issues Projects Releases Packages Wiki Activity

Clarified negation types

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-10-13 11:54:25 -05:00
parent 4b7d4e7679
commit c8ed2ba887
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
docs/_posts/2022-10-31-luau-semantic-subtyping.md
View file

@ -186,7 +186,7 @@ For these two reasons (which are largely about ergonomics rather than anything t
## Negation types
The other difference between Luau’s type system and off-the-shelf semantic subtyping is that Luau does not support negated types.
The other difference between Luau’s type system and off-the-shelf semantic subtyping is that Luau does not support all negated types.
The common case for wanting negated types is in typechecking conditionals:
```lua
@ -199,7 +199,7 @@ end
```
This uses a negated type `~string` inhabited by values that are not strings.
In Luau, we only allow this kind of typing refinement on named types like `string`, `function`, `Part` and so on, and *not* on structural types like `(A) -> B`, which avoids the common case of general negated types.
In Luau, we only allow this kind of typing refinement on *test types* like `string`, `function`, `Part` and so on, and *not* on structural types like `(A) -> B`, which avoids the common case of general negated types.
## Prototyping and verification
@ -236,4 +236,5 @@ If you want to find out more about Luau and semantic subtyping, you might want t
* Giuseppe Castagna, *Covariance and Contravariance*, Logical Methods in Computer Science 16(1), 2022. <https://arxiv.org/abs/1809.01427>
* Giuseppe Castagna and Alain Frisch, *A gentle introduction to semantic subtyping*, Proc. Principles and practice of declarative programming (PPDP), pp 198–208, 2005. <https://doi.org/10.1145/1069774.1069793>
* Giuseppe Castagna, Mickaël Laurent, Kim Nguyễn, Matthew Lutze, *On Type-Cases, Union Elimination, and Occurrence Typing*, Principles of Programming Languages (POPL), 2022. <https://doi.org/10.1145/3498674>
* Sam Tobin-Hochstadt and Matthias Felleisen, *Logical types for untyped languages*. International Conference on Functional Programming (ICFP), 2010. https://doi.org/10.1145/1863543.1863561