In type theories where type checking is decidable do we have estimates for how much time/space it takes to find a typing derivation tree of a valid typing judgment? Do any published references do this kind of analysis?

  • 1
    $\begingroup$ You are asking about the complexity of type inference? In practise, type inference in ML-like languages is fast, so for a long time it was believed that the problem is in P. Then Mairson, Kfoury, Tiuryn, and Urzyczyn show that polymorphic type inference is EXPTIME-complete. The algorithm works well in practise b/c the 'bad' parameter is nesting depth of let. But human programmers never nest deeply. It can be shown that under the assumption that types have bounded size and that programs have bounded "scheme depth", type inference may be performed in quasi-linear time. $\endgroup$ Mar 23 at 12:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy