News for hackers. Stuff that matters.
Re:Extension Points, or how OCaml is becoming more like Lisp by read on Friday May 09, 2014 @07:17AM (#7720239)
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 mind when you hear that phrase. You don't hear people say "Oh no, that wouldn't be Turing complete". Complete or not, how does it affect a real application?

Re:Extension Points, or how OCaml is becoming more like Lisp by pjc50 on Friday May 09, 2014 @09:58AM (#7720847)
For a type system, being Turing complete is a disadvantage: you can't prove that your typechecker will always terminate.
Re:Extension Points, or how OCaml is becoming more like Lisp by chriswarbo on Friday May 09, 2014 @10:57AM (#7721182)
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.

Re:Extension Points, or how OCaml is becoming more like Lisp by hajile on Friday May 09, 2014 @12:00PM (#7721563)
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.
Re:Extension Points, or how OCaml is becoming more like Lisp by chongli on Friday May 09, 2014 @01:14PM (#7721993)
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.