Functional dependencies in Haskell

Question

I'm trying to wrap my head around functional dependencies, but I am not getting anywhere on my own. In the paper "Monad Transformers Step by Step", the author gives these two typeclasses definitions:

class (Monad m) => MonadError e m | m -> e where     throwError :: e -> m a     catchError :: m a -> (e -> m a) -> m a  class (Monad m) => MonadReader r m | m -> r where     ask :: m r     local :: (r -> r) -> m a -> m a 

From my understanding of some of the material I found online, it means that the type variable e is determined by m. I just don't understand what that means. How is it determined? Can anyone shed some light with minimal theory at first, and then link the more heavy theory stuff?

Thanks

Answer 1

When you have a multiparameter typeclass, by default, the type variables are considered independently. So when the type inferencer is trying to figure out which instance of

class Foo a b 

to choose, it has to determine a and b independently, then go look check to see if the instance exists. With functional dependencies, we can cut this search down. When we do something like

class Foo a b | a -> b 

We're saying "Look, if you determine what a is, then there is a unique b so that Foo a b exists so don't bother trying to infer b, just go look up the instance and typecheck that". This let's the type inferencer by much more effective and helps inference in a number of places.

This is particularly helpful with return type polymorphism, for example

class Foo a b c where   bar :: a -> b -> c 

Now there's no way to infer

  bar (bar "foo" 'c') 1 

Because we have no way of determining c. Even if we only wrote one instance for String and Char, we have to assume that someone might/will come along and add another instance later on. Without fundeps we'd have to actually specify the return type, which is annoying. However we could write

class Foo a b c | a b -> c where   bar :: a -> b -> c 

And now it's easy to see that the return type of bar "foo" 'c' is unique and thus inferable.