[Haskell-cafe] When are undecidables ok?

[Michael Snoyman]

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>
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20091206/1fd1ce2b/attachment.html