No Termination Checking

Originally my PhD had an element in it on Termination Checking, and since someone asked on IRC how that bit was going, I thought I'd let everyone know that my PhD now doesn't include termination checking - there are several reasons why:

Related Work

Not long before I started working on the termination thing, this piece of work came out: Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages. That does a really good job. The authors behind that paper have been working on term rewriting termination for a really long time, and have built up a very powerful framework. Their encoding of Haskell into their framework means they have a very powerful tool - based on years of experience. I don't think I could hope to come anywhere near that.

Less Motivation

I want the tool I produce to solve a practical problem. I want it to be something that people can use on a daily basis. In Haskell termination is rarely a problem, and if it is, usually the problem occurs in all circumstances - not just the corner cases (of course there are exceptions, but this is my overall impression). A lot of termination issues relate to variables being bound unexpectedly, lazy evaluation and black holes - and these will occur on any sufficient test input. Once non-termination has occured, there is no point in running a static checker - use a dynamic tool such as Hat-Nonterm or Black-Hat - both specially designed to pinpoint the cause. These factors mean that my motivation to work on a termination checker is less - I don't see it as fulfiling a massive practical need in Haskell. (I know some will disagree, but this is the reason for me not doing it, not for others not doing it - motivation is a personal thing)

Hard to Proove

If you have a static checker, there are two main reasons for using it - to obtain a proof of safety and to find real bugs. It is most useful when the issues that are spotted can be worked around in some way, so that even if they were not a valid problem, afterwards you can obtain a statically checked version that you can gurantee will terminate for all inputs. Pattern-match checking has this property, by completing the patterns or performing extra (potentially redundant) checks, you can be sure all patterns are safe. From my understanding, termination checking does not - to introduce a decreasing variable into an algorithm that does not already have one is a lot of work, and potentially requires a rethink of the entire algorithm. For this reason, even with the help of a willing programmer, I see termination checking as something that will obtain less successful results than I would like.