[Haskell-cafe] Comparison of functional dependencies and type
families [was: Re: Type families not as useful over functions]
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Sun Feb 15 22:02:48 EST 2009
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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
More information about the Haskell-Cafe
mailing list