3 ms·

What it means in practice is that any Java typechecker is either (a) incomplete - it will disallow some programs that should typecheck; (b) unsound - it will al

by rntz 10y ago

What it means in practice is that any Java typechecker is either (a) incomplete - it will disallow some programs that should typecheck; (b) unsound - it will allow some programs that shouldn't typecheck; or (c) non-total - it will fail to terminate on some programs. (Or some combination of these three.)

gpderetta 10y ago
No, that's in theory. In practice not much: any practical sufficiently complex type system quickly gets extended to become Turing complete; from time to time the compiler might get yell at you when you hit the maximum allowed type recursion limit, but usually everything just work. I believe that type checking in unextended Hindley-Milner type systems is exponential, so, even if the algo is guaranteed to terminate in theory it might not do so before the heat death of the universe. Again, in practice outside of test cases demonstrating this 'feature' it doesn't matter.
- valarauca1 10y ago
  >I believe that type checking in unextended Hindley-Milner type systems is exponential Yes it recursively solves for function typing parameters though the call graph. This isn't guaranteed to exit. If the language you are using annotates function argument's with types[1] then this behavior is avoided and Hindly-Milner becomes effectively linear. This is why type-inference is starting to become a common feature in most languages. [1] Nearly every language does this, but inline clojure are sometimes type inferred. Depends on language/language family.
- jameshart 10y ago
  "the compiler might get yell at you when you hit the maximum allowed type recursion limit" is an example of the compiler failing to compile something which is valid in the type system.
  - gpderetta 10y ago
    Sure, the point is that it happens rarely with real world code and you can always bump the compiler limit.
    - jameshart 10y ago
      Right, but that's precisely how Turing completeness works. It's possible to write a program that can figure out whether most real world code terminates. All Turing completeness tells you is that no matter how clever that program gets, there will be some programs (not necessarily 'real world programs') which it won't be able to process. The fact that the Java programming language is Turing complete doesn't prevent us being able to write programs in it (indeed it means we can write interesting programs in it!). It is just a result that tells us there are some things we can't say about ALL Java programs. This is a similar result. The fact that the Java type system is turing complete doesn't stop us expressing things with it. It just tells us there are some things we can't say about ALL Java type declarations.

by rntz 10y ago

gpderetta 10y ago

No, that's in theory. In practice not much: any practical sufficiently complex type system quickly gets extended to become Turing complete; from time to time the compiler might get yell at you when you hit the maximum allowed type recursion limit, but usually everything just work. I believe that type checking in unextended Hindley-Milner type systems is exponential, so, even if the algo is guaranteed to terminate in theory it might not do so before the heat death of the universe. Again, in practice outside of test cases demonstrating this 'feature' it doesn't matter.

valarauca1 10y ago
>I believe that type checking in unextended Hindley-Milner type systems is exponential Yes it recursively solves for function typing parameters though the call graph. This isn't guaranteed to exit. If the language you are using annotates function argument's with types[1] then this behavior is avoided and Hindly-Milner becomes effectively linear. This is why type-inference is starting to become a common feature in most languages. [1] Nearly every language does this, but inline clojure are sometimes type inferred. Depends on language/language family.
jameshart 10y ago
"the compiler might get yell at you when you hit the maximum allowed type recursion limit" is an example of the compiler failing to compile something which is valid in the type system.
- gpderetta 10y ago
  Sure, the point is that it happens rarely with real world code and you can always bump the compiler limit.
  - jameshart 10y ago
    Right, but that's precisely how Turing completeness works. It's possible to write a program that can figure out whether most real world code terminates. All Turing completeness tells you is that no matter how clever that program gets, there will be some programs (not necessarily 'real world programs') which it won't be able to process. The fact that the Java programming language is Turing complete doesn't prevent us being able to write programs in it (indeed it means we can write interesting programs in it!). It is just a result that tells us there are some things we can't say about ALL Java programs. This is a similar result. The fact that the Java type system is turing complete doesn't stop us expressing things with it. It just tells us there are some things we can't say about ALL Java type declarations.