Bidirectional typechecking:
| Polymorphism | Predicative | Impredicative |
|---|---|---|
| Rank-0 | Decidable, Complete | - |
| Rank-1/2 | Decidable [3], Complete | Decidable |
| Higher-rank | Decidable, Complete | Undecidable [1,2], Complete with hints [1] |
Hindley-Milner typechecking:
| Polymorphism | Predicative | Impredicative |
|---|---|---|
| Rank-0 | Decidable | - |
| Rank-1/2 | Decidable [3] | |
| Higher-rank | Undecidable [1,2] |
A typechecking algorithm is complete if it can infer types of programs without type annotations.
- [1] Greedy bidirectional polymorphism
- [2] Practical type inference for arbitrary-rank types
- [3] Types and Programming Languages
Tags: type theory