<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2//EN">
<HTML>
<HEAD>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
<META NAME="Generator" CONTENT="MS Exchange Server version 6.5.7654.12">
<TITLE>RE: [Haskell-cafe] Type class context propagation investigation</TITLE>
</HEAD>
<BODY>
<!-- Converted from text/plain format -->
<P><FONT SIZE=2>Thanks Wren, that makes sense.<BR>
<BR>
Ryan Ingram wrote:<BR>
> Think of classes like data declarations; an instance with no context<BR>
> is a constant, and one with context is a function. Here's a simple<BR>
> translation of your code into data; this is very similar to the<BR>
> implementation used by GHC for typeclasses:<BR>
><BR>
> > data EqDict a = EqDict { eq :: a -> a -> Bool }<BR>
> > data ShowDict a = ShowDict { show :: a -> String }<BR>
> > data NumDict a = NumDict { num_eq :: EqDict a, num_show :: ShowDict a, plus :: a -> a -> a }<BR>
><BR>
> The goal of the compiler is to turn your instance declarations into<BR>
> these structures automatically.<BR>
<BR>
Another way of explaining this, if you're a Curry--Howard fan, is that<BR>
the compiler is looking for a proof that the type belongs to the class,<BR>
where => is logical implication. This is very similar to how Prolog<BR>
searches for proofs, if you're familiar with logic programming.<BR>
<BR>
Classes declare the existence of logical predicates, along with the form<BR>
of what a "proof" of the predicate looks like. Instances declare a<BR>
particular proof (or family of proofs if there are free type variables).<BR>
<BR>
<BR>
Thus, the Num class is declared as,<BR>
<BR>
class (Eq a, Show a) => Num a where ...<BR>
<BR>
which says: for any type |a|, we can prove |Num a| if (and only if) we<BR>
can prove |Eq a| and |Show a|, and can provide definitions for all the<BR>
functions in the class using only the assumptions that |Eq a|, |Show a|,<BR>
and |Num a|.<BR>
<BR>
<BR>
When you declare,<BR>
<BR>
instance Eq b => Eq (Foo b) where ...<BR>
<BR>
you're providing a proof of |Eq b => Eq (Foo b)|. That is, you can<BR>
provide a conditional proof of |Eq (Foo b)|, given the assumption that<BR>
you have a proof of |Eq b|.<BR>
<BR>
Notice how the context for instances is subtly different from the<BR>
context for classes. For instances you're saying that this particular<BR>
proof happens to make certain assumptions; for classes you're saying<BR>
that all proofs require these assumptions are valid (that is, providing<BR>
the functions isn't enough to prove membership in the class).<BR>
<BR>
<BR>
Later on you declare,<BR>
<BR>
instance Num (Foo b) where ...<BR>
<BR>
but remember that this proof must have the same form as is declared by<BR>
the class definition. This means that you must have proofs of |Eq (Foo<BR>
b)| and |Show (Foo b)|. Unfortunately, you don't actually have a proof<BR>
of |Eq (Foo b)|, you only have a proof of |Eq b => Eq (Foo b)|. In order<BR>
to use that proof you must add the |Eq b| assumption to this proof as well:<BR>
<BR>
instance Eq b => Num (Foo b) where ...<BR>
<BR>
When the compiler is complaining about the original one, what it's<BR>
telling you is that the |Num (Foo b)| proof can never exist because you<BR>
can never provide it with a proof of |Eq (Foo b)| in order to fulfill<BR>
its requirements.<BR>
<BR>
--<BR>
Live well,<BR>
~wren</FONT>
</P>
</BODY>
</HTML>