On Sun, Dec 6, 2009 at 7:36 AM, Luke Palmer <[email protected]> wrote:
> On Sat, Dec 5, 2009 at 10:04 PM, Michael Snoyman <[email protected]> > 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 > 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
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
