TypeFamilies vs. FunctionalDependencies & type-level recursion

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

At Wed, 15 Jun 2011 10:10:14 -0700,
Iavor Diatchki wrote:
> 
> Hello,
> 
> On Wed, Jun 15, 2011 at 12:25 AM, Simon Peyton-Jones <simonpj at microsoft.com>
> 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.

>  The fact that -XUndecidableInstances accepts this is exactly the
> bug that keeps being mentioned on the lists every now and then.  The
> reason that this instance violates the functional dependency is that
> it allows us to conclude both "C [Int] [Bool]", and "C [Int]
> [Char]", and clearly "[Int] = [Int]", but "[Bool] /= [Char]".

If, instead of FunctionalDependencies, the extension were called
ChooseInstancesWithoutKnowingAllTypeVariables, would you still have
this objection?

In other words, is the problem that the name FunctionalDependencies
conveys the wrong intuition and makes it sound like classes should
behave like non-polymorphic functions, or do you think there is
something inherently problematic (beyond non-termination of the type
checker) with lifting the coverage condition?

I mean it's easy to get the behavior you want from
FunctionalDependencies.  All you have to do is declare an instance for
a ground type.  But conversely, if you eliminated the ability to lift
the coverage condition, all kinds of useful stuff would no longer be
possible.  Particularly since type safety is not the issue here, I'd
rather have the more general option available.

> The general rule defining an FD on a class like "C" is the following logical
> statement:
> "forall a b1 b2.  (C a b1, C a b2) => (b1 = b2)"

And in fact b1 and b2 are equal, up to alpha-conversion.  They are
both just free type variables.  Suppose instead we had the following
code:

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

   class C a b | a -> b where
     getb :: a -> b

   instance C Bool Int where
     getb _ = 0
   instance C Char [b] where
     getb _ = []
   instance C Int  [b] where
     getb _ = []

We are saying that when a is a bool, getb gets you an Int.  When a is
a Char or an Int, getb returns a list of any type that you want.
What's so wrong with that?

Really this boils down to the question of whether it makes sense to
say that non-ground types can be equal.  I think it does.  Consider
the following two functions:

	  f1 :: String -> a
	  f1 = error

	  f2 :: String -> b
	  f2 = error

Doesn't it make sense to say that f1 and f2 have the same type, even
though, yes, for f1 the free type variable happens to be called "a",
and for f2 it happens to be called "b"?

> With simple instances (no contexts) it is easy to check if a set of instances
> is consistent with the FDs of the classes, however when we have conditional
> instance the task is harder.  This is why we have approximations that ensure
> consistency (e.g., the Coverage Condition).  My understanding is that the
> coverage condition in GHC ensures both consistency with the FDs, and
> termination of the process.  In the past we had another condition,  which
> ensured consistency but not necessarily termination (I forget its name now
> but, basically, the rule said that all variables in the target of an FD should
> be determined from the variables in the source of the FD, but we can use FDs
> in the context of the instance).

I think you are thinking of the Paterson condition and the Coverage
condition.  They are both still required, and both simultaneously
lifted by -XUndecidableInstances.  See here:

	http://www.haskell.org/ghc/docs/7.0-latest/html/users_guide/type-class-extensions.html#instance-rules

David