On 9/14/07, Thomas Schilling
The type system doesn't help you avoid writing non-terminating programs, so i see no problem with it being possible giving programmers the power to express and check more complex properties of their programs -- as long as type-checking remains sound. From a practical standpoint, non-terminating type checks are just as much a bug as non-terminating library functions. Type systems need more thought anyways, so why not make sure it's terminating, too? The other extreme is to use dependent types everywhere, but this has a bit more drastic consequences to the accessibility and practicality of the language.
While I love all the exceedingly cool type hackery, I also like the compiler to terminate. Some people in this forum may be old enough to remember Turbo Prolog. It did mode inference (i.e. data-flow analysis) on programs, but unfortunately it didn't always terminate. So what you got was a hung compiler, leaving you to guess what it was about your [quite possibly correct] program that caused the analysis to loop. With C++ templates, the problem is addressed by having a limit to the depth of the "call stack" for template evaluation. I recall with Forte 5, there was no flag to let you increase the depth, so at one point we had to do something like if (0) { // Horrible nasty expression to force the evaluation of some of the // the lower parts of the template stack } This works because (at least in Forte 5, and probably most implementations) template instantiations are hash-consed. I would *much* rather have a simpler type system, than a compiler which might not terminate. cheers, T. -- Thomas Conway drtomc@gmail.com Silence is the perfectest herald of joy: I were but little happy, if I could say how much.