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