[Haskell] really undecidable instances?

[Simon Peyton-Jones]

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 at haskell.org [mailto:haskell-bounces at 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 at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell