TypeFamilies vs. FunctionalDependencies & type-level recursion

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

At Wed, 15 Jun 2011 16:54:24 -0700,
Iavor Diatchki wrote:
> 
>     >     | >    class C a b | a -> b where
>     >     | >      foo :: a -> b
>     >     | >      foo = error "Yo dawg."
>     >     | >
>     >     | >    instance C a b where
>     >
>     >     Wait.  What about
>     >            instance C [a] [b]
>     >
>     > No, those two are not different, the instance "C [a] [b]" should also be
>     > rejected because it violates the functional dependency.
>    
>     But now you are going to end up rejecting programs like this:
>    
>            {-# LANGUAGE MultiParamTypeClasses #-}
>            {-# LANGUAGE FunctionalDependencies #-}
>            {-# LANGUAGE UndecidableInstances #-}
>    
>            class C a b | a -> b
>            class D a b | a -> b
>            instance (D a b) => C [a] [b]
>    
>     And a lot of useful code (including HList) depends on being able to do
>     things like the above.
> 
> Nope, this program will not be rejected because "b" is in the FD closure of
> "a".  This stuff used to work  a few GHC releases back, and I think that this
> is the algorithm used by Hugs.

What do you mean "b" is in the FD closure of A (particularly since the
code above does not contain any instances of class D)?  Would you also
disallow the following code on the grounds that b is not in the FD
closure of a'?

	class C a a' b | a a' -> b
	class D a b | a -> b
	instance (D a b) => C [a] [a'] [b]

What about the following?

	class C a b | a -> b, b -> a
	instance C [a] [a]

Can you give a specific example of code that you believe worked in GHC
a few releases back but that doesn't work now (or vice versa)?

I still don't understand if you object to the name
FunctionalDependencies, or if you think there's something inherently
bad with allowing code such as the above.

> A functional dependency on a class imposes a constraint on the valid class
> instances  (in a similar fashion to adding super-class constraints to a
> class).

Exactly.  It's a constraint on *instances*, not on classes or types.
It says that in a situation such as the following:

    class C a b | a -> b

You can define "instance C Int Bool", or "instance C Int Char", or
even "instance C Int a".  But you cannot define more than one such
instance, because for a given first argument, whatever you use as the
second argument has to be unique (up to alpha conversion).  If you
want, you can even define overlapping instances, so long as they agree
in the final argument:

	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE FunctionalDependencies #-}
	{-# LANGUAGE UndecidableInstances #-}
	{-# LANGUAGE OverlappingInstances #-}
	{-# LANGUAGE FlexibleInstances #-}

	class C a b | a -> b
	instance C (m a) [b]
	instance C (Maybe a) [c]  -- alpha-conversion is okay, because
                                  -- (forall b. [b]) ~ (forall c. [c])

Once you've bought into OverlappingInstances and
FunctionalDependencies, ruling out code such as the above is akin to
ruling out functions such as "error :: String -> a".  You can object
that, hey, error is not a function!  I mean, if I call it twice on the
exact same argument, I get two different things back:

    error "Same" :: Int
    error "Same" :: Bool

But it's more useful to think of error as returning bottom, which has
all types, and to think of error's type signature as saying: "for a
given argument, you always get back the same thing, but that thing
happens to have all possible types."

Would you be happier if I used bottom as a type variable?

	class C a b | a -> b where
            f :: a -> b
	instance C [a] [bottom] where
            f _ = []

There's only one function f here.  It always returns the same list.
But that list happens to be a valid list of every possible type.

> For any three ground types "a", "b1", and "b2", if we can prove that
> both "C a b1" and "C a b2" hold, then "b1" and "b2" must be the same
> type.   The theory of functional dependencies comes from
> databases.  In that context, a class corresponds to the schema for a
> database table (i.e., what columns there are, and with what
> types).   An instance corresponds to a rule that adds row(s) to the
> table.   With this in mind, the rule that I wrote above exactly
> corresponds to the notion of a functional dependency on a database
> table.

I think we are going around in circles.  Is the point to be faithful
to the database community, or to make it easier to program?
UndecidableInstances, in their current form, pose no danger of making
it into the Haskell standard, but they do make it easier to program,
sometimes drastically reducing code size or clutter, eliminating
boilerplate, and making code less error-prone.  I don't think anyone
is disputing that they fill some unmet need.  So why don't we fix the
name, and not reduce polymorphism.

But just to make sure people don't agree with me too quickly, here's a
more elaborate example that should make the non-believers scream:

	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE FunctionalDependencies #-}
	{-# LANGUAGE UndecidableInstances #-}
	{-# LANGUAGE OverlappingInstances #-}
	{-# LANGUAGE FlexibleInstances #-}

	class C a b | a -> b
	instance C [a] [b]
	instance C [m a] [Either b c]
	instance C [[a]] [Either a c]

David