At Wed, 15 Jun 2011 20:48:07 -0400, Dan Doel wrote: > > 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:
I don't understand how this code would work under any circumstances. At the very least, you are missing a context for coerce and the type of foo would have to be ... => a -> b -> c -> c. If two types are the same, you are not allowed to declare them to be different. Also, it's easy to add a method of some class to do the coercion, while it's hard to emulate polymorphic types if you don't have them. So I'd say the current behavior is more useful--allowing massive code reduction in some cases, while I'm not yet convinced of the utility of what you did above. > 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) I don't understand the difference, but admittedly I don't totally follow your dictionary syntax. Recall the functional dependency goes from right to left in this case: MonadState s m | m -> s, and certainly the type forall m s. m -> s is equivalent to forall m. m -> (forall s. s). It's only when the parentheses close before the last argument that you need higher-rank types. But I think I'm probably misunderstanding your example. > > 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. :) Ah, we find agreement! I, too, am all in favor of rules with theoretical grounding. The only thing I would add is that I don't want to have to define N^2 instances for libraries like the mtl. David _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
