 What is the runtime of type inference of OCAML - is it EXPTIME?

I was told that type inference (deciding the type of a term or program) in OCAML is EXPTIME. I was wondering why this was true (for such a simple operation), why in practice it’s doable and most importantly a reference for this.

The page Hindley–Milner type system - Wikipedia gives the following references:

• Mairson, Harry G. (1990). “Deciding ML typability is complete for deterministic exponential time”. Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '90 . Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages . POPL '90. ACM. pp. 382–401. doi:10.1145/96709.96748. ISBN 978-0-89791-343-0. S2CID 75336.
• Kfoury, A. J.; Tiuryn, J.; Urzyczyn, P. (1990). ML typability is dexptime-complete . Lecture Notes in Computer Science . CAAP '90. 431 . pp. 206–220. doi:10.1007/3-540-52590-4_50. ISBN 978-3-540-52590-5.

Google helps me to find the following answer lambda calculus - Concise example of exponential cost of ML type inference - Computer Science Stack Exchange for a simple example of exponential behavior:

let f1 x f = f x x
let f2 x = f1 (f1 x)
let f3 x = f2 (f2 x)
let f4 x = f3 (f3 x)
...
5 Likes

it didn’t occur to me to google it as “ML type inference”. Thanks for that and for pointing that out! This is a real dense article that is tough to follow without reading up on hindley-milner inference, but it has some great insights as to how the ocaml inference is so fast: Efficient and Insightful Generalization

1 Like

McAllester (2003) has shown that (under some assumptions about the program), ML type inference takes quasi-linear time in the worst case. This explains why the algorithm behaves well in practice.

3 Likes