[Haskell-cafe] Comparison of functional dependencies and type families [was: Re: Type families not as useful over functions]

[Manuel M T Chakravarty]

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