from Hacker News

Sets, types and type checking

by kaleidawave on 10/30/24, 6:53 PM with 33 comments

  • by haileys on 11/1/24, 1:02 PM

    > In Rust we have Option<T>, which is equivalent to T | null

    No, not true!

    As the author correctly states earlier in the post, unions are not an exclusive-or relation. Unions are often made between disjoint types, but not always.

    This becomes important when T itself is nullable. Let's say T is `U | null`. `Option<Option<U>>` in Rust has one more inhabitant than `U | null | null` in TypeScript - `Some(None)`.

    Union types can certainly be very useful, but they are tricky because they don't compose like sum types do. When writing `Option<T>` 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 does depend on what T is at runtime.

  • by nikeee on 11/1/24, 6:17 AM

    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 "foo".

    Similar to this, I proposed inequality types for TS. They allow constraining a number range. For example, it is possible to have the type "a number that is larger than 1". You can combine them using intersection types, forming intervals like "a number between 0 and 1". Because TS has type narrowing via control flow, these types automatically come forward if you do an "if (a<5)". The variable will have the type "(<5)" inside the if block.

    You can find the proposal here [1]. Personally I think the effort for adding these isn't worth it. But maybe someone likes it or takes it further.

    [1]: https://github.com/microsoft/TypeScript/issues/43505

  • by o11c on 10/31/24, 10:33 PM

    `never` is better known as `bottom`. `noreturn` in some languages is the same thing

    `any`, however, is not `top`, it is `break_the_type_system`. The top type in TS is `unknown`.

  • by throwaway17_17 on 10/31/24, 10:25 PM

    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.

  • by James_K on 11/3/24, 11:12 AM

    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 <=: string would imply that a function f : string => int could be called as f(string) on the type of strings (which is actually how they handle it Perl6/Raku). Overall it seemed very TS-centric and not much on type theory.

  • by skybrian on 10/31/24, 9:08 PM

    > Like sets, types can be by description have an infinite number of distinct entries

    I think they might have meant "entities" instead of "entries?"

    The term "diagonal identity" seems to be non-standard as well?

  • by disqard on 11/1/24, 11:38 PM

    Could someone here shed some light on "Why the intersection with any is always any"?

    I didn't feel satisfied with the explanation in TFA.

  • by Mathnerd314 on 11/1/24, 3:42 PM

    > Free variables and closures

    Are these even types? I always mentally filed closures under "implementation detail of nested functions".

  • by ingen0s on 11/1/24, 8:27 AM

    Finally, something useful to read