RE: Overlapping, undecidable, incoherent -- or worse?
You don't say what you are trying to achieve. However it looks as if you mean "If you want PO T, for some type T, first try (Bounded T, Enum T, SemiRing T) and if that fails try CSemiRing T. Or maybe the other way round. In any case, GHC simply does not implement this kind of backtracking search. It would make sense, and some of the more exotic users of type classes would like it, but (a) there are numerous tricky corners, and (b) it's awkward to implement the way GHC is now. If the specification was completely clear I might be tempted to fix (b), but it isn't. The main difficulty is that a compiler does not solve constraints "all at once". Instead it does a bit of solving, then then a bit more later. If the "later" part doesn't pan out, it's jolly difficult to go back to the original part (in another module, perhaps) and change it. As a trivial example, try f a = a |= a What type shall we infer for f? f :: (Bounded a, Enum a, SemiRing a) => a -> a or f :: (CSemiRing a) => a -> a Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Alex Ferguson | Sent: 20 May 2004 00:53 | To: glasgow-haskell-users@haskell.org | Subject: Overlapping, undecidable, incoherent -- or worse? | | | The following rings a faint bell from somewhere, but if there's a standard | workaround I can't recall or lay my hand on it currently: | | > class PO a where | > (|=) :: a -> a -> Bool | > | > class Num a => SemiRing a | > | > class SemiRing a => CSemiRing a | > | > instance (Bounded a, Enum a, SemiRing a) => PO a where | > a |= b | > = or [ a + c == b | c <- boundedEnumFrom minBound ] | > | > instance CSemiRing a => PO a where | > a |= b = a + b == b | | The above is in any event requires the "-fallow-undecidable-instances" | flag, due to the format of the instance clauses, and they're worse than | merely "overlapping" due to the identical heads. But I'm not quite | clear why "incoherent" doesn't help here: isn't the gist of that to | allow the second to override the first, where they conflict? Is there | otherwise a means to have it behave in such a way? | | (I can hack around this by removing the distinction betweem the two | classes and encoding it as run-time property (which may get compiled out | statically anyway, and I suspect what I actually want are hierarchical | defaults rather than instances, but that's more like fodder for another | list.) | | Cheers, | Alex. | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones wrote:
As a trivial example, try
f a = a |= a
What type shall we infer for f? f :: (Bounded a, Enum a, SemiRing a) => a -> a or f :: (CSemiRing a) => a -> a
This has always confused me - GHC always seems to use the strongest possible conditions when inferring types (CSemiRing is stronger than PO because it implies it). Why isn't the type just f :: (PO a) => a -> a ? Isn't this the most straight-forward (and universal) typing, especially in the presence of overlapping/undecidable instances? -Stefan
On Thu, May 20, 2004 at 08:52:45AM +0100, Simon Peyton-Jones wrote: | You don't say what you are trying to achieve. However it looks as if | you mean "If you want PO T, for some type T, first try (Bounded T, Enum | T, SemiRing T) and if that fails try CSemiRing T. Or maybe the other | way round. Sorry, I suppose I was a little gnomic. I mean the other way round, ideally. The difference in the remainder of the contexts isn't significant for my purposes, so I could as well have (some redundantly) made the latter declaration:
instance (Bounded a, Enum a, CSemiRing a) => PO a where a |= b = a + b == b
which'd make it strictly more specific than the other. i.e. if it's a CSemiRing, use that, if not but is (only) a semiring If that'd help at all... | In any case, GHC simply does not implement this kind of backtracking | search. It would make sense, and some of the more exotic users of type | classes would like it, but (a) there are numerous tricky corners, and | (b) it's awkward to implement the way GHC is now. If the specification | was completely clear I might be tempted to fix (b), but it isn't. The | main difficulty is that a compiler does not solve constraints "all at | once". Instead it does a bit of solving, then then a bit more later. | If the "later" part doesn't pan out, it's jolly difficult to go back to | the original part (in another module, perhaps) and change it. I can see the possible difficulties all right. Well, enough of them for it to seem... difficult. I'd think this would be relatively easy to do if Haskell had some notion of 'naming' instance declarations, and then of specifying a 'priority' to 'em, but that'd by a pretty significant looking language extension. I'd just gotten the impression that -fallow-incoherent-instances might make some ad hoc 'forcing' choice in such circumstances that might serve my current purposes.
As a trivial example, try
f a = a |= a
What type shall we infer for f? f :: (Bounded a, Enum a, SemiRing a) => a -> a or f :: (CSemiRing a) => a -> a
I'm with Stefan on this one. Surely the type is simply PO a => a -> Bool? Or is there a 'top level binding' issue here? (Surely not, the MR doesn't apply.) Cheers, Alex.
participants (3)
-
Alex Ferguson -
Simon Peyton-Jones -
Stefan Reich