TypeFamilies vs. FunctionalDependencies & type-level recursion

[dm-list-haskell-prime at scs.stanford.edu]

At Tue, 14 Jun 2011 12:31:47 -0400,
Dan Doel wrote:
> 
> Sorry about the double send, David. I forgot to switch to reply-all in
> the gmail interface.
> 
> Okay. I don't really write a lot of code like this, so maybe I missed
> the quirks.
> 
> In that case, HList has been relying on broken behavior of fundeps for
> 7 years. :) Because the instance:
> 
>    instance TypeEq a b c
> 
> violates the functional dependency, by declaring:
> 
>    instance TypeEq Int Int Int
>    instance TypeEq Int Int Char
>    instance TypeEq Int Int Double

No, these are not equivalent.  The first one "TypeEq a b c" is just
declaring an instance that works "forall c".  The second is declaring
multiple instances, which, if there were class methods, could have
different code.  The second one is illegal, because given just the
first two types, a and b, you cannot tell which instance to pick.

>    class C a b | a -> b where
>      foo :: a -> b
>      foo = error "Yo dawg."
> 
>    instance C a b where
> 
>    bar :: Int
>    bar = foo "x"
> 
>    baz :: Char
>    baz = foo "x"
> 
> so we're using an instance C String Int and an instance C String Char
> despite the fact that there's a functional dependency from the first
> argument to the second.

A functional dependency such as "| a b -> c d" just guarantees that a
and b uniquely determine the instance.  Hence, it is okay to have
class methods that do not mention type variables c and d, because the
compiler will still know which instance to pick.

Since your code only has one instance of class C, the unique instance
is trivially guaranteed and the code is fine.  In fact, your code is
effectively the same as:

	class C a where
	  foo :: a -> b
	  foo = error "Yo dawg."

	instance C a where

The same issues happen with type families.  The following code is
obviously illegal, because you have a duplicate instance of class C:

	class C a where
	    type Foo a
	    foo :: a -> Foo a
	    foo = error "Yo dawg."
	instance C [Char] where
	    type Foo [Char] = Int
	instance C [Char] where
	    type Foo [Char] = Char

On the other hand, though the compiler won't accept it, you could at
least theoretically allow code such as the following:

	instance C [Char] where
	    type Foo [Char] = forall b. () => b

David