[Haskell-cafe] When are undecidables ok?
simonpj at microsoft.com
Mon Dec 7 03:59:54 EST 2009
I don’t think it’s all that complicated or fragile.
To resolve the constraint (C T1 T2), use the appropriate instance declaration to express it in terms of (hopefully simpler) constraints. Keep doing that. If you terminate, GHC should.
Example: to resolve Eq [Int], use the instance declaration
instance Eq a => Eq [a]
That gives rise to the new constraint Eq Int. Use the instance declaration
instance Eq Int
That gives rise to no new instances. Done.
If you terminate and GHC does not, write down your reasoning (ie how you resolved the instance) and send it in.
[NB: There is a wrinkle for “recursive dictionaries”, described in the SYB3 paper.]
Well, the reasoning for the "devil" camp (which I admit to being
firmly in) 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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe