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