[Haskell-cafe] When are undecidables ok?

[Luke Palmer]

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/