On Tue, Jun 14, 2011 at 1:19 PM, 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. 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). So I guess HList will still work fine, and UndecidableInstances are actually more evil than I'd previously thought (thanks for the correction, Andrea :)).

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. 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. If it were just about variable sets determining the instance, then we could just list those. But I can write: class C a b c d | a b -> c And it will actually be a, b and d that determine the particular instance, but just listing 'a b d', or using the fundep 'a b d -> c' is wrong, because the fundep above specifies that there is a single choice of c for each a and b. So we could have: C Int Int Char Int C Int Int Char Double C Int Int Char Float but trying to add: C Int Int Int Char to the first three would be an error, because the first two parameters determine the third, rather than the first, second and fourth. 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.

On the other hand, though the compiler won't accept it, you could at least theoretically allow code such as the following:

       instance C [Char] where            type Foo [Char] = forall b. () => b

The fundep equivalent of this is not 'instance C [Char] b'. It is: instance C [Char] (forall b. b) except types like that aren't allowed in instances (for good reason in general). The closest you could come to 'instance C T b' would be something like: type instance F T = b except that is probably interpreted by GHC as being (forall b. b). -- Dan

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, | > 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

At Tue, 14 Jun 2011 19:21:38 -0400, Dan Doel wrote:

If this is really about rules for selecting instances unambiguously without any regard to whether some parameters are actually functions of other parameters, then the name "functional dependencies" is pretty poor.

Maybe "functional dependencies" is a poor name. I'm not going to argue it's a good one, just that the extension is quite useful. Despite what the name suggests, it is most useful to think of "| a b -> c d" as meaning "any method that uses types a and b does not need to use types c and d for the compiler to determine a unique instance". Once you start thinking of fundeps that way (and always keep in mind that contexts play no role in instance selection), then I think it gets a bit easier to reason about fundeps.

I know the actual implementation is, too. But it's because of the limited way in which fundeps are used. If I'm not mistaken, if they were modified to interact with local constraints more like type families (that is, correctly :)), then soundness would be a concern with these examples.

I don't think so. Because fundeps (despite the name) are mostly about instance selection, incoherent fundeps won't violate safety. Your program may incoherently chose between methods in multiple instances that should be the same instance, but at least each individual method is type safe. With type families, you can actually undermine type safety, and there's no cheating way to fix this, which is why I think TypeFamilies could by very dangerous when combined with dynamic loading.

I understand why the instance resolution causes these to be different in Haskell. I think the first one is a bad definition by the same criteria (although it is in practice correct due to the constraint), but UndecidableInstances turns off the check that would invalidate it.

Though I realize you are unlikely ever to like lifting the coverage condition, let me at least leave you with a better example of why Undecidable instances are useful. Suppose you want to define an instance of MonadState for another monad like MaybeT. You would need to write code like this: instance (MonadState s m) => MonadState s (MaybeT m) where get = lift get put = lift . put This code fails the coverage condition, because class argument (MaybeT m) does not contain the type variable s. Yet, unlike the compiler, we humans can look at the type context when reasoning about instance selection. We know that even though our get method is returning an s--meaning really "forall s. s", since s is mentioned nowhere else--there is really only one s that will satisfy the MonadState s m requirement in the context. Perhaps more importantly, we know that in any event, if the code compiles, the s we get is the one that the surrounding code (calling get or put) expects. Now if, in addition to lifting the coverage condition, you add OverlappingInstances, you can do something even better--you can write one single recursive definition of MonadState that works for all MonadTrans types (along with a base case for StateT). This is far preferable to the N^2 boilerplate functions currently required by N monad transformers: instance (Monad m) => MonadState s (StateT s m) where get = StateT $ \s -> return (s, s) instance (Monad (t m), MonadTrans t, MonadState s m) => MonadState s (t m) where get = lift get put = lift . put This is not something you can do with type families. So while UndecidableInstances and OverlappingInstances aren't very elegant, the fact that they can reduce source code size from O(N^2) to O(N) is a good indication that there is some unmet need in the base language. David

On Wed, Jun 15, 2011 at 11:36 AM, Simon Peyton-Jones wrote:

|       instance (Monad m) => MonadState s (StateT s m) where |           get = StateT $ \s -> return (s, s) | |       instance (Monad (t m), MonadTrans t, MonadState s m) => |              MonadState s (t m) where |               get = lift get |               put = lift . put

Why do you need the first instance?  Isn't the second sufficient for (StateT s m) as well?

Simon

The second will define /an/ instance for StateT s m, but it'll be the wrong one :) the second instance says 'pass the responsibility for dealing with state to the transformed monad', whereas the StateT wants to deal with the state itself.

On Tue, Jun 14, 2011 at 9:56 PM, wrote:

Maybe "functional dependencies" is a poor name.  I'm not going to argue it's a good one, just that the extension is quite useful. Despite what the name suggests, it is most useful to think of "| a b -> c d" as meaning "any method that uses types a and b does not need to use types c and d for the compiler to determine a unique instance".  Once you start thinking of fundeps that way (and always keep in mind that contexts play no role in instance selection), then I think it gets a bit easier to reason about fundeps.

