RE: [Haskell] really undecidable instances?
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. Functional dependencies make things much worse. Suppose you have instance C Int a => D Char [a] which looks safe enough. But now class C x y | x -> y instance D Char [b] => C Int [[b]] and now we loop. There's a paper on my home page explaining why functional dependencies are tricky (co-authored with Martin Sulzmann, Peter Stuckey and Gregory Duck). Simon | -----Original Message----- | From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Wolfgang | Jeltsch | Sent: 17 October 2005 16:12 | To: Haskell ML | Subject: Re: [Haskell] really undecidable instances? | | Am Montag, 17. Oktober 2005 15:57 schrieben Sie: | > This one | | [That is the instance declaration instance C Int a => D Char [a].] | | > can't. But it's hard to formulate a general rule. | > -fallow-undecidable-instances simply says that you, the programmer, take | > responsibility for termination. Without the flag, GHC uses a simple but | > sometimes over-conservative rule | > | > Simon | | [Could you please put citations at the top of the respective mail?] | | Section 7.4.4.3 of the GHC User's guide says about the restrictions for | ensuring decidability: | | These restrictions ensure that context reduction terminates: each reduction | step removes one type constructor. | | But as far as I can see, in my example there is also one type constructor | removed. Why isn't this allowed then? | | Best wishes, | Wolfgang | _______________________________________________ | Haskell mailing list | Haskell@haskell.org | http://www.haskell.org/mailman/listinfo/haskell
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/ -------
participants (2)
-
Johannes Waldmann -
Simon Peyton-Jones