> A decision problem is decidable if for any input we can compute whether the input satifies the problem in finite time. Examples of decidable problems include primality testing and boolean satisfiability. The halting problem for example is undecidable: We cannot check whether a program runs infinitely long in finite time.
This isn't important for type systems though. Any undecidable type system can trivially be made decidable by putting a cap on how many instructions you can run when evaluating the type. Such limitations works really well in practice since useful types takes relatively little to evaluate, and you can put it as a compiler option in the few edge cases where someone needs a huge complicated type that goes above the cap.
This isn't important for type systems though. Any undecidable type system can trivially be made decidable by putting a cap on how many instructions you can run when evaluating the type. Such limitations works really well in practice since useful types takes relatively little to evaluate, and you can put it as a compiler option in the few edge cases where someone needs a huge complicated type that goes above the cap.