From 689bba98817224769480ea5594ba352b6694fb4c Mon Sep 17 00:00:00 2001 From: Alexander McCord Date: Tue, 16 Apr 2024 10:51:31 -0700 Subject: [PATCH 1/6] Add negation type RFC. --- docs/negation-types.md | 86 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) create mode 100644 docs/negation-types.md diff --git a/docs/negation-types.md b/docs/negation-types.md new file mode 100644 index 00000000..0f38e6db --- /dev/null +++ b/docs/negation-types.md @@ -0,0 +1,86 @@ +# Negation types + +## Summary + +A type that represents the complement of the type being negated, which is a union type of all inhabited types (`unknown`) excluding the type being negated. + +## 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 invariances beyond the scope of the branch. + +A [cofinite set](https://en.wikipedia.org/wiki/Cofiniteness) arises when you have a negation type in conjunction with intersection types. For example, `string & ~"a"` is a cofinite string set that accepts any `string` excluding `"a"`. This typically happens all the time with type refinements, where `typeof(x) == "string" and x ~= "a"` gives rise to the type `string & ~"a"`. + +## Design + +### Syntax + +The notation is `~T` where `T` is a type annotation. It binds tightly to the type it negates, so `~T | U` is `(~T) | U`, not `~(T | U)`. There's really not much to it, syntax-wise. It has the same precedence as the `not` expression, which is why `~T | U` is `(~T) | U` in the same way `not t or u` is `(not t) or u`. + +We propose to allow users to write such a type. Formally: + +```ebnf +ty ::= `~` ty + | name [`<` [ty] {`,` ty} `>`] + | ty {`|` ty} + | ty {`&` ty} + | `(` ty `)` + | `typeof` `(` exp `)` + | table_ty (* omitted for brevity *) + | function_ty (* omitted for brevity *) +``` + +### Semantics + +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) + +### 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 and also a type error. This means `~{ p: P }` and `~(T) -> U` are nonsensical. + +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: + +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. + +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. + +## Alternatives + +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. + +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 a90e0fd22eacf23f3212d107c9c50ccffd7335c0 Mon Sep 17 00:00:00 2001 From: Alexander McCord <11488393+alexmccord@users.noreply.github.com> Date: Wed, 8 May 2024 13:07:20 -0700 Subject: [PATCH 2/6] Update docs/negation-types.md Co-authored-by: aaron --- 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 0f38e6db..af39bf61 100644 --- a/docs/negation-types.md +++ b/docs/negation-types.md @@ -6,7 +6,7 @@ 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 invariances 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. A [cofinite set](https://en.wikipedia.org/wiki/Cofiniteness) arises when you have a negation type in conjunction with intersection types. For example, `string & ~"a"` is a cofinite string set that accepts any `string` excluding `"a"`. This typically happens all the time with type refinements, where `typeof(x) == "string" and x ~= "a"` gives rise to the type `string & ~"a"`. From a55cce91f2982f56604fbf27cf40543ba4ca84f5 Mon Sep 17 00:00:00 2001 From: Alexander McCord <11488393+alexmccord@users.noreply.github.com> Date: Wed, 8 May 2024 13:07:27 -0700 Subject: [PATCH 3/6] Update docs/negation-types.md Co-authored-by: aaron --- 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 af39bf61..70112770 100644 --- a/docs/negation-types.md +++ b/docs/negation-types.md @@ -8,7 +8,7 @@ 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. -A [cofinite set](https://en.wikipedia.org/wiki/Cofiniteness) arises when you have a negation type in conjunction with intersection types. For example, `string & ~"a"` is a cofinite string set that accepts any `string` excluding `"a"`. This typically happens all the time with type refinements, where `typeof(x) == "string" and x ~= "a"` gives rise to the type `string & ~"a"`. +A [cofinite set](https://en.wikipedia.org/wiki/Cofiniteness) arises when you have a negation type in conjunction with intersection types. 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"`. ## Design From 0947a3d517d05f0e5fa68a7b12468252319f6783 Mon Sep 17 00:00:00 2001 From: Alexander McCord <11488393+alexmccord@users.noreply.github.com> Date: Wed, 8 May 2024 21:46:25 -0700 Subject: [PATCH 4/6] Extract the and clause into its own sentence. --- 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 70112770..18d69e7e 100644 --- a/docs/negation-types.md +++ b/docs/negation-types.md @@ -55,7 +55,7 @@ As you can see, since through the series of rewrites `~~any` did not produce a t 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 and also a type error. This means `~{ p: P }` and `~(T) -> U` are nonsensical. +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 types, you get a type error. Another restriction is that negation types cannot negate generic types. So `(T) -> ~T` is also not legible. From 82626520a1db23bf551e4a2660a01eb553f024f3 Mon Sep 17 00:00:00 2001 From: Alexander McCord <11488393+alexmccord@users.noreply.github.com> Date: Wed, 8 May 2024 21:53:46 -0700 Subject: [PATCH 5/6] Fluff around what a cofinite set is. --- 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 18d69e7e..e51f814f 100644 --- a/docs/negation-types.md +++ b/docs/negation-types.md @@ -8,7 +8,7 @@ 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. -A [cofinite set](https://en.wikipedia.org/wiki/Cofiniteness) arises when you have a negation type in conjunction with intersection types. 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"`. +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"`. ## Design From ba38a41ef1ec41c7fe5cc64a0db89e0b55365973 Mon Sep 17 00:00:00 2001 From: Alexander McCord <11488393+alexmccord@users.noreply.github.com> Date: Wed, 8 May 2024 22:02:23 -0700 Subject: [PATCH 6/6] Shouldn --- 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 e51f814f..bc0eecf2 100644 --- a/docs/negation-types.md +++ b/docs/negation-types.md @@ -55,7 +55,7 @@ As you can see, since through the series of rewrites `~~any` did not produce a t 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 types, you get a type error. +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.