RE: [Haskell-cafe] When are undecidables ok?
I don’t think it’s all that complicated or fragile. To resolve the constraint (C T1 T2), use the appropriate instance declaration to express it in terms of (hopefully simpler) constraints. Keep doing that. If you terminate, GHC should. Example: to resolve Eq [Int], use the instance declaration instance Eq a => Eq [a] That gives rise to the new constraint Eq Int. Use the instance declaration instance Eq Int That gives rise to no new instances. Done. If you terminate and GHC does not, write down your reasoning (ie how you resolved the instance) and send it in. [NB: There is a wrinkle for “recursive dictionaries”, described in the SYB3 paper.] Simon 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. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] When are undecidables ok?
On Sun, Dec 6, 2009 at 7:36 AM, Luke Palmer wrote: > On Sat, Dec 5, 2009 at 10:04 PM, Michael Snoyman > 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] When are undecidables ok?
On Sat, Dec 5, 2009 at 10:04 PM, Michael Snoyman 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/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
