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