[Haskell] really undecidable instances?

Simon Peyton-Jones simonpj at microsoft.com
Tue Oct 18 04:24:05 EDT 2005

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


| -----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,
| > responsibility for termination.  Without the flag, GHC uses a simple
| > sometimes over-conservative rule
| >
| > Simon
| [Could you please put citations at the top of the respective mail?]
| Section of the GHC User's guide says about the restrictions
| 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
| removed.  Why isn't this allowed then?
| Best wishes,
| Wolfgang
| _______________________________________________
| Haskell mailing list
| Haskell at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell

More information about the Haskell mailing list