TypeFamilies vs. FunctionalDependencies & typelevel recursion
Simon PeytonJones
simonpj at microsoft.com
Wed Jun 15 00:20:02 CEST 2011
Some brief rejoinders.
1. Golly, functional dependencies are tricky aren't they? A big reason I like type families better is simply that I can understand them.
2. Thank you for correcting my equality example. The code I gave
> class Eq a b c  a b > c
> instance Eq k k True
> instance Eq j k False
doesn't work, and has never worked. The form that does work is
> class Eq a b c  a b > c
> instance Eq k k True
> instance (r~False) => Eq j k r
3. There have been some questions about soundness and fundeps. Don't worry. I'm certain GHC's implementation fundeps is sound. Fundeps in GHC are used *only* to add extra equality constraints that do some extra unifications. (Yes this is a statement about the type inference algorithm, rather than about the type system. I don't know how to give a satisfactory nonalgorithmic treatment of fundeps.)
GHC then translates the typechecked program into System FC, and (if you use dcorelint) is redundantly typechecked there (no fundeps involved). So, no soundness worries: GHC may reject a program you want it to accept, but a program it accepts won't go wrong at runtime. [Barring the notorious Trac #1496]
4. Dan asks why
instance (r~False) => Eq j k r
could possibly differ from
instance Eq j k False
The reason is this. You could imagine permitting this:
instance C a => C [a]
instance D a => C [a]
meaning "to satisfy C [a] try to satisfy C a. Failing that, you can instead try D a". So constraint solving would need a search process. But Haskell doesn't do that. It insists that instance "heads", C [a] in this case, are distinct. (Usually nonoverlapping.) So the instance head (Eq j k r) is different from (Eq j k False); the latter matches more often, but then requires (r~False).
Simon
 Original Message
 From: haskellprimebounces at haskell.org [mailto:haskellprime
 bounces at haskell.org] On Behalf Of dmlisthaskellprime at scs.stanford.edu
 Sent: 14 June 2011 22:39
 To: Dan Doel
 Cc: haskellprime at haskell.org
 Subject: Re: TypeFamilies vs. FunctionalDependencies & typelevel recursion

 At Tue, 14 Jun 2011 15:09:02 0400,
 Dan Doel wrote:
 >
 > On Tue, Jun 14, 2011 at 1:19 PM,
 > <dmlisthaskellprime 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
 righthand 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 typelevel 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 righthand 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
 superuseful 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

 _______________________________________________
 Haskellprime mailing list
 Haskellprime at haskell.org
 http://www.haskell.org/mailman/listinfo/haskellprime
More information about the Haskellprime
mailing list