"The signature contexts in a mutually recursive group should all be identical"; why?
Simon Peyton-Jones
simonpj@microsoft.com
Fri, 21 Dec 2001 01:35:37 -0800
[Note to the Haskell list. The question this thread is discussing
is whether the H98 rule that all the functions in a mutually=20
recursive group must have the same context, is a show stopper.]
| Oeer. Come to think of it, if f is getting the dictionary=20
| (in the real world
| example) from the context, rather than from the existential=20
| type, I fear it may be getting the wrong dictionary, and will=20
| crash badly when I try to run the code. =20
No I don't think that can happen. But I have thought of a test
case
data T =3D forall a. Eq a =3D> MkT a a T
| Nil
f :: T -> Bool
f Nil =3D True
f (MkT x y t) =3D g x y t
g :: Eq b =3D> b -> b -> T -> Bool
g x y t =3D (x=3D=3Dy) && f t
Notice that
(a) f and g are mutually recursive
(b) They have different contexts in their type sig
(c) If they were made the same, f would get an
ambiguous type f :: Eq a =3D> T -> Bool
(d) Haskell's polymorphic recursion is essential here;
each call to g may be at a different type
So it looks to me that, in the presence of existentials, the H98
rule goes from being moot to being throughly awkward.=20
Mark's THIH paper shows that there's no real need for the rule,
because one can type-check the bindings without type sigs as
a group, and then the ones with type sigs one by one. =20
But what happens for pattern-bindings that bind more than
one variable. Must all those variables have the same context?
(I hope so.)
Needless to say, I'm not proposing any changes in H98! But
I thought the example would be of interest. Maybe it's well known,
but it wasn't to me.
Simon