Hello, Edsko de Vries wrote:
In this figure, there are rules for annotated abstractions (AABS1 and AABS2) and annotated terms (ANNOT). What I'm wondering about: are the rules AABS1 and AABS2 really necessary? As in, if you would remove those two rules, does there exist a program that can be typed with the original set of rules than cannot be typed with the set of rules with AABS1/2 removed? It seems to me that any program that can be typed using AABS1/2, can also be typed with ANNOT.
You mean that whenever |- \x::sigma.e :<up/down> s1 -> r2 then |- ((\x.e) ::<up/down> sigma -> r2) : s1 -> r2 or sth similar I guess. Yes in that sense we dont really need aabs1/2. The rules are included more to indicate how should one deal with annotated abstractions rather than to improve the expressivity of the language.
More importantly, in the absence of lexically scoped type variables, a type such as
forall a. (forall b. (a, b) -> (b, a)) -> [a] -> [a] (*)
(the example given on page 11, section 4.1 in the paper) cannot even be typed using AABS1/2, but must be typed with ANNOT.
Again, you mean we cannot meaningfully annotate some lambda expression so that the whole expression has this type and the annotation "forall b. (a,b) -> (b,a)" be somehow fixed to its argument? Yes, this is right, we have to use annot.
Perhaps I am missing something here though, because in Odersky and Laufer's original paper, they do not do "local type inference" (they don't specify a bidirectional version), which would make type (*) impossible to specify in their original system?
No this has nothing to do with the OL type system, OL allow any arbitrary rank types. Nor with bidirectionality. Perhaps more clear discussion and facts about the metatheory of these systems can be found in the new (and final) version of the paper you have, available from SPJ's page. Regards, -d
Thanks,
Edsko _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell