Live data from Hacker News

Sets, types and type checking

kaleidawave.github.io

1–10 of 36 posts

Re: Sets, types and type checking

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

Re: Sets, types and type checking

#3
post #2

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

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.

Re: Sets, types and type checking

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

Re: Sets, types and type checking

#7

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.

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.

Re: Sets, types and type checking

#8
post #7

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.

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…

[deleted]

Re: Sets, types and type checking

#9
post #7

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.

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.

Re: Sets, types and type checking

#10
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. Never had a chance to use such types before.)

Post reply on HN