When are undecidables ok?

6 Dec 2009

      ...
...
= ...
  return ...
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?

I've had to cases in particular that made me want undecidables. Both of
them, IMO, could be solved by creating new extensions to GHC which would not
require undecidables. Nonetheless, for now we only have undecidables at our
disposal. The examples are:

* Context synonyms (eg, MonadFailure = Monad + Failure).
* Subclass function defaulting

For an example of the second, a nifty definition of Monad would be:

class Applicative m => Monad m where
  pure = return
  (<*>) = ap
  fmap = liftM

Of course, neither of these is possible in Haskell, so we can use
undecidables. How can a programmer prove that a set of instances is, in
fact, safe? And if they make a mistake and right a bad set of
undecidable/overlapping instances, what's the worst case scenario? Is it a
compile-time or run-time error*?

Michael

* Yes, I mean error.

Michael Snoyman

Luke Palmer

Michael Snoyman

Simon Peyton-Jones

tags

participants (3)