daniel@dolores.Stanford.EDU (Daniel Weise) (08/07/90)
>I accept your point that since we can write programs that don't >terminate then perhaps we shouldn't worry too much about >non-termination during compilation. However, when you say "why >should I insist THEY terminate at compile time". Your argument >relies on the fact that the only programs which don't terminate at >compile time are the ones which don't terminate at run time. Even >if you didn't mean the "THEY" to have such emphasis then I think >there is still a point to be made : the kind of type checking >algorithm you suggest, which is far more powerful than, for >instance, Milner-style type checking is surely quite likely to fail >to terminate (before you get fed up waiting :-) for valid programs >as well as programs which would not terminate anyway. Hence, you >cannot ignore problems with non-termination and time complexity. In the guise of developing partial evaluators, we have hit precisely the problem of a "type system" that includes concrete values in type descriptors. For example, our partial evaluator can describe pairs whose first element is 5. Furthermore, by including online abstract interpretation into a partial evaluator, one can answer many interesting questions about the program that depend on actual data values. The termination properties of such tools are directly related to the termination of the partial evalutor. (And there are many people working on improving the termination behavior of partial evaluators.) So we aren't so far off from deriving the type of information that Tom wants. (You can read all about it if my POPL paper gets accepted, or ask me for a copy of the technical summary.) Daniel Weise