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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
