On 26/08/2008, at 13:30, Simon Peyton-Jones wrote:
| E.g., the type below is generated for :DNum, the datacon of a Num
| dictionary.
| At least, this is what :print obtains from a tcLookupDatacon
on :DNum.
|
| :DNum :: (a -> a -> a)
| -> (a -> a -> a)
| -> (a -> a -> a)
| -> (a -> a)
| -> (a -> a)
| -> (a -> a)
| -> (GHC.Integer.Integer -> a)
| -> (GHC.Num.:TNum) a)
|
| There is one element for every function in Num.
| But where did the dictionaries for the (Eq a, Show a) context go ?
They are certainly there! I compiled the Foo.hs below and asked
for the type of DB:
*Foo> :i DB
data Dict a where
DB :: forall a. (Eq a) => (a -> a) -> (a -> Int) -> Dict a
-- Defined at Foo.hs:10:2-3
*Foo>
I don't know how :print works, but the data constructor certainly
has those arguments, both in its type and in its runtime
representation.
How are Bar and DB related in your example ?
Are you saying that GHC generates something like Dict for dictionaries
of Bar ?
If you can refine your question I'll try to help.
I will try to rephrase my question better.
In the encoding of a type class instance as a tycon with a single
datacon,
I understand that the dictionaries for the superclasses are the first
fields
of the datacon. But that doesn't match what (fmap dataConRepType .
tcLookupDataCon)
is telling me.
Using your example, since DB is a GADT with a context in the
constructor,
GHC will embed a dictionary in its runtime representation, which will
look like:
dcRepType DB = :TEq a -> (a -> a) -> (a -> Int) -> Dict a
where the type class constraint has been desugared to an extra argument.
When :print finds a value with the DB constructor, it will see the
dictionary
in the first argument, and then reconstruct it as a term and give it a
type.
The [HHWP] paper says that a dictionary carries in it the dictionaries
for every superclass,
and :print confirms this, but the type of the datacon disagrees.
To see this let's define a simple class with one superclass,
and at least one function so that GHC will not try to optimize it
away.
> class Eq a => Eq2 a where eq :: a -> a -> Bool
> instance Eq2 Bool where eq = (==)
Now a GADT with the appropriate constructor to embed a Bar dictionary
> data SomeEq2 a where SomeEq2 :: Eq2 a => a -> SomeEq2 a
> value = SomeEq2 False
and now let's see what we get at runtime:
*Main> seq value ()
()
*Main> :p value
value = SomeEq2 (_t1::t) False
*Main> seq _t1 ()
()
*Main> :p value
value = SomeEq2 (Main.:DEq2 (GHC.Base.:DEq <function> <function>)
(_t4::t1))
False
Based on the runtime representation above, I expect the type of
Main.:DEq2 to be
Main.:DEq2 :: GHC.Base.:TEq a -> (a -> a -> Bool) -> Main.:TEq2 a
but GHC tells me, via (fmap dataConRepType . tcLookupDatacon), the
following
Main.:DEq2 :: (a -> a -> Bool) -> Main.:TEq2 a
Why does the type of :DEq2 differ from what :print sees at runtime ?
Thanks,
pepe
[HHPW] - "Type Classes in Haskell", Hall, Hammond, Peyton Jones, Wadler
_______________________________________________
Cvs-ghc mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/cvs-ghc
