There's nothing particularly good or particularly bad about a Turing-undecidable type system. For example, typing the lambda calculus is undecidable, but that doesn't make the lambda calculus bad. What IS a problem is a type system that tries too hard to make things "easy" on the programmer. Thus, PL/I's type system was insufficiently strict, that it was too "easy" to write really, really slow programs, and programs that had too many surprising hidden type conversions. With C++'s overloading, essentially _every_ C++ program appears to be an entry into an "obfuscated C" contest. The ML/Haskell typing system is a pretty decent tradeoff between having to declare everything and having to declare nothing. If you really work at it, you can cause the ML/Haskell typing system to work very hard (e.g., blowing up the space required--exponentially?), but mostly it just works. The hygiene required by this typing system is also good for documentation: Common Lisp could have benefited tremendously by utilizing a similar type system. At 10:33 AM 6/8/2014, Warren D Smith wrote:
My view: if it is Turing-undecidable whether you have written a legal program, then it was a bad programming language.
So if this is true, Ceylon is bad (C++ definitely bad by this criterion).