[Haskell-cafe] When are undecidables ok?
Michael Snoyman
michael at snoyman.com
Sun Dec 6 00:04:46 EST 2009
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
>>= ...
return ...
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20091205/d6ba84d5/attachment.html
More information about the Haskell-Cafe
mailing list