18 ms·
For languages with Hindley-Milner typing, like SML and OCaml, it has long been known that type-checking is even worse in the worst case (DEXPTIME hard) [1]. But
by lower 5y ago
For languages with Hindley-Milner typing, like SML and OCaml, it has long been known that type-checking is even worse in the worst case (DEXPTIME hard) [1]. But the programs where this matters aren't what one would write by hand, typically.
[1] https://dl.acm.org/doi/10.1145/96709.96748 https://dl.acm.org/doi/10.1145/96709.96748
- contravariant 5y agoTo some extent it wouldn't even be surprising for a sufficiently powerful language to be EXPSPACE. Pretty much anything with sufficiently powerful macros would be EXPSPACE, or worse.
- Ericson2314 5y agoNote that is is polynomial with respect to the size of the output. That is to say, pathological expressions don't stay small but induce horrendous searching, but rather merely get a log bigger (and that can cause more trouble for the rest of the program). That means a heuristic to bail out when something grows a lot probably not violate the users intent and get it back into polynomial time.
- chalst 5y agoNo, this is the time complexity of type checking before any computation on the terms is performed.
- Ericson2314 5y agoYes I am saying that while it is exponential with respect to the input, and it is polynomial with respect to the output.
- lower 5y agoMaybe it's a good idea to add a concrete example (can't edit the reply anymore): OCaml: let x1 = fun y -> (y, y) in let x2 = fun y -> x1 (x1 y) in let x3 = fun y -> x2 (x2 y) in let x4 = fun y -> x3 (x3 y) in let x5 = fun y -> x4 (x4 y) in let x6 = fun y -> x5 (x5 y) in x6 (fun z -> z) Haskell: test = let x1 = \y -> (y, y) x2 = \y -> x1 (x1 y) x3 = \y -> x2 (x2 y) x4 = \y -> x3 (x3 y) x5 = \y -> x4 (x4 y) x6 = \y -> x5 (x5 y) in x6 (\z -> z) If you can compile these, add x7. The effort increases exponentially as one adds x7, x8 and so on.
- NieDzejkob 5y agoThe fact that x1 is \y -> (y, y) is superficial, though. Something like x1 = Just also increases exponentially, and makes clear that using a deduplicated DAG for representing type terms doesn't solve this.
- lower 5y agoWith x1 = Just, the program is accepted instantly by ghc. I think you need a type variable to appear twice.
- NieDzejkob 5y agoAh, it's still exponential, but in the size of the type, and the constants of the complexity are a bit different, so you need around x30.
- lower 5y agoAh, you're right. If one goes to x_{i+1}, then there will be 2^i Maybes in the type. The number of Maybe-occurrences in the type doubles in each step and sharing won't help there.
- daxfohl 5y agoFormerly id id id id id id id id id... would do it, but looks like someone has put in a fix for that.
- lower 5y agoYes, types are usually represented by a DAG with sharing. OCaml does so, for example, and I assume ghc does something similar. So, while id id has type ('a -> 'a) -> ('a -> 'a), this is stored in memory by a pointer structure that amounts to let 'b = ('a -> 'a) in ('b -> 'b). The type of id id id would become let 'b = ('a -> 'a) in let 'c = ('b -> 'b) in ('c -> 'c). This grows linearly. If one were to write out the types without sharing then their size would grow exponentially.