[Haskell-cafe] Re: how would this be done? type
classes?existentialtypes?
Brian Hulley
brianh at metamilk.com
Thu Mar 23 14:07:49 EST 2006
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.
More information about the Haskell-Cafe
mailing list