4 ms·

> For instance, Qi's type inferencing engine is Turing complete Why is that good? Decidability is a nice property of a type system...

• Locke1689 16y ago
  It's not good, it's very bad. Haskell researchers spent years, in fact, attempting to make sure that it was both decidable and ran in less than exponential time. The fact that some people actually think an undecidable type system is an advantage is simply an astounding disconnect from reality.
  • Dn_Ab 16y ago
    This is also an issue in Dependent Types. But the case is not as clear cut as you paint it as some argue that the expressibility lost and complexity gained in the system by forcing type checking to terminate is not worth it in practice. http://www.seas.upenn.edu/~liminjia/research/papers/lambda-eek.pdf http://www.seas.upenn.edu/~liminjia/research/papers/lambda-e...
    • Locke1689 16y ago
      I'm aware of differing opinions, I just think I'm right ;)
  • njs12345 16y ago
    Did they succeed? I vaguely remember a lecture last year where the lecturer told us that type checking in SML was exponential in the worst case ..
    • Locke1689 16y ago
      Type annotations have reduced those cases to very rare instances, but yes there are still cases where the type checker can produce exponential runtime.