[HN Gopher] Sets, types and type checking
___________________________________________________________________
Sets, types and type checking
Author : kaleidawave
Score : 103 points
Date : 2024-10-30 18:53 UTC (2 days ago)
(HTM) web link (kaleidawave.github.io)
(TXT) w3m dump (kaleidawave.github.io)
| skybrian wrote:
| > 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 wrote:
| 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 wrote:
| 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 wrote:
| 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/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-fo...
|
| I believe Java's checked exceptions behave somewhat like union
| types.
| om2 wrote:
| 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 wrote:
| 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 wrote:
| _> 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 wrote:
| I think they just mean that sum types are defined by the
| programmer using the `enum` keyword
| randomdata wrote:
| 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 wrote:
| Off topic, but rust really messed up the terminology by using
| 'enums' for sum types.
| o11c wrote:
| `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 wrote:
| Adding the unknown type was such a big deal. I love it.
| Nevermark wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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
| klysm wrote:
| 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 wrote:
| 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 wrote:
| Finally, something useful to read
| haileys wrote:
| > _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 wrote:
| 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 wrote:
| > 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 wrote:
| 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 wrote:
| > Free variables and closures
|
| Are these even types? I always mentally filed closures under
| "implementation detail of nested functions".
___________________________________________________________________
(page generated 2024-11-01 23:01 UTC)