[Haskell-cafe] Fundeps and overlapping instances

AntC 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:
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




More information about the Haskell-Cafe mailing list