3 ms·
Wow! This may help with the intuition that typechecking for some type systems is an undecidable problem.
by schoen 3y ago
Wow! This may help with the intuition that typechecking for some type systems is an undecidable problem.
- amenghra 3y agohttps://beza1e1.tuxen.de/articles/accidentally_turing_complete.html 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 3y agoSorry, 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!