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.
Thanks in advance!
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.
Thanks in advance!
The page Hindley–Milner type system - Wikipedia gives the following references:
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)
...
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
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.