5 ms·

Thank you for Shen Lisp, I wasn't aware of it. The downside of the phrase Turing complete is that there isn't a practical limitation that instantly comes to mi

• pjc50 12y ago
  For a type system, being Turing complete is a disadvantage: you can't prove that your typechecker will always terminate.
  • chriswarbo 12y ago
    The result is even stronger: we can prove that it will sometimes not terminate! Still that's not too bad, since type checking is always conservative: if a program passes, we know it's correct(ly typed). If it doesn't pass, we don't gain any knowledge: it may be incorrect, or it may be correct in a way which the type checker's limited algorithm cannot determine (ie. a Goedel sentence). I'm very concerned whether my programs terminate/coterminate, since having to kill them part-way-through could cause corruption and other nastiness. Whether the type-checker terminates or not I don't really care about; I can just kill it after a certain timeout and keep fiddling with my code until it passes, just like any other type error. Of course, a timeout removes Turing-completeness, but that timeout is under my control at the commandline, rather than being an inherent property of the algorithm.
  • hajile 12y ago
    This is only partially true. The type system is only unable to prove termination if you choose to use those constructs which may disallow termination.
    • chongli 12y ago
      I don't know about you but I'd rather not have my type checker hang and force me to interrupt the process all the time.