overlapping instances and constraints

[Simon Peyton-Jones]

Overlapping instances are undoubtedly useful, but they raise lots of
interesting questions.  Such as

- A program that type checks can have its meaning changed by adding an
instance declaration

- Similarly adding "import M()" can change the meaning of a program (by
changing which instances are visible

- Haskell would need to be a lot more specific about exactly where
context reduction takes place.  Consider
	f xs x = xs == [x]
Do we infer the type (Eq a) => [a] -> a -> Bool?  Thereby committing to
a particular choice of instance?  Or do we (as GHC does) infer the type
(Eq [a]) => [a] -> a -> Bool, so that if f is applied at (say) type
Char, then an instance Eq [Char] instance would apply.  GHC is careful
to do the latter.

- When exactly is overlap permitted?  Is this ok?
	instance C a Int
	instance C Bool b
Previously GHC rejected this, on the grounds that it could be ambiguous
when you came across (C Bool Int).  But not GHC accepts it, on the
grounds that (C Bool Char) is quite unambiguous.  

[Actually this last point is relevant for MPTCs even if overlap isn't
allowed.]


Concerning using the instance context, yes, it's attractive, but it
involves *search* which the current mechanism does not.  Presumably you
have in mind that the type system should "commit" only when there is
only one remaining instance declaration that can fit.  You need to be
very careful not to prune off search branches prematurely, because in a
traditional HM type checker you don't know what all the type are
completely.  And you need to take functional dependencies into account
during the search (but not irrevocably).   I have not implemented this
in GHC.  I don't know anyone who has.   I don't even know anyone who has
specified it.


All good stuff to debate.  I'd be happy to see the traffic on MPTCs
reach half the level that syntax debates do!  In general, I think that
type-system proposals are much easier to evaluate when accompanied with
formal type rules.  It's not just a macho thing -- it really helps in
debugging the dark corners.


Simon

| -----Original Message-----
| From: haskell-prime-bounces at haskell.org
[mailto:haskell-prime-bounces at haskell.org] On Behalf Of
| Claus Reinke
| Sent: 26 February 2006 16:28
| To: haskell-prime at haskell.org
| Subject: overlapping instances and constraints
| 
| 
| the point about overlapping instances is that they shouldn't,
| so we are looking for ways to resolve what looks like overlaps
| unambiguously, so that there are no overlapping instances left.
| 
| we don't want overlapping instances in the language definition,
| but we do want more expressive means of defining non-
| overlapping instances.
| 
| 1. resolving overlaps in favour of the most specific declaration
|     does so, so why is that approach slated as "adopt: probably no"?
| 
|     http://hackage.haskell.org/trac/haskell-prime/ticket/54
| 
| 2. FDs can help to make types in instance declarations more
|     specific, thus avoiding some overlaps or at least helping the
|     "best-match" to resolve overlaps. defaults resolve some of
|     the simplest overlaps (which instance of Num did you mean?),
|     but not others, because their overloading is not expressed in
|     terms of classes (which empty list did you mean?).
| 
| 3. in this context, could someone please remind me what exactly
|     is the reason that class constraints in instance declarations are
|     ignored when deciding whether two instances overlap?
| 
| we have two worlds to consider, the unconstrained world of
| semi-decidable type class programming, and the restricted
| world which guarantees termination of type class inference.
| 
| in the first world, it seems there is no reason not to look at
| the constraints, because there are no termination guarantees
| anyway. and in the second world, it seems there is no reason
| not to look at the constraints, because we know that doing
| so will terminate nicely, thank you.
| 
| so why are some instance declarations still rejected as
| overlapping even if their constraints clearly say they don't?
| 
| cheers,
| claus
| 
| _______________________________________________
| Haskell-prime mailing list
| Haskell-prime at haskell.org
| http://haskell.org/mailman/listinfo/haskell-prime