A practical (and solvable in practical cases!) EXPTIME-complete problem is type inference (or even typability) in the ML type system (that is Hindley–Milner extended with let-polymorphism) or in Trevor Jim’s much nicer System P₂ (equivalently rank-2 intersection types; a fortiori his System P; no, I’m not going to stop shilling System P, it’s too neat to not have a language built upon it at least once). Interesting d…
That's very interesting. In which variable is type inference EXPTIME complete? Whichever variable it is, I suppose in practice humans can't create programs that are big enough in that way for type inference to become impractical. However, I wonder whether someone could comment on what this means about the utility of HM-like type systems in future AI generated software.
Here's an example of the pathological pattern in OCaml: https://cs.stackexchange.com/questions/6617/concise-example-...