Hacker News Reader

Comment by abeppu | Hacker News Reader

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.

View on HN

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?

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.

>To me, unsoundness doesn't sound too concerning

Just debug enough TypeScript and it will sound concerning.

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.

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.

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/Dat...

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

Reply on news.ycombinator.com