Idris 2 0.6.0 is now available for the JVM

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.

[ Parent | on HN ]

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.

[ Parent | on HN ]

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.

[ Parent | on HN ]

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/

[ Parent | on HN ]