On Thursday, 22 October 2020 at 19:24:53 UTC, Bruce Carneal wrote:
On a related topic, I believe that type functions enable a large amount of code in the "may be hard to prove decidable" category (templates) to be (re)written as clearly decidable code. Easier for the compiler to deal with and, more importantly, easier to teach.
Type functions, like regular functions, are Turing-complete, and therefore undecidable in the general case.
