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 non-algorithmic treatment of fundeps.) GHC then translates the type-checked program into System FC, and (if you use -dcore-lint) 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 non-overlapping.) 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: haskell-prime-bounces@haskell.org [mailto:haskell-prime- | bounces@haskell.org] On Behalf Of dm-list-haskell-prime@scs.stanford.edu | Sent: 14 June 2011 22:39 | To: Dan Doel | Cc: haskell-prime@haskell.org | Subject: Re: TypeFamilies vs. FunctionalDependencies & type-level recursion | | 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@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 | | _______________________________________________ | Haskell-prime mailing list | Haskell-prime@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-prime