Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Sets, types and type checking

kaleidawave.github.io

Post reply on HN
Print view View original

11–20 of 36 posts

Re: Sets, types and type checking

#11

Post by nikeee »

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 (aYou 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

Re: Sets, types and type checking

#12

Post by noelwelsh »

om2 wrote: post #9
jasdfasd wrote: post #7

Earlier quoted context omitted.

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 excepti…

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.

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.

Re: Sets, types and type checking

#14

Post by klysm »

nikeee wrote: post #11

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…

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.

Re: Sets, types and type checking

#15

Post by thechao »

nikeee wrote: post #11

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…

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?

Re: Sets, types and type checking

#16

Post by haileys »

> In Rust we have Option, 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>` 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` 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.

Re: Sets, types and type checking

#17

Post by randomdata »

throwaway17_17 wrote: post #4

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.

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

Re: Sets, types and type checking

#19

Post by tubthumper8 »

randomdata wrote: post #17
throwaway17_17 wrote: post #4

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.

> 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 gene…

I think they just mean that sum types are defined by the programmer using the `enum` keyword

Re: Sets, types and type checking

#20

Post by tubthumper8 »

Nevermark wrote: post #10
o11c wrote: post #5

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

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

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

Post reply on HN