[Haskell-cafe] Re: how would this be done? type classes?existential types?

[Ben Rudiak-Gould]

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