TypeFamilies vs. FunctionalDependencies & type-level recursion

[Dan Doel]

On Tue, Jun 14, 2011 at 5:36 AM, Simon Peyton-Jones
<simonpj at microsoft.com> wrote:
> There was an interesting thread on haskell-prime [1], about the relationship between functional dependencies and type families.  This message is my attempt to summarise the conclusions of that thread.  I'm copying other interested parties (eg Oleg, Dimitrios)
>  [1] http://www.haskell.org/pipermail/haskell-prime/2011-May/003416.html
>
> 1. As things stand in GHC you can do some things with functional dependencies that you can't do with type families. The archetypical example is type equality.  We cannot write
>        type family Eq a b :: *
>        type instance Eq k k = True
>        type instance Eq j k = False
> because the two instances overlap.  But you can with fundeps
>        class Eq a b c | a b -> c
>        instance Eq k k True
>        instance Eq j k False
> As Alexey mentioned, fundeps have other disadvantages, so it's reasonable to ask whether type families could extend to handle cases like this.

Fundeps no longer allow this as of GHC 7, it seems. It causes the same
fundep violation as the case:

    class C a b | a -> b
    instance C a R
    instance C T U

for R /~ U. Which I find somewhat sensible, because the definitions
together actually declare two relations for any type:

    Eq T T False
    Eq T T True

and we are supposed to accept that because one is in scope, and has a
particular form, the other doesn't exist. But they needn't always be
in scope at the same time.

Essentially, GHC 7 seems to have separated the issue of type-function
overlapping, which is unsound unless you have specific conditions that
make it safe---conditions which fundeps don't actually ensure (fundeps
made it 'safe' in the past by not actually doing all the computation
that type families do)---from the issue of instance overlapping, which
is always sound at least. But if I'm not mistaken, type families can
handle these cases.

I'd personally say it's a step in the right direction, but it probably
breaks a lot of HList-related stuff.

-- Dan