Simon Peyton-Jones
[from 7 Jul 2010. I've woken up this thread at Oleg's instigation http://www.haskell.org/pipermail/haskell-prime/2011-July/003491.html ]
I'm not going to talk about Fundeps. This is about introducing overlapping instances into type families. But I mean dis-overlapped overlaps, with dis- equality guards on the instances: http://www.haskell.org/pipermail/haskell-prime/2012-May/003689.html This is essentially the same proposal as the July 2011 discussion, but a little updated with actual experience of type families in their more mature form. Example type family equations: type instance F Int = Bool type instance F a | a /~ Int = [a] -- explicit dis-equality guard The July 2010 thread shows how prescient SPJ was about introducing overlaps into type families (or FunDeps). The requirements he ends up with are spot-on, and I believe I have anticipated them in the proposal for dis-overlapped overlaps.
Imagine a system “FDL” that has functional dependencies and local type constraints. The big deal about this is that you get to
exploit
type equalities in *given* constraints. Consider Oleg’s example, cut down a bit:
class C a b | a -> b
instance C Int Bool
newtype N2 a = N2 (forall b. C a b => b)
t2 :: N2 Int
t2 = N2 True
We end up type-checking (True :: forall b. C Int b => b). From the functional dependency we know that (b~Bool), so the function should typecheck. GHC rejects this program; FDL would not.
GHC 7.2.1 still rejects this program, but accepts a version re-written to use type families: type family CF a type instance CF Int = Bool newtype N2 a = N2 (CF a) -- could be = N2 (forall b. b ~ CF a => b) t2 :: N2 Int t2 = N2 True
But making use of these extra equalities in “given” constraints is quite tricky. To see why look first at ... [snip]
SPJ works through 4 examples, gathering "tricky" and "nasty" situations that are unsound. The examples involve overlaps, so can't be rewritten to use type families. (And GHC rejects attempts to encode them with type classes avoiding fundeps + "a functional-dependency-like mechanism (but using equalities) for the result type".) So let me cut to SPJ's conclusions, and compare them against dis-overlapped overlaps ...
So FDL must
· embody eager checking for inconsistent instances, across modules
(Type families already implement this, SPJ notes below.) Yes: I expect dis-overlapped overlaps to do this. (Eager checking is Hugs' approach FWIW, and although at first it seems a nuisance, it leads to more 'crisp' development. Contrast GHC compiles inconsistent instances, but then you find you can't reach them, or get obscure failures.) Eager checking also detects and blocks the irksome imported-instances- silently-changing-behaviour behaviour.
· never resolve overlap until only a unique instance can possibly match
Yes-ish -- instance matching doesn't have to be as strict as that: type inference must gather evidence of the dis-equality(s) in the guards before matching to the type function equation. Because the instances can't overlap, it's safe to apply the instance, as soon as the dis-equality(s) are discharged, and the head matches.
· put all overlapping instances in a single module
I don't think we need this, providing each instance 'stands alone' with its dis-equality guards. Instead, for each imported module, we validate that its instances, do not overlap, taking the guards into account. [SPJ admits that such a restriction "loses part of the point of overlap in the first place."]
Type families already implement the first of these. I believe that if we added the second and third, then overlap of type families would be fine. (I may live to eat my words here.)
AntC