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.