Need help understanding the Coverage Condition
L.S., I have difficulty understanding the Coverage Condition. Hopefully, someone has the time and is willing to explain this to me. Obviously, I went ahead and hacked together something horribly entangled, but I found a small example that already shows the behaviour I do not understand. Type-level addition of Church numerals: {- begin -} {-# OPTIONS -fglasgow-exts #-} data Z -- Zero data S x -- Successor of x class Add a b c | a b -> c instance Add Z q q instance Add p q r => (S p) q (S r) {- end -} The error GHCi produces is: Illegal instance declaration for `Add (S x) y (S z)' (the Coverage Condition fails for one of the functional dependencies; Use -fallow-undecidable-instances to permit this) In the instance declaration for `Add (S x) y (S z)' Failed, modules loaded: none. I checked the user guide (7.4.4.1) for criteria for functional dependencies and checked that I do not violate the assertions. I don't violate assertions 1a and 1b, but assertion 2 (the coverage condition) I have trouble reading: The coverage condition. For each functional dependency, tvc_left -> tvs_right, of the class, every type variable in S(tvs_right) must appear in S(tvs_left), where S is the substitution mapping each type variable in the class declaration to the corresponding type in the instance declaration. In my mind, in this case: tvs_left = {a,b} tvs_right = {c} S(tvs_left) = {p,q} S(tvs_right) = {r} What "occur in" means (mappings of type variables occurring in mappings of other type variables), I really don't quite understand. The example in the manual under 7.4.4.2, viz: instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v seams related, but unfortunately is not elaborated upon beyond "[it] does not obey the coverage condition" The suggested flag to "allow undecidable instances" is throwing me off, since it seems very unambiguously decidable to me. Regards, Philip
Philip K.F. H??lzenspies wrote: [snip]
{- begin -} {-# OPTIONS -fglasgow-exts #-}
data Z -- Zero data S x -- Successor of x
class Add a b c | a b -> c instance Add Z q q instance Add p q r => (S p) q (S r)
{- end -}
[snip]
The coverage condition. For each functional dependency, tvc_left -> tvs_right, of the class, every type variable in S(tvs_right) must appear in S(tvs_left), where S is the substitution mapping each type variable in the class declaration to the corresponding type in the instance declaration.
In my mind, in this case: tvs_left = {a,b} tvs_right = {c} S(tvs_left) = {p,q} S(tvs_right) = {r}
What "occur in" means (mappings of type variables occurring in mappings of other type variables), I really don't quite understand. The example in the manual under 7.4.4.2, viz:
It's subset check. S(tvs_right) must be a subset of S(tvs_left) which is clearly not the case. The condition is sufficient (but not necessary) to let type checking terminate.
The suggested flag to "allow undecidable instances" is throwing me off, since it seems very unambiguously decidable to me.
Ambiguity is not the issue here, ensuring termination is. The consequence of using -fundecidable-instances is that there is no a priori guarantee that type checking will terminate. [*] If it does terminate, the final result will be correct. HTH, Bertram [*] In your particular example termination will probably be guaranteed by a structural property: In deriving Add (S x) y (S z) the compiler will look for an instance Add x y z where all three type terms are smaller. The nice thing about the coverage condition is save and can be checked easily per instance.
Philip Have you read "Understanding functional dependencies via Constraint Handling Rules"? http://research.microsoft.com/~simonpj/papers/fd-chr If not, I urge you to consider doing so. It goes into the whole thing in great detail. I'm submerged for the next 3 weeks, though others may be able to help you. Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of | Philip K.F. Hölzenspies | Sent: 04 July 2007 09:33 | To: glasgow-haskell-users@haskell.org | Subject: Need help understanding the Coverage Condition | | L.S., | | I have difficulty understanding the Coverage Condition.
On Wed, Jul 04, 2007 at 05:35:44PM +0100, Simon Peyton-Jones wrote:
Have you read "Understanding functional dependencies via Constraint Handling Rules"? http://research.microsoft.com/~simonpj/papers/fd-chr
If not, I urge you to consider doing so. It goes into the whole thing in great detail. I'm submerged for the next 3 weeks, though others may be able to help you.
Simon, I knew I had a "to read" scribbled down in the back of my mind somewhere, but it had slipped out. I will read that paper and see how far I get (although it still seems that it should be possible to relax the covering condition somewhat, being that the example I gave is decidable on paper ;) ) Thank you for the reference. Regards, Philip
participants (3)
-
Bertram Felgenhauer -
Philip K.F. Hölzenspies -
Simon Peyton-Jones