10 ms·

Sets, types and type checking

118 points by kaleidawave 2y ago

skybrian 2y ago
> 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?
- dec0dedab0de 2y ago
  I usually say items or members, but entries basically means the same thing, and js set objects have an entries method, so there is precedence.
throwaway17_17 2y ago
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.
- jasdfasd 2y ago
  disjoint union vs union. Scala3 is the only programming language to implement both AFAIK. C# has a proposal to add both unions and disjoint unions: https://github.com/dotnet/csharplang/blob/main/proposals/TypeUnions.md https://github.com/dotnet/csharplang/blob/main/proposals/Typ... OCaml has polymorphic variants which are open disjoint unions. Kotlin is looking to add union types for errors: https://youtrack.jetbrains.com/issue/KT-68296/Union-Types-for-Errors https://youtrack.jetbrains.com/issue/KT-68296/Union-Types-fo... I believe Java's checked exceptions behave somewhat like union types.
  - deleted 2y ago
    [deleted]
  - om2 2y ago
    What’s the difference between a union type and a disjoint union type? In that C# proposal I couldn’t tell which syntax was which branch of your dichotomy.
    - noelwelsh 2y ago
      disjoint union is sum type / enum / algebraic data type. Defined at the point of declaration. Each case is distinct (hence, disjoint) union is what Typescript has. Defined at the point of use. Cases need not be distinct.
- randomdata 2y ago
  > Rust has sum types, implemented as Enums Do you mean implemented with enums? Enums themselves are not a type. They are a mechanism for value generation, providing automatic numbering (hence enumeration) for constants. Indeed, they, like all values, are ultimately represented by a type, but that type can range from something like a simple integer or something more complex like a tagged union (typically with the generated value being the tag) with different ecosystems favouring different type approaches.
  - tubthumper8 2y ago
    I think they just mean that sum types are defined by the programmer using the `enum` keyword
    - randomdata 2y ago
      Like how subroutines are implemented as Functions. And by Functions you don't mean functions, but rather the letters fn? That is certainly an interesting way to communicate.
- kaba0 2y ago
  Off topic, but rust really messed up the terminology by using 'enums' for sum types.
o11c 2y ago
`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`.
- teaearlgraycold 2y ago
  Adding the unknown type was such a big deal. I love it.
- Nevermark 2y ago
  When someone gives you a truly completely unconstrained object, what they hand you is “unknown”. You don’t even know how to query it to find anything out about it. But you could pass it to someone else. When someone asks you for a completely unconstrained object, the type is “any”. It’s technically the same type from two perspectives. (Not saying this extreme version of the concepts are how they are implemented. Never had a chance to use such types before.)
  - tubthumper8 2y ago
    I don't think this is right, for two reasons: 1. As a nit-pick "unconstrained object" is not best modeled by `unknown` because that includes non-objects as well, there's better types to use for that 2. Someone asking you for any unconstrained data would also be `unknown` `any` is not a type at all, it is an annotation to disable the type system
    - matt_kantor 2y ago
      I suspect they were talking more about general terminology than TypeScript's specific usage of `unknown` and `any`. "This box contains an unknown item" and "I'll accept any item" both sound natural, while "this box contains any item" and "I'll accept an unknown item" both sound weird (to me, anyway).
      - tubthumper8 2y ago
        Hmm, I'm not sure about that interpretation, they said "It’s technically the same type from two perspectives." It's not the same type at all. I do agree with your example of the usage of those words in spoken English, but I don't think that is what we're going for in a discussion in Sets, Types, and Type Checking
nikeee 2y ago
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 https://github.com/microsoft/TypeScript/issues/43505
- klysm 2y ago
  I have no idea what I’m talking about, but it seems like these restricted cases of inequality flow control type checking are very similar in power to dependent types, but don’t require the same level of complexity. It’s nice being able to write imperative proofs of correctness guided by the compiler.
- thechao 2y ago
  We had something like this in Spad — the extension language for the computer algebra system Axiom. They're not terrible to implement; but, utilization was always low. There's amusingly high effort optimizations with range-dependent integral types deduced from flow control around blocks that are tail calls. I mean ... theoretically, yes, we can; but should we?
ingen0s 2y ago
Finally, something useful to read
haileys 2y ago
> 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.
- randomdata 2y ago
  Yes, technically it is closer to (T | null) & {__tag: K}, but the context where "equivalent" is used is clearly about practical usage. Option<T> is most similar to T | null in code people actually write on a normal basis.
- marcosdumay 2y ago
  > but they are tricky because they don't compose like sum types do Just to point that this part is very literally true. They compose perfectly well, but they don't compose on the same way that tagged unions do. Tagged unions compose by function abstraction, untagged ones compose by function dispatching. Maybe one can argue that untagged unions compose in less useful ways. But I've never seen this argument made.
- kaba0 2y ago
  Rich Hickey has a presentation titled 'Maybe Not' that talks about this exact distinction, but he actually argues the reverse (and often criticized quite wildly, even though both sides are sort of right here, I believe). He says that nullability is better [1], as refactoring a function that accepted T to T?, or a function's return type from T? to T are both backwards compatible, while the sum type variants require code change. Your last sentence put the whole argument even better in place in my head, it depending on the runtime is both a blessing and a curse and is what let's us change function signatures in a backwards compatible way, while also what hinders our ability to reason/encode stuff in it statically. [1] I think part of the misunderstanding here between the "two camps" is that some people work on systems that are a closed world. You know and control everything, so an all-encompassing type system that can evolve with the universe itself makes the most sense. Hickey on the other hand worked/works mostly in an area where big systems developed by completely different entities have to communicate with each other with little to no coordination. You can't willy nilly refactor your code and just trust the compiler to do its job, this is the open sea. Also, I think this area is a bit neglected by more modern/hyped languages, e.g. the dynamicism that the JVM has is not really reproduced anywhere anymore?
Mathnerd314 2y ago
> Free variables and closures Are these even types? I always mentally filed closures under "implementation detail of nested functions".
disqard 2y ago
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.
James_K 2y ago
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.
deleted 2y ago
[deleted]

118 points by kaleidawave 2y ago

> 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?

dec0dedab0de 2y ago
I usually say items or members, but entries basically means the same thing, and js set objects have an entries method, so there is precedence.

throwaway17_17 2y ago

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.

jasdfasd 2y ago
disjoint union vs union. Scala3 is the only programming language to implement both AFAIK. C# has a proposal to add both unions and disjoint unions: https://github.com/dotnet/csharplang/blob/main/proposals/TypeUnions.md https://github.com/dotnet/csharplang/blob/main/proposals/Typ... OCaml has polymorphic variants which are open disjoint unions. Kotlin is looking to add union types for errors: https://youtrack.jetbrains.com/issue/KT-68296/Union-Types-for-Errors https://youtrack.jetbrains.com/issue/KT-68296/Union-Types-fo... I believe Java's checked exceptions behave somewhat like union types.
- deleted 2y ago
  [deleted]
- om2 2y ago
  What’s the difference between a union type and a disjoint union type? In that C# proposal I couldn’t tell which syntax was which branch of your dichotomy.
  - noelwelsh 2y ago
    disjoint union is sum type / enum / algebraic data type. Defined at the point of declaration. Each case is distinct (hence, disjoint) union is what Typescript has. Defined at the point of use. Cases need not be distinct.
randomdata 2y ago
> Rust has sum types, implemented as Enums Do you mean implemented with enums? Enums themselves are not a type. They are a mechanism for value generation, providing automatic numbering (hence enumeration) for constants. Indeed, they, like all values, are ultimately represented by a type, but that type can range from something like a simple integer or something more complex like a tagged union (typically with the generated value being the tag) with different ecosystems favouring different type approaches.
- tubthumper8 2y ago
  I think they just mean that sum types are defined by the programmer using the `enum` keyword
  - randomdata 2y ago
    Like how subroutines are implemented as Functions. And by Functions you don't mean functions, but rather the letters fn? That is certainly an interesting way to communicate.
