🚀 go-pugleaf

In article <3283@stl.stc.co.uk>, tom@nw.stl.stc.co.uk (Tom Thomson) writes:
> ...
> Even if I restrict myself to compile-time type checking, there doesn't
> appear to be any reason to restrict myself to type checking which is 
> guaranteed to terminate (since I can probably write programs which won't
> terminate at run time, why should I insist they terminate at compile time?)
>  - but maybe that wasn't your point?
> ...

That was roughly my point (I think :-). I think the problem with your idea for
enhanced type checking is that it puts type checking algorithms into a
completely
different ballpark. There are enough problems with the time complexity etc. of
current type checkers (which don't even scratch the surface of what you are
suggesting).

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.

Dave.