[Haskell-cafe] Fundeps and overlapping instances
anthony_clayden at clear.net.nz
Thu May 24 14:14:36 CEST 2012
Simon Peyton-Jones <simonpj <at> microsoft.com> writes:
> [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:
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
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
> Imagine a system “FDL” that has functional dependencies
> and local type constraints. The big deal about this is that you get to
> 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 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
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
So let me cut to SPJ's conclusions, and compare them against dis-overlapped
> 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-
> · never resolve overlap until only a unique instance can possibly
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
> be fine. (I may live to eat my words here.)
More information about the Haskell-Cafe