Simon Peyton-Jones wrote:
It's all very delicate. I believe, though I am not certain, that in the
absence of functional dependencies, removing at least one type
constructor might be an example of a rule that is sufficient to ensure
termination. There are lots of such rules. Alas none known to me
capture all cases.
Of course they couldn't - because of undecidability of termination
(of term rewriting, or Prolog-like programs).
But then, there are a lot of (nontrivially) decidable subcases,
and consequently there are quite a few automated methods
for termination proofs,
see http://www.lri.fr/%7Emarche/termination-competition/2005/
Would it be interesting to "beef up" the termination analysis in ghc a
bit, using some of those methods?
But then, the current solution is just use "-fundecidable.."
and the see if the type checker (apparently) loops.
This might still be more efficient than invoking a larger machinery
that would prove (non)termination because after the proof
you'd still have to invest the time into doing the rewrite sequence.
Best regards,
--
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
