[Haskell-cafe] Type class context propagation investigation

[wren ng thornton]

Ryan Ingram wrote:
> Think of classes like data declarations; an instance with no context
> is a constant, and one with context is a function.  Here's a simple
> translation of your code into data; this is very similar to the
> implementation used by GHC for typeclasses:
> 
> > data EqDict a = EqDict { eq :: a -> a -> Bool }
> > data ShowDict a = ShowDict { show :: a -> String }
> > data NumDict a = NumDict { num_eq :: EqDict a, num_show :: ShowDict a, plus :: a -> a -> a }
> 
> The goal of the compiler is to turn your instance declarations into
> these structures automatically.

Another way of explaining this, if you're a Curry--Howard fan, is that 
the compiler is looking for a proof that the type belongs to the class, 
where => is logical implication. This is very similar to how Prolog 
searches for proofs, if you're familiar with logic programming.

Classes declare the existence of logical predicates, along with the form 
of what a "proof" of the predicate looks like. Instances declare a 
particular proof (or family of proofs if there are free type variables).


Thus, the Num class is declared as,

     class (Eq a, Show a) => Num a where ...

which says: for any type |a|, we can prove |Num a| if (and only if) we 
can prove |Eq a| and |Show a|, and can provide definitions for all the 
functions in the class using only the assumptions that |Eq a|, |Show a|, 
and |Num a|.


When you declare,

     instance Eq b => Eq (Foo b) where ...

you're providing a proof of |Eq b => Eq (Foo b)|. That is, you can 
provide a conditional proof of |Eq (Foo b)|, given the assumption that 
you have a proof of |Eq b|.

Notice how the context for instances is subtly different from the 
context for classes. For instances you're saying that this particular 
proof happens to make certain assumptions; for classes you're saying 
that all proofs require these assumptions are valid (that is, providing 
the functions isn't enough to prove membership in the class).


Later on you declare,

     instance Num (Foo b) where ...

but remember that this proof must have the same form as is declared by 
the class definition. This means that you must have proofs of |Eq (Foo 
b)| and |Show (Foo b)|. Unfortunately, you don't actually have a proof 
of |Eq (Foo b)|, you only have a proof of |Eq b => Eq (Foo b)|. In order 
to use that proof you must add the |Eq b| assumption to this proof as well:

     instance Eq b => Num (Foo b) where ...

When the compiler is complaining about the original one, what it's 
telling you is that the |Num (Foo b)| proof can never exist because you 
can never provide it with a proof of |Eq (Foo b)| in order to fulfill 
its requirements.

-- 
Live well,
~wren