I wasn't really posting in this thread because I'm confused about how fundeps actually behave in GHC. Rather, I care about what functional dependencies mean, and what they should do, not just what they do actually do in one implementation or another.

I don't think so.  Because fundeps (despite the name) are mostly about instance selection, incoherent fundeps won't violate safety.  Your program may incoherently chose between methods in multiple instances that should be the same instance, but at least each individual method is type safe.  With type families, you can actually undermine type safety, and there's no cheating way to fix this, which is why I think TypeFamilies could by very dangerous when combined with dynamic loading.

I know that the actual, current implementation won't violate type safety. But there are reasonable expectations for how *functional dependencies* might work that would cause problems. Here's an example. class C a b | a -> b instance C Int b foo :: forall a b c d. (C a c, C b d, a ~ b) => a -> b -> c -> d foo _ _ x = x coerce :: forall a b. a -> b coerce = foo (5 :: Int) (5 :: Int) This currently gets complaints about not being able to deduce c ~ d. However, actually reading things as genuine functional dependencies, there's nothing wrong with the logic: a ~ b c ~ F a -- for some F d ~ F b -- for the same F c ~ d The only thing stopping this is that fundeps in GHC don't actually introduce the information that they in theory represent. But this in turn means that they don't fulfill certain usages of type families. This is not inherent to fundeps. Fundeps could interact with local constraints more like type families. And in fact, if fundeps ever become sugar for type families (which is at least possible), then they will (I think) work exactly this way, and the above instance would need to be rejected to avoid unsoundness.

Though I realize you are unlikely ever to like lifting the coverage condition, let me at least leave you with a better example of why Undecidable instances are useful.  Suppose you want to define an instance of MonadState for another monad like MaybeT.  You would need to write code like this:

       instance (MonadState s m) => MonadState s (MaybeT m) where            get = lift get            put = lift . put

This code fails the coverage condition, because class argument (MaybeT m) does not contain the type variable s.  Yet, unlike the compiler, we humans can look at the type context when reasoning about instance selection.

Yes, I'm familiar with the mtl examples. I had forgotten that they actually need the coverage condition to be lifted, but they are similar to the type cast case in that they're (possibly) uncheckably all right. I consider the fact that you need undecidable instances to be an advertisement for type families, though.

 We know that even though our get method is returning an s--meaning really "forall s. s", since s is mentioned nowhere else--there is really only one s that will satisfy the MonadState s m requirement in the context.  Perhaps more importantly, we know that in any event, if the code compiles, the s we get is the one that the surrounding code (calling get or put) expects.

No, the s in the instance does not mean (forall s. s). What it means is that forall s there is an instance for s, where the quantification is outside the instance. The difference is significant. If we move to explicit dictionary construction and arbitrary rank types, it'd look like: instance (MonadState s m) => MonadState s (T m) ==> forall s m. (MSDict s m -> MSDict s (T m)) And having access to forall s m. MSDict s (T m) is not at all the same as having access to forall m. MSDict (forall s. s) (T m) Similarly, (forall a b. CDict a b) is not the same as (forall a. CDict a (forall b. b)). And: instance C a b corresponds to the former, not the latter. Viewing C as a relation, the former expresses that C relates every particular type to every other type. The latter says that C relates every type to the single type (forall b. b). And in the absence of any other instances, the latter is a functional relation, and the former is not.

Now if, in addition to lifting the coverage condition, you add OverlappingInstances, you can do something even better--you can write one single recursive definition of MonadState that works for all MonadTrans types (along with a base case for StateT).  This is far preferable to the N^2 boilerplate functions currently required by N monad transformers:

       instance (Monad m) => MonadState s (StateT s m) where            get = StateT $ \s -> return (s, s)

       instance (Monad (t m), MonadTrans t, MonadState s m) =>            MonadState s (t m) where                get = lift get                put = lift . put

This is not something you can do with type families.  So while UndecidableInstances and OverlappingInstances aren't very elegant, the fact that they can reduce source code size from O(N^2) to O(N) is a good indication that there is some unmet need in the base language.

This will probably come as no surprise, but I'm not too big on instances like: instance C (f a) either. I tend to view type classes as being justified by induction on the structure of types. So instances of the form 'F <t>' are justified by F being a constructor of *. But 'f a' is not in that manner. We are similarly not able to define: data T = C1 Int | C2 Char Int foo :: T -> T foo (f a) = f (a + 1) And this wasn't addressed to me, but:

If, instead of FunctionalDependencies, the extension were called ChooseInstancesWithoutKnowingAllTypeVariables, would you still have this objection?

No. In that case I would object that there are ad-hoc, unprincipled rules for resolving instances in GHC, and there should instead be some theoretical grounding to guide them. :) -- Dan