Just for the record, here a few clarifications. Expressiveness ~~~~~~~~~~~~~~ From a theoretical point of view, type families (TFs) and functional dependencies (FDs) are equivalent in expressiveness. There is nothing that you can do in one and that's fundamentally impossible in the other. See also Related Work in <http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html
. In fact, you could give a translation from one into the other.
Haskell ~~~~~~~ This simple equivalence starts to break down when you look at the use of the two language features in Haskell. This is mainly because there are some syntactic contexts in Haskell, where you can have types, but no class contexts. An example, are "newtype" definitions. Implementation in GHC ~~~~~~~~~~~~~~~~~~~~~ The situation becomes quite a bit more tricky once you look at the interaction with other type system features and GHC's particular implementation of FDs and TFs. Here the highlights: * GADTs: - GADTs and FDs generally can't be mixed (well, you can mix them, and when a program compiles, it is type correct, but a lot of type correct programs will not compile) - GADTs and TFs work together just fine * Existential types: - Don't work properly with FDs; here is an example: class F a r | a -> r instance F Bool Int data T a = forall b. F a b => MkT b add :: T Bool -> T Bool -> T Bool add (MkT x) (MkT y) = MkT (x + y) -- TYPE ERROR - Work fine with TFs; here the same example with TFs type family F a type instance F Bool = Int data T a = MkT (F a) add :: T Bool -> T Bool -> T Bool add (MkT x) (MkT y) = MkT (x + y) (Well, strictly speaking, we don't even need an existential here, but more complicated examples are fine, too.) * Type signatures: - GHC will not do any FD improvement in type signatures; here an example that's rejected as a result (I assume Hugs rejects that, too): class F a r | a -> r instance F Bool Int same :: F Bool a => a -> Int same = id -- TYPE ERROR (You may think that this is a rather artificial example, but firstly, this idiom is useful when defining abstract data types that have a type dependent representation type defined via FDs. And secondly, the same situation occurs, eg, when you define an instance of a type class where one method has a class context that contains a type class with an FD.) - TFs will be normalised (ie, improved) in type signatures; the same example as above, but with a TF: type family F a type instance F Bool = Int same :: F Bool -> Int same = id * Overlapping instances: - Type classes with FDs may use overlapping instances (I conjecture that this is only possible, because GHC does not improve FDs in type signatures.) - Type instances of TFs cannot use overlapping instances (this is important to ensure type safety) It's a consequence of this difference that closed TFs are a features that is requested more often than closed classes with FDs. Manuel PS: Associated types are just syntactic sugar for TFs, there is nothing that you can do with them that you cannot do with TFs. Moreover, it is easy to use type families for bijective type functions; cf. <http://www.haskell.org/pipermail/haskell-cafe/2009-January/053696.html
. (This follows of course from the equivalence of expressiveness of TFs and FDs.)
Ahn, Ki Yung:
My thoughts on type families:
1) Type families are often too open. I causes "rigid variable" type error messages because when I start writing open type functions, I often realize that what I really intend is not truly open type functions. It happens a lot that I had some assumptions on the arguments or the range of the type function. Then, we need help of type classes to constrain the result of open type functions. For example, try to define HList library using type families instead of type classes with functional dependencies. One will soon need some class constraints. Sometimes, we can use associated type families, but many times it may become tedious when there are multiple arguments and result have certain constraints so that we might end up associating/splitting them over multiple type classes. In such cases, it may be more simple working with functional dependencies alone, rather than using both type classes and type families. I wish we had closed kinds so that we can define closed type functions as well as open type functions.
2) Type families are not good when we need to match types back and forth (e.g. bijective functions), or even multiple ways. We need the help of functional dependencies for these relational definitions. I know that several people are working on the unified implementation for both type families and functional dependencies. Once GHC have common background implementation, type families will truly be syntactic sugar of type classes with functional dependencies, as Mark Jones advocates, or maybe the other way around too.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe