Brian Hulley wrote:
Is there a reason for using && instead of
[exists a. Resource a=>a]
?
Only that => looks like a function arrow, && looks like a tuple. I stole
this notation from an unpublished paper by SimonPJ et al on adding
existential quantification to Haskell. I'm not especially attached to it.
Actually I rather like
forall a | Resource a. a
exists a | Resource a. a
a) A value 'v' of type 'exists a. Resource a=>a 'would have to be
internally represented as something like (dictResource_t, value_t)
Yes.
b) Given such a value, there is no syntactic way to distinguish the pair
from the value_t stored inside it, unlike the use of 'forall' where the
syntax for the constructor conveniently "represents" any dictionaries
that have been glued onto the value (ie pattern matching against R x
gives us back the dictionaries "R" and the plain value x)?
Yes, but that doesn't necessarily mean you can't work out when to construct
and deconstruct these implicit tuples. That's exactly what the type
inference process does with implicit type arguments, and implicit type
returns are dual to that, so the process should be similar.
It is tricky, though. E.g. given (f (g "z")) where
f :: forall a. [a] -> Int
g :: String -> (exists b. [b])
in principle you should be able to call g first, getting a type b and a list
[b], then instantiate f with the type b, then pass the list to it,
ultimately getting an Int. But I don't know how to design a type inference
algorithm that will find this typing. If on the other hand
f :: (exists a. [a]) -> Int
then it's easy to do the right thing---which is a little odd since these two
types for f are otherwise indistinguishable.
Hope I'm not making this more confusing but I'm still trying to get my
head around all these invisible happenings regarding dictionaries so I
can visualise what's happening in terms of bytes and pointers in the
runtime....
Once you understand where the types go in System F, the dictionaries are
easy: they always follow the types around. Any time you have
forall a b c. (C1 a b, C2 b c) => ...
in the source, you have five corresponding parameters/arguments in GHC Core,
one for each type variable and constraint. These are always passed around as
a unit (at least prior to optimization). In principle you could box them in
a 5-tuple. The dictionary values are nothing more or less than proofs that
the corresponding constraints hold.
-- Ben
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
