3 ms·

I think people focus on the "turing complete" part of type checking a bit too much - what's more compelling (and a real design decision) is that when designing

by duped 5y ago

I think people focus on the "turing complete" part of type checking a bit too much - what's more compelling (and a real design decision) is that when designing a type system you need to choose if the type checking algorithm is decidable. That's not usually an accident, since when implementing the system you need to write the type checker, and you'll see quite plainly if it has an infinite loop case.

ReleaseCandidat 5y ago
A turing complete type system is undecidable.
- silon42 5y ago
  I think it's tolerable if the recursion limit is low, preferably single digit.
- duped 5y ago
  My point is that's not as interesting or practical as a type system for which you can write an expression that can't be checked. They may be roughly equivalent, but only one is esoteric.