News for hackers. Stuff that matters.
Re:Idris 2 0.6.0 is now available for the JVM by avgcorrection on Monday February 27, 2023 @09:18AM (#34956644)
That doesn’t make sense. `null | false | true` is not equivalent to `Option<bool>` or `Option<false | true>`. Just like `zero | one | two` is not equivalent to `Option<one | two>`.

Assuming that `true | false` is equivalent to something like `enum { true, false }`.

Re:Idris 2 0.6.0 is now available for the JVM by evomassiny on Monday February 27, 2023 @09:28AM (#34956776)
> Just like `zero | one | two` is not equivalent to `Option<one | two>`

Isn't it ? both cases represent a type than can express 3 variants

Re:Idris 2 0.6.0 is now available for the JVM by valenterry on Monday February 27, 2023 @10:13AM (#34957321)
It is equivalent in the amount of information you can encode, but not in how you can use it.

Classical example is wrapping multiple times: Option<Option<one | two>>. If you have null | null | one | two, well... that just boils down to null | one | two.

Re:Idris 2 0.6.0 is now available for the JVM by Nullabillity on Monday February 27, 2023 @10:14AM (#34957327)
Those two types are indeed equivalent by themselves. The problem comes when you want to store them somewhere nullable. `zero | one | two | zero` flattens back down to `zero | one | two`, you can't distinguish between the two zero/null cases.

On the other hand, `Option<Option<one | two>>` allows you to distinguish between None and Some(None).

This makes union types unsound in the presence of type parameters/generics.

TypeScript supports both anyway, because Hejlsberg cares more about being able to type existing JS antipatterns than about providing a sound type system.

Re:Idris 2 0.6.0 is now available for the JVM by valenterry on Monday February 27, 2023 @11:11AM (#34958073)
> This makes union types unsound in the presence of type parameters/generics.

I'm not sure if "unsound" is a good adjective here. There are cases where this is actually desired behaviour and the rules can definitely be "sound".

For example, I might want to know what errors can appear, but not care where they come from. So `ErrorA | ErrorB` is what I want to see, not some nested structured that allows me to differentiate where ErrorA came from in case that there are multiple possible options.

Re:Idris 2 0.6.0 is now available for the JVM by ObscureScience on Monday February 27, 2023 @03:50PM (#34961688)
I did not catch from you comment if you knew, but "sound" and "unsound" are specific concepts in type theory, and they are binary properties. A system either is or is not sound.
Re:Idris 2 0.6.0 is now available for the JVM by valenterry on Monday February 27, 2023 @04:15PM (#34961953)
Yeah I know that.

So: > This makes union types unsound in the presence of type parameters/generics.

Sounds a bit strange to me. Why would union types + type parameters be generally unsafe? I doubt that that's true.

Re:Idris 2 0.6.0 is now available for the JVM by trenchgun on Tuesday February 28, 2023 @05:16AM (#34967695)
Sound type system is not one of the design goals of TypeScript

https://effectivetypescript.com/2021/05/06/unsoundness/

Re:Idris 2 0.6.0 is now available for the JVM by avgcorrection on Monday February 27, 2023 @11:26AM (#34958294)
No.

There is an isomorphism between them, but they aren’t equivalent since for one you will have to match on the `Option` first in order to see whether it is `None` or `Some(Next)` and then inspect `Next` (if `Some(…)`).

Same reason that `Nothing | Pointer` is not equivalent to `Option<Pointer>`. And it makes a huge practical difference, since the first type allows for “nothing-pointer dereference” while the second one does not.

Re:Idris 2 0.6.0 is now available for the JVM by mixedCase on Monday February 27, 2023 @12:07PM (#34958946)
> And it makes a huge practical difference, since the first type allows for “nothing-pointer dereference”

That's not how strict TypeScript works. If you have a nullable you'll need to prove to the compiler first that it is not currently null before dereferencing.

Re:Idris 2 0.6.0 is now available for the JVM by avgcorrection on Monday February 27, 2023 @12:58PM (#34959691)
Here’s what I originally replied to:

> the type `null | true | false` is different from `true | false`, a type checker can assert that you handle the `null` case before using a function that wants a boolean. This is how rust handles it (with the Option<T> type).

If the variant `null` here is handled specially in general in TS then yeah, I was wrong. However, I was mostly replying to the part about “this is how Rust handles it”.