[Haskell-cafe] When are undecidables ok?
michael at snoyman.com
Sun Dec 6 01:20:09 EST 2009
On Sun, Dec 6, 2009 at 7:36 AM, Luke Palmer <lrpalmer at gmail.com> wrote:
> On Sat, Dec 5, 2009 at 10:04 PM, Michael Snoyman <michael at snoyman.com>
> > 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
> > correct me if I am wrong), the problem with undecidables is that they can
> > create non-terminating instances. However, for certain cases the
> > should be able to prove to him/herself that the instances will terminate.
> > question is: how can you make such a proof?
> Well, the reasoning for the "devil" camp (which I admit to being
> firmly in) 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).
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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe