3 ms·

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 ext

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 decidable problems with even more insane complexity include provability in Presburger arithmetic (the one where you’re forbidden from multiplying variables together, so avoid the undecidability of Peano) and over the reals (with addition and multiplication only).

apatil 3y ago
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.
- kachnuv_ocasek 3y ago
  It's the size of the term. See this paper which proves the result for details: https://link.springer.com/chapter/10.1007/3-540-52590-4_50 https://link.springer.com/chapter/10.1007/3-540-52590-4_50
  - mmoskal 3y ago
    More specifically, time is almost linear with the size of the type, which can be doubly exponential compared to the program but people don't write such programs.
- disjunction181 3y ago
  It's not that humans don't write such large programs, it's that the kind of pattern that causes the exponential behavior doesn't naturally occur in long chains in any kind of written code. You can provide the pathological inputs yourself and quickly freeze e.g. OCaml's typechecker, they just don't ever naturally occur to the point of becoming a problem. Here's an example of the pathological pattern in OCaml: https://cs.stackexchange.com/questions/6617/concise-example-of-exponential-cost-of-ml-type-inference https://cs.stackexchange.com/questions/6617/concise-example-...
carterschonwald 3y ago
Is there any PDFs of that type system? I tried to dig some up but I found only some post script files about polar type inference
- mananaysiempre 3y ago
  I mean, ps2pdf be with you (it ships with Ghostscript), or, if you must, use a Web service[1]. PostScript was fairly common for papers before PDFTeX and while Adobe still attempted to control PDF using their patents. That said, the System P₂ papers might be more helpful[2,3]. The System P paper[4] is indeed more about the inference algorithm and less about the motivation—perhaps the accompanying slides[5] will help some, alongside the first two papers? [1] https://www.ps2pdf.org/ https://www.ps2pdf.org/ [2] “What are principal typings and what are they good for?” (POPL ’96), https://dl.acm.org/doi/10.1145/237721.237728 https://dl.acm.org/doi/10.1145/237721.237728 [3] “Rank 2 type systems and recursive definitions” (MIT-LCS-TM-531), https://hdl.handle.net/1721.1/149246.2 https://hdl.handle.net/1721.1/149246.2 [4] “A polar type system” (ITRS ’00), http://trevorjim.com/papers/polar.ps.gz http://trevorjim.com/papers/polar.ps.gz or http://www.macs.hw.ac.uk/~jbw/itrs/itrs00/papers/Jim:ITRS-2000.ps.gz http://www.macs.hw.ac.uk/~jbw/itrs/itrs00/papers/Jim:ITRS-20... or https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=3f96631a7352873403df5c7238b050d70f82c27a https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&d... [5] http://www.macs.hw.ac.uk/~jbw/itrs/itrs00/slides/Jim:ITRS-2000:slides.pdf.gz http://www.macs.hw.ac.uk/~jbw/itrs/itrs00/slides/Jim:ITRS-20...
  - carterschonwald 3y ago
    Thx! I was failing to find the related papers

apatil 3y ago

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.

kachnuv_ocasek 3y ago
It's the size of the term. See this paper which proves the result for details: https://link.springer.com/chapter/10.1007/3-540-52590-4_50 https://link.springer.com/chapter/10.1007/3-540-52590-4_50
- mmoskal 3y ago
  More specifically, time is almost linear with the size of the type, which can be doubly exponential compared to the program but people don't write such programs.
disjunction181 3y ago
It's not that humans don't write such large programs, it's that the kind of pattern that causes the exponential behavior doesn't naturally occur in long chains in any kind of written code. You can provide the pathological inputs yourself and quickly freeze e.g. OCaml's typechecker, they just don't ever naturally occur to the point of becoming a problem. Here's an example of the pathological pattern in OCaml: https://cs.stackexchange.com/questions/6617/concise-example-of-exponential-cost-of-ml-type-inference https://cs.stackexchange.com/questions/6617/concise-example-...

carterschonwald 3y ago

Is there any PDFs of that type system? I tried to dig some up but I found only some post script files about polar type inference

mananaysiempre 3y ago
I mean, ps2pdf be with you (it ships with Ghostscript), or, if you must, use a Web service[1]. PostScript was fairly common for papers before PDFTeX and while Adobe still attempted to control PDF using their patents. That said, the System P₂ papers might be more helpful[2,3]. The System P paper[4] is indeed more about the inference algorithm and less about the motivation—perhaps the accompanying slides[5] will help some, alongside the first two papers? [1] https://www.ps2pdf.org/ https://www.ps2pdf.org/ [2] “What are principal typings and what are they good for?” (POPL ’96), https://dl.acm.org/doi/10.1145/237721.237728 https://dl.acm.org/doi/10.1145/237721.237728 [3] “Rank 2 type systems and recursive definitions” (MIT-LCS-TM-531), https://hdl.handle.net/1721.1/149246.2 https://hdl.handle.net/1721.1/149246.2 [4] “A polar type system” (ITRS ’00), http://trevorjim.com/papers/polar.ps.gz http://trevorjim.com/papers/polar.ps.gz or http://www.macs.hw.ac.uk/~jbw/itrs/itrs00/papers/Jim:ITRS-2000.ps.gz http://www.macs.hw.ac.uk/~jbw/itrs/itrs00/papers/Jim:ITRS-20... or https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=3f96631a7352873403df5c7238b050d70f82c27a https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&d... [5] http://www.macs.hw.ac.uk/~jbw/itrs/itrs00/slides/Jim:ITRS-2000:slides.pdf.gz http://www.macs.hw.ac.uk/~jbw/itrs/itrs00/slides/Jim:ITRS-20...
- carterschonwald 3y ago
  Thx! I was failing to find the related papers