kaba0 2y ago
Off topic, but rust really messed up the terminology by using 'enums' for sum types.

o11c 2y ago

`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`.

teaearlgraycold 2y ago
Adding the unknown type was such a big deal. I love it.
Nevermark 2y ago
When someone gives you a truly completely unconstrained object, what they hand you is “unknown”. You don’t even know how to query it to find anything out about it. But you could pass it to someone else. When someone asks you for a completely unconstrained object, the type is “any”. It’s technically the same type from two perspectives. (Not saying this extreme version of the concepts are how they are implemented. Never had a chance to use such types before.)
- tubthumper8 2y ago
  I don't think this is right, for two reasons: 1. As a nit-pick "unconstrained object" is not best modeled by `unknown` because that includes non-objects as well, there's better types to use for that 2. Someone asking you for any unconstrained data would also be `unknown` `any` is not a type at all, it is an annotation to disable the type system
  - matt_kantor 2y ago
    I suspect they were talking more about general terminology than TypeScript's specific usage of `unknown` and `any`. "This box contains an unknown item" and "I'll accept any item" both sound natural, while "this box contains any item" and "I'll accept an unknown item" both sound weird (to me, anyway).
    - tubthumper8 2y ago
      Hmm, I'm not sure about that interpretation, they said "It’s technically the same type from two perspectives." It's not the same type at all. I do agree with your example of the usage of those words in spoken English, but I don't think that is what we're going for in a discussion in Sets, Types, and Type Checking

nikeee 2y ago

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 https://github.com/microsoft/TypeScript/issues/43505

klysm 2y ago
I have no idea what I’m talking about, but it seems like these restricted cases of inequality flow control type checking are very similar in power to dependent types, but don’t require the same level of complexity. It’s nice being able to write imperative proofs of correctness guided by the compiler.
thechao 2y ago
We had something like this in Spad — the extension language for the computer algebra system Axiom. They're not terrible to implement; but, utilization was always low. There's amusingly high effort optimizations with range-dependent integral types deduced from flow control around blocks that are tail calls. I mean ... theoretically, yes, we can; but should we?

ingen0s 2y ago

Finally, something useful to read

haileys 2y ago

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

randomdata 2y ago
Yes, technically it is closer to (T | null) & {__tag: K}, but the context where "equivalent" is used is clearly about practical usage. Option<T> is most similar to T | null in code people actually write on a normal basis.
marcosdumay 2y ago
> but they are tricky because they don't compose like sum types do Just to point that this part is very literally true. They compose perfectly well, but they don't compose on the same way that tagged unions do. Tagged unions compose by function abstraction, untagged ones compose by function dispatching. Maybe one can argue that untagged unions compose in less useful ways. But I've never seen this argument made.
kaba0 2y ago
Rich Hickey has a presentation titled 'Maybe Not' that talks about this exact distinction, but he actually argues the reverse (and often criticized quite wildly, even though both sides are sort of right here, I believe). He says that nullability is better [1], as refactoring a function that accepted T to T?, or a function's return type from T? to T are both backwards compatible, while the sum type variants require code change. Your last sentence put the whole argument even better in place in my head, it depending on the runtime is both a blessing and a curse and is what let's us change function signatures in a backwards compatible way, while also what hinders our ability to reason/encode stuff in it statically. [1] I think part of the misunderstanding here between the "two camps" is that some people work on systems that are a closed world. You know and control everything, so an all-encompassing type system that can evolve with the universe itself makes the most sense. Hickey on the other hand worked/works mostly in an area where big systems developed by completely different entities have to communicate with each other with little to no coordination. You can't willy nilly refactor your code and just trust the compiler to do its job, this is the open sea. Also, I think this area is a bit neglected by more modern/hyped languages, e.g. the dynamicism that the JVM has is not really reproduced anywhere anymore?

Mathnerd314 2y ago

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

disqard 2y ago

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.

James_K 2y ago

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.

deleted 2y ago

[deleted]