TypeFamilies vs. FunctionalDependencies & type-level recursion
Simon Peyton-Jones
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 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 at haskell.org [mailto:haskell-prime-
| bounces at haskell.org] On Behalf Of dm-list-haskell-prime at scs.stanford.edu
| Sent: 14 June 2011 22:39
| To: Dan Doel
| Cc: haskell-prime at 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 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
|
| _______________________________________________
| Haskell-prime mailing list
| Haskell-prime at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-prime
More information about the Haskell-prime
mailing list