| > > Just as a sanity check, following an augmented proposal "A" where we can also
| > > annotate the return type as well, consider these:
| > >
| > > f :: a -> (a -> a) -> a
| > > f x = \g -> (g :: a -> a) x
| > >
| > > f (x :: a) :: (a -> a) -> a = \g -> (g :: a -> a) x
| > >
| > > Which of these two is correct, and why? Why not both?
| >
| > Under "A+B", these would be equivalent. Under "A++" (Mark's original
| > "A", only, plus the return types), the second of these is "correct"
| > (assuming a restricted interpretation of "a" is what was intended), but
| > in the first, the a's in sig and body are bound quite separately, so the
| > local type annotation would be too general.
| >
|
| I'm not sure what the parenthetical comment about the interpretation of a means -
| take the definition at face value.
|
| I should have been more explicit - I'm interested not in why the first one would
| be incorrect, but how, for example, you would explain that to someone learning
| Haskell. It's not at all clear to me that people should expect the a's to be
| different - I can't think of a good rationale for it (aside from the "don't break
| old code" argument, which, if that's the only argument, doesn't seem strong enough
| to me).
One could also argue that the culprit is Haskell's interpretation of
type variables of which Report (p. 34) says: `[...] the type variables
in a Haskell expression are all assumed to be universally quantified
[..]'. Here is an even more irritating list of possibilities ...
rapply :: a -> (a -> a) -> a
rapply a f = f a
rapply (a :: a) f = f a
rapply a (f :: a -> a) = f a
rapply a f :: a = f a
rapply a f = (f :: a -> a) a
rapply a f = f (a :: a)
rapply a f = f a :: a
rapply a = \f -> f a
rapply (a :: a) = \f -> f a
rapply a:: (a -> a) -> a= \f -> f a
rapply a = \(f :: a -> a) -> f a
rapply a = \f -> f a :: a
and so forth ... A solution could be to consider the type variables
universally quantified at the _outermost_ possible level (currently
it's the innermost). So `f e1 ... en = e' means `forall a1 .. am.f e1
... en = e' where the `ai's are the type variables occuring free in the
definition. If we had explicit syntax for universal quantification
(which I consider absolutely necessary) the former interpretation could
be recovered using explicit quantifiers: ... (f :: forall a.a -> a)
...
Ralf
PS: I don't like the scope-mixture of type signatures and definitions.
