Re: [Haskell-cafe] When are undecidables ok?

On Sun, Dec 6, 2009 at 7:36 AM, Luke Palmer wrote:

...

I know this is basically a rewording of a previous e-mail, but I realized this is the question I *really* wanted to ask.

We have this language extension UndecidableInstances (not to mention OverlappingInstances), which seem to divide the Haskell camp into two factions:

* Hey, GHC said to turn on this flag. Ok! * Undecidables are the devil!

I get the feeling the truth lies in the middle. As I understand it (please correct me if I am wrong), the problem with undecidables is that they can create non-terminating instances. However, for certain cases the

On Sat, Dec 5, 2009 at 10:04 PM, Michael Snoyman wrote: programmer

...

should be able to prove to him/herself that the instances will terminate. My question is: how can you make such a proof?

Well, the reasoning for the "devil" camp (which I admit to being firmly in[1]) is that such proofs must rely on the algorithm the compiler uses to resolve instances. You might be able to prove it, but the proof is necessarily only valid for (possibly current versions of) GHC. The typeclass resolution algorithm is not in the report, and there are several conceivable ways of of going about it.

So it is fine to use them if you are okay with making your code unportable and future-brittle. I am typically against the mere existence of code that that is future-brittle, because it encourages compiler authors not to innovate (and by that token, unportable too, because it discourages compiler competition).

Luke

[1] http://lukepalmer.wordpress.com/2008/04/08/stop-using-undecidable-instances/

So in that case, perhaps the compiler authors can give us some ideas as to when it's safe to use undecidables? Seems like we should go straight to the horse's mouth. Michael