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