TypeFamilies vs. FunctionalDependencies & type-level recursion

[Simon Peyton-Jones]

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