<div dir="ltr"><br><br><div class="gmail_quote">On Sun, Dec 6, 2009 at 7:36 AM, Luke Palmer <span dir="ltr">&lt;<a href="mailto:lrpalmer@gmail.com">lrpalmer@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div class="im">On Sat, Dec 5, 2009 at 10:04 PM, Michael Snoyman &lt;<a href="mailto:michael@snoyman.com">michael@snoyman.com</a>&gt; wrote:<br>
&gt; I know this is basically a rewording of a previous e-mail, but I realized<br>
&gt; this is the question I *really* wanted to ask.<br>
&gt;<br>
&gt; We have this language extension UndecidableInstances (not to mention<br>
&gt; OverlappingInstances), which seem to divide the Haskell camp into two<br>
&gt; factions:<br>
&gt;<br>
&gt; * Hey, GHC said to turn on this flag. Ok!<br>
&gt; * Undecidables are the devil!<br>
&gt;<br>
&gt; I get the feeling the truth lies in the middle. As I understand it (please<br>
&gt; correct me if I am wrong), the problem with undecidables is that they can<br>
&gt; create non-terminating instances. However, for certain cases the programmer<br>
&gt; should be able to prove to him/herself that the instances will terminate. My<br>
&gt; question is: how can you make such a proof?<br>
<br>
</div>Well, the reasoning for the &quot;devil&quot; camp (which I admit to being<br>
firmly in[1]) is that such proofs must rely on the algorithm the<br>
compiler uses to resolve instances.  You might be able to prove it,<br>
but the proof is necessarily only valid for (possibly current versions<br>
of) GHC.  The typeclass resolution algorithm is not in the report, and<br>
there are several conceivable ways of of going about it.<br>
<br>
So it is fine to use them if you are okay with making your code<br>
unportable and future-brittle. I am typically against the mere<br>
existence of code that that is future-brittle, because it encourages<br>
compiler authors not to innovate  (and by that token, unportable too,<br>
because it discourages compiler competition).<br>
<br>
Luke<br>
<br>
[1] <a href="http://lukepalmer.wordpress.com/2008/04/08/stop-using-undecidable-instances/" target="_blank">http://lukepalmer.wordpress.com/2008/04/08/stop-using-undecidable-instances/</a><br></blockquote><div><br>So in that case, perhaps the compiler authors can give us some ideas as to when it&#39;s safe to use undecidables? Seems like we should go straight to the horse&#39;s mouth.<br>
<br>Michael <br></div></div><br></div>