type families not advertised for 6.8
simonpj at microsoft.com
Fri Oct 19 03:25:22 EDT 2007
| What does this imply for 6.8 support for FD's, as they now use
| the same type-coercions?
Actually FDs do not use type coercions, in GHC at least. As Mark originally described them, FDs guide inference; and in particular, they give rise to some unifications that would not otherwise occur. In terms of the intermediate language, that means there is no "evidence" associated with a FD; it's just the type checker's business. That means that various potentially-useful things can't be expressed, notably when FDs are combined with existentials or GADTs, that involve *local* equalities, which were beyond the scope of Marks's original paper.
As the recent thread about FDs shows, FDs are quite tricky, at least if one goes beyond the well-behaved definition that Mark originally gave. (And FDs are much more useful if you go beyond.)
Our current plan is to regard FDs as syntactic sugar for indexed type families. We think this can be done -- see our IFL workshop paper http://research.microsoft.com/%7Esimonpj/papers/assoc-types
No plans to remove them, however. After all, we do not have much practical experience with indexed type families yet, so it's too early to draw many judgements about type families vs FDs.
I recommend Iavor's thesis incidentally, which has an interesting chapter about FDs, including some elegant (but I think unpublished) syntactic sugar that makes a FD look more like a function. I don't think it's online, but I'm sure he can rectify that.
More information about the Glasgow-haskell-users