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] 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 0f38e6d..af39bf6 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"`.