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

21–30 of 36 posts

Re: Sets, types and type checking

#21

Post by randomdata »

haileys wrote: post #16

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

Yes, technically it is closer to (T | null) & {__tag: K}, but the context where "equivalent" is used is clearly about practical usage. Option is most similar to T | null in code people actually write on a normal basis.

Re: Sets, types and type checking

#22

Post by randomdata »

tubthumper8 wrote: post #19
randomdata wrote: post #17

Earlier quoted context omitted.

> 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

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.

Re: Sets, types and type checking

#23

Post by matt_kantor »

tubthumper8 wrote: post #20
Nevermark wrote: post #10

Earlier quoted context omitted.

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

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

Re: Sets, types and type checking

#24

Post by marcosdumay »

haileys wrote: post #16

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

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

Re: Sets, types and type checking

#25

Post by tubthumper8 »

matt_kantor wrote: post #23
tubthumper8 wrote: post #20

Earlier quoted context omitted.

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

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

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

Re: Sets, types and type checking

#26

Post by kaba0 »

haileys wrote: post #16

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

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?

Re: Sets, types and type checking

#27

Post by kaba0 »

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.

Off topic, but rust really messed up the terminology by using 'enums' for sum types.

Re: Sets, types and type checking

#29

Post by Nevermark »

tubthumper8 wrote: post #25
matt_kantor wrote: post #23

Earlier quoted context omitted.

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

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

If we step away from any particular language:

If I give you a reference, address, or some other identifier, for something you know nothing else about, you can't do anything with the reference but pass it on. You have no information about the thing itself. You don't even know how to dereference the reference.

Whatever it is that I gave you a reference for, is unknown to you.

Now if I say, go ahead and give me some thing, with no constraints, you can give me any thing.

Which without further information, will just be a reference to an unknown to me.

Mathematically, "unknown" and "any" both represent something without any constraints or information known about them, but in opposite roles.

But one is when you receive a reference to something you know nothing else about, the other is when you provide something without any requirement to give any information about it.

The two roles necessarily happen simultaneously in that exchange.

--

I expect in most languages that "unknown" and "any" gets used, this gets watered down.

Most languages provide some kind of baseline information with the "things" in it. For instance, objects whose type can be always be queried via reflection, or some other baseline accessible information.

Also, languages use words differently. So maybe they are not consistent with the unknown/any symmetry I described at all.

Re: Sets, types and type checking

#30

Post by James_K »

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 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.
Post reply on HN