| 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.

Simon


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Reply via email to