Class EXPTIME is defined as follows.
Definition. EXPTIME = ∪p TIME(2p(n)) where p(n) is a polynomial.
EXPTIME is a very large class. It is know that P ⊆ NP ⊆ PSPACE ⊆ EXPTIME, and it is conjectured that all of those inclusions are proper: that is, P ⊂ NP ⊂ PSPACE ⊂ EXPTIME.
P and EXPTIME are defined in terms of deterministic algorithms and both in terms of time. That makes it possible to prove that P ≠ EXPTIME from the hierarchy theorems in Chapter 9.1 of Sipser.
So we know that at least one of the inclusions P ⊆ NP ⊆ PSPACE ⊆ EXPTIME is a proper inclusion. Of course, all of them are conjectured to be proper.
The time hierarchy theorem says that, if you have enough more time, then you can solve more problems.
Time Hierarchy Theorem. Suppose that f(n) is a time-honest function. There is a decision problem that is solvable in O(f(n)) time but not solvable in O(f(n)/log2(n)) time.
For example, there is a problem that can be solved in O(n3) time but that cannot be solved in O(n2) time.
The time hierarchy theorem also implies that there is a problem solvable in time O(2n) but is not solvable in time O(nk) for any k.
Definition. Problem A is EXPTIME-complete if
A ∈ EXPTIME.
For every X ∈ EXPTIME, X ≤p A.
ML is a programming language. It is a typed language, and an ML compiler performs type checking.
But programmers are not required to write any type information in programs. The compiler has to infer type information from the way things are used in the program.
The ML-typability problem is as follows.
Input. An ML program q.
Question. Is q free from type errors?
It turns out that the ML-typability problem is EXPTIME-complete. That means that it is very difficult to solve for some short ML programs.
But that does not mean that it is difficult to solve on all ML programs.
In fact, ML programmers tend naturally to avoid the kinds of programs that are difficult to check. In practice, ML compilers run quickly.
But it should be possible to write a fairly short program that causes a compiler either to crash (typically because it runs out of memory) or to run so long that nobody would be willing to wait for it to finish.
Here is the idea behind an ML program that will overwhelm an ML compiler.
f0(x) = (x,x) f1(x) = f0(f0(x)) f2(x) = f1(f1(x)) f3(x) = f2(f2(x)) f4(x) = f3(f3(x)) f5(x) = f4(f4(x)) f6(x) = f5(f5(x)) f7(x) = f6(f6(x)) f8(x) = f7(f7(x)) f9(x) = f8(f8(x)) f10(x) = f9(f9(x))
The types for a few of those are:
f0 has type α → (α, α).
f1 has type α → ((α, α), (α, α)).
f2 has type α → ((((α, α), (α, α)), ((α, α), (α, α))), (((α, α), (α, α)), ((α, α), (α, α)))).
The type of f3 has 256 α's to the right of →.
The type of f4 has 65536 α's to the right of →.
The type of f5 has 4,294,967,296 α's to the right of →.