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