🚀 go-pugleaf

  >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