3 ms·

I guess, unsoundness sounds concerning. But is undecidability? When this is an issue, it's always because someone worked to do some really elaborate or general

by abeppu 6y ago

I guess, unsoundness sounds concerning. But is undecidability? When this is an issue, it's always because someone worked to do some really elaborate or general compile-time computation. It seems a lot (literally too much) to ask that you can do really unrestrained type-level computation and also still always have termination.

enricozb 6y ago
I think this is an important point to focus on when writing a new type-safe language. LEAN for example has a very impressive type system (honestly seems like magic sometimes), and clearly all of the "impossibility" is shoved into the computational complexity of the type-checker. Despite the fact that some of the languages listed here have undecidable type systems, it doesn't feel like many common-purpose languages have purposefully gone down the undecidable route to bring some really cool type-safety.
mhh__ 6y ago
I agree. If undecidability (or some stricter but still off-putting set)in a given language means an extremely complicated compiler that would be a mark against it, but if it's just an obscure edge case or something that is already not possible in a normal language, then I really don't care. I would, however, like to see termination analysis applied to code more often - e.g. rather like only accepting a pure function in an interface, this function must terminate but might not be pure.
gjulianm 6y ago
To me, unsoundness doesn't sound too concerning. It is a theoretical property, and when programming I care about practice, which means that I care about consistency and predictability. If a type system is unsound because of certain edge cases, but works well in practice and those edge cases case an error later anyways, I don't care too much. I mean, most typed languages will have casting operators that can make unsafe operations precisely because programmers sometimes want to bypass the type system. Why sacrifice usability in the name of 'soundness' when in practice people are just going to bypass the type system when that happens?
- mixedCase 6y ago
  >To me, unsoundness doesn't sound too concerning Just debug enough TypeScript and it will sound concerning.
- robinei 6y ago
  Soundness gives an important benefit: Performance, for a compiler capable of utilising the type information properly. It can omit run-time checks, and unbox primitives etc.
habitue 6y ago
To your point, the example of Idris is sound and decidable, but in practice the decidability doesn't matter: you add fuel[1] to limit recursion, but it can just be some arbitrarily large number (but not infinite) number of loops. [1] https://www.idris-lang.org/docs/current/contrib_doc/docs/Data.Fuel.html https://www.idris-lang.org/docs/current/contrib_doc/docs/Dat...
lmm 6y ago
It might seem a lot, but Idris shows that it's possible.

by abeppu 6y ago

enricozb 6y ago

I think this is an important point to focus on when writing a new type-safe language. LEAN for example has a very impressive type system (honestly seems like magic sometimes), and clearly all of the "impossibility" is shoved into the computational complexity of the type-checker. Despite the fact that some of the languages listed here have undecidable type systems, it doesn't feel like many common-purpose languages have purposefully gone down the undecidable route to bring some really cool type-safety.

mhh__ 6y ago

I agree. If undecidability (or some stricter but still off-putting set)in a given language means an extremely complicated compiler that would be a mark against it, but if it's just an obscure edge case or something that is already not possible in a normal language, then I really don't care. I would, however, like to see termination analysis applied to code more often - e.g. rather like only accepting a pure function in an interface, this function must terminate but might not be pure.

gjulianm 6y ago

To me, unsoundness doesn't sound too concerning. It is a theoretical property, and when programming I care about practice, which means that I care about consistency and predictability. If a type system is unsound because of certain edge cases, but works well in practice and those edge cases case an error later anyways, I don't care too much. I mean, most typed languages will have casting operators that can make unsafe operations precisely because programmers sometimes want to bypass the type system. Why sacrifice usability in the name of 'soundness' when in practice people are just going to bypass the type system when that happens?

mixedCase 6y ago
>To me, unsoundness doesn't sound too concerning Just debug enough TypeScript and it will sound concerning.
robinei 6y ago
Soundness gives an important benefit: Performance, for a compiler capable of utilising the type information properly. It can omit run-time checks, and unbox primitives etc.

habitue 6y ago

To your point, the example of Idris is sound and decidable, but in practice the decidability doesn't matter: you add fuel[1] to limit recursion, but it can just be some arbitrarily large number (but not infinite) number of loops. [1] https://www.idris-lang.org/docs/current/contrib_doc/docs/Data.Fuel.html https://www.idris-lang.org/docs/current/contrib_doc/docs/Dat...

lmm 6y ago

It might seem a lot, but Idris shows that it's possible.