TypeFamilies vs. FunctionalDependencies & type-level recursion

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

At Tue, 14 Jun 2011 15:09:02 -0400,
Dan Doel wrote:
> 
> On Tue, Jun 14, 2011 at 1:19 PM,
> <dm-list-haskell-prime at scs.stanford.edu> wrote:
> > 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.
> 
> Then why am I not allowed to write:
> 
>     class C a b | a -> b
>     instance C T [a]
> 
> without undecidable instances? GHC actually complains in that case
> that the coverage condition is violated. But it is a single well
> specified instance that works for all a.

Undecidable instances are orthogonal to both FunctionalDependencies
and OverlappingInstances.  They concern whether or not the compiler
can guarantee that the typechecker will terminate.  You can have
undecidable instances without either of the other two extensions, for
instance:

	{-# LANGUAGE FlexibleInstances #-}

	class A a
	class B a
	instance (A a) => B a	-- illegal w/o UndecidableInstances

The coverage condition is part of a pair of pair of sufficient (but
not necessary) conditions that GHC applies to know that typechecking
is decidable.  It just says that if you have a dependency "a -> b",
and you have type variables in b, then they should mention all the
type variables in a.  Thus, the following code is legal without
UndecidableInstances:

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

	class A a b | a -> b
	instance A [a] (Either String a)

But the following program is not:

	class A a b | a -> b
	instance A a (Either String b)

> The answer is that such an instance actually violates the functional
> dependency, but UndecidableInstances just turns off the checks to make
> sure that fundeps are actually functional. It's a, "trust me," switch
> in this case (not just a, "my types might loop," switch).

No, that's not right.  Even with UndecidableInstances, you cannot
define conflicting instances for functional dependencies.  Moreover,
just because the GHC's particular typechecker heuristics don't
guarantee the above code is decidable doesn't mean it isn't decidable.

> So I guess HList will still work fine, and UndecidableInstances are
> actually more evil than I'd previously thought (thanks for the
> correction, Andrea :)).

I think you are thinking of UndecidableInstances in the wrong way.
For instance, the following code does not require
UndecidableInstances, but has polymorphic type variables on the
right-hand side of a functional dependency, which seems to be what you
object to:

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

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

	instance C (Either a b) (Maybe b) where
	    foo _ = Nothing

	bar :: Maybe Int
	bar = foo (Left "x")

	baz :: Maybe Char
	baz = foo (Left "x")

Remember, FunctionalDependencies are all about determining which
instance you select.  The functional dependency "class C a b | a -> b"
says that for a given type a, you can decide which instance of C
(i.e., which particular function foo) to invoke without regard to the
type b.  It specifically does *not* say whether or not type b has to
be grounded, or whether it may include free type variables, including
just being a type variable if you enable FlexibleInstances:

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

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

	instance C (Either a b) b where  -- no UndecidableInstances needed
	    foo _ = undefined

> > 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.
> 
> It specifies that a and b uniquely determine c and d, so the choice of
> instances is unambiguous based only on a and b.

Yes, but it doesn't say the c and d are ground types.  c can be
(Maybe c'), or, with flexible instances it can just be some free type
variable c''.

> This is the basis for type level computation that people do with
> fundeps, because a fundep 'a b -> c' allows one to compute a unique
> c for each pair of types.

Again, unique but not grounded.  Either Maybe c or "forall c" is a
perfectly valid unique type, though it's not grounded.  People do
weird type-level computations with fundeps using types that aren't
forall c.  (The compiler will fail if you additionally have an
instance with forall c.)

> Being allowed to elide variables from the types of methods is one of
> the uses of fundeps, and probably why they were introduced, but it is
> not what fundeps mean.

I think the reason you have the right-hand side is so you can
say things like "| a -> b, b -> a".

But anyway, even if you think of fundeps as primarily being functions
on types, those functions can be polymorphic.  Just as it's not
super-useful to have functions like "f :: String -> a" other than
error, people often don't do this for fundeps.  But relaxing the
coverage condition still doesn't lead to conflicting functional
dependencies.  No combination of flags to GHC will allow you to have
conflicting functional dependencies.

David