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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
