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.