There was an interesting thread on haskell-prime [1], about the relationship 
between functional dependencies and type families.  This message is my attempt 
to summarise the conclusions of that thread.  I'm copying other interested 
parties (eg Oleg, Dimitrios)
  [1] http://www.haskell.org/pipermail/haskell-prime/2011-May/003416.html

1. As things stand in GHC you can do some things with functional dependencies 
that you can't do with type families. The archetypical example is type 
equality.  We cannot write
        type family Eq a b :: *
        type instance Eq k k = True
        type instance Eq j k = False
because the two instances overlap.  But you can with fundeps
        class Eq a b c | a b -> c
        instance Eq k k True
        instance Eq j k False
As Alexey mentioned, fundeps have other disadvantages, so it's reasonable to 
ask whether type families could extend to handle cases like this.

2.  In a hypothetical extension to type families, namely *closed* type 
families, you could support overlap:
        closed type family Eq a b :: * where
          type instance Eq k k = True
          type instance Eq j k = False
The idea is that you give all the equations together; matching is 
top-to-bottom; and the type inference only picks an equation when all the 
earlier equations are guaranteed not to match.  So there is no danger of making 
different choices in different parts of the program (which is what gives rise 
to unsoundness).

3.  Closed type families are not implemented yet.  The only tricky point I see 
would be how to express in System FC the proof that "earlier equations don't 
match".   Moreover, to support abstraction one might well want David's /~ 
predicate, so that you could say
        f :: forall a b. (a /~ b) => ..blah..
This f can be applied to any types a,b provided they don't match.   I'm frankly 
unsure about all the consequences here.

4.  As Roman points out, type families certainly do support recursion; it's 
just they don't support overlap.

5.  David wants a wiki page fixed.  But which one? And how is it "locked down"?

6. There is a very old Trac wiki page about "total" type families here
        http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions/TotalFamilies
Written by Manuel, I think it needs updating.

That's my summary!

Simon

_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime

Reply via email to