Idris 2 0.6.0 is now available for the JVM

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.

[ Parent | on HN ]

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

[ Parent | on HN ]