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

[Brian Hulley]

Ben Rudiak-Gould wrote:
> 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
>


The bar is certainly consistent with the use in guards etc, but would lead 
to:

      exists a | (Show a, Eq a) . a

which looks a bit clunky because of the need for () as well because of the 
comma (to limit the scope of the comma). Also, it might be confusing to have 
to use a different notation to qualify type variables just because these 
type variables are being existentially qualified, when => is used everywhere 
else.
Personally I'd get rid of => altogether, and enclose constraints in {} eg

      foo :: forall a {Resource a} a  -- dot is optional after }
      bar :: {Show a, Eq a} a->Bool
      [exists a {Resource a} a]
      class {Monad m} MonadIO m where ...

This would fit into the rest of the syntax for Haskell as it stands at the 
moment.

[snip]
>
> 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.

If the two types for f are indistinguishable, perhaps the forall in f's type 
could be converted into an existential as a kind of normal form before doing 
type inference?

>
>> 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.

Thanks, this helps a lot,

Brian.