Sets, types and type checking

&gt; <i>In Rust we have Option&lt;T&gt;, which is equivalent to T | null</i><p>No, not true!<p>As the author correctly states earlier in the post, unions are not an exclusive-or relation. Unions are often made between disjoint types, but <i>not always</i>.<p>This becomes important when T itself is nullable. Let&#x27;s say T is `U | null`. `Option&lt;Option&lt;U&gt;&gt;` in Rust has one more inhabitant than `U | null | null` in TypeScript - `Some(None)`.<p>Union types can certainly be very useful, but they are tricky because they don&#x27;t compose like sum types do. When writing `Option&lt;T&gt;` where T is a generic type, we can treat T as a totally opaque type - T could be anything and the code we write will still be correct. On the other hand, union types pierce this opacity. The meaning of `T | null` and the meaning of code you write with such a type <i>does</i> depend on what T is at runtime.

An honorable mention is the string template literal type. It is between the string literal type (-unions); which allow a finite set of strings and the string type which, in theory, is an infinite set of strings. Template literal types can be infinite as well, but only represent a fraction. For example `foo${string}` represent all strings that start with &quot;foo&quot;.<p>Similar to this, I proposed inequality types for TS. They allow constraining a number range. For example, it is possible to have the type &quot;a number that is larger than 1&quot;. You can combine them using intersection types, forming intervals like &quot;a number between 0 and 1&quot;. Because TS has type narrowing via control flow, these types automatically come forward if you do an &quot;if (a&lt;5)&quot;. The variable will have the type &quot;(&lt;5)&quot; inside the if block.<p>You can find the proposal here [1]. Personally I think the effort for adding these isn&#x27;t worth it. But maybe someone likes it or takes it further.<p>[1]: <a href="https:&#x2F;&#x2F;github.com&#x2F;microsoft&#x2F;TypeScript&#x2F;issues&#x2F;43505">https:&#x2F;&#x2F;github.com&#x2F;microsoft&#x2F;TypeScript&#x2F;issues&#x2F;43505</a>

`never` is better known as `bottom`. `noreturn` in some languages is the same thing<p>`any`, however, is not `top`, it is `break_the_type_system`. The top type in TS is `unknown`.

I don’t think it is appropriate to say Rust has ‘union types’. Rust has sum types, implemented as Enums and (unsafe) Union types. There is a distinct difference between sum types and union types from a type theoretic perspective.

I think this post should have made a greater distinction between terms and types. The type 4 and the term 4 are separate entities with the same name. Otherwise string &lt;=: string would imply that a function f : string =&gt; int could be called as f(string) on the type of strings (which is actually how they handle it Perl6&#x2F;Raku). Overall it seemed very TS-centric and not much on type theory.

&gt; Like sets, types can be by description have an infinite number of distinct entries<p>I think they might have meant &quot;entities&quot; instead of &quot;entries?&quot;<p>The term &quot;diagonal identity&quot; seems to be non-standard as well?

Could someone here shed some light on &quot;Why the intersection with any is always any&quot;?<p>I didn&#x27;t feel satisfied with the explanation in TFA.

&gt; Free variables and closures<p>Are these even types? I always mentally filed closures under &quot;implementation detail of nested functions&quot;.

Finally, something useful to read