Comment by dons
15 years ago
> For instance, Qi's type inferencing engine is Turing complete
Why is that good? Decidability is a nice property of a type system...
15 years ago
> For instance, Qi's type inferencing engine is Turing complete
Why is that good? Decidability is a nice property of a type system...
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.
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-e...
I'm aware of differing opinions, I just think I'm right ;)
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 ..
Type annotations have reduced those cases to very rare instances, but yes there are still cases where the type checker can produce exponential runtime.