Show HN: Program will only compile if the grid on line 30 is a magic square (typescriptlang.org) 10 points by amenghra 2y ago ↗ HN
[–] amenghra 2y ago ↗ It's ugly and hardcoded for a 3x3 grid. Can we improve this?Slightly better: https://www.typescriptlang.org/play?#code/PTAEBUAsEsGdQA4CcD... [–] amenghra 2y ago ↗ Tada: https://www.typescriptlang.org/play?#code/PTAEBUAsEsGdQA4CcD...
[–] schoen 2y ago ↗ Wow! This may help with the intuition that typechecking for some type systems is an undecidable problem. [–] amenghra 2y ago ↗ https://beza1e1.tuxen.de/articles/accidentally_turing_comple... lists a few type-related things.Type inference has been proven to be undecidable in some cases (e.g. with dependent types). [–] schoen 2y ago ↗ Sorry, by "the intuition that..." I didn't mean "reason to believe (a result that isn't established)" but more like "an aid to understanding (a result that was already proven)".Thanks for the link!
[–] amenghra 2y ago ↗ https://beza1e1.tuxen.de/articles/accidentally_turing_comple... lists a few type-related things.Type inference has been proven to be undecidable in some cases (e.g. with dependent types). [–] schoen 2y ago ↗ Sorry, by "the intuition that..." I didn't mean "reason to believe (a result that isn't established)" but more like "an aid to understanding (a result that was already proven)".Thanks for the link!
[–] schoen 2y ago ↗ Sorry, by "the intuition that..." I didn't mean "reason to believe (a result that isn't established)" but more like "an aid to understanding (a result that was already proven)".Thanks for the link!
5 comments
[ 1.6 ms ] story [ 20.8 ms ] threadSlightly better: https://www.typescriptlang.org/play?#code/PTAEBUAsEsGdQA4CcD...
Type inference has been proven to be undecidable in some cases (e.g. with dependent types).
Thanks for the link!