From 31dcebacccc3c3b247f5731bf9262fe530e46e3d Mon Sep 17 00:00:00 2001 From: Alexander McCord <11488393+alexmccord@users.noreply.github.com> Date: Mon, 6 Apr 2026 07:54:44 -0700 Subject: [PATCH 1/7] Allow negation types on non-testables --- docs/negation-types.md | 18 ++---------------- 1 file changed, 2 insertions(+), 16 deletions(-) diff --git a/docs/negation-types.md b/docs/negation-types.md index 9a6dd5938..d3e918e38 100644 --- a/docs/negation-types.md +++ b/docs/negation-types.md @@ -51,28 +51,14 @@ As you can see, since through the series of rewrites `~~any` did not produce a t 5. `~never | ~*error*` 6. `unknown | *error*` (`any` is an alias to `unknown | *error*`, so equivalence is achieved) -### Restrictions - -We currently only support negation of _testable_ types. Intuitively, a testable type is one that can be tested by type refinements at runtime. This includes singleton types, primitive types, and classes. Of course, unions and intersections can be negated as well if and only if all of its constituent types are also testable types, due to the distributivity property of unions and intersections. - -Since types like `{ p: P }` and `(T) -> U` are structural types and the runtime offers no way to test for them, they cannot be negated. An attempt to negate this will just turn the negation type into an error suppressed type. This means `~{ p: P }` and `~(T) -> U` are nonsensical. In the event that you negate some non-testable type, you get a type error. - -Another restriction is that negation types cannot negate generic types. So `(T) -> ~T` is also not legible. - ### Implementation -Most of the implementation of negation types are already in place. The three things missing are: +Most of the implementation of negation types are already in place. The one thing missing is: -1. the syntax, -2. some guarantee that no negation types survive if it negates non-testables, and -3. a type error if it negates a non-testable type in any way, shape, or form. +1. the syntax. The parser change for this is trivial, so this is of no concern. -We can use type families to have this guarantee. Add a `negate` type family which would be internal to the type inference engine, and have the syntax `~T` produce that type family, not a `NegationType`. - -As for the type error, we can just consider `negate<{ p: P }>` to be an uninhabited type family, and resolve that as an error type. - ## Drawbacks Language design has a concept called weirdness budget. It's a fine line to balance, especially in this case where, even in popular type systems that have negation types, they are seldom used except by power users. From 10095a72991a2783187905ceaa61b96976f4ab95 Mon Sep 17 00:00:00 2001 From: Alexander McCord <11488393+alexmccord@users.noreply.github.com> Date: Mon, 6 Apr 2026 08:59:52 -0700 Subject: [PATCH 2/7] Update negation-types.md --- docs/negation-types.md | 28 ++++++---------------------- 1 file changed, 6 insertions(+), 22 deletions(-) diff --git a/docs/negation-types.md b/docs/negation-types.md index d3e918e38..dbe466745 100644 --- a/docs/negation-types.md +++ b/docs/negation-types.md @@ -33,31 +33,15 @@ ty ::= `~` ty The basis set we want to perform set exclusion on is `unknown`, _not_ `any`. This means given the type `~"a"`, it is equivalent to the type `unknown & ~"a"`. -Choosing `unknown` as the basis makes a lot of things fall in place properly, including the property we wish to maintain where `~~T` is equivalent to `T`. It's crucial that we handle negation of error types properly, otherwise double negations won't actually be consistent. It'd allow error suppression to be improperly suppressed! See below, where `~~any` ends up as `unknown` instead of `any`. - -1. `~~any` -2. `~~(unknown | *error*)` -3. `~(~unknown & ~*error*)` -4. `~(never & unknown)` -5. `~never` -6. `unknown` (not equivalent to `any`!) - -As you can see, since through the series of rewrites `~~any` did not produce a type equivalent to `any`, our basis set must be `unknown`, and negation of an error suppression is still an error suppressing type. Therefore `~*error*` is `*error*`. This fixes the double-negation inconsistency: - -1. `~~any` -2. `~~(unknown | *error*)` -3. `~(~unknown & ~*error*)` -4. `~(never & *error*)` -5. `~never | ~*error*` -6. `unknown | *error*` (`any` is an alias to `unknown | *error*`, so equivalence is achieved) - ### Implementation -Most of the implementation of negation types are already in place. The one thing missing is: +The parser change for this is trivial, so this is of no concern. -1. the syntax. +Most of the real work would be spent on revising the type system to handle negation types of non-testable types, e.g. -The parser change for this is trivial, so this is of no concern. +- implement normalization and simplification rules involving negation types with non-testable types +- implement subtyping rules on negation of non-testables +- allow `types.negationof` to be applied on function types and table types ## Drawbacks @@ -67,6 +51,6 @@ Language design has a concept called weirdness budget. It's a fine line to balan We could provide a set of type aliases for some common use cases, e.g. `not_nil` for `~nil` and `not_string` for `~string` and so on. But this is limited, i.e. no way to negate for a specific string singleton except by a `typeof` hack. -Alternatively, provide a type family `not`, which can be generalized to any type, so long as they obey the restrictions above! This alternative proposal is essentially the above proposal, sans syntax. +Alternatively, provide a type family `not`, which can be generalized to any type! This alternative proposal is essentially the same as the proposal, sans syntax. Unless we rename it to `negate`, this still requires changing the parser anyway since `not` is a keyword. We could also use the set exclusion syntax `T \ U` which does provide an advantage of an explicit set to exclude a subset of, but there are downsides with this, e.g. it is neither commutative nor associative, which makes for the implementation more annoying since you cannot fold over them as easily. From 61c7445e156c0c2d88e3f12064fe2739aa70d100 Mon Sep 17 00:00:00 2001 From: Alexander McCord <11488393+alexmccord@users.noreply.github.com> Date: Mon, 6 Apr 2026 09:02:19 -0700 Subject: [PATCH 3/7] Update negation-types.md --- docs/negation-types.md | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/docs/negation-types.md b/docs/negation-types.md index dbe466745..ea91a7168 100644 --- a/docs/negation-types.md +++ b/docs/negation-types.md @@ -37,11 +37,7 @@ The basis set we want to perform set exclusion on is `unknown`, _not_ `any`. Thi The parser change for this is trivial, so this is of no concern. -Most of the real work would be spent on revising the type system to handle negation types of non-testable types, e.g. - -- implement normalization and simplification rules involving negation types with non-testable types -- implement subtyping rules on negation of non-testables -- allow `types.negationof` to be applied on function types and table types +Most of the real work would be spent on revising the type system to handle negation types of non-testable types in normalization, simplification, and subtyping rules, as well as adjusting `types.negationof` to allow function types and table types. ## Drawbacks From 680b6e63898fab309a3eaa1bd553877f6eaec8a6 Mon Sep 17 00:00:00 2001 From: Alexander McCord <11488393+alexmccord@users.noreply.github.com> Date: Mon, 6 Apr 2026 09:47:20 -0700 Subject: [PATCH 4/7] Update negation-types.md --- docs/negation-types.md | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/docs/negation-types.md b/docs/negation-types.md index ea91a7168..ce6b7f9ff 100644 --- a/docs/negation-types.md +++ b/docs/negation-types.md @@ -6,9 +6,32 @@ A type that represents the complement of the type being negated, which is a unio ## Motivation -Type refinements will produce negation types to get the complementation. For the most part, users will never need to write these negation types themselves, except for when they want to _maintain_ some invariants beyond the scope of the branch. +Type refinements will produce negation types to get the complementation. For the most part, users will never need to write these negation types themselves, except for when they want to _maintain_ some invariants beyond the scope of the branch, or if the user has overloaded a specific type in a forall quantifier. For example, React has a function called `useState` whose signature is `(state: (() -> S) | S, ...) -> (S, Dispatcher>)`. The problem here is that both `S` and `() -> S` are valid unifiers for the function `() -> T`, so you end up with this monstrosity: -A [cofinite set](https://en.wikipedia.org/wiki/Cofiniteness) arises when you have some negated `X` in conjunction with some supertype of `X`. For example, `string & ~"a"` is a cofinite string set that accepts any `string` excluding `"a"`. This happens often with type refinements where `typeof(x) == "string" and x ~= "a"` gives rise to the type `string & ~"a"`. +``` +((() -> (() -> T) | T) | (() -> T) | T) -> ((() -> T) | T, Dispatcher T) | T>>) +``` + +Another consequence of this signature: functions whose arity does not satisfy the expected arity of `() -> S` will go into `S` which defeats the whole point. This is why when you write `if typeof(state) == "function" then s() else s`, you get a type error at `s()`: ``Cannot call a value of type `S & function` in union: `(() -> S) | (S & function)` ``. The current workaround is `(s :: () -> S)()` which is unsound. The counterexample: + +```luau +local function useState(s: (() -> S) | S): S + return if typeof(s) == "function" + then (s :: () -> S)() + else s +end + +local function foo(x: number) + return x + 1 +end + +-- s: ((x: number) -> number) | number +local s = useState(foo) -- no type errors here +``` + +This program passes the type checker like nothing is wrong, but it's clear that `S` in this case is intended to be the _residual_ of whatever the unifier of `() -> S` is, and a residual is a complement, so the correct signature for `useState` requires negation types: ` ...unknown>(state: (() -> S) | S, ...) -> (S, Dispatcher>)`. + +...which is perfectly valid use case of negation types. By allowing negation types on non-testable types, the intersection `S & function` becomes absurd from the bound `S: ~(...unknown) -> ...unknown`, so `S & function` normalizes to `never`, leaving `s` with the type `() -> S` in the then branch, and in the else branch, `s` is of type `S`, and we can reject code that has no unifiers for `() -> S` and `S: ~(...unknown) -> ...unknown` like `useState(foo)`. ## Design @@ -33,6 +56,8 @@ ty ::= `~` ty The basis set we want to perform set exclusion on is `unknown`, _not_ `any`. This means given the type `~"a"`, it is equivalent to the type `unknown & ~"a"`. +A [cofinite set](https://en.wikipedia.org/wiki/Cofiniteness) arises when you have some negated `X` in conjunction with some supertype of `X`. For example, `string & ~"a"` is a cofinite string set that accepts any `string` excluding `"a"`. This happens often with type refinements where `typeof(x) == "string" and x ~= "a"` gives rise to the type `string & ~"a"`. + ### Implementation The parser change for this is trivial, so this is of no concern. From 867aa64d362f69305f65ae4b32ae3e4ffe8e019a Mon Sep 17 00:00:00 2001 From: Alexander McCord <11488393+alexmccord@users.noreply.github.com> Date: Mon, 6 Apr 2026 09:50:53 -0700 Subject: [PATCH 5/7] Update negation-types.md --- docs/negation-types.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/docs/negation-types.md b/docs/negation-types.md index ce6b7f9ff..14651edc9 100644 --- a/docs/negation-types.md +++ b/docs/negation-types.md @@ -9,16 +9,16 @@ A type that represents the complement of the type being negated, which is a unio Type refinements will produce negation types to get the complementation. For the most part, users will never need to write these negation types themselves, except for when they want to _maintain_ some invariants beyond the scope of the branch, or if the user has overloaded a specific type in a forall quantifier. For example, React has a function called `useState` whose signature is `(state: (() -> S) | S, ...) -> (S, Dispatcher>)`. The problem here is that both `S` and `() -> S` are valid unifiers for the function `() -> T`, so you end up with this monstrosity: ``` -((() -> (() -> T) | T) | (() -> T) | T) -> ((() -> T) | T, Dispatcher T) | T>>) +(state: (() -> (() -> T) | T) | (() -> T) | T) -> ((() -> T) | T, Dispatcher T) | T>>) ``` -Another consequence of this signature: functions whose arity does not satisfy the expected arity of `() -> S` will go into `S` which defeats the whole point. This is why when you write `if typeof(state) == "function" then s() else s`, you get a type error at `s()`: ``Cannot call a value of type `S & function` in union: `(() -> S) | (S & function)` ``. The current workaround is `(s :: () -> S)()` which is unsound. The counterexample: +Another consequence of this signature: functions whose arity does not satisfy the expected arity of `() -> S` will go into `S` which defeats the whole point. This is why when you write `if typeof(state) == "function" then state() else state`, you get a type error at `state()`: ``Cannot call a value of type `S & function` in union: `(() -> S) | (S & function)` ``. The current workaround is `(state :: () -> S)()` which is unsound. The counterexample: ```luau -local function useState(s: (() -> S) | S): S +local function useState(state: (() -> S) | S): S return if typeof(s) == "function" - then (s :: () -> S)() - else s + then (state :: () -> S)() + else state end local function foo(x: number) From c879af9806b2cd2f312801fcc6833762fcac7e40 Mon Sep 17 00:00:00 2001 From: Alexander McCord <11488393+alexmccord@users.noreply.github.com> Date: Mon, 6 Apr 2026 09:57:51 -0700 Subject: [PATCH 6/7] Update negation-types.md --- docs/negation-types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/negation-types.md b/docs/negation-types.md index 14651edc9..5b88f6f02 100644 --- a/docs/negation-types.md +++ b/docs/negation-types.md @@ -31,7 +31,7 @@ local s = useState(foo) -- no type errors here This program passes the type checker like nothing is wrong, but it's clear that `S` in this case is intended to be the _residual_ of whatever the unifier of `() -> S` is, and a residual is a complement, so the correct signature for `useState` requires negation types: ` ...unknown>(state: (() -> S) | S, ...) -> (S, Dispatcher>)`. -...which is perfectly valid use case of negation types. By allowing negation types on non-testable types, the intersection `S & function` becomes absurd from the bound `S: ~(...unknown) -> ...unknown`, so `S & function` normalizes to `never`, leaving `s` with the type `() -> S` in the then branch, and in the else branch, `s` is of type `S`, and we can reject code that has no unifiers for `() -> S` and `S: ~(...unknown) -> ...unknown` like `useState(foo)`. +...which is perfectly valid use case of negation types. By allowing negation types on non-testable types, the intersection `S & function` becomes absurd from the bound `S: ~(...unknown) -> ...unknown`, so `S & function` normalizes to `never`, leaving `state` with the type `() -> S` in the then branch, and the type `S` in the else branch. We can also now reject code that has no unifiers for `() -> S` and `S: ~(...unknown) -> ...unknown` like `useState(foo)`, and type inference behaves as expected for these overloaded polymorphic functions where you are expected to pass in either a function of the signature `() -> T` _or_ a value of type `T` and nothing in-between. ## Design From 19a1792b4c45c3b0d1b04c7ba4388395fecbf595 Mon Sep 17 00:00:00 2001 From: Alexander McCord <11488393+alexmccord@users.noreply.github.com> Date: Mon, 6 Apr 2026 10:48:30 -0700 Subject: [PATCH 7/7] fffffff. Single letter Haskell habit. --- docs/negation-types.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/negation-types.md b/docs/negation-types.md index 5b88f6f02..72121a849 100644 --- a/docs/negation-types.md +++ b/docs/negation-types.md @@ -16,7 +16,7 @@ Another consequence of this signature: functions whose arity does not satisfy th ```luau local function useState(state: (() -> S) | S): S - return if typeof(s) == "function" + return if typeof(state) == "function" then (state :: () -> S)() else state end