RE: [Haskell-cafe] Type class context propagation investigation[MESSAGE NOT SCANNED]
Thanks. GHC at one stage suggested I add (Num a) =
to my Num instance (after I'd added (Eq a) = to my Eq
instance) and I didn't make the connection.
-Original Message-
From: Ryan Ingram [mailto:ryani.s...@gmail.com]
Sent: Thu 28/05/2009 01:18
To: Paul Keir
Cc: haskell-cafe@haskell.org
Subject: Re: [Haskell-cafe] Type class context propagation
investigation[MESSAGE NOT SCANNED]
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. Here's a translation of your original
instance:
eq_foo :: EqDict (Foo a)
eq_foo = EqDict { eq = undefined }
show_foo :: ShowDict (Foo a)
show_foo = ShowDict { show = undefined }
num_foo :: NumDict (Foo a)
num_foo = NumDict { num_eq = eq_foo, num_show = show_foo, plus = undefined }
Now if you add a constraint on the Eq instance, this means that eq
from eq_foo might refer to eq in the dictionary for a. How do we
get that dictionary? We just pass it as an argument!
eq_foo :: EqDict a - EqDict (Foo a)
eq_foo eq_a = EqDict { eq = undefined }
However, you don't have a similar constraint on the Num instance:
num_foo :: NumDict (Foo a)
num_foo = NumDict { num_eq = eq_foo something, num_show = show_foo, plus =
undefined }
The compiler wants to fill in something, but it can't; it doesn't
have a dictionary of the type EqDict a. So it tells you so, saying
that Eq a is missing!
Once you add the (Eq a) constraint to the Num instance, it works:
num_foo :: EqDict a - NumDict (Foo a)
num_foo eq_a = NumDict { num_eq = eq_foo eq_a, num_show = show_foo, plus =
undefined }
You can also add a (Num a) constraint instead, and the compiler can
use it to get the Eq instance out:
num_foo :: NumDict a - NumDict (Foo a)
num_foo num_a = NumDict { num_eq = eq_foo (num_eq num_a), num_show =
show_foo, plus = undefined }
Of course, I'm glossing over the interesting details of the search,
but the basic idea is to attempt to fill in the blanks in these
definitions.
-- ryan
On Wed, May 27, 2009 at 2:10 PM, Paul Keir pk...@dcs.gla.ac.uk wrote:
Hi,
How does the context of a class instance declaration affect its subclasses?
The Num class instance outlined below has its requirement for Eq and Show
satisfied on the preceding lines, and the code will compile. But if I, say,
add an (Eq a) constraint to the Eq instance, in preparation for a simple
(==) definition, I find that the Num instance declaration is left lacking.
If I add the same (Eq a) constraint now to Num, calm is restored.
data Foo a = F a
instance Eq (Foo a) where
(==) = undefined
instance Show (Foo a) where
show = undefined
instance Num (Foo a)
(+) = undefined
... etc.
The thing that confuses me with this is that it seems like Num knows that
an (Eq a) context has been applied, and so what it sees as a problem, is
somehow also the solution. Any advice/rules of thumb? Does this situation
occur elsewhere? How do these constraints propagate?
Thanks,
Paul
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Type class context propagation investigation
Thanks Wren, that makes sense.
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type class context propagation investigation
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. Here's a translation of your original
instance:
eq_foo :: EqDict (Foo a)
eq_foo = EqDict { eq = undefined }
show_foo :: ShowDict (Foo a)
show_foo = ShowDict { show = undefined }
num_foo :: NumDict (Foo a)
num_foo = NumDict { num_eq = eq_foo, num_show = show_foo, plus = undefined }
Now if you add a constraint on the Eq instance, this means that eq
from eq_foo might refer to eq in the dictionary for a. How do we
get that dictionary? We just pass it as an argument!
eq_foo :: EqDict a - EqDict (Foo a)
eq_foo eq_a = EqDict { eq = undefined }
However, you don't have a similar constraint on the Num instance:
num_foo :: NumDict (Foo a)
num_foo = NumDict { num_eq = eq_foo something, num_show = show_foo, plus =
undefined }
The compiler wants to fill in something, but it can't; it doesn't
have a dictionary of the type EqDict a. So it tells you so, saying
that Eq a is missing!
Once you add the (Eq a) constraint to the Num instance, it works:
num_foo :: EqDict a - NumDict (Foo a)
num_foo eq_a = NumDict { num_eq = eq_foo eq_a, num_show = show_foo, plus =
undefined }
You can also add a (Num a) constraint instead, and the compiler can
use it to get the Eq instance out:
num_foo :: NumDict a - NumDict (Foo a)
num_foo num_a = NumDict { num_eq = eq_foo (num_eq num_a), num_show =
show_foo, plus = undefined }
Of course, I'm glossing over the interesting details of the search,
but the basic idea is to attempt to fill in the blanks in these
definitions.
-- ryan
On Wed, May 27, 2009 at 2:10 PM, Paul Keir pk...@dcs.gla.ac.uk wrote:
Hi,
How does the context of a class instance declaration affect its subclasses?
The Num class instance outlined below has its requirement for Eq and Show
satisfied on the preceding lines, and the code will compile. But if I, say,
add an (Eq a) constraint to the Eq instance, in preparation for a simple
(==) definition, I find that the Num instance declaration is left lacking.
If I add the same (Eq a) constraint now to Num, calm is restored.
data Foo a = F a
instance Eq (Foo a) where
(==) = undefined
instance Show (Foo a) where
show = undefined
instance Num (Foo a)
(+) = undefined
... etc.
The thing that confuses me with this is that it seems like Num knows that
an (Eq a) context has been applied, and so what it sees as a problem, is
somehow also the solution. Any advice/rules of thumb? Does this situation
occur elsewhere? How do these constraints propagate?
Thanks,
Paul
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type class context propagation investigation
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
